Linear algebra primitives (spec layer)

This file defines the basic matrix/vector operations used across model specifications:

• matMulSpec (matrix × matrix)
• matVecMulSpec (matrix × vector)
• vecMatMulSpec (vector × matrix)
• outerProductSpec

All operations are shape-indexed in their types, so misuse is caught by elaboration.

These are kept simple, “obvious” definitions (folding over List.finRange) so that:

• they are easy to reason about in proofs, and
• they can be instantiated over many scalar backends (Float, ℚ, ExecFloat.Binary 8 23, ℝ, …).

PyTorch analogies:

• matMulSpec A B is A @ B
• matVecMulSpec A v is A @ v
• vecMatMulSpec v A is v @ A
• outerProductSpec a b is like a.unsqueeze(1) * b.unsqueeze(0) (result is (m,n)).

def Spec.identityTensorSpec {α : Type} [TorchLean.Storage α] [Zero α] [One α] (n : ℕ) : TorchLean.Tensor α [n, n]

Create an identity matrix (n x n).

Notes:

• The n = 0 case is an empty matrix; it still exists as a well-typed tensor.
• We use i.val == j.val rather than DecidableEq (Fin n) to keep the definition directly executable across backends.

def Spec.matMulSpec {α : Type} [TorchLean.Storage α] [Add α] [Mul α] [Zero α] {m n p : ℕ} (A : TorchLean.Tensor α [m, n]) (B : TorchLean.Tensor α [n, p]) : TorchLean.Tensor α [m, p]

Matrix multiplication (m x n) @ (n x p) = (m x p).

This is the simplest definitional version: sum over the shared n dimension. For performance-oriented runtime code, use the runtime layer; this spec is about clarity and proofs.

def Spec.matVecMulSpec {α : Type} [TorchLean.Storage α] [Add α] [Mul α] [Zero α] {m n : ℕ} (A : TorchLean.Tensor α [m, n]) (v : TorchLean.Tensor α [n]) : TorchLean.Tensor α [m]

Matrix-vector multiplication (m x n) @ (n) = (m).

def Spec.vecMatMulSpec {α : Type} [TorchLean.Storage α] [Add α] [Mul α] [Zero α] {m n : ℕ} (v : TorchLean.Tensor α [m]) (A : TorchLean.Tensor α [m, n]) : TorchLean.Tensor α [n]

Rank-one tensor by matrix multiplication: (m) @ (m x n) = (n).

def Spec.outerProductSpec {α : Type} [TorchLean.Storage α] [Mul α] {m n : ℕ} (a : TorchLean.Tensor α [m]) (b : TorchLean.Tensor α [n]) : TorchLean.Tensor α [m, n]

Outer product (m) otimes (n) = (m x n).

@[simp]

theorem Spec.get2_outerProductSpec {α : Type} [TorchLean.Storage α] [Mul α] {m n : ℕ} (left : TorchLean.Tensor α [m]) (right : TorchLean.Tensor α [n]) (i : Fin m) (j : Fin n) : get2 (outerProductSpec left right) i j = left.getScalar i * right.getScalar j

A coordinate of an outer product is the product of the corresponding vector entries.