four_distinct_M2_or_M3_disjoint_noncollinear
plain-language theorem explainer
For four planar points with two designated distinct endpoint pairs and not all collinear, at least one of the two crossing-type K4 matchings has geometrically non-intersecting segments. The strong four-point dichotomy cites this as the (M2, M3) half of the matching disjunction. Proof is pure contradiction: both matchings meeting forces every triple orientation to vanish.
Claim. Let $a,b,c,d$ be points in the Euclidean plane with $a \neq b$ and $c \neq d$. If they are not all collinear (at least one of $\mathrm{orient}(a,b,c)$, $\mathrm{orient}(a,b,d)$, $\mathrm{orient}(a,c,d)$, $\mathrm{orient}(b,c,d)$ is nonzero), then either the closed segments $ac$ and $bd$ do not meet, or the closed segments $ad$ and $bc$ do not meet.
background
This 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 bookkeeping, so ordered multiplicity is twice the unordered count and classical thresholds scale by two.
Points live in the planar point type from the bipartite distance spectrum. Two ordered edges are geometrically disjoint when their closed straight-line segments do not intersect; the doc notes this is the correct Hopf-Pannwitz / thrackle predicate, since mere endpoint-disjointness wrongly excludes crossing diameter diagonals.
The three perfect matchings of $K_4$ on vertices ${a,b,c,d}$ are $M_1={ab,cd}$, $M_2={ac,bd}$, $M_3={ad,bc}$. This lemma is the pairwise at-least-one-disjoint statement for the pair $(M_2,M_3)$. Non-collinearity is expressed via the usual 2D orientation (signed area) predicate on triples.
proof idea
Contradiction. Assume neither $M_2$ nor $M_3$ is geometrically disjoint. From each meeting assumption, the same-side segment criterion is blocked in both edge orders: the four product-of-orientations witnesses involving the triples around $ac$, $bd$, $ad$, and $bc$ are each forced non-positive (using geometric-disjointness symmetry on the swapped ordered edges).
The combinatorial lemma on M2/M3 pair failure then yields that all four triple orientations vanish. Each branch of the non-collinearity hypothesis is an immediate contradiction.
why it matters
This is the $(M_2,M_3)$ half of the strong four-point dichotomy. The parent theorem upgrades the pairwise statement to: for any four distinct non-collinear points, at least two of the three perfect matchings of $K_4$ are geometrically disjoint (stated as a disjunction over the three two-disjoint combinations).
That dichotomy is the geometric engine behind distance-shell multiplicity bounds in the RS reading of Erdős #132: sparse shells and diameter shells constrain how many ordered pair-events can share one recognition-energy value without forcing thrackle-type crossings or collinear collapse. The argument is pure planar combinatorial geometry; it does not invoke the forcing chain (T5-T8) or the J-cost directly, but it supplies the discrete incidence control those continuum bridges later consume when shells are read as two-body posting costs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.