CollinearSeparatedDiameterContradiction
plain-language theorem explainer
Names the collinear separated-diameter contradiction as a pure proposition: two equal-length diameter segments on a line, with all four cross distances at most that diameter and distinct endpoints, cannot satisfy collinear segment separation. Combinatorial geometers working the Erdős #132 shell-multiplicity bound cite it as the collinear case hypothesis. It is a Prop abbreviation, not a proved statement; the matching theorem discharges it unconditionally.
Claim. The following assertion holds as a named proposition: for all points $a,b,c,d\in\mathbb{R}^2$ and all $\Delta\in\mathbb{R}$, if the four endpoints are pairwise distinct across the two pairs, $\mathrm{dist}(a,b)=\mathrm{dist}(c,d)=\Delta$, every cross distance among $\{a,b\}$ and $\{c,d\}$ is at most $\Delta$, and the pairs satisfy collinear segment separation, then falsehood follows.
background
The module 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 the classical multiplicity bound $\le n$ becomes $\le 2n$.
A diameter shell is a distance value $\Delta$ realized as a longest pairwise distance. The collinear case concerns two segments of length $\Delta$ whose four endpoints lie on a single line and are separated in the collinear-segment sense (the two segments are endpoint-disjoint on that line). The geometric content is elementary: on a line, two disjoint intervals of length $\Delta$ force at least one endpoint-to-endpoint cross distance strictly larger than $\Delta$.
Point2 is the ambient Euclidean plane type imported from the bipartite distance-spectrum layer. The separation predicate packages the collinear configuration that the diameter-crossing arguments must rule out.
proof idea
No proof body: the declaration is a bare Prop abbreviation. It quantifies over four plane points and a real $\Delta$, packages the endpoint-distinctness, equal-diameter, and cross-distance $\le\Delta$ hypotheses, and concludes False from collinear segment separation. Downstream theorems treat this name as a hypothesis interface that is already discharged by the matching theorem collinearSeparatedDiameterContradiction, which reduces to the sharper collinear endpoint contradiction by dropping an unused disjointness field.
why it matters
This proposition is the collinear half of the separated-diameter bridge used throughout the Erdős #132 assembly chain. Downstream, collinear_contradiction_from_separated_diameter derives it from the unified separated-diameter contradiction; collinearSeparatedDiameterContradiction proves it outright. The four-point diameter-crossing lemma takes it (with the proper-separated twin and a segment-separation case split) as an input hypothesis. Reduced assemblies such as erdos132_from_proper_separation_thrackle_and_convex_layer_screening note that because the collinear case is now a theorem, only the proper-separated contradiction, thrackle support, and convex-layer screening remain as external hypotheses. In the RS reading, ruling out over-occupied diameter shells is the combinatorial step that keeps recognition-energy shell multiplicities inside the ordered bound $\le 2n$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.