CollinearSegmentSeparation
plain-language theorem explainer
Packages the collinear half of planar segment separation: four points are collinear on the supporting line of the first edge, and the two closed ordered segments are geometrically disjoint. Cited by the diameter-shell contradiction bridges in the Erdős #132 multiplicity module. Pure definitional packaging of orientation vanishing plus geometric disjointness; no proof content.
Claim. For planar points $a,b,c,d$, the collinear segment-separation certificate holds when $\mathrm{orient}(a,b,c)=0$, $\mathrm{orient}(a,b,d)=0$, and the closed segments $[a,b]$ and $[c,d]$ are geometrically disjoint (no shared interior or endpoint).
background
The module physicalizes Erdős problem #132: classical distance shells become two-body recognition-energy shells, with ordered-pair multiplicity twice the unordered count (threshold $\le n$ becomes $\le 2n$). Points are planar Point2 values from the bipartite distance spectrum.
Segment separation in the plane splits into a strict-orientation case and a collinear case. In the collinear case the usual orientation products vanish, so a separate certificate is needed: both third and fourth points lie on the supporting line of the first edge, and the closed segments still do not meet. Geometric disjointness of ordered edges is the shared non-intersection hypothesis used by both branches.
This definition is the collinear branch of that classical case split. It is pure Prop packaging; the nontrivial geometry lives in the bridges that consume it.
proof idea
Definitional abbreviation only: the body is the conjunction of two vanishing 2D orientations (collinearity of $c$ and $d$ with the directed edge $ab$) and the already-defined geometric disjointness of the ordered closed edges $(a,b)$ and $(c,d)$. No tactics, no lemmas applied.
why it matters
Feeds the standard planar segment-separation case split DisjointSegmentsHaveSeparation: endpoint-disjoint non-meeting segments yield either a proper orientation separation or this collinear certificate. That split is then used by the collinear and unified diameter contradictions (CollinearSeparatedDiameterContradiction, CollinearDiameterEndpointContradiction, SeparatedDiameterContradiction), which rule out two diameter-length disjoint segments whose cross distances stay at most the diameter.
Those contradictions are the geometric engine behind uniqueness and sparsity control for diameter shells in the ordered distance spectrum, the RS reading of Erdős #132 shell multiplicity. Without isolating the collinear branch, orientation-product arguments would silently fail when all four points are collinear.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.