Ch28: LUP-SOLVE correctness proof (lupSolve_correct, Theorem 28.2)

[TankTechnology]

Background

Chapter 28 has partial formalization from @caiwei2026 (PR #85).

lupSolve is defined as: forward-substitute Ly = Pb, then back-substitute Ux = y.
forwardSubst_spec and backSubst_spec are fully proved.

What needs to be done

Prove lupSolve_correct:

theorem lupSolve_correct (A : Mat n n) (b : Vec n) :
    Matrix.mulVec A (lupSolve A b) = b := by
  sorry

This corresponds to CLRS Theorem 28.2. The proof composes:

1. lupDecomp_spec — PA = LU (proved, reads from structure field)
2. forwardSubst_spec — Ly = Pb (proved)
3. backSubst_spec — Ux = y (proved)
4. Permutation algebra — applying P and its inverse

Dependencies

Requires lupDecomp_exists (#TODO) to be filled first, since lupDecomp
currently uses Classical.choice non-constructively.

Impact

lupSolve_correct is the transitively-used lemma that blocks:

• matrixInverse_mul_eq_one
• one_mul_matrixInverse_eq_one
• matrixInverse_column_spec
• leastSquares_normal_eq

All of these are "proved" in the current code but their proofs call
lupSolve_correct which is a sorry. Filling lupSolve_correct would
make all of them genuine kernel-checked proofs.

References

• CLRS §28.1, pp. 824–825
• PR feat: formalize CLRS Chapters 27-35 (issues #70-#84) #85 skeleton: Section_28_1_LUP_Decomposition.lean

[TankTechnology]

Issue cleanup note: current main has no Chapter 28 module. References to forward/back substitution and downstream theorems from PR #85 are historical design context, not kernel-checked code on main. This target follows #123 under roadmap #77.

[TankTechnology]

Boundary clarification after #149: inv_eq_lup is only an algebraic consequence of an existing LUP equality; it is not CLRS Theorem 28.2. This issue remains open for the executable lupSolve pipeline and lupSolve_correct, composing forward substitution, back substitution, and permutation algebra.