proper_segment_separation_geometrically_disjoint
plain-language theorem explainer
Proper orientation separation of two planar segments forces their closed segments to be geometrically disjoint. Anyone working Hopf–Pannwitz or thrackle geometry inside the Erdős #132 distance-shell analysis would cite this. Proof is short contradiction: a common point would make a same-strict-sign convex combination of orientations vanish.
Claim. Let $a,b,c,d\in\mathbb{R}^2$. If $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)$ (each pair of endpoints lies strictly on one side of the line through the other segment), then the closed segments $[a,b]$ and $[c,d]$ do not intersect.
background
This module physicalizes Erdős problem #132 in Recognition Science terms: a classical distance value is a shell in the pairwise Euclidean spectrum; physically it is a two-body recognition-energy shell whose multiplicity is shell occupancy. Ordered pairs are used for Lean simplicity, so positive-distance ordered multiplicity is twice the unordered count and classical thresholds double.
A proper separation certificate says each segment's endpoints lie strictly on one side of the supporting line of the other: the two orientation products are strictly positive. Geometric disjointness of ordered edges means the closed straight-line segments do not meet; that is the correct Hopf–Pannwitz / thrackle predicate (endpoint-disjointness alone would wrongly exclude crossing diameter diagonals).
Point2 is the planar point type from the bipartite distance spectrum. Orientation orient2 is the usual signed area witness for sidedness and collinearity.
proof idea
Contradiction on a geometric meeting point. Assume some $x$ lies on both closed segments. On-segment membership on $[a,b]$ forces $\mathrm{orient}(a,b,x)=0$. On-segment membership on $[c,d]$ supplies an affine parameter $t\in[0,1]$ writing the orientation of $x$ as the convex combination $(1-t),\mathrm{orient}(a,b,c)+t,\mathrm{orient}(a,b,d)$.
Unpack the proper-separation hypothesis to same-strict-sign alternatives for $\mathrm{orient}(a,b,c)$ and $\mathrm{orient}(a,b,d)$. The lemma that a convex combination of two same-strict-sign reals is nonzero then contradicts the zero orientation of $x$.
why it matters
Supplies the strict-orientation half of the segment-disjointness toolkit used when counting distance-shell occupancies and thrackle-type configurations in the planar Erdős #132 physicalization. The module keeps a separate collinear certificate because orientation products vanish on a line; this theorem is the non-collinear branch.
No recorded downstream users yet (used_by empty), so it is infrastructure rather than a cited leaf. It underwrites later shell-multiplicity and sparse-shell arguments that need closed segments not to cross improperly when building ordered distance spectra and diameter shells. Framework link is mathematical support for two-body recognition-energy shells, not a direct T0–T8 forcing step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.