D Edition and proof scope
On this page · Visual guide: Read the certificates with the pictures · Permalink · Source line 1
The traditional article is a single edition organized by topic. The expanded branch supplies the written proofs of common refinements, complete filtered inversion, lattice gluing, rectangular Smith congruences, and analytic and multilevel defects. The canonical v1.2.1 release supplies the inherited specializations, finite graph construction, worked realizations, and three algorithm specifications.
Read current verification snapshot
The inherited Lean contract has 25 rows: 21 canonical numbered items, one Smith-phase identity, and three algorithm specifications. It remains a dated source contract. The current correspondence separately records the exact present statements, proof targets, source hashes, and execution evidence. A row may use several declarations, and several source labels may refer to one written theorem; these are distinct counting units.
The original branch sources and historical reports remain preserved. The current editorial log records the hypothesis, notation, and endpoint clarifications, including the verified rectifiable-cycle citation. Current navigation metadata records printed pages and PDF destinations. Historical proof-preservation reports retain their original scope and date; they do not describe later edited proof text.
The visual guide gives exact worked models. The Lean guide opens with the current proof scope and then explains the inherited declaration-level contract. Illustrations and finite checks support understanding and implementation. Universal claims depend on their written proofs and the exact formal statements where coverage is recorded.
This monograph includes the twenty-four worked plates after this account of the proof scope. Their statement references use the printed pages of this volume. The separate visual guide contains the same models for readers who want to follow the examples on their own.