Reflection is an involution on the whole lattice
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.
The reflection is an involution on the WHOLE lattice 0…10, and every pair sums to it: the ten is the constant the involution preserves, not a number asserted beside it.
Proposition
∀ d ∈ List.range (digitLattice + 1), reflect (reflect d) = d ∧ d + reflect d = digitLatticeProof
By decide in corpus.lean. Checked by the Lean kernel: it depends on no 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
- The genus reads back from chi at every genus
- 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
- 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