Reflection has no fixed point
NOT A NOVELTY CLAIM. This is a machine-checked formalisation, decided 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.
NO cell is its own reflection. ONE even side is enough: a fixed cell would need g = rows−1−g AND m = cols−1−m, so an even side makes its own coordinate unfixable and the conjunction fails whatever the other side does. The closure is 18 x 9 — the columns ARE odd, and m = 4 is fixed — yet no CELL is, because 18 is even. Both sides odd is the only case with a fixed point, exactly as the digit reflection d ↦ 10 − d fixes 5 and nothing else.
Proposition
reflHasNoFixedPoint 18 9 = trueProof
By decide in three.lean. The kernel reduces the proposition and reports no axiom dependency.
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--reflection_has_no_fixed_point
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
- The closure is eighty one orbits
- Orbit positions cancel
- Reflection complements the address
- The involution laws are general