collinearSeparatedDiameterContradiction
plain-language theorem explainer
Two collinear diameter-length segments whose four cross-distances stay at most the diameter cannot carry a collinear separation certificate. Anyone wiring the collinear branch of the Erdős #132 assembly cites this discharge. The proof is a one-line reduction to the sharper collinear endpoint contradiction, dropping the disjointness field of the separation hypothesis.
Claim. For points $a,b,c,d$ in the plane and $\Delta\in\mathbb{R}$, if the endpoints are pairwise distinct across the two segments, $\mathrm{dist}(a,b)=\mathrm{dist}(c,d)=\Delta$, all four cross-distances are $\le\Delta$, and the segments satisfy collinear segment separation, then a contradiction follows.
background
The module physicalizes Erdős problem #132: a classical distance value is a shell in the pairwise Euclidean spectrum; in RS 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$ on ordered pairs.
A diameter shell is a distance value $\Delta$ realized as a longest pairwise distance. The proposition packaged here asserts that two diameter-length segments cannot coexist with all four cross-distances $\le\Delta$ once a collinear separation certificate is present. That certificate (collinear segment separation) packages collinearity and separation data for the two segments; the older bridge treated the whole package as a hypothesis interface.
The sharper upstream fact is the collinear endpoint contradiction: under the same distance hypotheses, already the collinear endpoint conditions force a cross-distance above the diameter. The present statement is the older separated-case form of that fact.
proof idea
One-line term wrapper. Introduce the four points, $\Delta$, the four distinctness hypotheses, the two diameter equalities, the four cross-distance upper bounds, and the collinear separation certificate. Apply the collinear endpoint contradiction to the same geometric data, feeding only the first two projections of the separation certificate (the collinear endpoint fields) and discarding the remaining disjointness component. No further case split or coordinate work is done here.
why it matters
This closes the collinear branch of the separated-diameter contradiction as an unconditional Lean theorem, so any use of the abstract bridge proposition can be discharged without an extra hypothesis. Downstream, the reduced Erdős #132 assembly notes that because this collinear case is now proved, Erdős #132 follows from the proper separated-diameter contradiction together with the segment-separation case split, the undirected thrackle support bound, and convex-layer screening. The unified assembly likewise consumes the separated-diameter contradiction that this fact helps populate. It also feeds the four-point Hopf–Pannwitz crossing theorem (diameter segments with cross-distances $\le\Delta$ must meet) and the support-level Conway thrackle transfer. In the RS reading, forbidding over-occupied diameter shells is exactly the geometric content of the #132 multiplicity bound on recognition-energy shells.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.