OrderedEdgesGeometricallyDisjoint
plain-language theorem explainer
Two ordered edges in the plane are geometrically disjoint when their closed straight-line segments have empty intersection. Workers on the Hopf–Pannwitz thrackle side of the RS physicalization of Erdős #132 cite this predicate as the correct meeting relation. Endpoint-only disjointness is too strong: it would exclude crossing diameter diagonals that thrackle geometry must allow. The body is the Boolean negation of geometric meeting.
Claim. For ordered edges $e=(a,b)$ and $f=(c,d)$ with $a,b,c,d\in\mathbb{R}^2$, the edges are geometrically disjoint when there is no point $x\in\mathbb{R}^2$ that lies on both closed segments $\overline{ab}$ and $\overline{cd}$.
background
The module physicalizes Erdős problem #132: classical distance shells become two-body recognition-energy shells, and shell multiplicity is occupancy. Ordered pairs are used for Lean simplicity; for a positive distance, ordered multiplicity is twice the unordered count, so classical thresholds $\le n$ become $\le 2n$.
Points live in the Euclidean plane: Point2 is $\mathbb{R}^2$. An ordered edge is a pair of points. Geometric meeting means the two closed straight-line segments share at least one point (including endpoints and proper crossings). Geometric disjointness is the complementary relation.
The doc-comment stresses the thrackle convention: this closed-segment predicate, not mere endpoint-disjointness, is the correct Hopf–Pannwitz meeting test. Crossing diameter diagonals meet geometrically and must remain admissible in thrackle support arguments.
proof idea
One-line definitional wrapper: the predicate is exactly the negation of geometric meeting of the two ordered edges. No tactics, no lemmas, no algebraic reduction.
why it matters
This is the thrackle meeting predicate for the whole distance-shell multiplicity development. Downstream certificates and bounds quantify over pairs of ordered edges that fail geometric disjointness (every pair meets) or that succeed it (separation case splits).
It appears in collinear and proper segment-separation certificates, in the abstract bridge that endpoint-disjoint non-meeting segments admit an orientation or collinear separation, and in exact four- and five-point non-star thrackle support bounds and K4 obstruction forms. The diameter ordered-multiplicity theorem routes through no-disjoint-diameter-edges plus an ordered thrackle bound; both sides speak this language.
In the RS reading, diameter shells are the extreme two-body recognition-energy shells. Controlling when diameter edges can be geometrically disjoint is the geometric gate between thrackle combinatorics and the ordered multiplicity bound that physicalizes Erdős #132.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.