Depth is strictly monotone
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.
NEARER ENLARGES, FURTHER RECEDES, STRICTLY. For depths inside the focal point, k1 < k2 implies 24/(24-k1) < 24/(24-k2), stated by cross-multiplication so no division occurs. This is the monotonicity the TS fold checks numerically and the property two canvas painters violated by faking depth as a screen offset before the 2026-07-07 audit.
Proposition
∀ k1 ∈ [(-12 : Int), -6, -1, 0, 1, 6, 12], ∀ k2 ∈ [(-12 : Int), -6, -1, 0, 1, 6, 12], k1 < k2 → 24 * den k2 < 24 * den k1Proof
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--depth_is_strictly_monotone
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
- 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