four_points_orientation_dichotomy
plain-language theorem explainer
Geometric Plücker dichotomy for four planar points: if some triple among {a,b,c,d} is noncollinear, then at least one of six same-side orientation products is positive. Those products are exactly the witnesses that one perfect matching of K4 has geometrically disjoint edges. Cited by the noncollinear Conway–K4 thrackle bound and the four-point matching dichotomy. Proof reduces via Plücker and orient2 identities to an algebraic four-real sign dichotomy, then contradicts total collinearity.
Claim. Let $a,b,c,d\in\mathbb{R}^2$. Write $\mathrm{orient}$ for the signed area of an ordered triple. If 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 at least one of the six products $\mathrm{orient}(X,Y,P)\cdot\mathrm{orient}(X,Y,Q)$ associated to the three perfect matchings $\{ab,cd\}$, $\{ac,bd\}$, $\{ad,bc\}$ of $K_4$ is strictly positive.
background
The module Distance Shell Multiplicity records the Recognition Science physicalization of Erdős problem #132: classical distance shells become two-body recognition-energy shells, with ordered multiplicity twice the unordered count. Points live in Point2 (planar points from the bipartite distance spectrum).
The signed orientation $\mathrm{orient2}(p,q,r)$ is the usual twice-signed area of triangle $pqr$. Vanishing means collinearity of that triple. For four labeled points the three perfect matchings of $K_4$ are $M_1={ab,cd}$, $M_2={ac,bd}$, $M_3={ad,bc}$. A product $0<\mathrm{orient}(X,Y,P)\cdot\mathrm{orient}(X,Y,Q)$ is the same-side hypothesis of the geometric lemma that two segments on a common supporting line are disjoint.
The four orientations of the triples among ${a,b,c,d}$ obey the classical Plücker (alternating-sum) linear identity, which is the algebraic engine of the dichotomy.
proof idea
Name the four triple orientations $o_1=\mathrm{orient}(b,c,d)$, $o_2=\mathrm{orient}(a,c,d)$, $o_3=\mathrm{orient}(a,b,d)$, $o_4=\mathrm{orient}(a,b,c)$. The Plücker identity $o_1-o_2+o_3-o_4=0$ is imported from the alternating-sum lemma and rewritten by linarith.
Cyclic and swap identities for $\mathrm{orient2}$ rewrite every matching witness as a signed product among ${o_i}$. Assume for contradiction that all six witnesses fail (all products $\le 0$). Pushing the six inequalities through the rewrite rules yields six bilinear sign constraints on the $o_i$.
The pure algebraic lemma four_reals_orientation_dichotomy_alg then forces $o_1=o_2=o_3=o_4=0$. Each case of the noncollinearity hypothesis is thereby contradicted.
why it matters
This is the orientation engine behind the geometric four-point matching dichotomy: every nondegenerate 4-point configuration routes into at least one geometrically disjoint perfect matching of $K_4$, using only same-side segment disjointness and Plücker. That matching theorem is quoted as "the heart of the Conway-K4 obstruction."
Downstream it feeds the unconditional noncollinear Conway-conditioned $K_4$ support bound, which combines a six-pair edge-support inclusion with the conditional thrackle bound under a noncollinearity hypothesis. In the module's Erdős #132 program, controlling thrackle-type edge supports on four-point configurations is a discrete geometric bottleneck for shell-multiplicity estimates.
No T0–T8 forcing step is invoked directly; the result is pure planar combinatorial geometry serving the distance-shell multiplicity pipeline.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.