Address inverts
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.
THE ADDRESS INVERTS. Row-major indexing recovers both coordinates for every cell, so a scene can be addressed by one number without losing which geometry and which material it names.
Proposition
∀ p ∈ cells 18 9, row 9 (idx 9 p.1 p.2) = p.1 ∧ col 9 (idx 9 p.1 p.2) = p.2Proof
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--address_inverts
Proved in the same file
- Closure is one hundred sixty two
- Closure is the product
- Closure has no duplicate
- Closure is complete
- 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
- The closure is eighty one orbits
- Orbit positions cancel
- Reflection complements the address
- The involution laws are general