Roadmap: Ch28.2-28.3 inversion, SPD decomposition, and least squares

[TankTechnology]

Role

Roadmap tracker for the core content of CLRS Sections 28.2 and 28.3.

Current state on main

Chapter 28 is not represented on current main. PR #85 is historical design
material rather than available Lean infrastructure. This tracker depends on the
Section 28.1 foundation in #77.

Atomic proof targets

• Matrix inversion through repeated LUP-SOLVE, with left/right inverse
  correctness and the principal cubic work claim.
• Ch28: LDL^T decomposition — existence proof (ldltDecomp_exists, Theorem 28.4) #125 — LDLᵀ decomposition existence for SPD matrices (Theorem 28.4)
• Ch28: Least-squares optimality proof (leastSquares_optimal, Theorem 28.5) #126 — least-squares optimality (Theorem 28.5)

A dedicated matrix-inversion child issue should be split from this tracker when
Section 28.1 lands and the concrete public interface is known.

Completion criteria

The represented algorithms and decompositions compile with their mathematical
correctness theorems; the progress source, proof map, chapter guide, and focused
interface tests agree.

Out of scope

Exercises, chapter-end Problems, numerical-stability analysis, floating-point
roundoff, and low-level linear-algebra kernels.

[TankTechnology]

Progress update: #149 added the algebraic Section 28.2 bridge inv_eq_lup plus permutation-matrix inverse lemmas. This does not complete matrix inversion: an executable repeated-LUP-SOLVE construction, left/right inverse correctness, and the cubic work claim remain, as do #125 and #126.

[TankTechnology]

Completed on main: Chapter 28 is main-proof-complete (9/9). §28.2 inversion (inv_eq_lup) and §28.3 SPD / least-squares optimality proved.