The original release has a frozen twenty-five-item formal contract: twenty-one numbered main-text definitions and results, one Smith-phase identity, and three algorithm specifications. Its dated source and evidence remain preserved. Current proof additions have a separate correspondence and replay record. The table below describes the inherited interfaces; the current map identifies the broader constructions. The visual models illustrate the mathematics, and their finite checks have recorded ranges.
Current Lean scope. 53 of 53 proof-level source records have kernel checked, semantically accepted scope. No partial or pending proof records are listed in this correspondence. These are source-record counts under their stated hypotheses, not counts of independent discoveries.
| Inherited interface | Inputs and checked scope | Boundary of that interface |
|---|---|---|
| Exact refinement | Complete projector families and a parent map when formulas relating parents to children are used. | A canonical refinement for every arbitrary pair of decompositions. |
| Fourier realization | A finite orthogonality table, or field/root hypotheses that provide it. | Orthogonality from multiplicative order alone over every ring. |
| Weighted inversion | A two-sided inverse of \(D\), a multiplicative filtration, and positive certified gains. | Convergence in every possible complete filtered algebra. |
| Graph rationality | A finite multigraph with positive weights, together with its actual determinant and adjugate. | Simple-path counts, analytic convergence everywhere, or operator noncancellation. |
| Spectral separation | Evaluated Bézout identities and explicit lattice-preservation data. | Automatic construction or minimality of every resultant certificate. |
| Smith congruences | Concrete diagonal data modulo \(p^L\), with \(p>1\). | An automatically constructed general-DVR Smith normal form. |
| Linear defects | Actual typed maps and the stated inverse or norm witnesses. | Small propagated errors independent of time or distance from a pole. |
Reproduce the explanatory calculations
The preserved model source contains 118 named exact checks. Each finite range is recorded in the file EXACT_CHECKS.json. They cover masks, CRT labels, modular inverse products, graph enumeration, rational recurrences, lattice denominators, complete finite fibers, phase identities, and defect formulas. Graphics are generated from those same exact model definitions. Numerical placement of geometric points is only a rendering step.
The historical monograph report records 48 passing Python tests, 118 exact visual checks, 22 byte-matching regenerated vector plates, 13 regenerated PDF/PNG figure pairs, and nine matching numerical summary rows. These finite computation records retain their tested ranges and dates. Current Lean replay and source coverage have separate records.
Read this as
Use the guide to understand what a theorem says and why its hypotheses matter. Use the theorem map and preserved proof sources to identify the precise formal result. Neither a picture nor a finite test expands that result's scope.