ProperSegmentSeparation
plain-language theorem explainer
Defines the standard planar orientation certificate that two endpoint-disjoint closed segments are properly separated: each pair of endpoints lies strictly on one side of the supporting line of the other segment. Cited throughout the distance-shell multiplicity development whenever geometric disjointness or diameter contradictions are reduced to sign patterns of twice-area determinants. The body is a two-conjunct product-of-orientations predicate, not a proved statement.
Claim. For planar points $a,b,c,d\in\mathbb{R}^2$, the predicate $\mathrm{ProperSegmentSeparation}(a,b,c,d)$ holds when $\mathrm{orient}(a,b,c)\cdot\mathrm{orient}(a,b,d)>0$ and $\mathrm{orient}(c,d,a)\cdot\mathrm{orient}(c,d,b)>0$, i.e., $c$ and $d$ lie on the same strict side of line $ab$, and $a$ and $b$ lie on the same strict side of line $cd$.
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 Point2, an abbreviation for the Euclidean plane $\mathbb{R}^2$. The signed orientation orient2(a,b,c) is the twice-area determinant $(b_0-a_0)(c_1-a_1)-(b_1-a_1)(c_0-a_0)$; its sign records which open half-plane contains $c$ relative to directed line $ab$, and zero means collinearity.
Proper separation is the non-collinear half of the classical segment-separation case split. Same-side products of orientations replace explicit half-plane membership, matching the standard computational-geometry witness that two closed segments are disjoint and non-collinear.
proof idea
Definitional: the predicate is the conjunction of two strict product inequalities on orient2. No tactics or lemmas are invoked. Downstream unpacking (same-side disjunctions of both signs positive or both negative) is handled by the sibling theorem that expands the products.
why it matters
This certificate is the positive-$\Delta$ orientation core of the four-point Hopf–Pannwitz geometry used for diameter shells. It feeds the geometric-disjointness implication (a meeting point would force an affine combination of same-strict-sign orientations to vanish), the abstract bridge that disjoint segments admit either a proper or a collinear separation certificate, and the proper-separated diameter contradiction (now discharged as a theorem). It also appears in the unified separated-diameter contradiction and in the opposite-sides meeting lemma that forces segments to intersect under diameter cross-bounds.
In the RS reading, diameter shells are maximal two-body recognition-energy shells; ruling out properly separated equal-length pairs under cross-distance bounds constrains shell occupancy and supports the ordered multiplicity bounds tied to Erdős #132.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.