geometricDihedralDenomSq
plain-language theorem explainer
Squared product of the two adjacent face-normal lengths at a tetrahedron edge: the denominator of the geometric dihedral cosine. Anyone matching Euclidean dihedral data to Cayley–Menger cofactors cites it. The body is a short let-binding: build the two face normals from the shared edge and opposite vertices, then multiply their self-dot products.
Claim. For a realized tetrahedron $T$ and edge index $e\in\{0,\ldots,5\}$, let $n_1,n_2$ be the face normals of the two faces incident to $e$ (each normal the cross product of two edge vectors from a common vertex). The geometric dihedral denominator square is $\|n_1\|^2\,\|n_2\|^2$.
background
This module builds the Euclidean side of the tetrahedral dihedral cosine: face normals from cross products, then the normalized inner product of the two normals adjacent to a chosen edge. The target is Berger's cofactor formula, equating that geometric cosine with a Cayley–Menger cofactor ratio from DihedralCayleyMenger.
A realized tetrahedron supplies four embedded vertices in $\mathbb{R}^3$. Each edge $e$ determines two incident triangular faces; adjacentFaceOppositeVertices names the two vertices opposite the shared edge, and faceNormal forms the cross product of the two edge vectors from one endpoint of the shared edge to the third vertex of each face. The self-dot of a normal is the squared area scale of that face parallelogram.
The geometric dihedral cosine is then a signed ratio whose denominator is the product of those two normal lengths (equivalently, the square root of this definition). Sign convention is chosen to match the internal Regge dihedral angle.
proof idea
Pure definition, not a proof. Resolve the six-edge index to the two endpoints of the shared edge and the two opposite vertices of the adjacent faces; form each face normal via faceNormal; return the product of the two self-dot products $(n_1\cdot n_1)(n_2\cdot n_2)$. No lemmas are applied.
why it matters
This is the geometric half of the Berger identification. Downstream, each edge index gets a theorem that the product of the two relevant Cayley–Menger diagonal cofactors equals $16$ times this quantity (e.g. cmCofactor3_edge0_diag_product_eq_sixteen_denomSq), and a square-root form scaling the geometric denominator by $4$. Those equalities are the cofactor side of matching geometric and CM dihedral cosines.
It also feeds interior bounds: geometricDihedralCos_strict_interior_of_faceNormals_independent unfolds this definition to show that linear independence of the two normals forces the cosine strictly inside $(-1,1)$. In the broader RS geometry stack, controlled dihedral data on realized tets sit under the $D=3$ forcing (T8) and the eight-tick discrete skeleton; this def is the concrete Euclidean denominator those comparisons need.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.