The closure is eighty one orbits
NOT A NOVELTY CLAIM. This is a machine-checked formalisation, checked by the Lean 4 kernel and depending on no axiom. It is dated and citable. Prior art, where it exists, is cited below. No discovery is claimed.
So the closure is 81 orbits of two, with nothing left over.
Proposition
(cells 18 9).length = 2 * 81Proof
By decide in three.lean. Checked by the Lean kernel: it depends on no axiom.
Sources and identifiers
- Lean source · src/pair/formal/proofs/three.lean
- Typeset paper · src/research/lean-theorems.tex
- Repository deposit · doi:10.5281/zenodo.21787144
- Author · ORCID 0009-0000-7312-9778
- Deposit record ·
three--the_closure_is_eighty_one_orbits
Proved in the same file
- Closure is one hundred sixty two
- Closure is the product
- Closure has no duplicate
- Closure is complete
- Address inverts
- Addresses are the interval
- The compound fraction clears
- Focal plane is unit scale
- Depth is strictly monotone
- Frustum brackets the focal plane
- Denominator is positive on the frustum
- Reflection is an involution
- Reflection closes on the closure
- Reflection has no fixed point
- Orbit positions cancel
- Reflection complements the address
- The involution laws are general