properSeparatedDiameterContradiction
plain-language theorem explainer
Two diameter segments in the plane, with every cross-distance at most the common length, cannot place both endpoints of the second segment on the same strict side of the first. Discrete geometers assembling the Erdős #132 shell-multiplicity bound cite this as the positive-orientation Hopf–Pannwitz core. The proof moves to lens coordinates via 2D Lagrange identities and collides a strict lens inequality with the second diameter length.
Claim. For all $a,b,c,d$ in the Euclidean plane and all $\Delta\in\mathbb{R}$: if the four points are pairwise distinct across the two segments, $\mathrm{dist}(a,b)=\Delta=\mathrm{dist}(c,d)$, every cross-distance is at most $\Delta$, and the segments are properly separated (both $c$ and $d$ lie on the same strict side of line $ab$), then a contradiction follows.
background
The module physicalizes Erdős problem #132: a distance value is a two-body recognition-energy shell, and its multiplicity is shell occupancy. Ordered pairs are used for Lean simplicity, so the classical unordered bound $\le n$ becomes ordered $\le 2n$.
Points are Point2 (Euclidean plane). A diameter shell is a distance value realized as a longest pairwise length $\Delta$. Proper segment separation means the two endpoints of one diameter lie on the same strict side of the supporting line of the other (strict orientation signs agree and are nonzero).
The abstract bridge proposition asserts that no four points can simultaneously realize two diameters, four cross-bounds $\le\Delta$, and proper separation. Squared distances unfold by the standard identity $(|u-v|)^2=(u_0-v_0)^2+(u_1-v_1)^2$.
proof idea
Introduce the four points and $\Delta$. The zero-diameter case collapses immediately: $\mathrm{dist}(a,c)=0$ forces $a=c$, contradicting distinctness.
For $\Delta>0$, unfold all five squared distances. Apply the 2D Lagrange identity to the pairs $(a,b,c)$ and $(a,b,d)$, and the polarized form to $(a,b,c,d)$. Pass to lens coordinates $\alpha_c=\langle c-a,b-a\rangle/\Delta$, $\beta_c=\mathrm{orient}_2(a,b,c)/\Delta$ (and likewise for $d$). These satisfy $\alpha_c^2+\beta_c^2=(\mathrm{dist},a,c)^2\le\Delta^2$ and $(\alpha_c-\Delta)^2+\beta_c^2=(\mathrm{dist},b,c)^2\le\Delta^2$, so $(\alpha_c,\beta_c)$ lies in the lens; same for $d$.
Proper separation forces $\beta_c\beta_d>0$. The strict Hopf–Pannwitz lens lemma then yields $(\alpha_c-\alpha_d)^2+(\beta_c-\beta_d)^2<\Delta^2$. Polarized Lagrange identifies the left-hand side with $(\mathrm{dist},c,d)^2=\Delta^2$, contradiction.
why it matters
This discharges the positive-orientation half of the four-point Hopf–Pannwitz geometry inside the RS treatment of Erdős #132. Downstream, the reduced assembly erdos132_from_proper_separation_thrackle_and_convex_layer_screening takes the proposition as an explicit hypothesis and obtains the ordered multiplicity theorem from segment-separation, thrackle support, and convex-layer screening. The further-reduced assembly drops that hypothesis entirely, because the present theorem supplies it unconditionally; only separation case-split, thrackle support, and layer screening remain.
It also feeds the opposite-sides meeting lemma: when orientations disagree, the same cross-bounds force the segments to intersect. In the Recognition reading, diameter shells are maximal two-body recognition-energy shells; forbidding same-side double diameters constrains shell occupancy and thereby the classical multiplicity bound.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.