faceNormal_edge4_right_self_gram
plain-language theorem explainer
Squared Euclidean norm of the face normal on vertices (1,3,2) of a realized tetrahedron equals an explicit quadratic polynomial in the 3×3 Gram matrix of edges from vertex 0. Used when matching geometric face areas to Cayley–Menger 3×3 cofactors in the Berger formula path. Proof expands the cross-product self-dot identity after rebasing both edges to the Gram basis, then closes by ring.
Claim. For a realized tetrahedron $T$, if $N$ is the coordinate face normal through vertices $1,3,2$ (cross product of the two edges from vertex $1$), then $\|N\|^2$ equals $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}$, where $g_{ij}$ are the Gram-matrix entries of the three edge vectors based at vertex $0$.
background
This module builds the Euclidean side of the tetrahedral dihedral cosine: face normals as cross products of coordinate edge vectors in $\mathbb{R}^3$, and 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. The Gram matrix gram3 records inner products of the three edge vectors from vertex $0$. Coordinate edge vectors are the $\mathbb{R}^3$ components of those edges; any edge $a\to b$ rebases as the difference of base edges $0\to b$ and $0\to a$. The face normal through $(a,b,c)$ is the cross product of the two edges from $a$.
Upstream, the squared-norm identity reduces $|N|^2$ to a combination of three edge-vector dots (Lagrange identity for the cross product). Dot products of coordinate edges agree with the real inner product of the corresponding Euclidean edges, so everything lands in Gram entries.
proof idea
One short algebraic expansion. First apply the general squared-norm identity for a face normal, replacing $|N|^2$ by the three pairwise dots of the two generating edges. Rebase both edges of face $(1,3,2)$ to differences of base edges from vertex $0$. Unfold coordinate dots into real inner products and those into Gram entries via the basis-edge and edge-vector definitions. Rewrite self-inner-products as squared norms, expand all bilinear differences with the usual inner-product rules and commutativity, then finish with ring_nf on the resulting quadratic polynomial in the six Gram entries.
why it matters
This identity is the geometric half of the bridge from face area to Cayley–Menger data. The sole direct consumer is cmCofactor3_edge4_left_diag_eq_neg_four_normalSq, which rewrites the $(1,1)$ entry of the $3\times 3$ Cayley–Menger cofactor as $-4$ times this same normal squared norm. That step is required for the module's remaining goal: Berger's cofactor formula identifying the geometric dihedral cosine (normalized product of adjacent face normals) with the cofactor ratio already defined on the Cayley–Menger side.
In the broader Recognition geometry stack, tetrahedral dihedrals and their cofactor expressions feed discrete curvature and packing arguments on the Freudenthal strip and related 3D lattices. The result is pure Euclidean 3-geometry; it does not itself invoke the forcing chain (T5–T8) or the Recognition Composition Law, but it supplies a concrete algebraic identity those later geometric layers rely on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.