proper_segment_separation_signs
plain-language theorem explainer
Proper separation of two planar segments forces each pair of endpoints onto the same strict side of the other supporting line. Anyone deriving geometric disjointness from an orientation certificate cites this unpacking step. The argument is a one-line term proof: apply the same-strict-sign-of-positive-product lemma to each factor inequality.
Claim. Let $a,b,c,d$ be points in the plane. Suppose $0 < \mathrm{orient}(a,b,c)\cdot\mathrm{orient}(a,b,d)$ and $0 < \mathrm{orient}(c,d,a)\cdot\mathrm{orient}(c,d,b)$. Then either both $\mathrm{orient}(a,b,c)$ and $\mathrm{orient}(a,b,d)$ are strictly positive, or both are strictly negative; and likewise for $\mathrm{orient}(c,d,a)$ and $\mathrm{orient}(c,d,b)$.
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. Points live in a planar model (Point2 from the bipartite distance spectrum). The 2D orientation form orient2 is the signed parallelogram area of three points; its sign records which open half-plane a third point occupies relative to a directed line.
A proper segment-separation certificate asserts that the two closed segments with endpoints $a,b$ and $c,d$ are endpoint-disjoint and non-collinear in the strong sense that each pair of endpoints lies strictly on one side of the line through the other segment. Algebraically this is written as positivity of the two orientation products. The present result unpacks those products into same-side alternatives for both supporting lines.
proof idea
Term-mode one-liner. The hypothesis is a conjunction of two strict product inequalities. Each conjunct is fed to the elementary real lemma that a positive product of two reals forces both factors to share a strict sign (both $>0$ or both $<0$). The resulting pair of disjunctions is packaged as the conjunction in the conclusion. No geometry beyond the algebraic sign rule is used.
why it matters
Immediate parent is proper_segment_separation_geometrically_disjoint, whose doc-comment states the geometric payoff: if the segments met, a point of $[c,d]$ would also lie on line $ab$, forcing an affine combination of two same-strict-sign orientation values to vanish. That contradiction needs the same-side unpacking supplied here.
In the broader Distance Shell Multiplicity development, orientation certificates are the planar toolkit that keeps ordered distance shells geometrically honest when counting multiplicities against the Erdős #132 threshold. The lemma is pure Euclidean bookkeeping; it does not itself invoke the RS forcing chain (T0–T8), but it sits under the geometric scaffolding that makes the shell-occupancy comparison well-defined.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.