four_distinct_points_two_matchings_disjoint_noncollinear
plain-language theorem explainer
For four distinct planar points that are not all collinear, at least two of the three perfect matchings of K₄ have geometrically disjoint segments. Discrete geometers and thrackle theorists cite this as the strong four-point dichotomy. The proof is pure casework: it chains three pairwise matching-disjointness lemmas and reassembles the three admissible pairs.
Claim. Let $a,b,c,d\in\mathbb{R}^2$ be pairwise distinct and not all collinear. Write $M_1=\{(a,b),(c,d)\}$, $M_2=\{(a,c),(b,d)\}$, $M_3=\{(a,d),(b,c)\}$ for the three perfect matchings of $K_4$. Then at least one of the following holds: both edges of $M_1$ and of $M_2$ are geometrically disjoint; both of $M_1$ and of $M_3$; or both of $M_2$ and of $M_3$. Geometric disjointness means the closed straight-line segments do not meet.
background
The module physicalizes Erdős problem #132: classical distance shells become two-body recognition-energy shells, with ordered multiplicity twice the unordered count. Points live in the plane (Point2).
Two ordered edges are geometrically disjoint when their closed segments do not intersect. The doc-comment stresses this is the correct Hopf–Pannwitz / thrackle predicate: endpoint-disjointness alone is too strong and would exclude crossing diameter diagonals.
The three perfect matchings of the complete graph on four labeled vertices are the only ways to pair four points into two edges. Non-collinearity is expressed by at least one oriented triple having nonzero orientation, so the configuration is genuinely planar rather than degenerate on a line.
proof idea
Term-mode case analysis on three upstream pairwise lemmas:
- Apply the M1-or-M2 disjointness lemma (under non-collinearity) to obtain either D1 or D2.
- In the D1 branch, apply M1-or-M3, then if needed M2-or-M3, and package the resulting pair as one of the three disjuncts.
- In the D2 branch, apply M2-or-M3, then if needed M1-or-M3, again packaging into the matching disjunct.
Every leaf of the case tree is an Or.inl / Or.inr constructor wrapping a pair of already-proved geometric-disjointness facts. No geometry is re-proved here; the argument only recombines the three binary dichotomies into the ternary strong form.
why it matters
This is the combinatorial engine behind the exact four-point Conway thrackle support bounds in the same module. Downstream, the conditional bound assumes the unordered edge support sits inside the standard six-pair Finset on four ambient points and concludes cardinality at most 4; the unconditional noncollinear theorem composes that with the subset-inclusion lemma.
The module doc ties the whole development to the RS physicalization of Erdős #132: shell multiplicity as recognition-energy occupancy. Bounding thrackle support on four points is the local geometric step that feeds global multiplicity controls. The immediately following section converts geometric disjointness of two matchings into a missing-edge count for any Conway thrackle, which is how the dichotomy becomes a cardinality bound.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.