Add verified matrix factorizations: Cholesky and QR (exact)

NN/Examples/Factorization.lean

@@ -0,0 +1,19 @@
+/-
+Copyright (c) 2026 TorchLean
+Released under MIT license as described in the file LICENSE.
+Authors: TorchLean Team
+-/
+
+module
+
+public import NN.Examples.Factorization.Common
+public import NN.Examples.Factorization.Cholesky
+public import NN.Examples.Factorization.QR
+
+/-!
+# Matrix-factorization examples (Cholesky and QR)
+
+Executable `#eval` witnesses for the exact finite factorizations: Cholesky `A = L·Lᵀ` and QR `A = Q·R`
+(with `Qᵀ·Q = I`). Each pairs a positive reconstruction/orthonormality check with a negative control,
+over `Float`, sorry/admit-free.
+-/

NN/Examples/Factorization/Cholesky.lean

@@ -0,0 +1,65 @@
+/-
+Copyright (c) 2026 TorchLean
+Released under MIT license as described in the file LICENSE.
+Authors: TorchLean Team
+-/
+
+module
+
+public import NN.Examples.Factorization.Common
+meta import NN.Examples.Factorization.Common
+
+/-!
+# Example: Cholesky factorization
+
+`choleskySpec A` returns the lower-triangular `L` with `A = L · Lᵀ` for a symmetric
+positive-definite `A`. Here we factor a 3×3 SPD matrix and check the reconstruction error.
+-/
+
+@[expose] public section
+
+
+namespace NN.Examples.Factorization.Cholesky
+
+/-- A symmetric positive-definite test matrix. -/
+def A : Spec.Tensor Float (.dim 3 (.dim 3 .scalar)) :=
+  mkMat [[4, 2, 2],
+         [2, 5, 3],
+         [2, 3, 6]]
+
+/-- The Cholesky factor `L` (lower-triangular). -/
+def L : Spec.Tensor Float (.dim 3 (.dim 3 .scalar)) := Spec.choleskySpec A
+
+/-- Reconstruction error `‖A - L·Lᵀ‖_max`. -/
+def reconErr : Float := maxMatErr A (mm L (tr L))
+
+-- Inspect the diagonal of the factor.
+#guard_msgs (drop info) in
+#eval vecToList (Spec.ofVecFn (fun i : Fin 3 => Spec.get2 L i i))
+
+-- Compiled assertion: the factorization reconstructs A (fails the build otherwise).
+#guard_msgs (drop info) in
+#eval assertLt "Cholesky A = L·Lᵀ" reconErr
+
+/-! ## Negative control: the positive-pivot hypothesis is necessary
+
+`isCholesky_of_pos` requires the executable pivots `L[j,j]` to be positive (`0 < choleskyFn A j j`),
+which is exactly the success condition over the reals (SPD is the expected — but here unformalized —
+sufficient condition for it). The matrix below is symmetric but *not* positive-definite (eigenvalues
+`3` and `-1`), so a pivot is non-positive, the diagonal step takes `√(negative)`, and the reconstruction
+is `NaN` — never a small error. This documents that the hypothesis genuinely bites. -/
+
+/-- A symmetric but **indefinite** matrix (eigenvalues `{3, -1}`), outside Cholesky's domain. -/
+def Abad : Spec.Tensor Float (.dim 2 (.dim 2 .scalar)) :=
+  mkMat [[1, 2],
+         [2, 1]]
+
+def Lbad : Spec.Tensor Float (.dim 2 (.dim 2 .scalar)) := Spec.choleskySpec Abad
+-- Use the *summed* Frobenius error here, not `maxMatErr`: IEEE `max` ignores `NaN`, whereas the sum
+-- propagates the `NaN` produced by `√(negative)`, faithfully reporting that no factor exists.
+def reconErrBad : Float := frobSqErr Abad (mm Lbad (tr Lbad))
+
+#guard_msgs (drop info) in
+#eval assertReconFails "Cholesky on indefinite A correctly fails (no SPD ⇒ no factor)" reconErrBad
+
+end NN.Examples.Factorization.Cholesky

NN/Examples/Factorization/Common.lean

