faceNormal_dot_self
plain-language theorem explainer
Squared Euclidean norm of a tetrahedron face normal equals the 2×2 Gram determinant of the two edge vectors that span the face. Anyone reducing geometric dihedral cosines to edge Gram data cites this identity. The proof is a one-line specialization of the general cross-dot-cross formula to identical faces.
Claim. Let $T$ be a realized tetrahedron in $\mathbb{R}^3$ and let $a,b,c\in\{0,1,2,3\}$. Write $e_{ab},e_{ac}$ for the coordinate edge vectors from vertex $a$, and $N_{abc}:=e_{ab}\times e_{ac}$ for the face normal. Then $\|N_{abc}\|^2=\|e_{ab}\|^2\|e_{ac}\|^2-(e_{ab}\cdot e_{ac})(e_{ac}\cdot e_{ab})$.
background
This module builds the Euclidean side of the tetrahedral dihedral cosine: face normals via cross products, then the normalized inner product of the two normals adjacent to a shared edge. The target is the Berger cofactor formula, equating that geometric cosine with a Cayley–Menger cofactor ratio from DihedralCayleyMenger.
A realized tetrahedron supplies four points in $\mathbb{R}^3$. The coordinate edge vector from $a$ to $b$ is the ordinary difference of those points. The face normal through $(a,b,c)$ is the cross product of the two edges leaving $a$. Dot products of such normals are controlled by the classical cross-dot-cross (Lagrange) identity, already packaged as the general two-face lemma in this file.
The squared-norm case is the diagonal specialization needed before one can write the geometric cosine denominator $|N||N'|$ in pure edge Gram entries.
proof idea
One-line wrapper. Instantiate the general two-face identity faceNormal_dot_faceNormal at identical index triples $(a,b,c)=(d,e,f)$, then simpa to match the expanded Gram form. No new algebraic work: the cross-dot-cross expansion already yields $|u\times v|^2=|u|^2|v|^2-(u\cdot v)^2$ when the two faces coincide.
why it matters
This is the self-dot stepping stone for every edge-local Gram rewrite in the module. Downstream, the six pairs faceNormal_edge*_left/right_self_gram each open with rw [faceNormal_dot_self] and then convert edge dots into gram3 entries. Those squares feed the geometric dihedral denominator and, with the numerator cross identity, the full geometric cosine.
The parent goal is the Berger cofactor formula: identify the geometric cosine (normals from cross products) with the Cayley–Menger cofactor ratio. That identification is the Euclidean half of the dihedral pipeline used in discrete gravity and Regge-type hinge analysis. Spatially it sits inside the $D=3$ geometry forced by the Recognition chain (T8); the cross product itself is a 3D structure.
No open scaffold here: the claim is fully proved and only packages a classical vector identity for the tetrahedron API.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.