four_distinct_points_one_matching_disjoint_noncollinear
plain-language theorem explainer
For any four planar points that are not all collinear, at least one of the three perfect matchings of K4 consists of two geometrically disjoint closed segments. This is the geometric heart of the Conway-conditioned K4 thrackle obstruction and is cited by the noncollinear four-point support bound. The proof cases on the six-way orientation dichotomy and applies same-side segment disjointness (with ordered-edge symmetry) in each branch.
Claim. Let $a,b,c,d$ be points in the Euclidean plane. If they are not all collinear (equivalently, at least one triple among them has nonzero $2$-orientation), then at least one of the three perfect matchings $\{ab,cd\}$, $\{ac,bd\}$, $\{ad,bc\}$ consists of a pair of closed straight-line segments that do not intersect.
background
The ambient module physicalizes Erdős problem #132: classical distance shells become two-body recognition-energy shells, with ordered-pair multiplicity twice the unordered count. Points live in Point2 (the planar point type from the bipartite distance spectrum). Edges are ordered pairs; geometric disjointness means the closed segments do not meet at all.
OrderedEdgesGeometricallyDisjoint is the Hopf–Pannwitz / thrackle meeting predicate: endpoint-disjointness alone is too strong (it would exclude legitimate crossing diameters). The complementary meeting relation is the one thrackle axioms constrain.
The local goal is a Conway-conditioned K4 obstruction. Earlier certificates that only assumed "every pair of ordered edges meets" fail on collinear five-edge non-star configurations where segments overlap on subsegments. Conway's simple-meeting condition repairs that; the present lemma handles the noncollinear half of the repaired bound.
proof idea
Term-mode case split on four_points_orientation_dichotomy, which, under the non-all-collinear hypothesis, yields six orientation configurations (which pairs of triples share a side pattern).
Each branch feeds the corresponding orientation witness into same_side_segments_disjoint, producing geometric disjointness of one ordered matching. In the three branches where the matching appears in reverse edge order, ordered_edges_geometrically_disjoint_symm flips the pair. The six outcomes are then packaged as the three-way disjunction over the perfect matchings of K4.
No metric estimates appear: the argument is pure planar orientation algebra (Plücker-type sign identities behind the dichotomy lemma).
why it matters
This lemma is named in the module's Conway-conditioned K4 section as the closed noncollinear half of the obstruction: under simple meeting, four ambient points cannot host more than four unordered support edges. It is consumed by exact_fourpoint_conway_thrackle_support_bound_noncollinear_thm, which combines the six-pair support subset with the conditional Conway thrackle bound under a four-point ambient set that is not all collinear.
In the broader Distance Shell Multiplicity development, thrackle-type support bounds limit how many ordered pairs can share a common distance shell without forcing geometric crossings or overlaps. That feeds the RS reading of Erdős #132, where shell occupancy is recognition-energy multiplicity and classical $\le n$ thresholds become ordered $\le 2n$ statements.
The collinear case remains separate hand geometry (sorting on a line); this declaration deliberately routes only the non-degenerate configurations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.