faceNormal_dot_faceNormal
plain-language theorem explainer
For a realized tetrahedron in R^3, the Euclidean dot product of two face normals equals the 2x2 Gram determinant of the four edge vectors that generate those normals. Anyone computing tetrahedral dihedral cosines from edge data cites this identity. The proof is a two-step rewrite: unfold the cross-product definition of the normals, then apply the classical cross-dot-cross formula.
Claim. Let $T$ be a realized tetrahedron in $\mathbb{R}^3$ with vertices indexed by $\mathrm{Fin}\,4$. For indices $a,b,c,d,e,f$, write $n_{abc}$ for the face normal obtained as the cross product of the edge vectors from $a$ to $b$ and from $a$ to $c$, and likewise $n_{def}$. Then $n_{abc}\cdot n_{def}=(u_{ab}\cdot u_{de})(u_{ac}\cdot u_{df})-(u_{ab}\cdot u_{df})(u_{ac}\cdot u_{de})$, where $u_{xy}$ denotes the coordinate edge vector from vertex $x$ to vertex $y$.
background
This module builds the Euclidean side of the tetrahedral dihedral cosine: face normals from cross products, then the normalized inner product of two adjacent face normals. The target is the Berger cofactor formula, which will match that geometric cosine to the Cayley-Menger cofactor ratio from DihedralCayleyMenger.
A realized tetrahedron supplies four points in $\mathbb{R}^3$. The coordinate edge vector from vertex $a$ to $b$ is the ordinary difference of their position vectors. A face normal is the cross product of two edge vectors sharing the face apex, so it is orthogonal to the face plane and its magnitude tracks the parallelogram area.
The classical vector identity $(u\times v)\cdot(w\times z)=(u\cdot w)(v\cdot z)-(u\cdot z)(v\cdot w)$ converts any normal-normal inner product into a combination of edge-edge dots only. That is exactly the reduction needed before comparing with Cayley-Menger minors.
proof idea
One short tactic proof. Unfold the definition of face normal (each side becomes a cross product of two coordinate edge vectors). Rewrite by Mathlib's cross_dot_cross, which is the standard identity $(u\times v)\cdot(w\times z)=(u\cdot w)(v\cdot z)-(u\cdot z)(v\cdot w)$. The right-hand side is then precisely the stated Gram-style combination of four edge-vector dots. No case splits or tetrahedron-specific geometry beyond the definitions.
why it matters
This is the algebraic engine under the geometric dihedral cosine. Downstream, faceNormal_dot_self specializes to the squared norm of a single normal (the Gram determinant of two edges of one face), and geometricDihedralNumerator_cross expands the numerator of the geometric cosine for an edge of the tetrahedron via the same identity.
Together those feed the module's remaining goal: identify the geometric cosine (normalized normal-normal product) with the Cayley-Menger cofactor ratio (Berger's formula). In the broader Recognition geometry stack this is pure Euclidean bookkeeping on realized tets; it does not itself invoke the forcing chain, but it supplies the classical side that any RS dihedral or volume identity must match.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.