Linear-algebra operations for the eager engine.

The definitions here cover matrix products, batched products, affine layers, and the corresponding runtime graph nodes shared by CPU and CUDA-backed execution.

def Runtime.Autograd.Tape.linear {α : Type} [TorchLean.Storage α] [Add α] [Mul α] [Zero α] {inDim outDim : ℕ} (t : Tape α) (wId bId xId : ℕ) : Result (Tape α × ℕ)

Fully-connected linear layer y = W x + b (matvec).

Type-level shapes enforce W : (outDim, inDim), x : (inDim,), b : (outDim,). PyTorch comparison: torch.nn.functional.linear.

def Runtime.Autograd.Tape.matmul {α : Type} [TorchLean.Storage α] [Context α] [DecidableRel fun (x1 x2 : α) => x1 > x2] {m n p : ℕ} (t : Tape α) (aId bId : ℕ) (batchA batchB batch : Spec.Shape := Spec.Shape.scalar) [broadcastA : batchA.BroadcastTo batch] [broadcastB : batchB.BroadcastTo batch] : Result (Tape α × ℕ)

Matrix-rank multiplication with explicit batch-prefix broadcasting.

a has shape batchA ++ [m, n], b has shape batchB ++ [n, p], and the result has shape batch ++ [m, p]. The empty-prefix defaults preserve ordinary 2D matrix multiplication. PyTorch comparison: torch.matmul(a, b) for operands of rank at least two.

def Runtime.Autograd.Tape.concatLeadingAxis {α : Type} [TorchLean.Storage α] {n m : ℕ} {s : Spec.Shape} (t : Tape α) (aId bId : ℕ) : Result (Tape α × ℕ)

Concatenate two tensors along dimension 0.

PyTorch comparison: torch.cat([a, b], dim=0).

def Runtime.Autograd.Tape.sliceLeadingAxisRange {α : Type} [TorchLean.Storage α] [Zero α] {n : ℕ} {s : Spec.Shape} (t : Tape α) (xId start len : ℕ) (h : start + len ≤ n) : Result (Tape α × ℕ)

Slice along dimension 0: x[start : start+len].

The proof argument h enforces bounds. PyTorch comparison: x[start:start+len] on tensors with a leading dimension.