Add verified matrix factorizations: Cholesky and QR (exact)

[NicolasRouquette]

A small, single-purpose contribution: the exact, finite half of a verified
matrix-factorization foundation that classical / scientific-ML models rely on —
Gaussian processes, kernel-ridge regression, PCA, least squares.

Context — this supersedes #1

#1 had grown to mix three separable things:

• generic matrix-factorization linear algebra,
• the Computational Hypergraph Discovery (CHD)-specific layers, and
• a KernelFlows port.

Following the question of whether this belongs in TorchLean or in a repo of its own, I've split them:

• For TorchLean (this PR and a follow-up):
  Only the generic, domain-independent factorizations — pure linear algebra, no CHD anywhere.
  To keep review small, even this is split into
  • an exact part (Cholesky / QR, here) and
  • an iterative part (symmetric eig / SVD, in a follow-up PR).
• A separate repository (CHDTorch):
  All CHD- and KernelFlows-specific work, as its own Lean package that takes TorchLean as a library dependency —
  zero changes to TorchLean's source.

So this PR is intentionally the minimal, self-contained piece.

Three layers — what is proved, what is run, what is trusted

This PR is genuinely adding verified linear algebra; please read it as three distinct layers, only the
first of which is a proof obligation:

1. Proved specs (over ℝ via Mathlib) — the verified contribution.
   In NN/Spec/Core/Tensor/Factorizations.lean and NN/Proofs/Tensor/Basic/Factorizations*.lean:

   • the predicates IsCholesky A L (lower-triangular L, A = L·Lᵀ) and IsQR A Q R
     (Qᵀ·Q = 1, upper-triangular R, A = Q·R);
   • triangularity of the Cholesky factor, straight from the column fold;
   • reconstruction A = L·Lᵀ — the theorem isCholesky_of_pos assumes positivity of the
     executable pivots, ∀ j, 0 < choleskyFn A j j, not Matrix.PosDef A. SPD is the expected
     sufficient condition for those pivots to be positive, but the implication
     PosDef A → ∀ j, 0 < choleskyFn A j j is not formalized here;
   • orthonormality Qᵀ·Q = 1 and reconstruction A = Q·R for qrSpec's classical
     Gram–Schmidt, under positive executable R-pivots (full column rank), bridged to Mathlib's
     gramSchmidt.

   These are exact finite identities — no iteration, no sweep count, no asymptotic limit.

2. Executable examples (over Float) — evidence, not proof.
   NN/Examples/Factorization/{Cholesky,QR}: concrete witnesses with residual checks
   (‖A − L·Lᵀ‖, ‖A − Q·R‖, ‖Qᵀ·Q − I‖ at machine zero), each paired with a negative control
   (indefinite A fails Cholesky; rank-deficient A breaks QR orthonormality), wrapped in
   #guard_msgs (drop info) so a regression fails the build. These show the definitions run and
   reconstruct; they are not claims about floating-point arithmetic.

3. Trusted runtime hooks — explicitly outside the proof.
   The strict-array @[implemented_by] replacements are runtime substitutions used so #eval stays
   fast. They are not proved equal to the clean proof definitions; that equivalence is a trusted
   boundary, and the examples are evidence for it, not a proof of it.

The triangular- and ridge-solve helpers that ride on the Cholesky factor (triSolveLower/Upper,
cholSolve, solveRidge) are shipped as executable APIs only — this PR does not prove their
correctness.

Scope honesty

The factorizations themselves are the verified contribution, and their hypotheses are the genuine
success conditions of the algorithms stated as executable-pivot positivity — 0 < choleskyFn A j j
for Cholesky, positive R diagonal (full column rank) for QR — not SPD / rank predicates proved from
scratch. The iterative factorizations — whose convergence needs an a-posteriori residual certificate,
since Mathlib has no Jacobi convergence theory — are deliberately kept out of this PR and into the
follow-up.

sorry / admit / unsafe / opaque-free.

Building it

lake build NN.Proofs.Tensor.Basic NN.Examples.Factorization
cd blueprint && lake build      # renders the new chapter

[Robertboy18]

Thanks for splitting this down to the exact Cholesky/QR core. I like the direction a lot: the main theorem endpoints look useful, and I did not find any new axioms, sorry, admit, unsafe, or opaque in the added proof files.