@@ -0,0 +1,96 @@
+/-
+Copyright (c) 2026 TorchLean
+Released under MIT license as described in the file LICENSE.
+Authors: TorchLean Team
+-/
+
+module
+
+public import NN.Spec.Core.Tensor.Factorizations
+
+/-!
+# Factorization examples — shared helpers
+
+Small `Float`-valued helpers used by the matrix-factorization examples (`Cholesky`, `QR`). These
+examples are *executable sanity checks*: each one 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.
+-/
+
+@[expose] public section
+
+
+namespace NN.Examples.Factorization
+
+/-- Build an `m × n` `Float` matrix tensor from a row-major nested list. Missing entries are `0`. -/
+def mkMat {m n : Nat} (rows : List (List Float)) : Spec.Tensor Float (.dim m (.dim n .scalar)) :=
+  Spec.ofMatFn (fun i j => (rows.getD i.val []).getD j.val 0.0)
+
+/-- Maximum entrywise absolute difference between two `m × n` matrices. -/
+def maxMatErr {m n : Nat} (A B : Spec.Tensor Float (.dim m (.dim n .scalar))) : Float :=
+  (List.finRange m).foldl (fun acc i =>
+    (List.finRange n).foldl
+      (fun a j => max a (Float.abs (Spec.get2 A i j - Spec.get2 B i j))) acc) 0.0
+
+/-- Matrix product `A · B` (thin wrapper over `matMulSpec`). -/
+def mm {m n p : Nat} (A : Spec.Tensor Float (.dim m (.dim n .scalar)))
+    (B : Spec.Tensor Float (.dim n (.dim p .scalar))) : Spec.Tensor Float (.dim m (.dim p .scalar)) :=
+  Spec.matMulSpec A B
+
+/-- Matrix transpose. -/
+def tr {m n : Nat} (A : Spec.Tensor Float (.dim m (.dim n .scalar))) :
+    Spec.Tensor Float (.dim n (.dim m .scalar)) :=
+  Spec.Tensor.matrixTransposeSpec A
+
+/-- Read a vector tensor back out as a `List Float` (for display). -/
+def vecToList {n : Nat} (v : Spec.Tensor Float (.dim n .scalar)) : List Float :=
+  (List.finRange n).map (fun i => Spec.Tensor.toScalar (Spec.get v i))
+
+/-- Squared Frobenius distance `Σ_{i,j} (A_ij - B_ij)²` between two `m × n` matrices. -/
+def frobSqErr {m n : Nat} (A B : Spec.Tensor Float (.dim m (.dim n .scalar))) : Float :=
+  (List.finRange m).foldl (fun acc i =>
+    (List.finRange n).foldl
+      (fun a j => let d := Spec.get2 A i j - Spec.get2 B i j; a + d * d) acc) 0.0
+
+/-- Shared tolerance for reconstruction-error assertions. -/
+def tol : Float := 1e-6
+
+/--
+Compiled **positive** assertion: print `name: OK (err)` when `err < 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 assertLt (name : String) (err : Float) (tolerance : Float := tol) : IO Unit :=
+  if err < tolerance then
+    IO.println s!"{name}: OK (err = {err})"
+  else
+    throw (IO.userError s!"{name}: FAIL (err = {err} ≥ tol = {tolerance})")
+
+/--
+Compiled **negative-control** assertion: succeeds only when `err ≥ 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 assertGe (name : String) (err : Float) (threshold : Float := 0.5) : IO Unit :=
+  if err ≥ threshold then
+    IO.println s!"{name}: OK (correctly rejected, err = {err} ≥ {threshold})"
+  else
+    throw (IO.userError s!"{name}: FAIL (err = {err} < {threshold}; expected the property to fail)")
+
+/--
+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.
+-/
+def assertReconFails (name : String) (err : Float) (tolerance : Float := tol) : IO Unit :=
+  if err < tolerance then
+    throw (IO.userError s!"{name}: FAIL (unexpectedly reconstructed, err = {err} < {tolerance})")
+  else
+    IO.println s!"{name}: OK (correctly failed, err = {err})"
+
+end NN.Examples.Factorization

NN/Examples/Factorization/QR.lean

