SeparatedDiameterContradiction
plain-language theorem explainer
Packages the claim that two equal-length diameter segments in the plane cannot be geometrically separated (proper orientation or collinear disjoint) while every cross-distance stays at most the diameter. Cited by the four-point diameter-crossing lemma and the final Erdős #132 ordered assembly. Pure Prop definition: no proof body, only the universal statement.
Claim. The proposition asserting: for all planar points $a,b,c,d$ and all $\Delta\in\mathbb{R}$, if the four endpoints are pairwise distinct across the two segments, $\mathrm{dist}(a,b)=\mathrm{dist}(c,d)=\Delta$, every cross-distance among $\{a,b\}\times\{c,d\}$ is at most $\Delta$, and the segments carry either a proper orientation-separation certificate or a collinear disjoint-segment certificate, then falsehood follows.
background
The module physicalizes Erdős problem #132: a distance value is a two-body recognition-energy shell, and ordered-pair multiplicity is twice the classical unordered count (so the classical bound $\le n$ becomes $\le 2n$).
Points live in the Euclidean plane (Point2). A diameter shell is a distance $\Delta$ realized by at least one pair and upper-bounding all other pairwise distances. Two segments of common length $\Delta$ with all four cross-distances $\le\Delta$ are the local geometric obstruction the multiplicity argument must rule out when the segments are separated.
Separation splits into two certificates kept distinct because orientation products vanish on a line: proper (strict orientation) separation, and collinear separation (both orientations zero and the closed segments geometrically disjoint). The unified proposition folds both cases into one hypothesis.
proof idea
Definitional packaging only: the body is the universal Prop above, not a proved theorem. Downstream one-line wrappers instantiate the disjunction with Or.inl (proper case) or Or.inr (collinear case) and apply this hypothesis. No algebraic reduction or tactic script lives here.
why it matters
Unifies the proper and collinear separated-diameter contradictions so later lemmas need a single hypothesis. Feeds proper_contradiction_from_separated_diameter and collinear_contradiction_from_separated_diameter (case projections), then four_point_diameter_crossing_from_separated_diameter (segment-separation plus this Prop yields the four-point crossing lemma). The final assembly erdos132_from_unified_separation_thrackle_and_convex_layer_screening takes this Prop together with thrackle support and convex-layer screening to obtain the ordered Erdős #132 statement. In the RS reading, forbidding separated diameter pairs controls shell occupancy on the planar distance spectrum.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.