The preserved v0.6.0 release records 56 of 56 manuscript-proved finite items, 392 named theorem declarations in 40 modules, and 66 separately counted construction audits. Of the theorem declarations, 19 are reused foundation results. These are inherited records, not a new Lean run for this editorial edition.
| Evidence | Its precise use here |
|---|---|
| Saved Lean records | Preserve the exact hypotheses and declared finite formalization boundary. |
| Fresh portable checks | Reproduce the guide's displayed matrices, identities, integer models, and finite optima. They are not extracted Lean proofs. |
| Vector drawings | Display explicit arrays, schedules, and sampled geometric formulas. Pixel accuracy is not algebraic certification. |
| Separate software checks | The release verification report records actual runs, tolerances, failures, and unavailable gates; these are separate from this guide's exact arithmetic. |
| Historical GPU corpus | Remains a record of the supplied original cases and environment. It is not a new measurement. |
The recompression distinction
The sixth block derives best-rank and singular-tail conclusions from ordered thin-SVD equations, rather than assuming an optimality certificate. It does not independently establish general SVD existence, certify a floating-point QR/SVD algorithm, or identify every result with a canonical singular-values API. Those are separate statements.
The four classical entries remain visible
The manuscript separately tracks Eckart–Young–Mirsky, the conjugate-gradient energy estimate, the floating-point product model, and simultaneous spectral decomposition. The strengthened ordered-SVD proof does not silently promote all associated existence and numerical-algorithm claims.
Limits of exact compilation
The optimizer needs a finite candidate tree with additive data. Nonlocal cache effects, overlapping decompositions, global rank coupling, and unrestricted discovery can destroy its optimal substructure. No new generic dense-matrix exponent or universal accelerator claim follows from this guide.
Read this as
This is a reader-facing reconstruction of the paper's finite concepts, with reproducible examples and preserved source evidence. It changes exposition, not the formal theorem contract.