four_reals_M1_M3_pair_sos
plain-language theorem explainer
Four reals obeying a Plücker linear relation and four opposite-sign product inequalities must vanish in paired blocks: either the first and third are zero, or the second and fourth. Cited in the four-point orientation analysis behind distance-shell multiplicity (Erdős #132 / Conway thrackle support). Proof is a short sum-of-squares reduction: Plücker equates a square to a nonpositive product, forcing both pairwise sums to zero, then a cross inequality kills one product.
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$ and the four product inequalities $o_3 o_4\le 0$, $o_1 o_2\le 0$, $o_2 o_3\le 0$, $o_1 o_4\le 0$. Then either $(o_1=0\land o_3=0)$ or $(o_2=0\land o_4=0)$.
background
The ambient module physicalizes Erdős problem #132: a classical distance value is a shell in the pairwise Euclidean spectrum; in RS it is a two-body recognition-energy shell whose occupancy is the multiplicity. Ordered pairs are used for bookkeeping, so classical multiplicity $\le n$ becomes ordered multiplicity $\le 2n$.
The four scalars here are orientation (signed-area) values among four points in the plane. Same-side witnesses for the pair of combinatorial modes labelled $M_1$ and $M_3$ are products of two orientations being strictly positive. Joint failure of those witnesses is exactly the four inequalities $o_i o_j\le 0$ in the hypothesis. The linear Plücker relation is the algebraic identity those four orientations satisfy when they arise from a single four-point configuration.
Downstream geometry reads the conclusion as two of the four orientations vanishing, which (with a nondegeneracy hypothesis on an edge) forces full collinearity of the four points.
proof idea
Rewrite Plücker as $o_1+o_3=o_2+o_4$. The four product inequalities imply, by nonlinear arithmetic, that the product $(o_1+o_3)(o_2+o_4)$ is nonpositive. Substituting the rewritten Plücker identity turns that product into $(o_1+o_3)^2$, so the square is $\le 0$. Antisymmetry against nonnegativity of squares forces $(o_1+o_3)^2=0$, hence $o_1+o_3=0$ and (again by Plücker) $o_2+o_4=0$. Thus $o_3=-o_1$ and $o_4=-o_2$.
Substitute into $o_2 o_3\le 0$ to obtain $-o_1 o_2\le 0$, i.e. $o_1 o_2\ge 0$. Combined with the given $o_1 o_2\le 0$ one gets $o_1 o_2=0$. The zero-divisor law on $\mathbb{R}$ splits into $o_1=0$ or $o_2=0$; each arm, with the sum relations, yields the corresponding paired vanishing.
why it matters
This is the pure real-algebra engine under the geometric lemma that joint failure of the $M_1$ and $M_3$ same-side witnesses forces all four orientations among ${a,b,c,d}$ to vanish (hence, with $b\ne d$, full collinearity). That collinearity lemma is quoted by the unconditional noncollinear Conway-conditioned $K_4$ support bound: on a four-point set that is not entirely collinear, a Conway thrackle edge set cannot realize the full six-pair support.
In the RS reading, those bounds control how many ordered pairs can sit on a single distance shell, which is the occupancy side of the Erdős #132 physicalization. The argument is local linear algebra over $\mathbb{R}$; it does not itself invoke the forcing chain (T5–T8) or the Recognition Composition Law, but it is load-bearing scaffolding for the combinatorial geometry those landmarks later constrain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.