Exact reconstruction of the finite factorizations (Cholesky and QR)

Exact algebraic reconstruction for the Cholesky and classical Gram–Schmidt specification recurrences in NN.Spec.Core.Tensor.Factorizations. Both use finite column folds; these theorems do not assert floating-point error bounds or correctness of Cholesky's materialized runtime override. Positive pivots are proof hypotheses, not a runtime success check.

Main results

• isCholesky_of_pos: for a symmetric A : Fin n → Fin n → ℝ whose executable Cholesky pivots are all positive (0 < choleskyFn A j j), the factor L = choleskyFn A satisfies Spec.Factorization.IsCholesky: lower-triangular and A = L · Lᵀ. choleskySpec_reconstruction is the tensor-level corollary.
• qr_mul_eq: for A : Fin m → Fin n → ℝ whose executable Gram–Schmidt R-pivots are positive (0 < Rmat A j j), the factors Q and R satisfy A = Q · R, with R upper-triangular (Rmat_upper_triangular). qrSpec_reconstruction is the tensor-level corollary.

Method

Each executable factor is built by a List.foldl that snocs one column per index. The core technical device is getD_foldl_snoc_read, a general lemma reading the j-th element of such a fold as the step function applied to the length-j prefix. From it, prefix_eq_map/qsPrefix_eq_map identify the prefix with the first j columns of the final factor, and take_map_sum_eq turns the code's List.foldl sums into masked Finset partial sums. The QR fold threads a GSState that snocs onto both the Q-list and the R-list at once; gs_proj_qs and gs_fold_split/rTail_getD recover the single-list read lemmas for each projection (the step depends only on the Q-history). The positive-pivot hypotheses discharge the √-radicand and divisor side conditions.

Scope

This file proves A = L · Lᵀ and A = Q · R purely algebraically. The remaining QR property, orthonormality of the Q factor, Qᵀ Q = 1, is proved in the companion file NN.Proofs.Tensor.Basic.FactorizationsOrthonormal by bridging the executable Gram–Schmidt to Mathlib's gramSchmidt, completing the full Spec.Factorization.IsQR predicate (isQR_of_pos).

List/Finset bridges

theorem Spec.Factorization.Reconstruction.foldl_addf_eq_sum {β : Type u_1} (h : β → ℝ) (l : List β) (a : ℝ) : List.foldl (fun (acc : ℝ) (x : β) => acc + h x) a l = a + (List.map h l).sum

A left fold acc + h x accumulates the mapped list sum.

theorem Spec.Factorization.Reconstruction.foldl_add_eq_sum (l : List ℝ) (a : ℝ) : List.foldl (fun (x1 x2 : ℝ) => x1 + x2) a l = a + l.sum

A left +-fold accumulates the list sum.

theorem Spec.Factorization.Reconstruction.foldl_addsq_eq_sum (l : List ℝ) (a : ℝ) : List.foldl (fun (s x : ℝ) => s + x * x) a l = a + (List.map (fun (x : ℝ) => x * x) l).sum

A left s + x*x-fold accumulates the sum of squares.

theorem Spec.Factorization.Reconstruction.finsum_eq_finRange_sum {n : ℕ} (h : Fin n → ℝ) : ∑ i : Fin n, h i = (List.map h (List.finRange n)).sum

A Fin n sum is the list sum over finRange n.

Cholesky: the column-building step

choleskyColsFn is a left fold that snocs one column per index. cholStep names the function it appends, so that the read lemmas above can be specialized to it.

noncomputable def Spec.Factorization.Reconstruction.cholStep {n : ℕ} (A : Fin n → Fin n → ℝ) (cols : List (Fin n → ℝ)) (j : Fin n) : Fin n → ℝ

The column appended at index j of the Cholesky fold, given the columns cols built so far.

theorem Spec.Factorization.Reconstruction.choleskyColsFn_eq {n : ℕ} (A : Fin n → Fin n → ℝ) : choleskyColsFn A = List.foldl (fun (cols : List (Fin n → ℝ)) (j : Fin n) => cols ++ [cholStep A cols j]) [] (List.finRange n)

choleskyColsFn is the snoc-fold appending cholStep.

