Reading map
On this page · Permalink · Source line 204
The five parts follow one mathematical record from discovery to certification, realization, compression, review, and reuse. The visual studies work through actual finite examples rather than replacing the proofs.
A short technical route Begin with Sections 3, 5, 9, and 10. For collective interpretation, read Sections 20 and 21 together.
Evidence in this edition The 41 prior result groups are retained. Six new groups specify trace checking and typed exchange. Eighteen Lean modules were freshly built, replayed with Lean's kernel, and axiom audited. Exact finite checks remain separate from the formal proofs.