The Atanasov--Ranganathan low-genus formalization #
Root module for the LowGenus library: the formalization of the
Atanasov--Ranganathan existence theorem in genera at most five. It builds on
the generic chip-firing, subdivision, and transmission theory of the
Utilities library.
Fifteen generated cover modules -- GenusFiveRow03FixedCover,
GenusFiveRow14FixedCover, the five-module row-04 chain and the eight-module
row-06 chain -- are not imported here. They are retained as independent
generated checks alongside the readable proofs used by the main library.
GenusFiveClosedCover supplies the affine-cover semantics for those generated
certificates and is outside the dependency closure of
brillNoetherExistenceThroughFive.
Add an import line above whenever a module is added under LowGenus/, or
lake build LowGenus will silently skip it.