theorem Spec.Factorization.Reconstruction.cholStep_diag {n : ℕ} (A : Fin n → Fin n → ℝ) (cols : List (Fin n → ℝ)) (j : Fin n) : cholStep A cols j j = MathFunctions.sqrt (A j j - List.foldl (fun (s x : ℝ) => s + x * x) 0 (List.map (fun (ck : Fin n → ℝ) => ck j) cols))

The diagonal value produced by cholStep.

theorem Spec.Factorization.Reconstruction.cholStep_offdiag {n : ℕ} (A : Fin n → Fin n → ℝ) (cols : List (Fin n → ℝ)) {i j : Fin n} (hij : ↑j < ↑i) : cholStep A cols j i = (A i j - List.foldl (fun (acc x : ℝ) => acc + x) 0 (List.map (fun (ck : Fin n → ℝ) => ck i * ck j) cols)) / MathFunctions.sqrt (A j j - List.foldl (fun (s x : ℝ) => s + x * x) 0 (List.map (fun (ck : Fin n → ℝ) => ck j) cols))

The below-diagonal value produced by cholStep.

noncomputable def Spec.Factorization.Reconstruction.prefixCols {n : ℕ} (A : Fin n → Fin n → ℝ) (j : Fin n) : List (Fin n → ℝ)

The length-j prefix of Cholesky columns built before index j.

theorem Spec.Factorization.Reconstruction.choleskyFn_eq_step {n : ℕ} (A : Fin n → Fin n → ℝ) (i j : Fin n) : choleskyFn A i j = cholStep A (prefixCols A j) j i

Entry (i, j) of the executable Cholesky factor equals cholStep evaluated on the prefix.

theorem Spec.Factorization.Reconstruction.prefix_eq_map {n : ℕ} (A : Fin n → Fin n → ℝ) (j : Fin n) : prefixCols A j = List.map (fun (k r : Fin n) => choleskyFn A r k) (List.take (↑j) (List.finRange n))

The prefix of Cholesky columns is exactly the first j columns of the final factor L, each presented as the function r ↦ L r k.

List/Finset partial-sum bridges

theorem Spec.Factorization.Reconstruction.mem_take_finRange {n m : ℕ} {x : Fin n} (hx : x ∈ List.take m (List.finRange n)) : ↑x < m

Every element of a finRange prefix has index below the cut.

theorem Spec.Factorization.Reconstruction.mem_drop_finRange {n m : ℕ} {x : Fin n} (hx : x ∈ List.drop m (List.finRange n)) : m ≤ ↑x

Every element of a finRange tail has index at least the cut.

theorem Spec.Factorization.Reconstruction.take_map_sum_eq {n : ℕ} (m : ℕ) (f : Fin n → ℝ) : (List.map f (List.take m (List.finRange n))).sum = ∑ k : Fin n, if ↑k < m then f k else 0

Mapping f over a finRange prefix and summing equals the masked full sum.

theorem Spec.Factorization.Reconstruction.cross_sum_eq {n : ℕ} (A : Fin n → Fin n → ℝ) (i j : Fin n) : List.foldl (fun (acc x : ℝ) => acc + x) 0 (List.map (fun (ck : Fin n → ℝ) => ck i * ck j) (prefixCols A j)) = ∑ k : Fin n, if ↑k < ↑j then choleskyFn A i k * choleskyFn A j k else 0

The Cholesky cross-sum equals the masked partial dot product of rows i and j of L.

theorem Spec.Factorization.Reconstruction.sumsq_eq {n : ℕ} (A : Fin n → Fin n → ℝ) (j : Fin n) : List.foldl (fun (s x : ℝ) => s + x * x) 0 (List.map (fun (ck : Fin n → ℝ) => ck j) (prefixCols A j)) = ∑ k : Fin n, if ↑k < ↑j then choleskyFn A j k * choleskyFn A j k else 0

The Cholesky diagonal sum-of-squares equals the masked partial squared norm of row j of L.

Closed-form entries of the executable Cholesky factor

