orient2_cyclic
plain-language theorem explainer
Cyclic permutation of three planar points leaves the signed orientation (twice-area determinant) unchanged: orient(a,b,c) equals orient(b,c,a). Anyone proving collinearity certificates or matching-disjointness witnesses in the distance-shell multiplicity development cites this identity. The proof unfolds the coordinate formula and closes by ring.
Claim. For any three points $a,b,c$ in the Euclidean plane $\mathbb{R}^2$, the signed orientation determinant satisfies $\mathrm{orient}(a,b,c)=\mathrm{orient}(b,c,a)$, where $\mathrm{orient}(a,b,c)=(b_0-a_0)(c_1-a_1)-(b_1-a_1)(c_0-a_0)$.
background
The module Distance Shell Multiplicity records the Recognition Science physicalization of Erdős problem #132: classical distance shells become two-body recognition-energy shells, and ordered-pair multiplicity is twice the unordered count.
Points live in Point2, an abbreviation for the Euclidean plane $\mathbb{R}^2$. The local orientation form is the signed twice-area determinant
$$\mathrm{orient}(a,b,c)=(b_0-a_0)(c_1-a_1)-(b_1-a_1)(c_0-a_0),$$
documented as "Signed twice-area / orientation determinant in the visible plane." Vanishing of this form is the affine collinearity test used throughout the shell-multiplicity arguments.
A companion swap identity (first two arguments negate orientation) sits beside this cyclic identity; together they generate the full $S_3$ action on triangle orientations.
proof idea
One-line algebraic proof: unfold the coordinate definition of the orientation form, then apply ring to the resulting polynomial identity in the six coordinates. No geometric lemmas are invoked; the equality is pure expansion and cancellation of bilinear terms.
why it matters
This is the basic cyclic symmetry of planar orientation. Downstream it feeds the second cyclic form orient2_cyclic', the four-point Plücker dichotomy four_points_orientation_dichotomy, the all-orientations-vanish lemmas (orient2_all_zero_of_o1_o2_zero, orient2_all_zero_of_o1_o4_zero), the matching-pair failure collinearity certificates (orient2_M1_M2_pair_fail_all_collinear and siblings), and the endpoint-disjoint two-point intersection collinearity theorem.
Those results certify when diameter representatives or perfect matchings of $K_4$ force collinearity, which is the geometric engine behind sparse-shell multiplicity bounds in the RS reading of Erdős #132. Without cyclic invariance, the six same-side witnesses and the orientation-dichotomy case splits would not close under relabeling.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.