orient2_alternating_sum_eq_zero
plain-language theorem explainer
The alternating sum of the four triangle orientations on any four planar points vanishes: a classical Plücker identity in zero-sum form. Anyone proving K4 geometric dichotomies, collinearity propagation, or four-point support bounds in the distance-shell multiplicity development would cite it. The proof expands the orientation determinants and closes by ring.
Claim. For any four points $a,b,c,d$ in the Euclidean plane $\mathbb{R}^2$, the signed twice-areas (orientation determinants) satisfy $\mathrm{orient}(a,b,c)-\mathrm{orient}(a,b,d)+\mathrm{orient}(a,c,d)-\mathrm{orient}(b,c,d)=0$.
background
The ambient module physicalizes Erdős problem #132: a distance value is a two-body recognition-energy shell, and its multiplicity is shell occupancy. Points live in the visible plane as Point2, an abbreviation for the Euclidean space $\mathbb{R}^2$.
The orientation form is the signed twice-area determinant of a triple: $\mathrm{orient}(a,b,c)=(b_x-a_x)(c_y-a_y)-(b_y-a_y)(c_x-a_x)$. It vanishes exactly when the three points are collinear (or coincident), and changes sign under swap of the first two arguments.
The four orientations among ${a,b,c,d}$ are the natural coordinates for planar $K_4$ geometry. Their linear dependence is the classical Plücker relation, restated here as a pure alternating sum equal to zero.
proof idea
Term-mode proof in two steps. Unfold the orientation determinant on each of the four triples, obtaining an explicit multilinear polynomial in the eight coordinates. Then ring cancels all monomials, establishing the identity over $\mathbb{R}$. No geometric lemmas are invoked; the relation is purely algebraic.
why it matters
This identity is the algebraic engine behind the geometric Plücker dichotomy for four points: if at least one of the four orientations is nonzero, then at least one of the six same-side disjointness witnesses for the three perfect matchings of $K_4$ holds. That dichotomy feeds the exact four-point support bound extracted from the $K_4$ obstruction certificate.
It is also the linear relation used by the six "all orientations vanish" lemmas (any two vanishing orientations with a shared edge force the remaining two to vanish, under a non-degeneracy hypothesis). Those lemmas close collinearity-propagation arguments in the ordered distance-shell analysis.
In the broader Recognition Science setting the module records the RS reading of Erdős #132 (distance shells as recognition-energy shells). The identity itself is pure planar geometry; it does not invoke the forcing chain T0–T8, the J-cost, or the phi ladder, but it underwrites the combinatorial geometry those shells live in.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.