A.3 Revision reconciliation
On this page · Permalink · Source line 56
Two retrieved archives carry version 0.2.0, but they do not have the same active source. The earlier four-module checkpoint has 59 mathematical theorems and four separately checked refutation controls. The later five-module checkpoint has 96 mathematical theorems and three rejected control files. Its proof receipt is the later verification/final/REPORT.json.
The original 22 finite-table statements are retained inside both checkpoints. They are not counted a second time. Likewise, \(59+96\) is not a meaningful theorem total: these are overlapping revisions of one formal development.
The earlier proof boundary disclosed that explicit projector transport and normalized-state matrix actions had not yet been supplied. The later source supplies both, connects the Fourier matrix to the usual complex exponential, and proves a histogram nonreconstruction theorem. The earlier boundary remains a record of its own revision, rather than a gap list for the current publication.
The entire later checkpoint is preserved under lean/checked_checkpoint. The source files are not edited to match this guide.