orient2_cyclic'
plain-language theorem explainer
Cyclic reordering of three planar points from (a,b,c) to (c,a,b) leaves the signed orientation (twice-area determinant) unchanged. Anyone normalizing triangle vertex order in collinearity or distance-shell arguments cites this. The proof is two successive rewrites of the one-step cyclic identity.
Claim. For any three points $a,b,c$ in the Euclidean plane $\mathbb{R}^2$, the signed orientation determinant satisfies $\operatorname{orient}(a,b,c)=\operatorname{orient}(c,a,b)$.
background
The module physicalizes Erdős problem #132: classical distance shells become two-body recognition-energy shells, with ordered-pair multiplicity twice the unordered count. Points live in the visible plane, written as the Euclidean space $\mathbb{R}^2$.
The orientation form is the standard signed twice-area determinant $\operatorname{orient}(a,b,c)=(b_0-a_0)(c_1-a_1)-(b_1-a_1)(c_0-a_0)$. It vanishes precisely on collinear triples and changes sign under odd permutations of the vertices.
The sibling one-step cyclic law already records $\operatorname{orient}(a,b,c)=\operatorname{orient}(b,c,a)$. The present statement is the other generator of the cyclic group on three labels.
proof idea
Term-style tactic proof by two rewrites. Apply the one-step cyclic identity once to send $(a,b,c)$ to $(b,c,a)$, then again to send $(b,c,a)$ to $(c,a,b)$. Equality is transitive, so the two-step cycle preserves orientation. No expansion of the determinant is needed.
why it matters
Downstream, the quadruple-vanishing bridge uses this identity: if the four canonical orientations on ${a,b,c,d}$ vanish, every triple drawn from those four points is collinear. That bridge converts a short list of orientation zeros into the full collinearity predicate needed for diameter-shell and sparse-shell arguments.
In the RS reading, planar orientation controls which ordered pair events sit on the same recognition-energy shell. Keeping cyclic order free of sign flips lets shell-multiplicity counts stay invariant under vertex rotation, which is the bookkeeping step behind the ordered-pair form of the Erdős #132 threshold.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.