@@ -0,0 +1,73 @@
+/-
+Copyright (c) 2026 TorchLean
+Released under MIT license as described in the file LICENSE.
+Authors: TorchLean Team
+-/
+
+module
+
+public import NN.Examples.Factorization.Common
+meta import NN.Examples.Factorization.Common
+
+/-!
+# Example: QR factorization
+
+`qrSpec A` returns `(Q, R)` with `A = Q · R`, `Q` having orthonormal columns and `R`
+upper-triangular (classical Gram–Schmidt). We check both `A = Q·R` and `Qᵀ·Q = I`.
+-/
+
+@[expose] public section
+
+
+namespace NN.Examples.Factorization.QR
+
+/-- A 3×3 test matrix (the classic Householder/QR example). -/
+def A : Spec.Tensor Float (.dim 3 (.dim 3 .scalar)) :=
+  mkMat [[12, -51, 4],
+         [6, 167, -68],
+         [-4, 24, -41]]
+
+/-- Orthonormal `Q` factor. -/
+def Q : Spec.Tensor Float (.dim 3 (.dim 3 .scalar)) := Spec.qrQSpec A
+/-- Upper-triangular `R` factor. -/
+def R : Spec.Tensor Float (.dim 3 (.dim 3 .scalar)) := Spec.qrRSpec A
+
+/-- Reconstruction error `‖A - Q·R‖_max`. -/
+def reconErr : Float := maxMatErr A (mm Q R)
+/-- Orthonormality error `‖Qᵀ·Q - I‖_max`. -/
+def orthoErr : Float := maxMatErr (mm (tr Q) Q) (Spec.identityTensorSpec 3)
+
+-- Compiled assertions (fail the build otherwise).
+#guard_msgs (drop info) in
+#eval assertLt "QR A = Q·R" reconErr
+#guard_msgs (drop info) in
+#eval assertLt "QR Qᵀ·Q = I" orthoErr
+
+/-! ## Negative control: full column rank is necessary for orthonormality
+
+`qrSpec_orthonormal` (`Qᵀ Q = 1`) requires full column rank — positive `R`-pivots
+(`0 < R[j,j]`). The matrix below has a dependent column (`col₂ = 2·col₁`), so Gram–Schmidt produces a
+**zero** `Q` column where the pivot vanishes: `A = Q·R` still holds, but `Qᵀ Q` has a `0` on the
+diagonal, so orthonormality fails. This separates the two guarantees and shows the rank hypothesis
+genuinely bites. -/
+
+/-- A rank-2 matrix (`col₂ = 2·col₁`): reconstructs, but `Q` cannot be orthonormal. -/
+def Adef : Spec.Tensor Float (.dim 3 (.dim 3 .scalar)) :=
+  mkMat [[1, 2, 0],
+         [2, 4, 1],
+         [1, 2, 0]]
+
+def Qdef : Spec.Tensor Float (.dim 3 (.dim 3 .scalar)) := Spec.qrQSpec Adef
+def Rdef : Spec.Tensor Float (.dim 3 (.dim 3 .scalar)) := Spec.qrRSpec Adef
+
+/-- Reconstruction still holds even without full rank. -/
+def reconErrDef : Float := maxMatErr Adef (mm Qdef Rdef)
+/-- Orthonormality fails: `Qᵀ·Q` has a zero diagonal entry, so it is far from `I`. -/
+def orthoErrDef : Float := maxMatErr (mm (tr Qdef) Qdef) (Spec.identityTensorSpec 3)
+
+#guard_msgs (drop info) in
+#eval assertLt "QR(rank-deficient) A = Q·R still reconstructs" reconErrDef
+#guard_msgs (drop info) in
+#eval assertGe "QR(rank-deficient) Qᵀ·Q = I correctly fails (needs full column rank)" orthoErrDef
+
+end NN.Examples.Factorization.QR

NN/Proofs/Tensor/Basic.lean

@@ -9,6 +9,9 @@ module
 public import NN.Proofs.Tensor.Basic.Core
 public import NN.Proofs.Tensor.Basic.Folds
 public import NN.Proofs.Tensor.Basic.LinearAlgebra
+public import NN.Proofs.Tensor.Basic.Factorizations
+public import NN.Proofs.Tensor.Basic.FactorizationsReconstruction
+public import NN.Proofs.Tensor.Basic.FactorizationsOrthonormal
 public import NN.Proofs.Tensor.Basic.BoundsNorms
 public import NN.Proofs.Tensor.Basic.Algebra