orient2_bcd_decomposition
plain-language theorem explainer
For any four points in the plane, the signed orientation of triangle bcd equals orient(a,b,c) minus orient(a,b,d) plus orient(a,c,d). Plane-geometry and combinatorial-distance arguments cite this solved Plücker form when reducing four-point configurations to a fixed basepoint. The proof unfolds the 2x2 determinant and closes by ring normalization.
Claim. For any four points $a,b,c,d$ in the Euclidean plane $\mathbb{R}^2$, the signed twice-area orientation satisfies $\mathrm{orient}(b,c,d)=\mathrm{orient}(a,b,c)-\mathrm{orient}(a,b,d)+\mathrm{orient}(a,c,d)$.
background
The module records the Recognition Science physicalization of Erdős problem #132: a classical distance value is a shell in the pairwise Euclidean spectrum; physically it is a two-body recognition-energy shell whose occupancy is the shell multiplicity. Ordered pairs are used for Lean simplicity, so positive-distance ordered multiplicity is twice the unordered count.
Points are elements of the Euclidean plane $\mathbb{R}^2$. The orientation form is the signed twice-area of a triangle: $\mathrm{orient}(a,b,c)=(b_x-a_x)(c_y-a_y)-(b_y-a_y)(c_x-a_x)$. It vanishes on collinear triples and flips sign under odd vertex permutations.
The identity is the classical Plücker relation among the four triangle orientations of a planar quadruple, rearranged so the orientation of $bcd$ is expressed relative to an auxiliary basepoint $a$.
proof idea
Unfold the determinant definition of orientation on every term. Both sides become explicit polynomials in the eight real coordinates of $a,b,c,d$. The ring tactic normalizes them to a common expanded form, establishing equality. No intermediate geometric lemmas are invoked; the argument is pure coordinate algebra.
why it matters
Four-point orientation bookkeeping is local infrastructure for the planar geometry layer of the Erdős #132 physicalization: signed areas control when three pairwise distances determine an embedding up to reflection and when shell multiplicities can change. The declaration is the solved form of the Plücker identity (the zero-sum alternating form appears as the next sibling comment). The dependency graph currently lists no downstream consumers; it sits beside diameter-shell uniqueness and sparse-shell divergence results in the same module. It does not touch the forcing chain T0–T8, the Recognition Composition Law, or the mass ladder, but supports the distance-shell multiplicity story that those physical claims rest on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.