OrderedEdgesMeetGeometrically
plain-language theorem explainer
Two ordered planar edges meet geometrically when their closed straight-line segments share at least one point. This is the Hopf–Pannwitz / thrackle intersection predicate used throughout the distance-shell multiplicity development (Erdős #132). Endpoint sharing and proper crossings both count. The body is a pure existential over a common point on both closed segments.
Claim. For ordered edges $e=(e_1,e_2)$ and $f=(f_1,f_2)$ with endpoints in the plane, the edges meet geometrically if there exists a point $x$ lying on both closed segments $[e_1,e_2]$ and $[f_1,f_2]$.
background
The module physicalizes Erdős problem #132: a classical distance value is a shell in the pairwise Euclidean spectrum; in RS it is a two-body recognition-energy shell whose multiplicity is shell occupancy. Ordered pairs are used for Lean simplicity; for positive distances, ordered multiplicity is twice the unordered count, so classical thresholds $\le n$ become $\le 2n$.
Point2 is the planar point type from the bipartite distance spectrum. An ordered edge is a pair of such points. Closed-segment membership is the standard Euclidean segment predicate: $x$ lies between the two endpoints inclusive.
The companion notion is geometric disjointness (no common point on the closed segments). The module doc stresses that endpoint-disjointness alone is the wrong thrackle predicate: it would exclude legitimate crossing diameter diagonals that share no vertex.
proof idea
Pure definition, not a proved theorem. The proposition is the existential $\exists x,; x\in[e_1,e_2]\land x\in[f_1,f_2]$ with no further side conditions. Unfolding in a proof is immediate; case splits typically branch on whether this holds (as in the four-point diameter crossing argument).
why it matters
This is the geometric meeting atom for the whole diameter-shell / thrackle stack in the module. Downstream it appears in FourPointDiameterCrossing (any two endpoint-disjoint diameter pairs with all six distances $\le\Delta$ have intersecting closed segments), in the local diameter-meeting lemmas, and in the transfer from ordered Conway thrackle bounds to support-level bounds.
It is the correct Hopf–Pannwitz intersection predicate: shared endpoints count as meetings, so crossing diameter diagonals are not falsely declared disjoint. That choice is what lets the four-point geometric core feed NoDisjointDiameterEdges and the Conway support cardinality estimates that bound shell multiplicity for Erdős #132.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.