I do think this needs another cleanup pass before merge. The biggest issue is not the math direction; it is that the PR still contains residue from the broader CHD/eig/SVD version, plus a couple of proof-engineering/trust-boundary details that should be made explicit. Once those are cleaned up, this will be a much easier PR to review and maintain.

[NicolasRouquette]

Thanks for the careful review — all six points addressed in 93f6272. Summary:

1. Spec header overstates scope — trimmed to just choleskySpec/qrSpec plus the ridge-solve helpers; removed the symEigJacobiSpec/svdSpec bullets, the eigendecompSpec relationship section, and the Jacobi-sweeps paragraph. Also dropped the now-dead ltBool/leBool (added only for sorting Jacobi eigenvalues) and the two stray CHD solve_variationnal mentions.

2. Proofs header reads like the old CHD/eig/SVD PR — rewrote the doc block to describe only what's present: the IsCholesky/IsQR predicates, the fold-indexing lemmas, and choleskyFn_lower_triangular. No more IsSymEig/IsSVD/Jacobi-residual references.

3. Blueprint "discharged from Matrix.PosDef" — you're right, there's no such theorem. Reworded to state plainly that isCholesky_of_pos assumes positive executable pivots (0 < choleskyFn A j j) directly as a hypothesis, and added an explicit note that the reduction PosDef A → ∀ j, 0 < choleskyFn A j j is not formalized here.

4. @[implemented_by] trust boundary — added a dedicated "Trust boundary" subsection in the Cholesky section: the strict-array …Impl companions are a trusted, not verified performance hook (no equivalence theorem choleskyColsFn = choleskyColsImpl), so #eval/runtime executes the …Impl body while the proofs constrain only the closure body, and the numeric examples are evidence rather than a proof. Softened every per-def "validate the two agree"/"Both compute the same" accordingly.

5. Duplicated snoc-fold lemmas — length_foldl_snoc/getD_foldl_snoc_lt (and the general getD_foldl_snoc_read) now live once, public, in Factorizations.lean; deleted the entire duplicate FoldSnoc section from FactorizationsReconstruction.lean (it imports the former, and the nested Spec.Factorization.Reconstruction namespace resolves the names).

6. Heavy imports — dropped the five unused spectral/Hermitian/unitary imports (Analysis.Matrix.Spectrum, Analysis.Matrix.PosDef, HermitianFunctionalCalculus, LinearAlgebra.Matrix.PosDef, UnitaryGroup, NonsingularInverse). The proof file now imports just the spec, the linear-algebra proof base, and Data.List.GetD.

I also cleaned the matching residue in NN/Examples/Factorization/Common.lean: the (Cholesky, QR, SymEig, SVD) header and the dead diagFromVec/diagOf/offDiagFrobSq/totalFrobSq/assertApproxEq helpers (the last referenced a removed symEigJacobi_frobenius_residual).

Still sorry/admit/unsafe/opaque-free; lake build NN.Proofs.Tensor.Basic NN.Examples.Factorization and the blueprint build both green. Net −71 lines.

[Robertboy18]

Thanks for the cleanup in 93f6272 — this is much closer, and I like the direction. The core contribution looks useful for TorchLean’s scientific-ML side: exact Cholesky/QR specs, tensor-level APIs, and reconstruction/structure proofs without new axiom/sorry/admit/unsafe/opaque. I also checked the focused build locally with lake build NN.Proofs.Tensor.Basic NN.Examples.Factorization, and that passed.

Before we merge, I think there are a few remaining cleanup/policy items:

1. Please remove the non-project footer lines from the git commit metadata.
   The commits currently include the old non-project footer line. Could you rewrite the commit messages and force-push without that trailer?

2. Please rename the QR algorithm/docs from “modified Gram-Schmidt” to classical/ordinary Gram-Schmidt, unless the implementation is changed.
   The current recurrence computes r[k,j] = q_k · a_j against the original column and subtracts the projections in one pass, which is the classical Gram-Schmidt presentation in exact math. That is totally okay for a first theorem, but the name/docs should match the implementation.

3. Please replace “omega-free” with “sorry/admit-free.”
   Using omega is absolutely fine; it is a normal Lean proof tactic. The only issue is that the current text appears to claim the proofs are omega-free while some proof scripts do use omega.

4. Please clean up the above/below-diagonal naming around R.
   Names/comments like rStep_above and R_below are easy to misread because R is indexed as row/column. Please rename or comment these so “above diagonal” and “below diagonal” are unambiguous.

