Documentation

LeanPool.BrillNoetherGraphs.LowGenus

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.