faceNormal_edge3_right_self_gram
plain-language theorem explainer
Squared Euclidean norm of the face normal on vertices 1,2,3 of a realized tetrahedron equals an explicit quadratic polynomial in the Gram entries of the three edge vectors from vertex 0. Anyone matching geometric dihedral data to Cayley–Menger cofactors cites this identity. Proof rewrites via the cross-product self-dot formula, rebases edges at the origin vertex, expands inner products, and closes by ring.
Claim. For a realized tetrahedron $T$, writing $g_{ij}$ for the Gram matrix of the three edge vectors from vertex $0$, the squared norm of the face normal on vertices $1,2,3$ equals $$\|n_{123}\|^2 = g_{00}g_{11}+g_{00}g_{22}-2g_{00}g_{12}+g_{11}g_{22}-2g_{11}g_{02}-2g_{22}g_{01}-g_{01}^{2}+2g_{01}g_{02}+2g_{01}g_{12}-g_{02}^{2}+2g_{02}g_{12}-g_{12}^{2}.$$
background
The module builds the Euclidean side of the tetrahedral dihedral cosine: face normals as cross products of coordinate edge vectors, then the normalized inner product of two adjacent face normals. The target is Berger's cofactor formula, equating that geometric cosine to a Cayley–Menger cofactor ratio.
A realized tetrahedron supplies four points in Euclidean 3-space. Coordinate edge vectors are the $\mathbb{R}^3$ differences of those points; the face normal on vertices $(a,b,c)$ is their cross product $e_{ab}\times e_{ac}$. The Gram matrix $g_{ij}$ records inner products of the three edges from vertex $0$. Upstream, the self-dot identity reduces $|n|^2$ to edge dots, and the rebase lemma writes every edge as a difference of base edges from vertex $0$. Coordinate dots agree with the real inner product of the corresponding Euclidean edge vectors.
proof idea
Start from the self-dot identity for face normals, which replaces $|n_{123}|^2$ by the $2\times 2$ Gram determinant of the two edge vectors from vertex $1$ to $2$ and from $1$ to $3$. Rebase both edges at vertex $0$ via the difference formula. Unfold coordinate dots into real inner products of Euclidean edge vectors, then into Gram entries of the three base edges. Expand the resulting differences of inner products with bilinearity and symmetry, and finish by ring normalization of the quadratic polynomial in the six Gram entries.
why it matters
This identity is the algebraic bridge from geometric face-normal squared length to Gram data. The sole downstream consumer equates the Cayley–Menger $3\times 3$ cofactor on the opposite edge to $-4$ times this normal squared length, after substituting the Gram form of squared edge lengths. That step is required for Berger's cofactor formula, which identifies the geometric dihedral cosine (normalized face-normal inner product) with the Cayley–Menger cofactor ratio. In the Recognition geometry stack this closes the Euclidean half of the dihedral comparison used for tetrahedral angle constraints; it does not itself invoke the forcing chain (T0–T8) or the Recognition Composition Law, but supplies the metric identity those later comparisons rely on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.