Real Tensor Proof Toolkit

This file is the ℝ-specialized proof-facing companion to the spec tensor layer.

The tensor proof folder has two layers:

• NN.Proofs.Tensor.Algebra is backend-generic and proves semiring facts about recursive tensor dot products and executable folds.
• this file works in Spec over ℝ, where calculus, norms, Frobenius products, and model-analysis lemmas live.

The statements use PyTorch-shaped names where that helps readers:

• flattenR / unflattenR give a Fin (Shape.size s) → ℝ view of Tensor ℝ s.
• lemmas relate toVec views to add_spec, scale_spec, etc.

We re-export selected generic helpers from NN.Proofs.Tensor.Algebra into the Spec.* namespace so downstream proof files can use one consistent tensor vocabulary (Spec.toVec, Spec.ofVec, Spec.finRange_foldl_add_eq_finset_sum) through shared fold and vector lemmas.

PyTorch correspondence / citations

• Flatten / reshape: torch.flatten, torch.reshape, and Tensor.view. https://pytorch.org/docs/stable/generated/torch.flatten.html https://pytorch.org/docs/stable/generated/torch.reshape.html https://pytorch.org/docs/stable/generated/torch.Tensor.view.html
• “numel”: tensor.numel() corresponds to Shape.size. https://pytorch.org/docs/stable/generated/torch.Tensor.numel.html

Algebraic instances for small tensor shapes

@[implicit_reducible]

instance Spec.instAddCommMonoidTensorRealScalar : AddCommMonoid (Tensor ℝ Shape.scalar)

Additive commutative monoid structure on scalar-shaped real tensors, transported by equivalence.

@[implicit_reducible]

instance Spec.instAddCommMonoidTensorRealDimScalar {n : ℕ} : AddCommMonoid (Tensor ℝ (Shape.dim n Shape.scalar))

Additive commutative monoid structure on 1D real tensors (transported via an equiv).

@[implicit_reducible]

instance Spec.instModuleRealTensorScalar {α : Type} [AddCommMonoid α] [Module ℝ α] : Module ℝ (Tensor α Shape.scalar)

Scalar tensors inherit an ℝ-module structure when their entries do, transported by equivalence.

@[implicit_reducible]

instance Spec.instModuleRealTensorDimScalar {α : Type} [AddCommMonoid α] [Module ℝ α] {n : ℕ} : Module ℝ (Tensor α (Shape.dim n Shape.scalar))

Tensor α (dim n scalar) inherits an ℝ-module structure when α is an ℝ-module (via an equiv).

@[implicit_reducible]

noncomputable instance Spec.instModuleRealTensorScalar_1 : Module ℝ (Tensor ℝ Shape.scalar)

Noncomputable ℝ-module instance on scalar real tensors (for calculus proofs).

@[implicit_reducible]

noncomputable instance Spec.instModuleRealTensorDimScalar_1 {n : ℕ} : Module ℝ (Tensor ℝ (Shape.dim n Shape.scalar))

Noncomputable ℝ-module instance on 1D real tensors (for calculus proofs).

1D helpers

theorem Spec.toVec_add_spec {n : ℕ} (x y : Tensor ℝ (Shape.dim n Shape.scalar)) : toVec (x.addSpec y) = fun (i : Fin n) => toVec x i + toVec y i

toVec distributes over pointwise addition (add_spec).

theorem Spec.toVec_scale_spec {n : ℕ} (x : Tensor ℝ (Shape.dim n Shape.scalar)) (c : ℝ) : toVec (x.scaleSpec c) = fun (i : Fin n) => toVec x i * c

toVec distributes over pointwise scaling (scale_spec).

def Spec.flattenR {s : Shape} (x : Tensor ℝ s) : Fin s.size → ℝ

Flatten a tensor of shape s into a 1D view Fin (Shape.size s) → ℝ.

This is the proof-facing counterpart of Spec.Tensor.flatten_spec specialized to ℝ. In PyTorch terms it is the functional analogue of flattening a tensor and then indexing it linearly (torch.flatten, tensor.view(-1)). See the spec file NN/Spec/Core/TensorReductionShape.lean for the definitional flatten/unflatten interface.

Citations: https://pytorch.org/docs/stable/generated/torch.flatten.html https://pytorch.org/docs/stable/generated/torch.Tensor.view.html

def Spec.unflattenR {s : Shape} (v : Fin s.size → ℝ) : Tensor ℝ s

Unflatten a 1D view Fin (Shape.size s) → ℝ back into a tensor of shape s.

This is the proof-facing counterpart of Spec.Tensor.unflatten_spec specialized to ℝ, and is intended to round-trip with flattenR under the spec lemmas in NN/Spec/Core/TensorReductionShape.lean.

Pointwise tensor algebra