four_reals_M1_M2_pair_sos
plain-language theorem explainer
Four real orientation products that simultaneously fail the M₁ and M₂ same-side witnesses, and obey the Plücker identity o₁−o₂+o₃−o₄=0, force a rigid zero pattern: either o₁=o₄=0 or o₂=o₃=0. Discrete-geometry and thrackle arguments cite this as the algebraic engine that turns pair-failure into collinearity of two triangles in a K₄. The proof is a short real-arithmetic reduction: Plücker equates two differences, the four sign bounds make their product nonpositive, hence a square vanishes, and a zero-divisor split finishes.
Claim. Let $o_1,o_2,o_3,o_4\in\mathbb{R}$ satisfy the Plücker relation $o_1-o_2+o_3-o_4=0$. Suppose the M₁ failure signs $o_3 o_4\le 0$ and $o_1 o_2\le 0$, and the M₂ failure signs $o_2 o_4\ge 0$ and $o_1 o_3\ge 0$. Then either $o_1=o_4=0$ or $o_2=o_3=0$.
background
The module Distance Shell Multiplicity is the Recognition Science physicalization of Erdős problem #132: a classical distance value is a shell in the pairwise Euclidean spectrum; physically it is a two-body recognition-energy shell whose occupancy is the shell multiplicity. Ordered pairs are used for Lean bookkeeping, so positive-distance ordered multiplicity is twice the unordered count and classical thresholds double.
In the four-point (K₄) analysis the quantities $o_i$ are orientation products (signed areas via orient2) that serve as same-side disjointness witnesses for two matchings M₁ and M₂ on the complete graph on four labeled points. Failure of a witness is a non-strict opposite-sign (or zero) product condition. The Plücker-type linear relation $o_1-o_2+o_3-o_4=0$ is the algebraic shadow of the dependence among the four triangle orientations on four points in the plane.
The companion statement for the pair (M₂, M₃) has the same shape with a different zero pattern; together these lemmas convert simultaneous matching-failure into collinearity of shared edges.
proof idea
Rewrite Plücker as $o_1-o_4=o_2-o_3$. The four sign hypotheses, fed to nonlinear arithmetic, give $(o_1-o_4)(o_2-o_3)\le 0$. Substituting the rewritten difference yields $(o_1-o_4)^2\le 0$. Antisymmetry against nonnegativity of squares forces $(o_1-o_4)^2=0$, hence $o_1=o_4$ and (again by Plücker) $o_3=o_2$.
Under these equalities the products $o_2 o_4$ and $o_1 o_2$ coincide, so the opposing bounds $o_1 o_2\le 0\le o_2 o_4$ collapse to $o_1 o_2=0$. The real zero-divisor law splits into $o_1=0$ or $o_2=0$; each case, with the equalities already obtained, produces one arm of the claimed disjunction.
why it matters
This is the pure real-arithmetic core behind the geometric lemma orient2_M1_M2_pair_fail_all_collinear, which states that if all four same-side witnesses for the pair (M₁, M₂) fail then every orient2 on the four points vanishes (full collinearity). That collinearity gate is consumed by exact_fourpoint_conway_thrackle_support_bound_noncollinear_thm, the unconditional noncollinear Conway-conditioned K₄ support bound: on a 4-point set that is not entirely collinear, a Conway thrackle cannot use too many unordered edges.
In the RS reading, thrackle-type support bounds control how many ordered pairs can sit on a single distance shell, which is exactly the multiplicity side of the Erdős #132 physicalization. The lemma therefore sits on the discrete-geometry spine that feeds shell-occupancy estimates, not on the T0–T8 forcing chain itself. It closes an algebraic gap rather than an open scaffold: claim status is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.