theorem Spec.Factorization.Reconstruction.choleskyFn_diag_eq {n : ℕ} (A : Fin n → Fin n → ℝ) (j : Fin n) : choleskyFn A j j = √(A j j - ∑ k : Fin n, if ↑k < ↑j then choleskyFn A j k * choleskyFn A j k else 0)

The diagonal entry of L in closed form: L[j,j] = √(A[j,j] − Σ_{k<j} L[j,k]²).

theorem Spec.Factorization.Reconstruction.choleskyFn_offdiag_eq {n : ℕ} (A : Fin n → Fin n → ℝ) {i j : Fin n} (hij : ↑j < ↑i) : choleskyFn A i j = (A i j - ∑ k : Fin n, if ↑k < ↑j then choleskyFn A i k * choleskyFn A j k else 0) / choleskyFn A j j

The below-diagonal entry of L in closed form: L[i,j] = (A[i,j] − Σ_{k<j} L[i,k]·L[j,k]) / L[j,j] for i > j.

Reconstruction A = L · Lᵀ

Closed-form entries and positive pivots give reconstruction on and below the diagonal. Symmetry then gives the remaining entries.

theorem Spec.Factorization.Reconstruction.choleskyFn_dot_eq {n : ℕ} (A : Fin n → Fin n → ℝ) (hpos : ∀ (j : Fin n), 0 < choleskyFn A j j) {i j : Fin n} (hji : ↑j ≤ ↑i) : ∑ k : Fin n, choleskyFn A i k * choleskyFn A j k = A i j

Per-entry reconstruction for the lower part (j ≤ i): the (i, j) entry of L · Lᵀ is A i j.

theorem Spec.Factorization.Reconstruction.choleskyFn_dot {n : ℕ} (A : Fin n → Fin n → ℝ) (hsymm : ∀ (i j : Fin n), A i j = A j i) (hpos : ∀ (j : Fin n), 0 < choleskyFn A j j) (i j : Fin n) : ∑ k : Fin n, choleskyFn A i k * choleskyFn A j k = A i j

Per-entry reconstruction for all (i, j), using symmetry of A.

theorem Spec.Factorization.Reconstruction.isCholesky_of_pos {n : ℕ} (A : Fin n → Fin n → ℝ) (hsymm : ∀ (i j : Fin n), A i j = A j i) (hpos : ∀ (j : Fin n), 0 < choleskyFn A j j) : IsCholesky (Matrix.of A) (Matrix.of (choleskyFn A))

For a symmetric A whose specification Cholesky pivots are all positive (0 < L[j,j]), the factor L = choleskyFn A is a Cholesky factor: lower-triangular with A = L · Lᵀ.

theorem Spec.Factorization.Reconstruction.choleskySpec_reconstruction {n : ℕ} (A : TorchLean.Tensor ℝ [n, n]) (hsymm : ∀ (i j : Fin n), get2 A i j = get2 A j i) (hpos : ∀ (j : Fin n), 0 < get2 (choleskySpec A) j j) (i j : Fin n) : get2 A i j = ∑ k : Fin n, get2 (choleskySpec A) i k * get2 (choleskySpec A) j k

For a symmetric tensor A whose choleskySpec pivots are positive, every entry of A is reconstructed by L · Lᵀ: A[i,j] = Σ_k L[i,k] · L[j,k], with L = choleskySpec A.

QR (classical Gram–Schmidt): exact reconstruction A = Q · R

gramSchmidtFn threads a GSState that snocs a column onto both the Q-list and the R-list at each index. The appended values depend only on the Q-history (st.qs), never on the R-history, so the Q-list is itself a single-list snoc-fold (gs_proj_qs) and the R-list is the Q-prefix-indexed tail rTail.

noncomputable def Spec.Factorization.Reconstruction.gsA {n m : ℕ} (A : Fin m → Fin n → ℝ) (j : Fin n) : Fin m → ℝ

Column j of A as a function of the row.

noncomputable def Spec.Factorization.Reconstruction.gsRkjs {n m : ℕ} (A : Fin m → Fin n → ℝ) (qs : List (Fin m → ℝ)) (j : Fin n) : List ℝ

The R off-diagonal entries rₖⱼ = qₖ · a for the columns qs built so far.

