four_distinct_M1_or_M2_disjoint_noncollinear
plain-language theorem explainer
For four planar points that are not all collinear, with the mild inequalities b≠c and a≠d, at least one of the two perfect matchings (ab,cd) or (ac,bd) has non-intersecting closed segments. Discrete-geometry and thrackle arguments cite this as the M₁/M₂ half of the K₄ matching dichotomy. The proof is contradiction: both matchings meeting forces all four orientations to vanish via the pair-fail collinearity lemma.
Claim. Let $a,b,c,d\in\mathbb{R}^2$. Suppose $b\neq c$, $a\neq d$, and the four points are not all collinear (at least one of the four oriented areas $\mathrm{orient}_2$ among triples is nonzero). Then either the closed segments $\overline{ab}$ and $\overline{cd}$ are disjoint, or the closed segments $\overline{ac}$ and $\overline{bd}$ are disjoint.
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 occupancy is the multiplicity. Ordered pairs are used for Lean bookkeeping, so positive-distance ordered multiplicity is twice the unordered count.
Point2 is the Euclidean plane $\mathbb{R}^2$. Geometric disjointness of ordered edges means the closed straight-line segments do not meet; the doc notes this is the correct Hopf–Pannwitz / thrackle predicate, since mere endpoint-disjointness would wrongly exclude crossing diameter diagonals. Orientation orient2 is the usual signed area of a triple (vanishing iff collinear).
The two matchings in view are $M_1=(ab,cd)$ and $M_2=(ac,bd)$, two of the three perfect matchings of $K_4$ on four labeled points. Symmetry of geometric disjointness is already available upstream.
proof idea
Proof by contradiction. Negate the conclusion to assume both $M_1$ and $M_2$ fail geometric disjointness. Each failure kills both same-side orientation witnesses: if a same-side product of orientations were positive, same_side_segments_disjoint (and its symmetric form via ordered_edges_geometrically_disjoint_symm) would force disjointness. The four negated witness inequalities, together with $b\neq c$ and $a\neq d$, are fed to orient2_M1_M2_pair_fail_all_collinear, which concludes that all four relevant orientations vanish. That contradicts the hypothesis that at least one orientation is nonzero. Case-split on the four-way disjunction finishes.
why it matters
This is the pair-level "at-least-one-disjoint" lemma for $(M_1,M_2)$ inside the distance-shell multiplicity development. It feeds directly into four_distinct_points_two_matchings_disjoint_noncollinear, the strong four-point dichotomy: for any four distinct non-collinear points, at least two of the three perfect matchings of $K_4$ are geometrically disjoint.
That dichotomy is geometric scaffolding for controlling how often a single distance can recur as a shell without forcing thrackle-type crossings or collinear collapses. In the RS reading, shell occupancy bounds on recognition-energy distances sit behind the classical Erdős #132 threshold (ordered form $\le 2n$). The argument is pure planar combinatorial geometry; it does not itself invoke the forcing chain T0–T8, but it underwrites the discrete geometry layer those physical claims rest on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.