faceNormal_edge1_left_self_gram
plain-language theorem explainer
For a realized tetrahedron, the squared Euclidean norm of the face normal on vertices (0,2,1) equals the 2×2 Gram determinant of the two spanning edges from vertex 0. Anyone matching geometric dihedral data to Cayley-Menger cofactors cites this bridge. The proof rewrites the general normal-self-dot identity, then simplifies through Gram and edge-vector definitions.
Claim. For any realized tetrahedron $T$, let $n$ be the coordinate face normal of the face through vertices $0,2,1$ (the cross product of the edge vectors from $0$ to $2$ and from $0$ to $1$). Then $\|n\|^2 = G_{11}G_{00}-G_{10}G_{01}$, where $G$ is the Gram matrix of the three basis edge vectors based at vertex $0$.
background
This module builds the Euclidean geometric side of the tetrahedral dihedral cosine: face normals from cross products, and the normalized inner product of two adjacent face normals. The remaining target is Berger's cofactor formula, identifying that geometric cosine with a Cayley-Menger cofactor ratio.
A realized tetrahedron is four points in Euclidean 3-space. Edge vectors are point differences. The three basis edge vectors from vertex 0 (to vertices 1, 2, 3) determine the Gram matrix $G$ with $G_{ij}=\langle e_i,e_j\rangle$. The face normal through vertices $(a,b,c)$ is the coordinate cross product of the two edge vectors from $a$ along that face.
Upstream, the squared norm of any face normal expands by the cross-dot-cross identity into edge-vector dots. Coordinate dots agree with the real inner product of the corresponding Euclidean edge vectors.
proof idea
Short tactic proof. Rewrite by the general identity that the squared face-normal norm equals $|u|^2|v|^2-\langle u,v\rangle^2$ for the two spanning coordinate edge vectors. Then simplify: replace coordinate dots by Euclidean inner products, unfold the Gram matrix and the basis/edge-vector definitions, and match indices for face $(0,2,1)$, spanned by edges $0\to 2$ and $0\to 1$ (basis slots 1 and 0).
why it matters
This specialization feeds the cofactor identification on the geometric side. Downstream it is used to prove that a particular Cayley-Menger 3-cofactor (the edge-1 right diagonal entry) equals $-4$ times this squared face-normal norm. That equality is a step toward Berger's formula: matching the geometric dihedral cosine to the Cayley-Menger cofactor ratio, the remaining theorem of the module.
In the Recognition geometry stack, tetrahedral dihedral data and Cayley-Menger determinants support discrete curvature and packing arguments tied to forced spatial dimension $D=3$ (forcing chain T8). Closing the geometric-cofactor bridge keeps discrete tetrahedron geometry aligned with continuum side formulas without extra hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.