noncomputable def Spec.Factorization.Reconstruction.gsV {n m : ℕ} (A : Fin m → Fin n → ℝ) (qs : List (Fin m → ℝ)) (j : Fin n) : Fin m → ℝ

The orthogonalized (not-yet-normalized) vector v = a − Σ rₖⱼ qₖ.

noncomputable def Spec.Factorization.Reconstruction.gsRjj {n m : ℕ} (A : Fin m → Fin n → ℝ) (qs : List (Fin m → ℝ)) (j : Fin n) : ℝ

The diagonal R entry rⱼⱼ = ‖v‖.

noncomputable def Spec.Factorization.Reconstruction.qStep {n m : ℕ} (A : Fin m → Fin n → ℝ) (qs : List (Fin m → ℝ)) (j : Fin n) : Fin m → ℝ

The Q column appended at index j: v / rⱼⱼ (or 0 when rⱼⱼ = 0).

noncomputable def Spec.Factorization.Reconstruction.rStep {n m : ℕ} (A : Fin m → Fin n → ℝ) (qs : List (Fin m → ℝ)) (j : Fin n) : Fin n → ℝ

The R column at column index j, as a function of the row index k (so the value is the matrix entry R[k, j]). With R indexed row-then-column, the nonzero part is on and above the diagonal: rₖⱼ for k < j (strictly above the diagonal), rⱼⱼ for k = j, and 0 for k > j (strictly below the diagonal).

theorem Spec.Factorization.Reconstruction.gramSchmidtFn_eq {n m : ℕ} (A : Fin m → Fin n → ℝ) : gramSchmidtFn A = List.foldl (fun (st : GSState m n ℝ) (j : Fin n) => { qs := st.qs ++ [qStep A st.qs j], rcols := st.rcols ++ [rStep A st.qs j] }) { qs := [], rcols := [] } (List.finRange n)

gramSchmidtFn as the dual-list snoc-fold appending qStep/rStep.

theorem Spec.Factorization.Reconstruction.gs_proj_qs {n m : ℕ} (A : Fin m → Fin n → ℝ) (l : List (Fin n)) (q0 : List (Fin m → ℝ)) (r0 : List (Fin n → ℝ)) : (List.foldl (fun (st : GSState m n ℝ) (j : Fin n) => { qs := st.qs ++ [qStep A st.qs j], rcols := st.rcols ++ [rStep A st.qs j] }) { qs := q0, rcols := r0 } l).qs = List.foldl (fun (qs : List (Fin m → ℝ)) (j : Fin n) => qs ++ [qStep A qs j]) q0 l

The Q-list projection of the structure fold is the single-list qStep snoc-fold.

noncomputable def Spec.Factorization.Reconstruction.qsPrefix {n m : ℕ} (A : Fin m → Fin n → ℝ) (j : Fin n) : List (Fin m → ℝ)

The Q columns built before index j.

noncomputable def Spec.Factorization.Reconstruction.rTail {n m : ℕ} (A : Fin m → Fin n → ℝ) (q0 : List (Fin m → ℝ)) : List (Fin n) → List (Fin n → ℝ)

The R-list tail: the R columns produced from Q-prefix q0 over the indices l.

theorem Spec.Factorization.Reconstruction.gs_fold_split {n m : ℕ} (A : Fin m → Fin n → ℝ) (l : List (Fin n)) (q0 : List (Fin m → ℝ)) (r0 : List (Fin n → ℝ)) : List.foldl (fun (st : GSState m n ℝ) (j : Fin n) => { qs := st.qs ++ [qStep A st.qs j], rcols := st.rcols ++ [rStep A st.qs j] }) { qs := q0, rcols := r0 } l = { qs := List.foldl (fun (qs : List (Fin m → ℝ)) (j : Fin n) => qs ++ [qStep A qs j]) q0 l, rcols := r0 ++ rTail A q0 l }

The structure fold splits into the qStep snoc-fold (Q-list) and the rTail (R-list).

