Exact reconstruction of the finite factorizations (Cholesky and QR)

This file proves the exact algebraic reconstruction of the finite executable Cholesky and QR factorizations from NN.Spec.Core.Tensor.Factorizations, building on the predicates and fold-indexing lemmas of NN.Proofs.Tensor.Basic.Factorizations. Because Cholesky and Gram–Schmidt are direct, finite constructions — no iteration, no convergence caveat — over ℝ they reconstruct their input on the nose under the success hypotheses (positive pivots / full column rank), an exact identity rather than an a-posteriori bound.

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 exact condition under which the algorithm succeeds over ℝ), the factor L = choleskyFn A satisfies the spec 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, full column rank), the factors Q = gramSchmidtFn A 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_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 foldl-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ᵀ

The diagonal of the rotated/peeled product is reconstructed using the closed-form entries and the positive-pivot hypothesis (0 < L[j,j]), which is exactly the condition under which the executable Cholesky succeeds over ℝ.

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))

Exact Cholesky reconstruction. For a symmetric A whose executable Cholesky pivots are all positive (0 < L[j,j], the success condition over ℝ), the factor L = choleskyFn A is a genuine Cholesky factor: lower-triangular with A = L · Lᵀ.

theorem Spec.Factorization.Reconstruction.choleskySpec_reconstruction {n : ℕ} (A : Tensor ℝ (Shape.dim n (Shape.dim n Shape.scalar))) (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

Tensor-level Cholesky reconstruction. 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 ℝ.

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.

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

Per-entry QR reconstruction. When every R pivot is positive (0 < R[j,j], the full column-rank success condition), 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

Matrix-level QR reconstruction. A = Q · R for the executable Gram–Schmidt factors, under positive R pivots (full column rank).

theorem Spec.Factorization.Reconstruction.qrSpec_reconstruction {n m : ℕ} (A : Tensor ℝ (Shape.dim m (Shape.dim n Shape.scalar))) (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

Tensor-level QR reconstruction. For a tensor A whose qrSpec R-pivots are positive (full column rank), 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.