four_reals_M2_M3_pair_sos
plain-language theorem explainer
Four real orientation scalars obeying the Plücker identity and the four product-sign conditions that mark simultaneous failure of the M₂ and M₃ same-side witnesses must vanish in pairs: either the first two are zero or the last two are zero. Discrete geometers handling the four-point Conway thrackle case cite this algebraic core. The argument is a short sum-of-squares collapse: Plücker turns a nonnegative product into a negated square, forcing equalities, then a zero-product case split.
Claim. Let $o_1,o_2,o_3,o_4\in\mathbb{R}$ satisfy the Plücker identity $o_1-o_2+o_3-o_4=0$, and the four sign conditions $o_2 o_4\ge 0$, $o_1 o_3\ge 0$, $o_2 o_3\le 0$, $o_1 o_4\le 0$. Then either $o_1=o_2=0$ or $o_3=o_4=0$.
background
The module physicalizes Erdős problem #132: a distance value is a two-body recognition-energy shell, and its multiplicity is shell occupancy. Ordered pairs are used for bookkeeping; for a positive distance, ordered multiplicity is twice the unordered count, so classical thresholds double.
In the four-point plane geometry layer, each $o_i$ stands for an oriented area (a $2$-orientation) of a triple drawn from four labeled points. Same-side disjointness witnesses for the combinatorial configurations labeled $M_2$ and $M_3$ are encoded by strict positivity of certain products of these orientations. Failure of those witnesses is the weak opposite: the four product inequalities in the hypothesis list.
The Plücker relation $o_1-o_2+o_3-o_4=0$ is the linear dependence among the four triple orientations on four points. The theorem is the purely real-algebraic engine that turns simultaneous $M_2$/$M_3$ failure plus Plücker into a pair of vanishing orientations, which later geometric lemmas read as shared-edge collinearity.
proof idea
Rewrite Plücker as $o_1-o_2=-(o_3-o_4)$. From the four sign hypotheses, nlinarith yields the product inequality $0\le(o_1-o_2)(o_3-o_4)$. Substitute the rewritten difference to obtain $(o_1-o_2)(o_3-o_4)=-(o_3-o_4)^2$. Nonnegativity of that product forces $(o_3-o_4)^2\le 0$, hence (by le_antisymm against sq_nonneg) the square vanishes, so $o_3=o_4$ and then $o_2=o_1$.
With those equalities, $o_2 o_3=o_1 o_3$. The opposing signs $o_2 o_3\le 0$ and $o_1 o_3\ge 0$ pin $o_1 o_3=0$. Split on the zero product: if $o_1=0$ then $o_2=0$; if $o_3=0$ then $o_4=0$.
why it matters
This is the real-algebraic heart of the $(M_2,M_3)$ collinearity closure. Downstream, orient2_M2_M3_pair_fail_all_collinear lifts the pair-of-zeros conclusion to all six orientations on four points (via shared-vertex transitivity and Plücker), and that full vanishing feeds the unconditional noncollinear Conway-conditioned $K_4$ support bound exact_fourpoint_conway_thrackle_support_bound_noncollinear_thm.
In the Recognition Science reading, distance shells are recognition-energy shells; controlling four-point thrackle support is a discrete step toward the ordered-multiplicity form of Erdős #132 recorded in this module. The lemma itself is pure real algebra (no continuum smuggling, no analytic registry), so it sits cleanly under the certified discrete layer that later interfaces with the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.