faceNormal_edge5_right_self_gram
plain-language theorem explainer
For a realized tetrahedron, the squared Euclidean norm of the face normal on vertices (2,3,1) expands to an explicit quadratic polynomial in the 3×3 Gram matrix of edge vectors from the base vertex. Downstream cofactor identities cite this to match Cayley–Menger minors with geometric normal squares. The proof rewrites the cross-product self-dot identity, rebases edges at vertex 0, and finishes by ring normalization of inner products.
Claim. For every realized tetrahedron $T$, writing $n$ for the coordinate face normal of the face through vertices $2,3,1$ and $G$ for the $3\times 3$ Gram matrix of the three edge vectors from vertex $0$, one has $\|n\|^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
This 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 adjacent normals. The target is Berger's cofactor formula, equating that geometric cosine to a Cayley–Menger cofactor ratio.
A face normal through vertices $(a,b,c)$ is the $\mathbb{R}^3$ cross product of the two coordinate edge vectors from $a$. Its squared norm reduces, by the cross-dot-cross identity, to a combination of edge-vector dots. Coordinate dots agree with the real inner product of the corresponding Euclidean edge vectors, and any edge can be rebased at vertex $0$ as a difference of base edges.
The $3\times 3$ Gram matrix $G$ records those base-edge inner products. The present identity specializes the self-dot formula to the face $(2,3,1)$ and expands fully in the entries of $G$.
proof idea
Start from the general self-dot identity for face normals, which replaces $|n|^2$ by a difference of products of coordinate edge dots. Rebase the two edges of face $(2,3,1)$ at vertex $0$ via the base-subtraction lemma. Unfold the coordinate-to-inner bridge and the definitions of the Gram matrix and edge vectors, then expand all differences of dots with the bilinearity rules for the real inner product. A final ring normalization matches the expanded Gram polynomial on the right-hand side.
why it matters
The immediate parent is the identity equating the $(1,1)$ Cayley–Menger $3\times 3$ cofactor of the squared-edge matrix to $-4$ times this same normal square. That step is the geometric half of the Berger cofactor bridge: once every relevant cofactor is tied to a normal square (or a normal–normal product), the geometric dihedral cosine becomes a pure cofactor ratio, matching the Cayley–Menger side developed in the companion module.
In the broader Recognition geometry stack this closes a Euclidean bookkeeping gap needed before dihedral angles of realized tetrahedra can be read off Gram or Cayley–Menger data without coordinate choices. It does not itself force dimension or the eight-tick structure; it is local solid-geometry algebra feeding the cofactor formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.