lagrange_identity_polarized_2d
plain-language theorem explainer
Classical polarized Lagrange identity on four points in the Euclidean plane: the product of two inner products plus the product of two oriented areas equals the remaining inner product times the squared length of the base vector. Diameter-shell arguments in the Erdős #132 physicalization cite it to convert orientation and projection data into squared distances. The proof is a one-line ring expansion.
Claim. For any four points $a,b,c,d\in\mathbb{R}^2$, writing vectors from $a$, one has $\langle c-a,b-a\rangle\,\langle d-a,b-a\rangle + \det(b-a,c-a)\,\det(b-a,d-a) = \langle c-a,d-a\rangle\,\|b-a\|^2$.
background
The module Distance Shell Multiplicity records the Recognition Science physicalization of Erdős problem #132. Classically a distance value is a shell in the pairwise Euclidean spectrum; physically it is a two-body recognition-energy shell whose multiplicity is shell occupancy. Ordered pairs are used for Lean simplicity, so classical multiplicity $\le n$ becomes ordered multiplicity $\le 2n$.
Point2 is an abbreviation for the Euclidean plane EuclideanSpace ℝ (Fin 2). The polarized form expands the classical Lagrange identity $|u|^2|v|^2 - \langle u,v\rangle^2 = \det(u,v)^2$ into a bilinear (polarized) statement in the four displacement vectors $b-a$, $c-a$, $d-a$. The two scalar factors on the left are the inner product of each of $c-a$ and $d-a$ against the base $b-a$, and the two 2D determinants are the signed areas (orientations) of the triangles $abc$ and $abd$.
proof idea
Pure algebraic identity on the eight real coordinates of the four points. The tactic ring expands both sides as polynomials in those coordinates and cancels; no geometric lemmas are invoked. There is no case split on degeneracy or nonzero base length.
why it matters
Feeds the two diameter contradictions that drive the sparse-shell analysis: properSeparatedDiameterContradiction and the sharper sameSideDiameterContradiction. The former places diameter segments in lens coordinates $(\alpha,\beta)$ with $\beta\cdot\Delta=\mathrm{orient}_2(a,b,\cdot)$ and $\alpha\cdot\Delta=\langle\cdot-a,b-a\rangle$; Lagrange converts $\alpha^2+\beta^2$ into squared distances, so same-side orientation products force a distance exceeding the diameter. The latter notes that only the first orientation product is needed. Together they support the RS reading of Erdős #132 (distance shells as recognition-energy shells) inside the planar bipartite distance spectrum. No forcing-chain landmark (T5–T8) is touched directly; the lemma is pure Euclidean algebra serving the combinatorial geometry layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.