faceNormal_edge2_left_self_gram
plain-language theorem explainer
Squared norm of the face normal on vertices (0,3,1) equals the 2×2 Gram determinant on the basis edges from 0 to 3 and 0 to 1. Anyone matching geometric face areas to Cayley–Menger cofactors cites this identity. The proof rewrites by the cross-product self-dot formula, then unfolds Gram entries via coordinate–inner agreement.
Claim. For a realized tetrahedron $T$, if $n$ is the coordinate face normal through vertices $0,3,1$ and $G$ is the Gram matrix of the three edges based at vertex $0$, then $\|n\|^2 = G_{22}G_{00}-G_{20}G_{02}$.
background
This module builds the Euclidean side of the tetrahedral dihedral cosine: face normals from cross products, 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 realized tetrahedron supplies four points in Euclidean 3-space. Edge vectors from vertex $0$ form a basis triple; their Gram matrix $G$ records all pairwise inner products. The face normal through $(a,b,c)$ is the coordinate cross product of the two edges from $a$ along those face edges. Its squared norm expands by the standard identity $|u\times v|^2=|u|^2|v|^2-(u\cdot v)^2$.
Upstream, faceNormal_dot_self already reduces any normal's squared length to edge-vector dots, and coordinate dots agree with the real inner product of the corresponding Euclidean edges.
proof idea
One rewrite plus simplification. First apply the general self-dot identity for face normals, which expands $|n|^2$ into the $2\times 2$ Gram determinant on the two generating edge vectors (here edges $0\to 3$ and $0\to 1$). Then unfold: coordinate dots become Euclidean inner products, those edges are identified with basis slots $2$ and $0$, and the resulting entries are exactly $G_{22}$, $G_{00}$, $G_{20}$, $G_{02}$.
why it matters
This is a concrete index specialization needed for the Berger cofactor bridge. Downstream, the cofactor identity equates the $(3,3)$ Cayley–Menger $3\times 3$ cofactor on squared edges to $-4$ times this same normal squared norm. That step converts pure Gram algebra into geometric face-area data, which is how the module intends to identify the geometric dihedral cosine with the Cayley–Menger cofactor ratio in DihedralCayleyMenger.
In the broader Recognition geometry stack, tetrahedral dihedrals feed discrete curvature and packing arguments on the eight-tick / $D=3$ side; the present lemma is local linear algebra, not a forcing-chain step, but it closes a necessary algebraic gap on the Euclidean side of that comparison.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.