The mathematical statements in the main text have explicit hypotheses and written proofs. The Lean guide separately identifies the checked declarations, hypotheses, and coverage. The machine native paper identifies the 108 stable foundation records and the checks executed on their structured representations. These are distinct forms of evidence.
| Topic | Mathematical content | What must be retained |
|---|---|---|
| Presentations and hulls | Evaluation, module quotients, and generation under a fixed algebra. | The grammar must be fixed independently of the target. |
| Finite packets | Idempotence, annihilation, completeness and exact finite synthesis. | Orthogonality requires an additional hypothesis. |
| Semisimple formula | Multiplicities over division rings determine the minimal free cover. | The stated classical inputs and decomposition data. |
| Primary and graph formulas | Primary components and scalar quotients give sharp generator counts. | The coefficient field and multiplicity conventions. |
| Paths and cycles | Formulas for paths of every size and for complex cycles have separate proofs. | Finite tests illustrate rather than prove claims for every size. |
| Coordinate algebra | Normal form, multiplication, packet identities and a unit seed. | Smooth projective geometry needs additional classical input. |
| Completion | Density and bounded extraction in the stated topology. | Infinite sequences are distinct from periodic finite arrays. |
Evidence travels with the examples
The release includes mathematical source, exact model definitions, deterministic graphics, Python checks, Lean source and theorem mapping, and the machine native record archive. The visual models use integer, rational, symbolic, or explicitly analytic calculations. The separate verification record distinguishes fresh executions from archived evidence.
Read this as
The pictures make the hypotheses visible. Read the traditional proof, the formal contract, and the executable record at their respective stated scopes.