theorem Spec.Factorization.Reconstruction.rTail_getD {n m : ℕ} (A : Fin m → Fin n → ℝ) (q0 : List (Fin m → ℝ)) (l : List (Fin n)) (k : ℕ) (hk : k < l.length) (d : Fin n → ℝ) : (rTail A q0 l).getD k d = rStep A (List.foldl (fun (qs : List (Fin m → ℝ)) (j : Fin n) => qs ++ [qStep A qs j]) q0 (List.take k l)) l[k]

Reading the k-th element of rTail recovers rStep applied to the length-k Q-prefix.

theorem Spec.Factorization.Reconstruction.gtBool_true_iff {x y : ℝ} : Context.gtBool x y = true ↔ y < x

Semantics of the Context > test over ℝ.

Entries of the executable Q and R factors

noncomputable def Spec.Factorization.Reconstruction.Qmat {n m : ℕ} (A : Fin m → Fin n → ℝ) (i : Fin m) (k : Fin n) : ℝ

Entry (i, k) of the Q factor produced by gramSchmidtFn.

noncomputable def Spec.Factorization.Reconstruction.Rmat {n m : ℕ} (A : Fin m → Fin n → ℝ) (k j : Fin n) : ℝ

Entry (k, j) of the R factor produced by gramSchmidtFn.

noncomputable def Spec.Factorization.Reconstruction.Qcol {n m : ℕ} (A : Fin m → Fin n → ℝ) (k : Fin n) : Fin m → ℝ

Column k of Q as a function of the row.

theorem Spec.Factorization.Reconstruction.Qmat_eq {n m : ℕ} (A : Fin m → Fin n → ℝ) (i : Fin m) (k : Fin n) : Qmat A i k = qStep A (qsPrefix A k) k i

Closed form of a Q entry: qStep evaluated on the Q-prefix.

theorem Spec.Factorization.Reconstruction.Rmat_eq {n m : ℕ} (A : Fin m → Fin n → ℝ) (k j : Fin n) : Rmat A k j = rStep A (qsPrefix A j) j k

Closed form of an R entry: rStep evaluated on the Q-prefix.

theorem Spec.Factorization.Reconstruction.rStep_below_diag_zero {n m : ℕ} (A : Fin m → Fin n → ℝ) (qs : List (Fin m → ℝ)) {j k : Fin n} (hjk : ↑j < ↑k) : rStep A qs j k = 0

R is upper-triangular: the entry R[k, j] at a row k strictly below the diagonal (column j < row k) vanishes.

theorem Spec.Factorization.Reconstruction.rStep_diag {n m : ℕ} (A : Fin m → Fin n → ℝ) (qs : List (Fin m → ℝ)) (j : Fin n) : rStep A qs j j = gsRjj A qs j

The diagonal R entry is rⱼⱼ.

theorem Spec.Factorization.Reconstruction.qStep_pos {n m : ℕ} (A : Fin m → Fin n → ℝ) (qs : List (Fin m → ℝ)) (j : Fin n) (h : 0 < gsRjj A qs j) (i : Fin m) : qStep A qs j i = gsV A qs j i / gsRjj A qs j

The Q column when the pivot is positive: qⱼ = v / rⱼⱼ.

The orthogonalization sum as a Finset sum

theorem Spec.Factorization.Reconstruction.cross_fold_eq {m : ℕ} (qs : List (Fin m → ℝ)) (g : (Fin m → ℝ) → ℝ) (i : Fin m) (a : ℝ) : List.foldl (fun (acc : ℝ) (x : (Fin m → ℝ) × ℝ) => match x with | (qk, r) => acc + r * qk i) a (qs.zip (List.map g qs)) = a + (List.map (fun (qk : Fin m → ℝ) => g qk * qk i) qs).sum

The zip-fold defining v collapses to a single map-fold over the Q columns.

theorem Spec.Factorization.Reconstruction.gsV_eq {n m : ℕ} (A : Fin m → Fin n → ℝ) (qs : List (Fin m → ℝ)) (j : Fin n) (i : Fin m) : gsV A qs j i = gsA A j i - (List.map (fun (qk : Fin m → ℝ) => dotFn qk (gsA A j) * qk i) qs).sum

Closed form of v i: A i j minus the partial projection sum.

