sameSideDiameterContradiction
plain-language theorem explainer
Under planar diameter hypotheses (two segments of common length Δ, all four cross-distances ≤ Δ, distinct cross-endpoints), placing both endpoints of the second segment strictly on the same side of the first segment's supporting line is already impossible. The four-point Hopf–Pannwitz crossing theorem cites this as the same-side obstruction. The proof is a coordinate reduction via 2D Lagrange identities to contradictory quadratic bounds on projected scalars.
Claim. Let $a,b,c,d$ be points in the plane and $\Delta\in\mathbb{R}$. Suppose $a\neq c$, $\mathrm{dist}(a,b)=\mathrm{dist}(c,d)=\Delta$, and all four cross-distances $\mathrm{dist}(a,c),\mathrm{dist}(a,d),\mathrm{dist}(b,c),\mathrm{dist}(b,d)$ are at most $\Delta$. If $c$ and $d$ lie strictly on the same side of the oriented line through $a$ and $b$ (i.e. the product of the two $2$D orientations is positive), 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 bookkeeping; for positive distances, ordered multiplicity is twice the unordered count, so classical thresholds double.
Points are planar (Point2). The geometric witness for two endpoint-disjoint non-collinear closed segments is proper segment separation: each pair of endpoints lies strictly on one side of the line through the other segment (product of orientations positive on both supporting lines). The present result isolates the first of those two orientation products.
Diameter shells are the maximal distance values realized in a finite planar set. The local setting is the four-point diameter configuration that feeds the Hopf–Pannwitz crossing statement: two segments of equal length Δ with all cross-distances at most Δ.
proof idea
Case-split on Δ = 0: then dist(a,c) ≤ 0 forces a = c, contradicting distinctness.
For Δ > 0, unfold all six squared distances via the planar expansion. Apply the 2D Lagrange identity at (a,b,c) and (a,b,d), plus the polarized Lagrange identity mixing c and d. Normalize by Δ to obtain projected scalars (αc, βc) and (αd, βd): α is the longitudinal projection along ab, β the signed transverse height (orientation over |ab|).
Rewrite the four cross-distance bounds and the cd-equality in (α,β)-coordinates. Same-side orientation means βc·βd > 0. Algebraic comparison of the quadratic forms then forces an impossible simultaneous upper bound on the cross terms and equality on |c−d|, yielding False. The argument is pure real nlinarith/field_simp after the identities are installed; no topology.
why it matters
This is the sharper same-side bridge used inside the four-point diameter crossing theorem: if dist(a,b) = dist(c,d) = Δ, all cross-distances ≤ Δ, and the four cross-endpoints are pairwise distinct, then the closed segments [a,b] and [c,d] meet geometrically (Hopf–Pannwitz in the diameter case).
Classically, proper separation needs orientation products on both supporting lines. The doc-comment records that the older proper-separated diameter contradiction only ever used the first product; this lemma closes that gap by proving the single same-side hypothesis already contradicts the diameter bounds. Downstream, the crossing theorem case-splits on orientations and discharges the same-side branch here.
In the Recognition Science reading, diameter shells are maximal two-body recognition-energy shells. Forcing a geometric crossing under diameter occupancy constraints is part of the planar shell-multiplicity control that physicalizes Erdős #132 (ordered multiplicity thresholds). No T0–T8 landmark is directly invoked; the result is pure Euclidean geometry serving the multiplicity pipeline.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.