orient2_zero_transitive
plain-language theorem explainer
If c and d both lie on the line through distinct planar points a and b, then a, c, d are collinear. Discrete-geometry and distance-shell arguments cite this when four-point orientation data collapses onto one line. The proof unfolds the signed-area form, builds two linear combinations that force the target cross product to vanish, and cases on a nonzero coordinate of a−b.
Claim. Let $a,b,c,d\in\mathbb{R}^2$ with $a\neq b$. Write $\mathrm{orient}(x,y,z)$ for the signed area of triangle $xyz$ (the 2D cross product $(y-x)\times(z-x)$). If $\mathrm{orient}(a,b,c)=0$ and $\mathrm{orient}(a,b,d)=0$, then $\mathrm{orient}(a,c,d)=0$. Equivalently: collinearity of $\{a,b,c\}$ and of $\{a,b,d\}$ implies collinearity of $\{a,c,d\}$.
background
The module physicalizes Erdős problem #132: classical distance shells become two-body recognition-energy shells, and shell occupancy is ordered-pair multiplicity (twice the unordered count for positive distances). Points are planar Point2 vectors from the bipartite distance spectrum.
The local primitive is the 2D orientation form: for three points, the signed parallelogram area of the two edge vectors from the first vertex. Vanishing orientation means the three points are collinear (affine dependence in the plane).
This lemma is pure plane geometry inside that shell calculus. It records that collinearity is transitive along a fixed supporting line once the base segment is nondegenerate ($a\neq b$). Downstream four-point analyses treat the four orientations among ${a,b,c,d}$ as real scalars subject to a Plücker relation and sign constraints from same-side witnesses.
proof idea
From $a\neq b$, extract a coordinate $i\in{0,1}$ with $a_i\neq b_i$. Unfold orientation into cross products and set $p,q$ for $b-a$, $r,s$ for $c-a$, $u,v$ for $d-a$. The two vanishing hypotheses are $ps-qr=0$ and $pv-qu=0$.
Linear combination yields $q(rv-su)=0$ and $p(rv-su)=0$. Case on the nonzero coordinate: if $p\neq 0$ (resp. $q\neq 0$), the ring fact that a product zero forces a factor zero gives $rv-su=0$, which is exactly $\mathrm{orient}(a,c,d)=0$. Finish each case by linarith.
why it matters
Inside the Erdős #132 shell-multiplicity development, four-point collinearity is the obstruction that collapses sparse-shell configurations. This lemma is the elementary engine for the family orient2_all_zero_of_o*_o*_zero: whenever two of the four orientations vanish on a shared edge, all four vanish, so the quartet is collinear.
It also feeds orient2_zero_transitive_swap, orient2_zero_two_zeros_share_bd, and the sum-of-squares pair analysis four_reals_M2_M3_pair_sos, whose doc-comment records that failed same-side witnesses force either $(o_1,o_2)=(0,0)$ or $(o_3,o_4)=(0,0)$. Those zero pairs are then expanded by the present transitivity into full collinearity.
Framework role is mathematical infrastructure for the RS reading of distance shells as recognition-energy shells, not a direct T0–T8 forcing step. It closes a pure geometry gap so shell-occupancy bounds can treat degenerate four-point configurations cleanly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.