NF Linear Algebra

Forward (runtime→spec) approximation lemmas for non-elementwise linear algebra ops over NF.

This extends NN.Proofs.RuntimeApprox.NF.Ops with bounds for the core sum-of-products patterns that appear in linear layers and matrix multiplication.

The central trick is to separate proof-friendly scalar fold bounds for dot products from tensor-level wrappers that turn those fold bounds into approxT theorems and graph nodes.

PyTorch correspondence / citations

This is the proof analogue of linear algebra building blocks used throughout PyTorch models: matrix-vector/matrix-matrix multiplication (torch.matmul) and linear layers (torch.nn.functional.linear). https://pytorch.org/docs/stable/generated/torch.matmul.html https://pytorch.org/docs/stable/generated/torch.nn.functional.linear.html

def Proofs.RuntimeApprox.NFBackend.vecGet {β : TorchLean.Floats.NeuralRadix} {fexp : ℤ → ℤ} {rnd : ℝ → ℤ} {n : ℕ} (v : Spec.Tensor (TorchLean.Floats.NF β fexp rnd) (Spec.Shape.dim n Spec.Shape.scalar)) (i : Fin n) : TorchLean.Floats.NF β fexp rnd

Extract the i-th entry of a runtime vector tensor as an NF scalar.

def Proofs.RuntimeApprox.NFBackend.matGet {β : TorchLean.Floats.NeuralRadix} {fexp : ℤ → ℤ} {rnd : ℝ → ℤ} {m n : ℕ} (A : Spec.Tensor (TorchLean.Floats.NF β fexp rnd) (Spec.Shape.dim m (Spec.Shape.dim n Spec.Shape.scalar))) (i : Fin m) (j : Fin n) : TorchLean.Floats.NF β fexp rnd

Extract matrix entry (i,j) from a runtime matrix tensor as an NF scalar.

theorem Proofs.RuntimeApprox.NFBackend.approxT_expand_to_col_spec {β : TorchLean.Floats.NeuralRadix} {fexp : ℤ → ℤ} {rnd : ℝ → ℤ} {n : ℕ} {s : Spec.Shape} {xS : Spec.SpecTensor (Spec.Shape.dim n s)} {xR : Spec.Tensor (TorchLean.Floats.NF β fexp rnd) (Spec.Shape.dim n s)} {eps : ℝ} (hx : approxT toSpec xS xR eps) : approxT toSpec (Spec.Tensor.expandToColSpec xS) xR.expandToColSpec eps

expand_to_col_spec preserves approximation.

This is a purely shape-level view operation (turn a vector into a singleton-column matrix), so it does not introduce new numeric error beyond the input approximation.

theorem Proofs.RuntimeApprox.NFBackend.approxT_matrix_transpose_spec {β : TorchLean.Floats.NeuralRadix} {fexp : ℤ → ℤ} {rnd : ℝ → ℤ} {m n : ℕ} {xS : Spec.SpecTensor (Spec.Shape.dim m (Spec.Shape.dim n Spec.Shape.scalar))} {xR : Spec.Tensor (TorchLean.Floats.NF β fexp rnd) (Spec.Shape.dim m (Spec.Shape.dim n Spec.Shape.scalar))} {eps : ℝ} (hx : approxT toSpec xS xR eps) : approxT toSpec (Spec.Tensor.matrixTransposeSpec xS) xR.matrixTransposeSpec eps

matrix_transpose_spec preserves approximation.

Transpose is a pure reindexing/view operation on tensor entries, so approxT is preserved with the same error budget.

noncomputable def Proofs.RuntimeApprox.NFBackend.dotStep {β : TorchLean.Floats.NeuralRadix} {fexp : ℤ → ℤ} [TorchLean.Floats.NeuralValidExp fexp] {rnd : ℝ → ℤ} {n : ℕ} (epsa epsb : ℝ) (aR bR : Fin n → TorchLean.Floats.NF β fexp rnd) : TorchLean.Floats.NF β fexp rnd × ℝ → Fin n → TorchLean.Floats.NF β fexp rnd × ℝ

One fold step for building a dot-product and tracking a forward error bound.

This is used to bound the error of foldl (fun acc k => acc + aR k * bR k) compared to the corresponding spec (real) dot-product.

