faceNormal_edge0_left_self_gram
plain-language theorem explainer
For a realized tetrahedron, the squared Euclidean length of the face normal on vertices 0,1,2 equals the 2×2 Gram determinant of the two edge vectors leaving vertex 0. Anyone matching geometric dihedral cosines to Cayley–Menger cofactors cites this identity. The proof rewrites via the cross-product self-dot formula and unfolds Gram entries to ordinary edge inner products.
Claim. Let $T$ be a realized tetrahedron in Euclidean space. Write $n$ for the coordinate face normal of the face through vertices $0,1,2$ (the cross product of the two edge vectors from $0$). Then $\|n\|^2$ equals the Gram determinant $G_{00}G_{11}-G_{01}G_{10}$ of those two edge vectors, where $G$ is the $3\times 3$ edge Gram matrix of $T$.
background
This module builds the Euclidean side of the tetrahedral dihedral cosine: face normals from cross products, then the normalized inner product of the two normals adjacent to a shared edge. The target is Berger’s cofactor formula, equating that geometric cosine with a Cayley–Menger cofactor ratio.
A realized tetrahedron supplies four points in $\mathbb{R}^3$. Edge vectors are differences of those points; coordEdgeVector is the same vector as a coordinate triple in $\mathbb{R}^3$. The face normal through $(a,b,c)$ is the cross product of the two edges leaving $a$. The Gram matrix gram3 records inner products of a chosen triple of basis edge vectors.
Upstream, coordEdgeVector_dot_eq_inner identifies coordinate dots with the real inner product of Euclidean edge vectors, and faceNormal_dot_self expands $|u\times v|^2$ into the usual Gram expression in $u$ and $v$.
proof idea
One short tactic proof. First rewrite the left-hand side by faceNormal_dot_self, which replaces the squared normal by the cross-product identity $|u\times v|^2=|u|^2|v|^2-(u\cdot v)^2$ in coordinate form. Then simp with coordEdgeVector_dot_eq_inner, the definition of gram3, and the unfoldings of basisEdgeVector and edgeVector matches each coordinate dot to the corresponding Gram entry, yielding $G_{00}G_{11}-G_{01}G_{10}$.
why it matters
This is the first of the edge-0 normal-square identities that feed the Berger cofactor comparison. Downstream, cmCofactor3_edge0_right_diag_eq_neg_four_normalSq rewrites a diagonal Cayley–Menger $3\times 3$ cofactor as $-4$ times this same normal square, after transporting squared edge lengths through the Gram presentation of the Cayley–Menger matrix.
Together these steps close the geometric half of the module’s program: express dihedral data purely in Gram/Cayley–Menger algebra so the cofactor ratio can be identified with the normalized face-normal inner product. In the broader Recognition geometry stack this is bookkeeping for rigid tetrahedral angles, not a forcing-chain landmark, but it is required scaffolding for any later claim that dihedral cosines are forced by discrete edge data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.