CollinearDiameterEndpointContradiction
plain-language theorem explainer
Defines the pure geometric proposition that four collinear plane points cannot carry two equal-length diameter segments whose four cross distances stay at most that length while all four endpoints remain pairwise distinct. Anyone working the collinear case of the ordered Erdős #132 shell-multiplicity bound cites this Prop as the statement discharged by the coordinate proof. The body is a bare universal Prop, not a proved theorem.
Claim. The following is false for all points $a,b,c,d$ in the plane and all real $\Delta$: $a,b,c,d$ are pairwise distinct at the endpoint pairs $(a,c)$, $(a,d)$, $(b,c)$, $(b,d)$; $\mathrm{dist}(a,b)=\mathrm{dist}(c,d)=\Delta$; every cross distance among $\{a,b\}\times\{c,d\}$ is at most $\Delta$; and both $c$ and $d$ are collinear with the directed segment $ab$ (vanishing $2$D orientation).
background
The module Distance Shell Multiplicity physicalizes Erdős problem #132 inside Recognition Science: a classical distance value is a shell in the pairwise Euclidean spectrum; physically it is a two-body recognition-energy shell whose occupancy is the shell multiplicity. Ordered pairs are used for Lean bookkeeping, so a classical unordered bound $\le n$ becomes an ordered bound $\le 2n$.
Point2 is the ambient Euclidean plane; dist is ordinary Euclidean distance; orient2 is the signed parallelogram area (twice the oriented area of the triangle), so orient2 a b c = 0 means $c$ lies on the line through $a$ and $b$. A diameter shell is a distance value realized as a global maximum pairwise distance; the present Prop isolates the collinear subcase in which two opposite pairs both realize that diameter length while every cross distance remains $\le\Delta$.
Sibling notions such as IsDiameterShell, uniqueness of the diameter shell, and the ordered spectrum feed the larger sparse-shell divergence argument; this definition strips away the unused geometric-disjointness package from the related separation structure and keeps only the four-point collinearity-plus-diameter data.
proof idea
No proof: the declaration is a bare def of a Prop. It packages the universal statement that will later be proved by the theorem of the same name in camelCase. That theorem (downstream) proceeds by cases on $\Delta=0$ versus $\Delta\ne 0$, then parametrizes the common line so that $a,b$ sit at $0$ and $1$ and $c,d$ at parameters $t,s\in[0,1]$, obtaining $|s-t|=1$, which forces ${t,s}={0,1}$ and therefore identifies $c$ with $a$ or $b$, contradicting endpoint distinctness. The definition itself contributes only the statement.
why it matters
This Prop is the exact statement proved by collinearDiameterEndpointContradiction, which the module uses to control collinear configurations inside the ordered distance-shell multiplicity analysis of Erdős #132. The downstream doc-comment stresses that geometric-disjointness data from the separation structure is deliberately unused: the four-point line parametrization alone yields the contradiction. In the RS reading, forbidding two distinct diameter-length pairs on a line with all cross distances $\le\Delta$ keeps diameter shells from over-occupying under collinear collapse, supporting the sparse-shell divergence and flux-bridge siblings that bound shell multiplicity. It is local Euclidean geometry, not a forcing-chain step (T5–T8), but it is load-bearing for the module’s physicalization of the classical combinatorial bound.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.