theorem Spec.Factorization.Reconstruction.qsPrefix_length {n m : ℕ} (A : Fin m → Fin n → ℝ) (j : Fin n) : (qsPrefix A j).length = ↑j

Length of the Q-prefix list.

theorem Spec.Factorization.Reconstruction.qsPrefix_eq_map {n m : ℕ} (A : Fin m → Fin n → ℝ) (j : Fin n) : qsPrefix A j = List.map (fun (k : Fin n) => Qcol A k) (List.take (↑j) (List.finRange n))

The Q-prefix is exactly the first j columns of the final factor Q.

theorem Spec.Factorization.Reconstruction.getD_map_dotFn {m : ℕ} (qs : List (Fin m → ℝ)) (a : Fin m → ℝ) (k : ℕ) (hk : k < qs.length) : (List.map (fun (qk : Fin m → ℝ) => dotFn qk a) qs).getD k 0 = dotFn (qs.getD k fun (x : Fin m) => 0) a

getD commutes with dotFn-mapping when the index is in range.

theorem Spec.Factorization.Reconstruction.qsPrefix_getD {n m : ℕ} (A : Fin m → Fin n → ℝ) {k j : Fin n} (hkj : ↑k < ↑j) : ((qsPrefix A j).getD ↑k fun (x : Fin m) => 0) = Qcol A k

A Q-prefix entry equals the final Q column at that index.

theorem Spec.Factorization.Reconstruction.Rmat_above_diag_dot {n m : ℕ} (A : Fin m → Fin n → ℝ) {k j : Fin n} (hkj : ↑k < ↑j) : Rmat A k j = dotFn (Qcol A k) (gsA A j)

The strictly-above-diagonal R entry R[k, j] (row k < column j) is the inner product of Q column k with column j.

theorem Spec.Factorization.Reconstruction.cross_sum_qr {n m : ℕ} (A : Fin m → Fin n → ℝ) (i : Fin m) (j : Fin n) : (List.map (fun (qk : Fin m → ℝ) => dotFn qk (gsA A j) * qk i) (qsPrefix A j)).sum = ∑ k : Fin n, if ↑k < ↑j then Rmat A k j * Qmat A i k else 0

The projection sum equals the masked partial sum Σ_{k<j} R[k,j]·Q[i,k].

Exact reconstruction A = Q · R

theorem Spec.Factorization.Reconstruction.Rmat_upper_triangular {n m : ℕ} (A : Fin m → Fin n → ℝ) {k j : Fin n} (hjk : ↑j < ↑k) : Rmat A k j = 0

R is upper-triangular: the entry R[k, j] strictly below the diagonal (column j < row k) vanishes.

theorem Spec.Factorization.Reconstruction.qr_reconstruction {n m : ℕ} (A : Fin m → Fin n → ℝ) (hrank : ∀ (j : Fin n), 0 < Rmat A j j) (i : Fin m) (j : Fin n) : A i j = ∑ k : Fin n, Qmat A i k * Rmat A k j

When every specification R pivot is positive, A[i,j] = Σ_k Q[i,k]·R[k,j].

theorem Spec.Factorization.Reconstruction.qr_mul_eq {n m : ℕ} (A : Fin m → Fin n → ℝ) (hrank : ∀ (j : Fin n), 0 < Rmat A j j) : Matrix.of A = (Matrix.of fun (i : Fin m) (k : Fin n) => Qmat A i k) * Matrix.of fun (k j : Fin n) => Rmat A k j

A = Q · R for the specification Gram–Schmidt factors under positive R pivots.

theorem Spec.Factorization.Reconstruction.qrSpec_reconstruction {n m : ℕ} (A : TorchLean.Tensor ℝ [m, n]) (hrank : ∀ (j : Fin n), 0 < get2 (qrRSpec A) j j) (i : Fin m) (j : Fin n) : get2 A i j = ∑ k : Fin n, get2 (qrQSpec A) i k * get2 (qrRSpec A) k j

For a tensor A whose qrSpec R-pivots are positive, every entry of A is reconstructed by Q · R: A[i,j] = Σ_k Q[i,k]·R[k,j], with Q = qrQSpec A, R = qrRSpec A.