DisjointSegmentsHaveSeparation
plain-language theorem explainer
Names the classical planar case split: two closed segments with four distinct endpoints that do not meet geometrically admit either a proper orientation separation or a collinear separation certificate. Cited by every reduced assembly of the ordered Erdős #132 bound and by the four-point diameter-crossing lemmas. The body is a pure Prop definition, not a proof.
Claim. The proposition asserting: for all points $a,b,c,d$ in the plane with pairwise distinct endpoints ($a\neq c$, $a\neq d$, $b\neq c$, $b\neq d$), if the closed segments $[a,b]$ and $[c,d]$ are geometrically disjoint, then either a proper orientation separation of the two segments holds, or a collinear separation certificate holds.
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$.
Point2 is the ambient plane. Geometric disjointness of ordered edges means the two closed segments share no point. The two disjuncts are the standard planar certificates: proper orientation separation (strict sidedness / lens geometry, feeding the Hopf–Pannwitz strict diameter inequality on the open half-lens) versus collinear separation (degenerate alignment handled by a separate contradiction).
This Prop is the abstract bridge that turns “segments do not meet” into one of those two certificates, so later diameter-crossing and thrackle arguments can case-split cleanly.
proof idea
No proof: the declaration is a def whose body is the quantified Prop itself. It packages the universal statement “endpoint-disjoint + geometrically disjoint ordered edges imply proper separation or collinear separation” as a named hypothesis interface for downstream assemblies. Callers assume the Prop and discharge cases via the proper and collinear separated-diameter contradictions.
why it matters
This is the segment-separation case split required by every reduced route to the ordered Erdős #132 theorem in the module. Downstream, erdos132_from_separation_thrackle_layer needs only this Prop plus undirected thrackle support and convex-layer screening once both separated-diameter contradictions are theorems; the proper-only and unified assemblies take it the same way. It also feeds four_point_diameter_crossing_from_separated_diameter and four_point_diameter_crossing_from_separation_bridges, which establish the four-point Hopf–Pannwitz crossing lemma used to control diameter shells.
In the RS reading, diameter shells are the extremal two-body recognition-energy shells; bounding their ordered multiplicity is the physical content of #132. The case split is classical planar geometry, not an RS forcing step (T5–T8), but it is the bridge that lets the thrackle and convex-layer screening close the multiplicity bound.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.