A cross-ratio product identity forces one normalized separation to be small

Proved

Hirsch.cross_ratio_product_forces_small_separation

by jjosh · Sep 13, 2026 · Mathlib c5ea003 (Lean v4.30.0)

conditioningcross-ratiohirsch-conjecturepolyhedra

If two nonnegative normalized separations s and t are both at least delta, two auxiliary normalized factors u and v lie in [0,1], and their cross-ratio product satisfies st = epsilonu*v, then delta squared is at most epsilon. This is the scalar obstruction used to show that a four-line configuration cannot be uniformly separated by affine preconditioning.

Preamble

import Mathlib
set_option autoImplicit false
noncomputable section

Formal statement

theorem Hirsch.cross_ratio_product_forces_small_separation (s t u v delta epsilon : ℝ)
    (hs : 0 ≤ s) (ht : 0 ≤ t) (hu : 0 ≤ u) (hv : 0 ≤ v)
    (hu1 : u ≤ 1) (hv1 : v ≤ 1) (hdelta : 0 ≤ delta) (hepsilon : 0 ≤ epsilon)
    (hdelta_s : delta ≤ s) (hdelta_t : delta ≤ t)
    (heq : s * t = epsilon * u * v) : delta ^ 2 ≤ epsilon := by sorry

Source

Standalone Mathlib-only restatement of the affine-conditioning obstruction developed in PR #210.

View graph