collinearDiameterEndpointContradiction
plain-language theorem explainer
Four collinear plane points with opposite pairs of equal length Δ and all cross distances ≤ Δ cannot be pairwise endpoint-distinct. Diameter-shell and Erdős-#132 arguments cite it to rule out collinear double occupancy of a diameter value. The proof parametrizes the common line by scalars t,s relative to ab, gets |s−t|=1 with t,s∈[0,1], and forces an endpoint collision.
Claim. For all $a,b,c,d$ in the plane and $\Delta\in\mathbb{R}$: if $a\neq c$, $a\neq d$, $b\neq c$, $b\neq d$, $\mathrm{dist}(a,b)=\Delta=\mathrm{dist}(c,d)$, the four cross distances are each $\le\Delta$, and both $c$ and $d$ are collinear with the directed segment $ab$ (vanishing planar orientation), then a contradiction follows. Geometric segment-disjointness is not assumed.
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 classical unordered multiplicity $\le n$ becomes ordered multiplicity $\le 2n$.
Points are Point2 (plane coordinates). Collinearity of $c$ (resp. $d$) with the directed pair $(a,b)$ is the vanishing of the planar orientation form $\mathrm{orient2}(a,b,c)=0$ (resp. $\mathrm{orient2}(a,b,d)=0$). A diameter shell is a distance value that realizes the global maximum pairwise distance; the local hypotheses only need the four cross distances bounded by the common opposite-pair length $\Delta$.
The proposition package is the sharpened collinear endpoint contradiction: equal-length opposite pairs on a line with cross distances $\le\Delta$ cannot be endpoint-disjoint. The older collinear separation certificate (orientations zero plus geometric edge-disjointness) is deliberately not required here.
proof idea
Introduce the four points, $\Delta$, the four endpoint inequalities, the two equalities $\mathrm{dist}(a,b)=\mathrm{dist}(c,d)=\Delta$, the four cross bounds, and the two vanishing orientations.
If $\Delta=0$, antisymmetry of $\le$ with nonnegativity of distance forces $\mathrm{dist}(a,c)=0$, hence $a=c$, contradicting endpoint distinctness.
For $\Delta>0$, $a\neq b$. Vanishing orientation yields scalars $t,s$ with $c-a=t(b-a)$ and $d-a=s(b-a)$. Distance-from-scalar identities give $\mathrm{dist}(a,c)=|t|\Delta$, $\mathrm{dist}(b,c)=|t-1|\Delta$, and likewise for $s$, plus $\mathrm{dist}(c,d)=|s-t|\Delta$. The cross bounds and $\mathrm{dist}(c,d)=\Delta$ force $|t|,|t-1|,|s|,|s-1|\le 1$ and $|s-t|=1$. Absolute-value bounds collapse to $t,s\in[0,1]$. Then $s-t=\pm 1$ on that interval forces ${t,s}={0,1}$, so $c=a$ or $c=b$, contradiction.
why it matters
This is the sharp collinear case in the distance-shell multiplicity development of Erdős #132. It feeds the older separated-case theorem, which is a one-line wrapper that drops the unused geometric-disjointness field and reapplies this result. It also feeds the uniqueness certificate for endpoint-disjoint diameter intersections under two-point collinearity: a second common intersection point would produce four collinear diameter endpoints and trigger this contradiction.
In RS terms, a diameter shell is a maximal two-body recognition-energy shell. Ruling out collinear double occupancy of that shell is a geometric step toward controlling ordered shell multiplicity (classical $\le n$ becomes ordered $\le 2n$). The argument is pure planar Euclidean geometry; it does not invoke the forcing chain T5–T8, the RCL, or the $\varphi$-ladder, but it sits in the combinatorial geometry layer those physical claims rely on for distance spectra.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.