Continuous tensor vectorization

The tape's flattened vectors and native real tensors use the same inner product. Bundling the existing conversion as a continuous linear equivalence lets derivatives pass through it without unfolding storage or choosing a second coordinate order. Context projections then return native tensors, including tensors with empty shapes.

noncomputable def Proofs.Autograd.tensorVecEquiv (shape : Spec.Shape) : TorchLean.Tensor ℝ shape ≃L[ℝ] Vec shape.size

The tape's existing tensor conversion as a continuous linear equivalence.

@[simp]

theorem Proofs.Autograd.tensorVecEquiv_apply {shape : Spec.Shape} (x : TorchLean.Tensor ℝ shape) : (tensorVecEquiv shape) x = tensorToVec x

The bundled map preserves the tape's flattening order.

@[simp]

theorem Proofs.Autograd.tensorVecEquiv_symm_apply {shape : Spec.Shape} (v : Vec shape.size) : (tensorVecEquiv shape).symm v = vecToTensor v

Its inverse uses the existing tensor reconstruction.

noncomputable def Proofs.Autograd.CtxVec.getTensorCLM {Γ : List Spec.Shape} {shape : Spec.Shape} (input : Idx Γ shape) : CtxVec Γ →L[ℝ] TorchLean.Tensor ℝ shape

Read a typed tensor block directly from a flattened context.

@[simp]

theorem Proofs.Autograd.CtxVec.getTensorCLM_apply {Γ : List Spec.Shape} {shape : Spec.Shape} (input : Idx Γ shape) (x : CtxVec Γ) : (getTensorCLM input) x = getIdx (unflattenCtx x) input

The continuous projection agrees with tensor-pack indexing after reconstruction.