The genus reads back from chi at every genus
NOT A NOVELTY CLAIM. This is a machine-checked formalisation, checked by the Lean 4 kernel and resting on no axiom beyond propext and Quot.sound. It is dated and citable. Prior art, where it exists, is cited below. No discovery is claimed.
…and at EVERY genus, proved rather than decided: the theorem above checks the first ten surfaces; this reads the genus back from χ(g) for all of them at once. A proof, not an exhaustion — it rests on the standard axioms propext and Quot.sound that core's integer lemmas carry, and the axiom probe reports it as general.
Proposition
∀ g : Nat, genusOf (chi g) = gProof
By intro g in corpus.lean. Checked by the Lean kernel: it rests on Quot.sound and propext and on no other axiom.
Sources and identifiers
- Lean source · src/pair/lean/proofs/corpus.lean
- Typeset paper · src/research/lean-theorems.tex
- Repository deposit · doi:10.5281/zenodo.21787144
- Author · ORCID 0009-0000-7312-9778
Proved in the same file
- Euler characteristic and genus are inverse
- Census bands are gapless and descending
- Census is one hundred twenty three
- Fibonacci partial sum identity
- Folding by chi is undone by unfolding
- Reflection is an involution
- Reflection pairs and one fixed point
- Reflection closes on the digits
- Reflection is an involution on the whole lattice
- Golden ratio bounds
- Golden ratio minus one bounds
- Splitting then burning water is the identity
- Verify beats recompute by magnitudes
- Hexbit receipt beats rebuild
- Hexbit advantage widens
- Sixty four components
- Shor state vectors unchanged
- Shor vector dwarfs the number
- Shor rsa gap is between exponents
- Shor zero skipping divides by the work register