5. Please make the theorem surface explicit for the solve helpers.
   The Cholesky and QR factorization claims are the verified contribution here. The triangular/ridge solve helpers are useful executable APIs, but as far as I can tell this PR does not yet prove full triangular-solve / ridge-solve correctness. A short note in the docs would prevent readers from thinking those solve correctness theorems have already landed.

6. For @[implemented_by], I’m okay with keeping it only if we keep the trust-boundary wording very explicit.
   The current note is a good start. Long-term, the best version would prove equivalence between the clean proof definitions and the strict array implementations. For this PR, either keeping the documented trust boundary or removing the hooks would both be reasonable; I just want us to be honest about which one we are choosing.

[NicolasRouquette]

Thanks for the detailed review; I made the requested changes and forced-pushed an update.

[Robertboy18]

Thanks for the updates here. Since TorchLean has now moved through the API refactor and Lean 4.31 upgrade, could you please rebase this PR onto current main and rerun the advertised build targets?

From my side, the remaining thing is mostly freshness against current main. Please also make sure the earlier review items remain resolved after the rebase, especially no non-project footer lines in the final git metadata and clear wording around the @[implemented_by] trust boundary.

[NicolasRouquette]

Yes, I'm working on rebasing my branches on top of the updated main using 4.31.0 and retesting...

[NicolasRouquette]

I verified on this branch that ./scripts/checks/check.sh --ci-all runs without any issues.

[Robertboy18]

Thanks for the updates here. I re-checked the current branch for mathematical/specification issues.

Overall, this is much cleaner now. I do not see a serious mathematical blocker in the current Cholesky/QR contribution. The important earlier issues look addressed:

• QR is now described as classical Gram-Schmidt, which matches the recurrence: coefficients are computed against the original column and the projection sum is subtracted in one pass.
• The Cholesky theorem now states the positive executable pivot hypothesis explicitly.
• The @[implemented_by] trust boundary is now described honestly: the strict array versions are runtime replacements, not proved equivalent to the clean proof definitions.
• I did not find new sorry, admit, axiom, unsafe, or opaque in the touched proof/spec files.

One remaining wording cleanup before merge: please keep the SPD story very sharp in the blueprint/docs. The theorem proves Cholesky correctness assuming positive executable pivots:

∀ j, 0 < choleskyFn A j j.

That is different from proving:

Matrix.PosDef A → ∀ j, 0 < choleskyFn A j j.

The docs currently mention that the SPD-to-pivots implication is expected but not formalized, which is good. I would just make sure no surrounding sentence still reads as if SPD itself is the formal hypothesis already proved by this PR.

I also think the final PR description should clearly separate three layers:

1. proved specs: IsCholesky, IsQR, reconstruction, triangularity, orthonormality;
2. executable examples: concrete Float witnesses and residual checks;
3. trusted runtime hooks: @[implemented_by] array-backed implementations used for fast evaluation.

That separation matters because this PR is genuinely adding verified linear algebra, and we should not blur that with runtime implementation-equivalence claims we have not proved yet.

After that wording cleanup, no mathematical blocker from my side.

[Robertboy18]

One last merge-readiness cleanup from my side: the commit metadata now looks clean, but the PR description still ends with:

the old non-project footer line

Please remove that from the PR body before merge. TorchLean is academic work, and I want the public PR metadata/history to reflect the human authorship cleanly. Please keep the PR text focused on the human-authored contribution and the technical scope.

Also, one tiny wording cleanup remains in NN/Spec/Core/Tensor/Factorizations.lean: the top bullet still says Cholesky is “for SPD A.” Since the theorem assumes positive executable pivots rather than proving the SPD-to-pivots implication, please change that phrase to something like “for matrices with positive executable Cholesky pivots.”

After those two small cleanup items, I’m comfortable with this from the math/spec side.

[Robertboy18]

Thanks, the PR body and commit metadata look clean now.

One final presentation cleanup: could you also edit the earlier comment where the old old tooling footer trailer is still quoted? I’m trying to keep the public TorchLean PR page free of tooling footer lines, since this is academic project history.

I’ll clean up my own comments on our side too. Thanks for bearing with the metadata polish.

[NicolasRouquette]

I checked the 3 commits on this PR: https://github.com/lean-dojo/TorchLean/pull/2/commits

i verified that there are no "co-authored..." trailers in the 3 commits for this PR:
2a97fd0
899009c
58d7d05

I removed the trailer in this comment:
#2 (comment)