Tensor constructors (spec layer)

These are small, total constructors for building Spec.Tensor values directly.

They are used heavily inside the spec layer (models/layers) and in proofs, where we want:

• straightforward definitional unfolding, and
• no dependence on IO or dynamic shape checks.

If you want a PyTorch-style user experience for examples (dynamic dims, runtime errors, and Float-literal casting), prefer NN/Tensor/API.lean instead.

Design choice (why these are "total"):

• In the spec layer we would rather make edge cases explicit than throw runtime exceptions.
• If something is shape-invalid, we want Lean to reject it at elaboration time.
• If something is index-invalid at runtime (e.g. array-backed constructor with wrong size), we choose a predictable fallback (usually Inhabited.default) and let verification code decide whether that situation is allowed.

def Spec.fill {α : Type} (value : α) (s : Shape) : Tensor α s

Fill a tensor of shape s with a constant value.

PyTorch analogy: torch.full(shape, value).

def Spec.scalarTensor {α : Type} (value : α) : Tensor α Shape.scalar

Scalar constructor (explicit name).

PyTorch analogy: a 0-dim tensor holding one value.

def Spec.vectorTensor {α : Type} {n : ℕ} (values : Fin n → α) : Tensor α (Shape.dim n Shape.scalar)

Vector constructor from a Fin n → α function.

PyTorch analogy: torch.tensor([...]) with shape (n,), but our input is a function, not a list.

def Spec.matrixTensor {α : Type} {m n : ℕ} (values : Fin m → Fin n → α) : Tensor α (Shape.dim m (Shape.dim n Shape.scalar))

Matrix constructor from an Fin m → Fin n → α function.

PyTorch analogy: torch.tensor([...]).reshape(m, n) (again, function input rather than a list).

def Spec.nDArrayTensor {α : Type} {n : ℕ} {s : Shape} : (Fin n → Tensor α s) → Tensor α (Shape.dim n s)

Generic dim constructor for call sites that build tensors one axis at a time.

def Spec.vectorN {α : Type} [Zero α] (n : ℕ) (f : Fin n → α) : Tensor α (Shape.dim n Shape.scalar)

Generic vector creation that works with any type (handles n = 0).

Why this exists:

• For n = 0, a function Fin 0 → α is fine (it has no inputs), but it can be awkward at call sites. This helper makes the intent explicit and keeps patterns uniform.
• The 0 case is definitionally a tensor with an empty outer dimension (so the function body is never evaluated).

def Spec.matrixMN {α : Type} [Zero α] (m n : ℕ) (f : Fin m → Fin n → α) : Tensor α (Shape.dim m (Shape.dim n Shape.scalar))

Generic matrix creation that works with any type.

def Spec.generate {α : Type} (n : ℕ) (f : Fin n → Tensor α Shape.scalar) : Tensor α (Shape.dim n Shape.scalar)

Build a length-n vector from a Fin n → scalar function.

This is a small wrapper that reads nicely at call sites where we already have scalar tensors.

def Spec.singleton {α : Type} (x : α) : Tensor α (Shape.dim 1 Shape.scalar)

A singleton vector.

PyTorch analogy: x.unsqueeze(0) for a scalar x.

def Spec.padLeft {α : Type} [Context α] {n : ℕ} {s : Shape} (x : Tensor α s) : Tensor α (Shape.padLeft n s)

Pad a tensor with n leading dimensions of size 1.

This is the tensor-level companion of Shape.padLeft. It is useful for broadcasting-style normalization: if you need a tensor to have extra leading batch dimensions of size 1, this does so without changing any underlying values.

PyTorch analogy: repeated unsqueeze(0) (or viewing a tensor as having extra leading singleton dims).

def Spec.Tensor.ofArray1D {α : Type} {n : ℕ} (xs : Array α) (h : n = xs.size) : Tensor α (Shape.dim n Shape.scalar)

Build a vector tensor from an array.

The caller provides an explicit proof that the target length matches the array size, so mismatches are visible at call sites.

def Spec.Tensor.ofArray2D {α : Type} [Inhabited α] {m n : ℕ} (xss : Array α) : m * n = xss.size → Tensor α (Shape.dim m (Shape.dim n Shape.scalar))

Build a matrix tensor from a flat array (row-major).

PyTorch analogy: xss.reshape(m, n) assuming xss is laid out row-major.

def Spec.Tensor.ofArrayDim {α : Type} {n : ℕ} {s : Shape} (xs : Array (Tensor α s)) (_h : n = xs.size) : Tensor α (Shape.dim n s)

Build a tensor with one leading dimension from an array of inner tensors.

This is the "tensor-of-tensors" analogue of Tensor.ofArray1D:

• input: Array (Tensor α s) of length n
• output: Tensor α (.dim n s)

We require an explicit proof that the array size matches n so callers do not silently drop/pad data.

def Spec.Tensor.vecToCol {α : Type} {n : ℕ} (v : Tensor α (Shape.dim n Shape.scalar)) : Tensor α (Shape.dim n (Shape.dim 1 Shape.scalar))

View a length-n vector as an n x 1 "column" matrix.

PyTorch analogy: v.unsqueeze(-1) for a 1D tensor v (or v.reshape(n, 1)).