orient2_plucker
plain-language theorem explainer
Among four points in the Euclidean plane, the signed twice-areas of the four triangles on triples obey one linear Plücker relation. Planar combinatorial geometers and anyone tracking orientation signs inside distance-shell arguments would cite it. The proof unfolds the 2×2 determinant definition and finishes by polynomial cancellation over ℝ.
Claim. For any four points $a,b,c,d\in\mathbb{R}^2$, the signed twice-areas satisfy $\operatorname{orient}(a,b,c)+\operatorname{orient}(a,c,d)=\operatorname{orient}(a,b,d)+\operatorname{orient}(b,c,d)$, where $\operatorname{orient}(p,q,r)=(q_0-p_0)(r_1-p_1)-(q_1-p_1)(r_0-p_0)$.
background
The ambient module physicalizes Erdős problem #132 inside Recognition Science: classical pairwise distance values become two-body recognition-energy shells, and shell occupancy is multiplicity (ordered pairs double the usual unordered count, so classical thresholds scale by two).
Points live in the visible plane: Point2 is the Euclidean space $\mathbb{R}^2$. The local orientation form is the signed twice-area determinant
$\operatorname{orient2}(a,b,c)=(b_0-a_0)(c_1-a_1)-(b_1-a_1)(c_0-a_0)$.
It is alternating in the first two arguments and vanishes on collinear triples. The four-point identity is the elementary Plücker (or Grassmann–Plücker) linear dependence among those areas.
proof idea
Pure algebraic identity. Unfold the definition of the orientation determinant on each of the four triples, expand the bilinear expressions in coordinates, and invoke the polynomial ring tactic over $\mathbb{R}$. All cross terms cancel, leaving equality with no geometric case split.
why it matters
Supplies the basic four-point orientation calculus used when comparing triangles inside planar point sets that carry distance shells. In the module’s RS reading of Erdős #132, shell occupancy and diameter-shell uniqueness sit on top of ordinary Euclidean geometry; this identity is the linear dependence that lets one rewrite one triangle area in terms of three others (the companion form solves for $\operatorname{orient2}(b,c,d)$).
No downstream consumers are wired yet in the graph, so the lemma is infrastructure rather than a forcing-chain step. It does not touch T5–T8, the RCL, or the mass ladder; it only stabilizes planar signed-area bookkeeping for later multiplicity and sparse-shell arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.