Linear Algebra IR Lowering

Checked lowering for matrix multiplication and payload-backed linear layers.

Both operations accept the same shapes as the IR semantics: any shared leading shape followed by the matrix axes. lowerMatmul obtains the output shape from OpContracts.inferMatmulOutShape, the contract shared with shape inference and evaluation, and only decomposes the parent shapes itself to build typed indices. The closures apply NN.IR.Graph.matmulLeading and NN.IR.Graph.linearLeading, the same typed operators the IR evaluator uses.

Each operation has its own small lower* definition. lowerLinearAlgebra only dispatches on the operation kind, and the lowerLinearAlgebra_* equation lemmas let correctness proofs reduce a dispatch to the branch they care about without unfolding the whole dispatcher.

def Runtime.Autograd.IRExec.Internal.lowerMatmul {α : Type} [TorchLean.Storage α] [Context α] {Γ : List Spec.Shape} (ctx : NodeLoweringContext α Γ) : NodeLoweringResult ctx

Checked lowering for .matmul over any shared leading shape.

The final two axes follow the matrix rule (... × m × n) · (... × n × p) → (... × m × p). The output shape is taken from OpContracts.inferMatmulOutShape; the typed decomposition below is checked against it so the contract remains the single source of truth.

def Runtime.Autograd.IRExec.Internal.lowerLinear {α : Type} [TorchLean.Storage α] [Context α] {Γ : List Spec.Shape} (ctx : NodeLoweringContext α Γ) : NodeLoweringResult ctx

Checked lowering for .linear over any leading shape.

The final input axis must equal the payload's inDim; every leading axis is preserved and the affine map y = Wx + b is applied independently at each leading index.

def Runtime.Autograd.IRExec.Internal.lowerLinearAlgebra {α : Type} [TorchLean.Storage α] [Context α] {Γ : List Spec.Shape} (ctx : NodeLoweringContext α Γ) (kind : NN.IR.OpKind) : NodeLoweringResult ctx

Checked lowering for matrix multiplication and payload-backed linear layers.

@[simp]

theorem Runtime.Autograd.IRExec.Internal.lowerLinearAlgebra_matmul {α : Type} [TorchLean.Storage α] [Context α] {Γ : List Spec.Shape} (ctx : NodeLoweringContext α Γ) : lowerLinearAlgebra ctx NN.IR.OpKind.matmul = lowerMatmul ctx

Dispatch equation for .matmul.

@[simp]

theorem Runtime.Autograd.IRExec.Internal.lowerLinearAlgebra_linear {α : Type} [TorchLean.Storage α] [Context α] {Γ : List Spec.Shape} (ctx : NodeLoweringContext α Γ) : lowerLinearAlgebra ctx NN.IR.OpKind.linear = lowerLinear ctx

Dispatch equation for .linear.