collinear_contradiction_from_separated_diameter
plain-language theorem explainer
If the unified separated-diameter contradiction holds, the collinear special case follows at once. Cite this when discharging four-point collinear diameter configurations in the Erdős #132 shell-multiplicity development. The proof is a one-line specialization: feed collinear segment separation into the disjunctive hypothesis of the unified statement via the right disjunct.
Claim. Assume that for all plane points $a,b,c,d$ and all $\Delta\in\mathbb{R}$, the data $a\neq c$, $a\neq d$, $b\neq c$, $b\neq d$, $\mathrm{dist}(a,b)=\Delta=\mathrm{dist}(c,d)$, and all four cross-distances $\le\Delta$, cannot coexist with either a proper or a collinear segment-separation certificate. Then the same package cannot coexist with a collinear segment-separation certificate alone: two disjoint collinear diameter-length segments force some cross-distance above $\Delta$.
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, and multiplicity is shell occupancy. Ordered pairs are used for Lean bookkeeping, so classical multiplicity $\le n$ becomes ordered multiplicity $\le 2n$.
The unified hypothesis asserts that no four points can carry two diameter segments of common length $\Delta$, keep every cross-distance at most $\Delta$, and still admit a separated-segment certificate of either kind (proper or collinear). The collinear target is the narrower bridge: the same diameter equalities and cross-distance bounds cannot coexist with a collinear segment-separation certificate. That collinear bridge is documented as now theorem-backed, so any hypothesis of that shape can be discharged unconditionally once the implication chain is closed.
Points live in the plane (Point2); distances are ordinary Euclidean lengths.
proof idea
Pure specialization of a universal quantifier. Introduce the four points, the common diameter $\Delta$, the four distinctness hypotheses, the two diameter equalities, the four cross-distance upper bounds, and the collinear separation certificate. Apply the unified hypothesis to the same data, packaging the collinear certificate as the right disjunct of the separation alternative (Or.inr). No geometric work occurs in this declaration; the geometry sits inside the unified hypothesis.
why it matters
In the distance-shell development this is the clean interface from the unified separated-diameter package down to the collinear bridge. The collinear bridge is the abstract statement that two disjoint collinear diameter-length segments force a cross-distance above the diameter; once available, it supports four-point crossing arguments used to control shell occupancy.
A nearby module comment records the intended landing: segment-separation together with the unified separated-diameter contradiction prove the four-point crossing lemma. That lemma is part of the RS reading of Erdős #132, where shell multiplicity bounds constrain how often a recognition-energy distance can recur. No downstream edges are currently wired in the graph for this exact declaration, so its immediate consumers are local to the module's crossing and multiplicity lemmas rather than a named parent theorem outside.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.