Highlights of the LowGenus library #
A public interface, in one file. Every main theorem of the
Atanasov–Ranganathan programme is restated below as an example whose type is
written out in full and whose proof is the real theorem. There is not a single
new definition or theorem here.
- For a reader. The shape of the whole programme — sixteen construction proofs, one classification boundary, one arithmetic reduction, one public conclusion — is visible in one screen.
- For the build. Each
exampleis checked by the kernel against the real declaration, so a refactor that silently changes a statement breaks this file loudly.
The shape of the argument. Brill–Noether existence for every connected
graph of genus at most five reduces (bnExists_of_genus_le_five_of_criticalPencils)
to two critical pencils: a degree-three rank-one divisor in genus four, and a
degree-four rank-one divisor in genus five. Fossilization and trivalent
expansion reduce genus four to six closed cubic rows. Genus five reduces to
the sixteen displayed AR constructions plus four bridge rows, all four handled
by the same checked (2,3) articulation. The public canonical classifiers
make both reductions exhaustive.
The key definitions #
One of the sixteen displayed 8-vertex, 12-edge cubic cores of AR's
genus-five section. (LowGenus/GenusFiveCoreAtlas.lean)
Instances For
The obligation for one row: choose a degree-four divisor throughout the
core's genus-preserving closed length orthant, and supply a tagged explicit
Dhar move at every off-support vertex. The closed form includes the positive
row and all of its nonloopy forest faces.
(LowGenus/GenusFiveConstructions.lean)
Equations
Instances For
The two genuinely geometric inputs left after the low-genus arithmetic
reduction: rank-one degree-three in genus four, rank-one degree-four in genus
five. (LowGenus/LowGenusExistence.lean)
Instances For
The remaining non-construction obligation: classify every valid loop-aware
pseudocore as a face of one of the sixteen closed constructions, or as an
already available structural case. (LowGenus/GenusFiveConstructions.lean)
Equations
Instances For
The sixteen-row ledger #
One line per displayed core. Each is an independently replaceable proof, and each is a reportable unit of progress; six are length-dependent families and ten are AR's straightforward constructions.