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 (kept for clarity at call sites).

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.

We require an explicit proof that the target length matches the array size. This keeps the spec construction honest and makes mismatches obvious 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)).