faceNormal_edge4_left_self_gram
plain-language theorem explainer
For a realized tetrahedron, the squared Euclidean norm of the face normal on vertices (1,3,0) equals the 2×2 Gram determinant built from the rebased edge Gram entries at indices 0 and 2. Geometry proofs that match face-normal magnitudes to Cayley–Menger cofactors cite this identity. The argument rewrites via the cross-product self-dot formula, rebases edges at vertex 0, then simplifies to a ring identity on inner products.
Claim. Let $T$ be a realized tetrahedron in Euclidean space. Write $N$ for the coordinate face normal of the face through vertices $(1,3,0)$, obtained as the cross product of the two edge vectors from vertex $1$. Then $\|N\|^2$ equals the Gram determinant $G_{00}G_{22}-G_{02}G_{20}$, where $G$ is the $3\times 3$ edge Gram matrix of $T$ in the vertex-$0$ basis.
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 normals. The target is Berger's cofactor formula, equating that geometric cosine to a Cayley–Menger cofactor ratio.
A faceNormal for vertices $(a,b,c)$ is the $\mathbb{R}^3$ cross product of the two coordinate edge vectors from $a$. Its squared self-dot expands by the cross-dot-cross identity to a $2\times 2$ Gram determinant in those edges (faceNormal_dot_self). Coordinate edge dots agree with the real inner product of the corresponding Euclidean edge vectors (coordEdgeVector_dot_eq_inner), and any edge can be rebased at vertex $0$ as a difference of base edges (coordEdgeVector_eq_base_sub).
The Gram entries gram3 are the inner products of the three basis edge vectors from the distinguished vertex in the tetrahedron realization. The present lemma specializes the general self-dot identity to the left face of the edge-$4$ dihedral pair and rewrites it purely in those Gram entries.
proof idea
Term-mode rewrite chain. First apply faceNormal_dot_self to expand $|N|^2$ into the $2\times 2$ determinant of coordinate edge dots on edges $(1,3)$ and $(1,0)$. Rebase both edges at vertex $0$ via coordEdgeVector_eq_base_sub. Unfold the resulting dots through coordEdgeVector_dot_eq_inner, gram3, basisEdgeVector, and edgeVector, converting everything to real inner products of edge vectors. Replace self-inner products by squared norms, expand the bilinear form with inner_sub_left/inner_sub_right and commutativity, then finish by ring_nf.
why it matters
This is a concrete bridge step inside the Berger cofactor program: it turns one face-normal squared length into a pure Gram determinant that Cayley–Menger minors can match. Downstream, cmCofactor3_edge4_right_diag_eq_neg_four_normalSq cites it to prove that the $(3,3)$ Cayley–Menger $3\times 3$ cofactor equals $-4$ times this same normal squared norm, after transporting squared edges through the Gram realization.
In the Recognition geometry stack, dihedral cosines of realized tetrahedra feed discrete curvature and packing arguments on the eight-tick / $D=3$ side of the forcing chain. Closing the geometric-versus-cofactor identification is the remaining theorem of the module; this lemma discharges the left-face Gram reduction that the cofactor comparison needs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.