four_distinct_M1_or_M3_disjoint_noncollinear
plain-language theorem explainer
For four planar points that are not all collinear, with the two opposite-pair inequalities b≠d and a≠c, at least one of the matchings M₁={(a,b),(c,d)} and M₃={(a,d),(b,c)} has geometrically non-intersecting segments. Combinatorial geometers working the Hopf–Pannwitz / thrackle side of Erdős #132 cite it. Proof is contradiction: both matchings meeting forces all four orientation determinants to vanish, contradicting non-collinearity.
Claim. Let $a,b,c,d\in\mathbb{R}^2$. Assume $b\neq d$, $a\neq c$, and that the four points are not all collinear (at least one of the four orientation determinants $\mathrm{orient}_2$ on triples is nonzero). Then either the closed segments $\overline{ab}$ and $\overline{cd}$ are disjoint, or the closed segments $\overline{ad}$ and $\overline{bc}$ are disjoint.
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 occupancy is the shell multiplicity. Ordered pairs are used for Lean bookkeeping, so ordered multiplicity is twice the unordered count and classical thresholds double.
Point2 is the Euclidean plane $\mathbb{R}^2$. The signed orientation orient2 a b c is twice the signed area of triangle $abc$, vanishing iff $a,b,c$ are collinear. Two ordered edges are geometrically disjoint when their closed straight-line segments do not meet; the module stresses 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={(a,b),(c,d)}$, $M_2={(a,c),(b,d)}$, and $M_3={(a,d),(b,c)}$. This lemma is the pairwise "at-least-one-disjoint" statement for the pair $(M_1,M_3)$.
proof idea
Proof by contradiction. Assume neither matching is geometrically disjoint, so both $M_1$ and $M_3$ have meeting segments.
From the $M_1$ failure one obtains that the same-side orientation products for base $ab$ against ${c,d}$ and for base $cd$ against ${a,b}$ are not strictly positive (else same_side_segments_disjoint, with symmetry of geometric disjointness, would force $M_1$ disjoint). The same argument on $M_3$ kills the corresponding products for bases $ad$ and $bc$.
The algebraic lemma orient2_M1_M3_pair_fail_all_collinear then concludes that all four triple orientations vanish. Each disjunct of the non-collinearity hypothesis is therefore false, contradiction.
why it matters
Feeds the parent theorem 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 the local geometric engine behind sparse-shell and diameter-shell control in the ordered distance spectrum.
In the RS reading of Erdős #132, shell multiplicity is recognition-energy occupancy. Geometric disjointness of matching edges is the thrackle-side obstruction that keeps high-multiplicity shells from packing too tightly in the plane. This lemma closes the $(M_1,M_3)$ case of the pairwise matching analysis; sibling pair lemmas cover the other matching pairs, and the parent assembles them into the full two-of-three statement.
No forcing-chain landmark (T5–T8) is invoked directly; the result is pure planar combinatorial geometry supporting the multiplicity bounds that later interface with the phi-ladder mass and energy bookkeeping.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.