lagrange_identity_2d
plain-language theorem explainer
Lagrange's identity in the plane: for any three points a, b, c in R², the squared inner product of (c−a) with (b−a) plus the squared planar cross product equals the product of the two squared Euclidean lengths. Combinatorial geometers handling Hopf–Pannwitz diameter configurations cite it to turn orientation and projection data into distance equalities. The proof is a one-line ring expansion of the six coordinate polynomials.
Claim. For any three points $a,b,c\in\mathbb{R}^2$, writing $u=c-a$ and $v=b-a$, one has $(u\cdot v)^2+(u_x v_y-u_y v_x)^2=|u|^2|v|^2$. Equivalently in coordinates: $((c_0-a_0)(b_0-a_0)+(c_1-a_1)(b_1-a_1))^2+((b_0-a_0)(c_1-a_1)-(b_1-a_1)(c_0-a_0))^2=((c_0-a_0)^2+(c_1-a_1)^2)\cdot((b_0-a_0)^2+(b_1-a_1)^2)$.
background
The module physicalizes Erdős problem #132 inside Recognition Science: 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 classical multiplicity $\le n$ becomes ordered multiplicity $\le 2n$.
Points live in Point2, an abbreviation for the Euclidean plane $\mathbb{R}^2=\mathrm{EuclideanSpace},\mathbb{R},(\mathrm{Fin},2)$. Vectors are formed by coordinate differences $c-a$ and $b-a$. The planar cross product is the scalar $u_x v_y-u_y v_x$ (the signed area of the parallelogram), and the identity is the classical Lagrange relation $(u\cdot v)^2+(u\times v)^2=|u|^2|v|^2$.
Downstream diameter arguments place a diameter segment along a basis direction and read off lens coordinates $(\alpha,\beta)$ with $\alpha\Delta=\langle c-a,b-a\rangle$ and $\beta\Delta=\mathrm{orient}_2(a,b,c)$; this identity converts those coordinates back into squared distances.
proof idea
Term-mode proof consisting of a single ring invocation. Both sides are polynomial expressions in the six real coordinates of $a,b,c$; expanding the left-hand squares and the right-hand product yields identical monomials, so the equality is pure commutative-ring arithmetic with no geometric lemmas required.
why it matters
Local algebraic engine for the diameter-contradiction half of the Erdős #132 physicalization. It is applied inside properSeparatedDiameterContradiction (two diameter segments with all cross-distances $\le\Delta$ cannot place both endpoints of the second segment strictly on the same side of the first) and the sharper sameSideDiameterContradiction (same-side orientation product alone already contradicts the diameter bounds).
Those theorems quote the identity explicitly: after rotating so $(b-a)/|b-a|$ is the first basis vector, Lagrange supplies $\alpha_c^2+\beta_c^2=(\mathrm{dist},a,c)^2$ and the analogous formulae for the other three distances, which feed the strict lens-coordinate comparison. Within the broader RS chain this keeps the planar distance-shell analysis on a fully proved algebraic footing before the sparse-shell divergence and flux-bridge results.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.