noncomputable def Proofs.RuntimeApprox.NFBackend.dotBound {β : TorchLean.Floats.NeuralRadix} {fexp : ℤ → ℤ} [TorchLean.Floats.NeuralValidExp fexp] {rnd : ℝ → ℤ} {n : ℕ} (epsa epsb : ℝ) (aR bR : Fin n → TorchLean.Floats.NF β fexp rnd) : ℝ

Closed-form bound for a runtime dot-product over List.finRange n.

dot_bound epsa epsb aR bR is the accumulated eps component produced by folding dot_step starting from 0.

noncomputable def Proofs.RuntimeApprox.NFBackend.dotBoundExport {β : TorchLean.Floats.NeuralRadix} {fexp : ℤ → ℤ} [TorchLean.Floats.NeuralValidExp fexp] {rnd : ℝ → ℤ} {n : ℕ} (epsa epsb : ℝ) (aR bR : Fin n → TorchLean.Floats.NF β fexp rnd) : ℝ

Public-facing alias of dot_bound.

This keeps exported tensor-bound constructors from depending directly on the local helper name that Lean treats as non-exportable in this file.

noncomputable def Proofs.RuntimeApprox.NFBackend.matVecMulBoundTensor {β : TorchLean.Floats.NeuralRadix} {fexp : ℤ → ℤ} [TorchLean.Floats.NeuralValidExp fexp] {rnd : ℝ → ℤ} {m n : ℕ} (epsA epsV : ℝ) (A : Spec.Tensor (TorchLean.Floats.NF β fexp rnd) (Spec.Shape.dim m (Spec.Shape.dim n Spec.Shape.scalar))) (v : Spec.Tensor (TorchLean.Floats.NF β fexp rnd) (Spec.Shape.dim n Spec.Shape.scalar)) : Spec.SpecTensor (Spec.Shape.dim m Spec.Shape.scalar)

Per-output bound tensor for mat_vec_mul_spec.

Entry i is a dot-product bound for row i of A dotted with v, using dot_bound.

theorem Proofs.RuntimeApprox.NFBackend.approxT_mat_vec_mul_spec {β : TorchLean.Floats.NeuralRadix} {fexp : ℤ → ℤ} [TorchLean.Floats.NeuralValidExp fexp] {rnd : ℝ → ℤ} [TorchLean.Floats.NeuralValidRndToNearest rnd] {m n : ℕ} {AS : Spec.SpecTensor (Spec.Shape.dim m (Spec.Shape.dim n Spec.Shape.scalar))} {vS : Spec.SpecTensor (Spec.Shape.dim n Spec.Shape.scalar)} {AR : Spec.Tensor (TorchLean.Floats.NF β fexp rnd) (Spec.Shape.dim m (Spec.Shape.dim n Spec.Shape.scalar))} {vR : Spec.Tensor (TorchLean.Floats.NF β fexp rnd) (Spec.Shape.dim n Spec.Shape.scalar)} {epsA epsV : ℝ} : approxT toSpec AS AR epsA → approxT toSpec vS vR epsV → approxT toSpec (Spec.matVecMulSpec AS vS) (Spec.matVecMulSpec AR vR) (linfNorm (matVecMulBoundTensor epsA epsV AR vR))

Forward approximation bound for matrix-vector multiplication.

In words: if A and v are each approximated by runtime AR/vR within epsA/epsV, then mat_vec_mul_spec AS vS is approximated by mat_vec_mul_spec AR vR, with error bounded by linf_norm (mat_vec_mul_bound_tensor epsA epsV AR vR).

noncomputable def Proofs.RuntimeApprox.NFBackend.matMulBoundTensor {β : TorchLean.Floats.NeuralRadix} {fexp : ℤ → ℤ} [TorchLean.Floats.NeuralValidExp fexp] {rnd : ℝ → ℤ} {m n p : ℕ} (epsA epsB : ℝ) (A : Spec.Tensor (TorchLean.Floats.NF β fexp rnd) (Spec.Shape.dim m (Spec.Shape.dim n Spec.Shape.scalar))) (B : Spec.Tensor (TorchLean.Floats.NF β fexp rnd) (Spec.Shape.dim n (Spec.Shape.dim p Spec.Shape.scalar))) : Spec.SpecTensor (Spec.Shape.dim m (Spec.Shape.dim p Spec.Shape.scalar))

