faceNormal_edge2_right_self_gram
plain-language theorem explainer
For a realized tetrahedron, the squared Euclidean norm of the face normal on vertices (0,3,2) equals the 2×2 Gram determinant of the two basis edges from vertex 0 that span that face. Anyone matching geometric dihedral data to Cayley–Menger cofactors cites this identity. The proof rewrites via the general normal self-dot formula, then unfolds coordinate dots into the Gram matrix.
Claim. Let $T$ be a realized tetrahedron in $\mathbb{R}^3$. Write $n$ for the coordinate face normal of the face through vertices $(0,3,2)$, obtained as the cross product of the edge vectors $0\to 3$ and $0\to 2$. Let $G$ be the $3\times 3$ Gram matrix of the three edges based at vertex $0$. Then $\|n\|^2 = G_{22}G_{11} - G_{21}G_{12}$.
background
This module builds the Euclidean side of the tetrahedral dihedral cosine: face normals from cross products, and the normalized inner product of 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. Edge vectors are differences of those points; the three edges from vertex 0 form a basis whose Gram matrix $G$ records all pairwise inner products. The face normal through vertices $(a,b,c)$ is the coordinate cross product of the two edges from $a$ to $b$ and $a$ to $c$.
Upstream, faceNormal_dot_self reduces any normal's squared norm to the Gram determinant of its two generating edge vectors in coordinate form. Coordinate dots agree with the real Euclidean inner product of the corresponding edge vectors, so those entries are exactly the Gram matrix entries once the basis labeling is unfolded.
proof idea
One short rewrite-and-simp chain. First apply the general identity that the squared norm of faceNormal T a b c equals the 2×2 Gram determinant of the two coordinate edge vectors from $a$. Specialize to $(a,b,c)=(0,3,2)$. Then simplify: replace each coordinate dot by the Euclidean inner product of the matching edge vectors, and unfold the Gram matrix and basis-edge definitions so the two edges $0\to 3$ and $0\to 2$ become basis indices 2 and 1. The right-hand side is then exactly $G_{22}G_{11}-G_{21}G_{12}$.
why it matters
This is a concrete bridge step inside the Berger cofactor program. Downstream, cmCofactor3_edge2_left_diag_eq_neg_four_normalSq rewrites a Cayley–Menger 3-cofactor diagonal entry as $-4$ times this same normal squared norm, using the present identity after expressing squared edges from the Gram matrix. That identification is required to match the geometric dihedral cosine (normalized adjacent-normal inner product) with the cofactor ratio living in DihedralCayleyMenger.
In the broader Recognition geometry stack, tetrahedral dihedral data feed discrete curvature and packing arguments on the Freudenthal strip and related lattices. Closing the geometric-to-cofactor dictionary keeps those angles computable from edge lengths alone, without choosing coordinates at use sites.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.