orient2_left_self
plain-language theorem explainer
Signed planar orientation of three points vanishes when the third point equals the first endpoint. Anyone using the twice-area determinant in the distance-shell multiplicity development (Erdős #132 physicalization) would cite this. The proof unfolds the coordinate formula and closes by ring.
Claim. For any points $a,b\in\mathbb{R}^2$, the signed twice-area orientation determinant satisfies $\mathrm{orient}(a,b,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, with multiplicity as shell occupancy. Ordered pairs are used for Lean simplicity, so classical multiplicity $\le n$ becomes ordered multiplicity $\le 2n$.
Points live in the Euclidean plane: Point2 is an abbreviation for $\mathbb{R}^2$ (via EuclideanSpace $\mathbb{R}$ (Fin 2) from BipartiteDistanceSpectrum). The local orientation map is the standard 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." It vanishes on degenerate triangles and changes sign under swap of the first two arguments.
proof idea
One-line algebraic identity. Unfold the definition of the orientation determinant, substitute the third argument equal to the first, and apply ring to the resulting polynomial in the coordinates; every term cancels.
why it matters
This is a basic geometric sanity check inside the planar toolkit supporting distance-shell multiplicity. Orientation is the signed area test used to reason about collinearity and combinatorial configurations of finite planar point sets when counting ordered pair events on each distance shell.
The module frames shells as recognition-energy levels rather than pure combinatorial objects, tying the classical Erdős #132 multiplicity question to RS two-body energetics. No downstream consumers are wired yet (used_by is empty); the lemma sits as local infrastructure beside siblings such as diameter-shell uniqueness, sparse-shell divergence, and the ordered spectrum definitions. It does not itself touch the forcing chain (T0–T8) or the RCL, but keeps the planar geometry layer free of degenerate-orientation edge cases.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.