Real Tensor Proof Toolkit

This file is the ℝ-specialized proof layer 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 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 (Spec.Shape.size s) → ℝ view of Tensor ℝ s.
• lemmas relate getScalar views to addSpec, scaleSpec, etc.

We re-export tensor-specific helpers from NN.Proofs.Tensor.Algebra into the Spec namespace. General list-fold lemmas retain their canonical List names.

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 Spec.Shape.size. https://pytorch.org/docs/stable/generated/torch.Tensor.numel.html

Algebraic instances

The pointwise AddCommGroup and Module instances on Tensor α s live in NN.Spec.Core.Tensor.Core; over ℝ they give Module ℝ (Tensor ℝ s) directly.

1D helpers

@[simp]

theorem Spec.toScalar_mapTensor {α β : Type} [TorchLean.Storage α] [TorchLean.Storage β] (f : α → β) (x : TorchLean.Tensor α Shape.scalar) : (TorchLean.Tensor.map f x).item = f x.item

Mapping a scalar tensor and then extracting it is the same as mapping its scalar value.

@[simp]

theorem Spec.getScalar_mapTensor {α β : Type} [TorchLean.Storage α] [TorchLean.Storage β] {n : ℕ} (f : α → β) (x : TorchLean.Tensor α [n]) (i : Fin n) : (TorchLean.Tensor.map f x).getScalar i = f (x.getScalar i)

Coordinate extraction commutes with a tensor map on vectors.

theorem Spec.getScalar_add_spec {n : ℕ} (x y : TorchLean.Tensor ℝ [n]) : (x.addSpec y).getScalar = fun (i : Fin n) => x.getScalar i + y.getScalar i

getScalar distributes over pointwise addition (addSpec).

theorem Spec.getScalar_scale_spec {n : ℕ} (x : TorchLean.Tensor ℝ [n]) (c : ℝ) : (x.scaleSpec c).getScalar = fun (i : Fin n) => x.getScalar i * c

getScalar distributes over pointwise scaling (scaleSpec).

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

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

This is the proof layer counterpart of TorchLean.Tensor.flattenSpec 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 → ℝ) : TorchLean.Tensor ℝ s

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

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

Pointwise tensor algebra