same_side_segments_disjoint
plain-language theorem explainer
If c and d lie strictly on the same side of the line through a and b, the closed segments ab and cd are geometrically disjoint. This is the elementary separation lemma behind all thrackle and K4 matching dichotomies in the distance-shell module. The proof is a short affine-orientation argument: any common point would force a same-sign convex combination of orientations to vanish.
Claim. Let $a,b,c,d\in\mathbb{R}^2$. If $\mathrm{orient}(a,b,c)\cdot\mathrm{orient}(a,b,d)>0$ (so $c$ and $d$ lie strictly on the same side of the directed line through $a$ and $b$), then the closed segments $\overline{ab}$ and $\overline{cd}$ do not intersect.
background
The module Distance Shell Multiplicity is the RS physicalization of Erdős problem #132: classical distance shells become two-body recognition-energy shells, and ordered-pair multiplicity is twice the unordered count (threshold $\le n$ becomes $\le 2n$).
Point2 is the planar point type from the bipartite distance spectrum. Geometric disjointness of ordered edges means the closed straight-line segments do not meet; the doc notes this is the correct Hopf–Pannwitz / thrackle predicate, since mere endpoint-disjointness would wrongly exclude crossing diameter diagonals.
Orientation orient2 a b x is the signed area of triangle $abx$. Positive product of orientations means $c$ and $d$ share a strict half-plane relative to line $ab$. The lemma is the core separation fact for thrackle and matching arguments in this file.
proof idea
Argue by contradiction. Suppose $p$ lies on both closed segments. Being on $\overline{ab}$ forces $\mathrm{orient}(a,b,p)=0$ via orient2_eq_zero_of_on_closed_segment. Parametrize $p=(1-t)c+td$ with $t\in[0,1]$. Affinity of orientation in the third argument (orient2_affine_third) yields
$$0=\mathrm{orient}(a,b,p)=(1-t),\mathrm{orient}(a,b,c)+t,\mathrm{orient}(a,b,d).$$
The hypothesis that the product of orientations is positive, via same_strict_sign_of_pos_mul, puts both orientations in the same strict half-line; convex_combo_ne_zero_of_same_strict_sign then says no convex combination can vanish, a contradiction.
why it matters
This is the geometric engine for the Conway–K4 obstruction chain that bounds distance-shell support. Downstream, four_distinct_points_one_matching_disjoint_noncollinear routes every non-degenerate 4-point configuration into a disjoint perfect matching of $K_4$ using only this lemma and the Plücker orientation identity; its doc calls that dichotomy "the heart of the Conway-K4 obstruction."
The three pairwise matching lemmas (four_distinct_M1_or_M2_disjoint_noncollinear and siblings) and the exact four-point support bound from the K4 obstruction certificate all depend on it. In the RS reading, those bounds control ordered shell multiplicity for recognition-energy shells (Erdős #132 physicalized). No forcing-chain landmark (T5–T8) is invoked here; the result is pure planar geometry feeding the multiplicity estimates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.