Exact Cholesky and QR Specifications

IsCholesky and IsQR state the factorization properties using mathlib matrices. The fold-indexing lemmas track columns appended by the specification recurrences, and choleskySpec_lower_triangular shows that the Cholesky recurrence sets above-diagonal entries to zero without a pivot assumption.

FactorizationsReconstruction proves Cholesky reconstruction under symmetry and positive pivots, and QR reconstruction under positive pivots. FactorizationsOrthonormal supplies QR orthonormality. These are exact real-arithmetic results about the specification bodies. They do not establish floating-point stability or the equivalence of Cholesky's implemented_by runtime override.

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.

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_matrix {m k : ℕ} (f : Fin m → Fin k → ℝ) (i : Fin m) (j : Fin k) : get2 (TorchLean.Tensor.matrix f) i j = f i j

Reading an entry of a matrix tensor 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 : TorchLean.Tensor ℝ [n, n]) {i j : Fin n} (hij : ↑i < ↑j) : get2 (choleskySpec A) i j = 0

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