ProperSeparatedDiameterContradiction
plain-language theorem explainer
Two equal-length diameter segments in the plane cannot have all four cross-distances at most the diameter while the second pair lies strictly on the same side of the first segment line. Discrete geometers and anyone assembling the RS route to Erdős #132 cite this as the Hopf–Pannwitz orientation core. The declaration is a Prop packaging that contradiction; the companion theorem discharges it by lens coordinates, Lagrange identity, and a strict lens inequality.
Claim. For all points $a,b,c,d$ in the Euclidean plane and all $\Delta \in \mathbb{R}$: if the four endpoints are pairwise distinct across the two segments, $\mathrm{dist}(a,b)=\Delta=\mathrm{dist}(c,d)$, every cross-distance among $\{a,b\}\times\{c,d\}$ is at most $\Delta$, and the segments are properly separated (both of $c,d$ strictly on the same side of line $ab$), then a contradiction follows.
background
The module physicalizes Erdős problem #132: a classical distance value is a shell in the pairwise Euclidean spectrum; in RS it is a two-body recognition-energy shell whose multiplicity is occupancy. Ordered pairs are used for Lean simplicity, so the classical multiplicity bound $\le n$ becomes $\le 2n$ for positive distances.
Point2 is the Euclidean plane. A diameter shell is a distance value realized as a longest pairwise distance. Proper segment separation means the two segments are disjoint as sets and both endpoints of one lie strictly on the same open half-plane determined by the line of the other (strict same-side orientation signs).
This Prop is the positive-$\Delta$ orientation-sign core of four-point Hopf–Pannwitz geometry: two diameter segments with all cross-distances bounded by the diameter cannot be properly separated. The doc-comment records that the companion theorem now proves the Prop outright, so any hypothesis of this shape discharges unconditionally.
proof idea
As a definition this is pure packaging: the body is the universal quantification over four points and $\Delta$ of the geometric hypotheses implying False. There is no tactic proof on the def itself.
The companion theorem that realizes the Prop proceeds by placing $a,b$ in coordinates, rotating so $(b-a)/|b-a|$ is the first basis vector, and reading $c,d$ in lens coordinates $(\alpha,\beta)$ with $\beta\cdot\Delta$ equal to the 2D orientation and $\alpha\cdot\Delta$ the projected inner product. Lagrange identity converts squared distances into $\alpha^2+\beta^2$. Proper separation forces $\beta_c\beta_d>0$ strictly. The strict Hopf–Pannwitz lens inequality then yields $(\alpha_c-\alpha_d)^2+(\beta_c-\beta_d)^2<\Delta^2$, while polarized Lagrange gives equality to $(\mathrm{dist},c,d)^2=\Delta^2$, contradiction. The $\Delta=0$ edge is handled by a separate short case.
why it matters
This Prop is the named hypothesis interface for the proper (strict same-side) branch of the four-point diameter geometry that feeds Erdős #132 in the module. Downstream, four_point_diameter_crossing_from_separation_bridges takes it together with the collinear twin and the segment-separation case split to obtain the four-point crossing lemma. The reduced assembly erdos132_from_proper_separation_thrackle_and_convex_layer_screening needs only this Prop (collinear already theorem-discharged) plus thrackle support and convex-layer screening to conclude the ordered Erdős #132 statement. A thin wrapper also derives it from the unified separated-diameter contradiction.
In the RS reading, diameter shells are maximal two-body recognition-energy shells; forbidding properly separated equal-diameter pairs constrains shell occupancy and supports the multiplicity bound. The doc-comment stresses the bridge is now a theorem, so scaffolding that still lists this Prop as an open hypothesis can be closed by citing the companion proof.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.