Fold and reduction lemmas for dependent tensors.

This module packages the algebra needed to reason about tensor reductions, finite sums, and shape-indexed traversals. The finite-sum and associativity results concern exact real arithmetic; they do not permit reassociating a floating-point reduction.

theorem Spec.mul_spec_assoc {s : Shape} (a b c : TorchLean.Tensor ℝ s) : a.mulSpec (b.mulSpec c) = (a.mulSpec b).mulSpec c

Elementwise multiplication is associative (mulSpec is pointwise (*)).

theorem Spec.mul_spec_comm {s : Shape} (a b : TorchLean.Tensor ℝ s) : a.mulSpec b = b.mulSpec a

Elementwise multiplication is commutative (mulSpec is pointwise (*)).

theorem Spec.add_spec_comm {s : Shape} (a b : TorchLean.Tensor ℝ s) : a.addSpec b = b.addSpec a

Elementwise addition is commutative (addSpec is pointwise (+)).

Real dot product and fold bridges

noncomputable def Spec.dot {s : Shape} (a b : TorchLean.Tensor ℝ s) : ℝ

Real dot product for same-shape tensors, defined as the sum of elementwise products.

This matches the common PyTorch idiom (a * b).sum() for same-shape tensors. Citations: https://pytorch.org/docs/stable/generated/torch.sum.html

This is the Spec-namespace dot product used by real-analysis proofs. The backend-generic recursive dot product is Proofs.TensorAlgebra.dot.

theorem Spec.foldlSpec_go_of_lt {α β : Type} [TorchLean.Storage α] (f : β → α → β) {n : ℕ} {s : Shape} (values : Fin n → TorchLean.Tensor α s) {k : ℕ} (acc : β) (hk : k < n) : TorchLean.Tensor.foldlSpec.go f n s values k acc = TorchLean.Tensor.foldlSpec.go f n s values (k + 1) (TorchLean.Tensor.foldlSpec f acc (values ⟨k, hk⟩))

Peel one slice from the proof-facing fold starting at k, when k < n.

theorem Spec.foldlSpec_go_of_not_lt {α β : Type} [TorchLean.Storage α] (f : β → α → β) {n : ℕ} {s : Shape} (values : Fin n → TorchLean.Tensor α s) {k : ℕ} (acc : β) (hk : ¬k < n) : TorchLean.Tensor.foldlSpec.go f n s values k acc = acc

Starting the proof-facing slice fold at or beyond its length returns the accumulator.

theorem Spec.get2_mat_mul_spec {m n p : ℕ} (A : TorchLean.Tensor ℝ [m, n]) (B : TorchLean.Tensor ℝ [n, p]) (i : Fin m) (j : Fin p) : get2 (matMulSpec A B) i j = ∑ k : Fin n, get2 A i k * get2 B k j

Coordinate formula for matMulSpec (matrix-matrix multiplication).

This is the coordinate identity (A @ B)[i,j] = ∑ k, A[i,k] * B[k,j], matching the textbook/PyTorch view of matrix multiplication.

Citations: https://pytorch.org/docs/stable/generated/torch.matmul.html

theorem Spec.sum_spec_eq_coord_sum {s : Shape} (t : TorchLean.Tensor ℝ s) : t.sumSpec = ∑ coordinate : s.Coord, TorchLean.Tensor.Internal.Rep.get t coordinate

A packed-buffer sum is the finite sum of the tensor's coordinate observations.

theorem Spec.sum_spec_dim {n : ℕ} {s : Shape} (t : TorchLean.Tensor ℝ (Shape.dim n s)) : t.sumSpec = ∑ i : Fin n, (get t i).sumSpec

Sum over the outer dimension unfolds into a Finset.univ sum of inner sumSpec.

This is the tensor analogue of torch.sum reducing over a leading dimension.

theorem Spec.dot_eq_tensorAlgebra_dot {s : Shape} (a b : TorchLean.Tensor ℝ s) : dot a b = Proofs.TensorAlgebra.dot a b

The packed real sum-of-products agrees with the generic shape-recursive dot product.

This bridge allows real-analysis proofs to reuse generic dot-product algebra. The equality uses exact addition; the two groupings need not agree for a rounded scalar model.