Factorization examples — shared helpers

Small Float-valued helpers used by the matrix-factorization examples (Cholesky, QR). Each example reconstructs the original matrix from its factors and asserts (via #eval) that the maximum entrywise reconstruction error is below a tolerance, so the build fails if a factorization is wrong.

These run over Float (the executable 64-bit runtime scalar), which is the precision the factorizations target for Gaussian-process / kernel-method use.

def NN.Examples.Factorization.mkMat {m n : ℕ} (rows : List (List Float)) : Spec.Tensor Float (Spec.Shape.dim m (Spec.Shape.dim n Spec.Shape.scalar))

Build an m × n Float matrix tensor from a row-major nested list. Missing entries are 0.

def NN.Examples.Factorization.maxMatErr {m n : ℕ} (A B : Spec.Tensor Float (Spec.Shape.dim m (Spec.Shape.dim n Spec.Shape.scalar))) : Float

Maximum entrywise absolute difference between two m × n matrices.

def NN.Examples.Factorization.mm {m n p : ℕ} (A : Spec.Tensor Float (Spec.Shape.dim m (Spec.Shape.dim n Spec.Shape.scalar))) (B : Spec.Tensor Float (Spec.Shape.dim n (Spec.Shape.dim p Spec.Shape.scalar))) : Spec.Tensor Float (Spec.Shape.dim m (Spec.Shape.dim p Spec.Shape.scalar))

Matrix product $AB$ (thin wrapper over matMulSpec).

def NN.Examples.Factorization.tr {m n : ℕ} (A : Spec.Tensor Float (Spec.Shape.dim m (Spec.Shape.dim n Spec.Shape.scalar))) : Spec.Tensor Float (Spec.Shape.dim n (Spec.Shape.dim m Spec.Shape.scalar))

Matrix transpose.

def NN.Examples.Factorization.vecToList {n : ℕ} (v : Spec.Tensor Float (Spec.Shape.dim n Spec.Shape.scalar)) : List Float

Read a vector tensor back out as a List Float (for display).

def NN.Examples.Factorization.frobSqErr {m n : ℕ} (A B : Spec.Tensor Float (Spec.Shape.dim m (Spec.Shape.dim n Spec.Shape.scalar))) : Float

Squared Frobenius distance $\sum_{i,j}(A_{ij}-B_{ij})^2$ between two m × n matrices.

def NN.Examples.Factorization.tol : Float

Shared tolerance for reconstruction-error assertions.

def NN.Examples.Factorization.assertLt (name : String) (err : Float) (tolerance : Float := tol) : IO Unit

Compiled positive assertion: print name: OK (err) when $\mathrm{err}<\mathrm{tol}$, otherwise raise an IO error so the build/#eval fails. Running this through #eval evaluates with the compiler (fast), unlike #guard, which forces slow kernel reduction of the whole factorization.

def NN.Examples.Factorization.assertGe (name : String) (err : Float) (threshold : Float := 0.5) : IO Unit

Compiled negative-control assertion: succeeds only when $\mathrm{err}\ge\mathrm{threshold}$, i.e. when a property that should not hold is correctly detected as violated. Gives the metric teeth — a reviewer can see the same maxMatErr/residual that reports 0 on a valid factorization reports a large value on an invalid one, so the positive checks are not vacuous.

def NN.Examples.Factorization.assertReconFails (name : String) (err : Float) (tolerance : Float := tol) : IO Unit

Compiled negative-control assertion that a reconstruction fails: succeeds when the error is not below tol — including the NaN produced when a hypothesis is violated (e.g. Cholesky of a non-positive-definite matrix takes √(negative)). Documents that the success hypotheses (positive Cholesky pivots, positive R pivots / full column rank) are genuinely necessary.