four_reals_orientation_dichotomy_alg
plain-language theorem explainer
Four real numbers linked by the Plücker identity o₁−o₂+o₃−o₄=0, and with all six bilinear products nonpositive in the stated pattern, must all be zero. Discrete geometers and thrackle analysts cite it as the algebraic core of the four-point orientation dichotomy. The proof is a short sum-of-squares argument: the linear relation forces (o₁+o₃)²≤0, then each pair collapses by sign hypotheses.
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 $o_3 o_4\le 0$, $o_1 o_2\le 0$, $o_2 o_4\ge 0$, $o_1 o_3\ge 0$, $o_2 o_3\le 0$, and $o_1 o_4\le 0$. Then $o_1=o_2=o_3=o_4=0$.
background
The module Distance Shell Multiplicity physicalizes Erdős problem #132: classical distance shells become two-body recognition-energy shells, with ordered-pair multiplicity twice the unordered count. In the plane, four points determine four triangle orientations (signed areas via the 2D orientation form). Those four scalars obey a linear Plücker identity coming from the Grassmann–Plücker relation on the six edge directions of $K_4$.
The six bilinear inequalities encode same-side / opposite-side sign patterns for the three perfect matchings of $K_4$. Geometrically they are the hypotheses that would feed a same-side segment-disjointness lemma; algebraically they are pure product signs on the four orientation numbers.
This declaration isolates the purely real-algebraic content: no geometry, only the linear relation plus the six product inequalities. The geometric wrapper that instantiates the four reals as orientations sits immediately downstream.
proof idea
Rewrite the Plücker hypothesis as $o_1+o_3=o_2+o_4$. Expand the product $(o_1+o_3)(o_2+o_4)$ and bound it by zero via the six sign hypotheses (nlinarith). Because the two sums are equal, that product equals $(o_1+o_3)^2$, so $(o_1+o_3)^2\le 0$. Antisymmetry with nonnegativity of squares forces $o_1+o_3=0$, hence $o_2+o_4=0$.
Then $o_3=-o_1$, so $o_1 o_3=-o_1^2$. The hypothesis $o_1 o_3\ge 0$ yields $o_1^2\le 0$, hence $o_1=0$ and $o_3=0$. The symmetric argument with $o_4=-o_2$ and $o_2 o_4\ge 0$ kills $o_2$ and $o_4$. The whole chain is elementary real arithmetic (linarith, ring, sq_eq_zero_iff, le_antisymm).
why it matters
This is the algebraic engine under the geometric Plücker dichotomy for four points: if any of the four triangle orientations is nonzero, then at least one of the six same-side witnesses for the three $K_4$ matchings holds, certifying a geometrically disjoint matching. That geometric theorem is used by the unconditional noncollinear Conway-conditioned $K_4$ support bound, which feeds the thrackle side of the distance-shell multiplicity program (Erdős #132 physicalized as recognition-energy shell occupancy).
In the Recognition Science ledger the result is pure mathematics supporting discrete geometric constraints on planar point sets; it does not itself invoke the forcing chain T0–T8, the J-cost, or the phi ladder, but it tightens the combinatorial geometry that bounds shell multiplicities in the plane.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.