faceNormal_edge5_left_self_gram
plain-language theorem explainer
For a realized tetrahedron, the squared Euclidean norm of the face normal on vertices (2,3,0) equals the 2×2 Gram determinant of the two edge vectors from the opposite base. Anyone proving the Berger cofactor identification of dihedral cosines with Cayley–Menger minors cites this identity. The proof is a short algebraic reduction: expand the cross-product self-dot, rebase edges at vertex 0, and match Gram entries.
Claim. Let $T$ be a realized tetrahedron in $\mathbb{R}^3$. Write $N$ for the coordinate face normal of the face through vertices $(2,3,0)$, obtained as the cross product of the two edge vectors from vertex $2$. Then $\|N\|^2$ equals the Gram determinant $G_{11}G_{22}-G_{12}G_{21}$ of the two basis edge vectors that span the complementary face pair (entries of the $3\times 3$ edge Gram matrix of $T$).
background
This module builds the Euclidean side of the tetrahedral dihedral cosine: face normals as cross products of coordinate edge vectors, and the normalized inner product of adjacent face normals. The target is Berger's cofactor formula, equating that geometric cosine with a Cayley–Menger cofactor ratio.
A realized tetrahedron supplies four points and their edge vectors. The coordinate edge vector between vertices $a$ and $b$ is the $\mathbb{R}^3$ difference of embedded positions; it may be rebased at vertex $0$ by subtraction. The face normal through $(a,b,c)$ is the cross product of the two edges from $a$. Its squared norm expands by the Lagrange identity to a $2\times 2$ Gram determinant of those edges.
Upstream, faceNormal_dot_self already reduces $|N|^2$ to edge-vector dots, and coordEdgeVector_dot_eq_inner identifies coordinate dots with the real inner product of Euclidean edge vectors. The Gram matrix gram3 packages those inner products for the three basis edges from a fixed origin.
proof idea
Start from faceNormal_dot_self on indices $(2,3,0)$, which writes the self-dot as a difference of products of coordinate edge dots. Rebase both edges via coordEdgeVector_eq_base_sub so they become differences of edges from vertex $0$. Unfold the coordinate dots to real inner products (coordEdgeVector_dot_eq_inner), then to Gram and basis-edge definitions. Replace self-inner products by squared norms, expand the bilinear form on differences (inner_sub_left/inner_sub_right and commutativity), and finish by ring_nf, which matches the target Gram determinant $G_{11}G_{22}-G_{12}G_{21}$.
why it matters
This identity is the geometric half of the edge-5 cofactor comparison. Downstream, cmCofactor3_edge5_right_diag_eq_neg_four_normalSq rewrites the Cayley–Menger $3\times 3$ cofactor on the squared-edge matrix as $-4$ times this same normal squared, citing the present theorem after equating squared edges to Gram data. That step is required for the module's remaining goal: Berger's formula identifying the geometric dihedral cosine (normalized face-normal inner product) with the Cayley–Menger cofactor ratio in DihedralCayleyMenger.
In the broader Recognition geometry stack, tetrahedral dihedral angles control local packing and curvature bookkeeping on the discrete side of the forcing chain (spatial dimension $D=3$ and the eight-tick octave live one layer up). Closing the cofactor match removes a scaffolding gap between pure Euclidean normals and the combinatorial distance matrix.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.