2607.19268v1 / BootsRoyle.lean

all files

import BootsRoyle.Arithmetic
import BootsRoyle.Identities

/-!
# Formal components of the Boots--Royle/Cao--Vince reproduction attempt

The modules imported here are the parts of the paper's proof that were
completed without additional axioms.  The exact completion status and the
missing planarity layer are documented in `README.md`.
-/