Correctness of the exact matrix factorizations (Cholesky and QR)

This file sets up the formal correctness layer for the two exact, finite spec-layer factorizations in NN.Spec.Core.Tensor.Factorizations (choleskySpec, qrSpec): the factorization predicates over real matrices, and the first structural theorem about the executable Cholesky factor.

Architecture (refinement)

• Specifications (IsCholesky, IsQR) are Props on Mathlib Matrix (Fin n) (Fin n) ℝ. Mathlib's Matrix m n α is definitionally m → n → α, so the function representation Spec.toMatFn produced by the executable specs bridges for free.
• Fold-indexing lemmas (length_foldl_snoc, getD_foldl_snoc_lt, getD_foldl_snoc_read, getD_foldl_finRange) read off the column produced at a given position of the left fold that both choleskyColsFn and gramSchmidtFn use to build their output, bridging the executable List.foldl form to per-entry reasoning. They live here once and are reused by FactorizationsReconstruction.
• Structural theorem. The executable Cholesky factor is lower-triangular (choleskyFn_lower_triangular, lifted to the tensor level as choleskySpec_lower_triangular), proved directly from the column fold — the above-diagonal entry is forced to 0 by construction.

Scope

This file proves only the predicates and the lower-triangularity fact. The exact algebraic reconstructions — A = L · Lᵀ for Cholesky (under positive pivots) and A = Q · R with Qᵀ Q = 1 for Gram–Schmidt (under full column rank) — are proved in the companion modules NN.Proofs.Tensor.Basic.FactorizationsReconstruction and NN.Proofs.Tensor.Basic.FactorizationsOrthonormal. Everything here is an exact identity over ℝ; the only hypotheses are the genuine success conditions of the algorithms.

Specifications

The mathematical meaning of each factorization, as a predicate over real matrices. Over ℝ, star = id so conjTranspose = transpose; we phrase everything with ᵀ.

def Spec.Factorization.IsCholesky {n : ℕ} (A L : Matrix (Fin n) (Fin n) ℝ) : Prop

L is a Cholesky factor of A: lower-triangular with A = L · Lᵀ.

def Spec.Factorization.IsQR {m k : ℕ} (A Q : Matrix (Fin m) (Fin k) ℝ) (R : Matrix (Fin k) (Fin k) ℝ) : Prop

(Q, R) is a QR factorization of A: Q has orthonormal columns, R is upper-triangular, A = Q · R.

Fold-indexing for the column-building specs

choleskyColsFn and gramSchmidtFn build their output with a left fold that appends one column per index. The lemmas here read off the column produced at a given position, bridging the executable List.foldl form to per-entry reasoning. They are generic over the appended-value function g and are the single home for these snoc-fold read lemmas — FactorizationsReconstruction reuses them.

theorem Spec.Factorization.length_foldl_snoc {β : Type u_1} {ι : Type u_2} (g : List β → ι → β) (l : List ι) (acc : List β) : (List.foldl (fun (s : List β) (a : ι) => s ++ [g s a]) acc l).length = acc.length + l.length

A left fold that appends one element per input grows the accumulator by l.length.

theorem Spec.Factorization.getD_foldl_snoc_lt {β : Type u_1} {ι : Type u_2} (g : List β → ι → β) (d : β) (l : List ι) (acc : List β) (k : ℕ) (hk : k < acc.length) : (List.foldl (fun (s : List β) (a : ι) => s ++ [g s a]) acc l).getD k d = acc.getD k d

A fold that only appends never changes an index already inside the accumulator.

theorem Spec.Factorization.getD_foldl_snoc_read {β : Type u_1} {ι : Type u_2} (g : List β → ι → β) (d : β) (l : List ι) (k : ℕ) (hk : k < l.length) : (List.foldl (fun (s : List β) (a : ι) => s ++ [g s a]) [] l).getD k d = g (List.foldl (fun (s : List β) (a : ι) => s ++ [g s a]) [] (List.take k l)) l[k]

The element at position k of the snoc-fold over an arbitrary list l is g applied to the fold of the length-k prefix and the k-th element.

theorem Spec.Factorization.getD_foldl_finRange {n : ℕ} {β : Type u_1} (g : List β → Fin n → β) (d : β) (j : Fin n) : (List.foldl (fun (s : List β) (a : Fin n) => s ++ [g s a]) [] (List.finRange n)).getD (↑j) d = g (List.foldl (fun (s : List β) (a : Fin n) => s ++ [g s a]) [] (List.take (↑j) (List.finRange n))) j

The element at position j of the snoc-fold over finRange n is g applied to the fold of the length-j prefix and the index j.

Cholesky factor is lower-triangular

A structural fact about the executable choleskyFn, proved directly from the column fold: the entry above the diagonal is forced to 0 by the construction.

theorem Spec.Factorization.get2_ofMatFn {m k : ℕ} (f : Fin m → Fin k → ℝ) (i : Fin m) (j : Fin k) : get2 (ofMatFn f) i j = f i j

Reading an entry of a matrix tensor built by ofMatFn returns the underlying function value.

theorem Spec.Factorization.choleskyFn_lower_triangular {n : ℕ} (A : Fin n → Fin n → ℝ) {i j : Fin n} (hij : ↑i < ↑j) : choleskyFn A i j = 0

The executable Cholesky factor is lower-triangular: entries strictly above the diagonal vanish.

theorem Spec.Factorization.choleskySpec_lower_triangular {n : ℕ} (A : Tensor ℝ (Shape.dim n (Shape.dim n Shape.scalar))) {i j : Fin n} (hij : ↑i < ↑j) : get2 (choleskySpec A) i j = 0

Tensor-level statement: the Cholesky factor choleskySpec A is lower-triangular.