Per-entry bound tensor for mat_mul_spec.

Entry (i,j) is a dot-product bound for row i of A dotted with column j of B, using dot_bound.

theorem Proofs.RuntimeApprox.NFBackend.approxT_mat_mul_spec {β : TorchLean.Floats.NeuralRadix} {fexp : ℤ → ℤ} [TorchLean.Floats.NeuralValidExp fexp] {rnd : ℝ → ℤ} [TorchLean.Floats.NeuralValidRndToNearest rnd] {m n p : ℕ} {AS : Spec.SpecTensor (Spec.Shape.dim m (Spec.Shape.dim n Spec.Shape.scalar))} {BS : Spec.SpecTensor (Spec.Shape.dim n (Spec.Shape.dim p Spec.Shape.scalar))} {AR : Spec.Tensor (TorchLean.Floats.NF β fexp rnd) (Spec.Shape.dim m (Spec.Shape.dim n Spec.Shape.scalar))} {BR : Spec.Tensor (TorchLean.Floats.NF β fexp rnd) (Spec.Shape.dim n (Spec.Shape.dim p Spec.Shape.scalar))} {epsA epsB : ℝ} : approxT toSpec AS AR epsA → approxT toSpec BS BR epsB → approxT toSpec (Spec.matMulSpec AS BS) (Spec.matMulSpec AR BR) (linfNorm (matMulBoundTensor epsA epsB AR BR))

Forward approximation bound for matrix-matrix multiplication.

In words: if A and B are approximated by runtime matrices AR/BR within epsA/epsB, then mat_mul_spec AS BS is approximated by mat_mul_spec AR BR, with error bounded by linf_norm (mat_mul_bound_tensor epsA epsB AR BR).

def Proofs.RuntimeApprox.NFBackend.matrixTransposeNode {β : TorchLean.Floats.NeuralRadix} {fexp : ℤ → ℤ} {rnd : ℝ → ℤ} {Γ : List Spec.Shape} {m n : ℕ} (x : Idx Γ (Spec.Shape.dim m (Spec.Shape.dim n Spec.Shape.scalar))) : FwdNode toSpec Γ (Spec.Shape.dim n (Spec.Shape.dim m Spec.Shape.scalar))

FwdNode for matrix transpose.

This lifts approxT_matrix_transpose_spec into the FwdGraph interface so transposes can be used inside larger verified graphs.

noncomputable def Proofs.RuntimeApprox.NFBackend.matVecMulNode {β : TorchLean.Floats.NeuralRadix} {fexp : ℤ → ℤ} [TorchLean.Floats.NeuralValidExp fexp] {rnd : ℝ → ℤ} [TorchLean.Floats.NeuralValidRndToNearest rnd] {Γ : List Spec.Shape} {m n : ℕ} (A : Idx Γ (Spec.Shape.dim m (Spec.Shape.dim n Spec.Shape.scalar))) (v : Idx Γ (Spec.Shape.dim n Spec.Shape.scalar)) : FwdNode toSpec Γ (Spec.Shape.dim m Spec.Shape.scalar)

FwdNode for matrix-vector multiplication.

The bound is computed by mat_vec_mul_bound_tensor and then reduced to a scalar budget via linf_norm.

noncomputable def Proofs.RuntimeApprox.NFBackend.matMulNode {β : TorchLean.Floats.NeuralRadix} {fexp : ℤ → ℤ} [TorchLean.Floats.NeuralValidExp fexp] {rnd : ℝ → ℤ} [TorchLean.Floats.NeuralValidRndToNearest rnd] {Γ : List Spec.Shape} {m n p : ℕ} (A : Idx Γ (Spec.Shape.dim m (Spec.Shape.dim n Spec.Shape.scalar))) (B : Idx Γ (Spec.Shape.dim n (Spec.Shape.dim p Spec.Shape.scalar))) : FwdNode toSpec Γ (Spec.Shape.dim m (Spec.Shape.dim p Spec.Shape.scalar))

FwdNode for matrix-matrix multiplication.

The bound is computed by mat_mul_bound_tensor and then reduced to a scalar budget via linf_norm.