ordered_edges_geometrically_disjoint_symm
plain-language theorem explainer
Geometric disjointness of ordered planar edges is symmetric in the two arguments: if the closed segments of e and f do not meet, neither do those of f and e. Downstream four-point matching dichotomies (Conway–K4 / distance-shell multiplicity) cite it to reorder matchings freely. The proof is a one-line contrappositive through symmetry of geometric meeting.
Claim. Let $e,f$ be ordered pairs of points in the plane. If the closed straight-line segments of $e$ and $f$ do not intersect, then the closed segments of $f$ and $e$ likewise do not intersect.
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 planar Point2 values from the bipartite distance spectrum.
Two ordered edges are geometrically disjoint when their closed segments do not meet. The doc stresses this is the correct Hopf–Pannwitz / thrackle predicate: endpoint-disjointness alone is too strong and would exclude crossing diameter diagonals. The dual predicate (geometric meeting) is already known to be symmetric in the two ordered edges.
Local work sits inside the noncollinear four-point analysis that routes $K_4$ configurations into disjoint perfect matchings.
proof idea
Disjointness is defined as the negation of geometric meeting. Assume the reversed pair meets. Apply the already-proved symmetry of meeting to obtain that the original ordered pair meets, contradicting the hypothesis. The whole argument is a two-tactic contrappositive; no geometry is re-derived here.
why it matters
This is bookkeeping symmetry needed so matching labels can be swapped without re-proving segment non-intersection. It is used by the three pairwise “at-least-one-disjoint” lemmas for matchings $(M_1,M_2)$, $(M_1,M_3)$, $(M_2,M_3)$, and by the full geometric four-point matching dichotomy: for any four non-all-collinear points, at least one of the three perfect matchings of $K_4$ consists of two geometrically disjoint segments.
That dichotomy is described as the heart of the Conway–K4 obstruction in the distance-shell multiplicity program (RS reading of Erdős #132). Without free reordering of edge pairs, the case splits on which matching is disjoint would double-count or miss orientations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.