orient2_right_self
plain-language theorem explainer
The planar orientation determinant vanishes when its third argument equals the second endpoint. Anyone working collinearity or segment geometry in the distance-shell module cites this. The proof unfolds the twice-area formula and closes by ring.
Claim. For any points $a,b$ in the Euclidean plane $\mathbb{R}^2$, the signed orientation determinant satisfies $\mathrm{orient}_2(a,b,b)=0$.
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 (threshold $\le n$ becomes $\le 2n$).
Point2 is the Euclidean plane $\mathbb{R}^2$. The orientation map is the signed twice-area determinant
$$\mathrm{orient}_2(a,b,c)=(b_0-a_0)(c_1-a_1)-(b_1-a_1)(c_0-a_0),$$
the standard 2D cross product of edge vectors from $a$. It vanishes precisely on collinear triples (with sign encoding left/right).
This lemma is the degenerate case $c=b$: the third point sits on the second endpoint, so the parallelogram has zero area.
proof idea
One-line algebraic identity. Unfold the definition of the orientation determinant; substitute $c=b$ to obtain
$(b_0-a_0)(b_1-a_1)-(b_1-a_1)(b_0-a_0)$.
The ring tactic cancels the two identical products and yields $0$. No geometric lemmas are required.
why it matters
Supports collinearity bookkeeping inside the distance-shell multiplicity development (Erdős #132 physicalization). The immediately following comment records the intended use: any point on a closed segment is collinear with its endpoints in the orientation determinant. That fact underpins diameter-shell uniqueness and sparse-shell arguments among the module siblings (isDiameterShell_unique, dist_le_of_diameter_shell, SparseShellsDiverge).
No downstream consumers are wired yet (used_by empty), so the lemma is local scaffolding for planar incidence identities rather than a forcing-chain landmark (T0–T8). It is pure Euclidean geometry in service of recognition-energy shell occupancy.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.