Frustum brackets the focal plane
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 frustum the camera declares is non-degenerate: near < FOCAL < far, in tenths, with the depth planes half a lattice pitch either side of the focal plane (near 19/10, far 29/10).
Proposition
(19 : Int) < 24 ∧ (24 : Int) < 29 ∧ (0 : Int) < 19Proof
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--frustum_brackets_the_focal_plane
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
- 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