geometricDihedralCos
plain-language theorem explainer
The internal geometric dihedral cosine at a tetrahedral edge is the normalized inner product of the two adjacent face normals, with sign fixed to the internal Regge convention. Anyone identifying Euclidean dihedrals with Cayley-Menger cofactor ratios, or proving strict interior bounds under affine independence, cites this quantity. It is a one-line ratio of the face-normal dot product to the square root of the product of the two squared norms.
Claim. For a realized tetrahedron $T$ (four affinely independent points in Euclidean $3$-space) and edge index $e\in\{0,\ldots,5\}$, the geometric dihedral cosine is $\frac{n_1\cdot n_2}{\sqrt{\|n_1\|^2\|n_2\|^2}}$, where $n_1,n_2$ are the face normals to the two faces meeting at $e$, each formed as a cross product of edge vectors from the shared edge to the opposite vertex of that face. The sign matches the internal Regge dihedral convention.
background
This module builds the Euclidean geometric side of the tetrahedral dihedral cosine: face normals via cross products, then the normalized inner product of the two normals adjacent to a given edge. The target theorem of the module is Berger's cofactor formula, equating that geometric cosine to the Cayley-Menger cofactor ratio from DihedralCayleyMenger.
A realized tetrahedron is four points $p:Fin,4\to\mathbb{R}^3$ that are affinely independent. For each of the six edges, the two opposite vertices of the adjacent faces determine two face normals $n_1,n_2$. The numerator is the plain dot product $n_1\cdot n_2$; the denominator square is $(|n_1|^2)(|n_2|^2)$. The cosine is their ratio after taking the positive square root of the denominator square.
Upstream, the numerator and denominator-square helpers package exactly those two scalar quantities so that later edge-by-edge identities and interior-range lemmas can unfold a single named cosine.
proof idea
Pure definition: the value is the quotient of the geometric numerator by the positive square root of the geometric denominator square. No tactic proof; both ingredients are themselves short lets that build the two adjacent face normals from the shared edge endpoints and the two opposite vertices, then take $n_1\cdot n_2$ and $(|n_1|^2)(|n_2|^2)$ respectively.
why it matters
This is the Euclidean left-hand side of the Berger cofactor program in the module. The target proposition asserts that for every realized tetrahedron and every edge, the geometric cosine equals the Cayley-Menger squared-edge cofactor ratio. Edge-0 through edge-3 equality theorems already discharge that identification for individual edges (edge 0 fully, others in progress), each by reducing to a square-root scaling identity between cofactor diagonals and the geometric denominator square.
Downstream interior lemmas use the same cosine to prove $-1<\cos\theta_e<1$ once the two adjacent face normals are linearly independent, and then lift that to every edge of an affinely independent realization. In the broader Recognition geometry stack this supplies the Euclidean dihedral input that Regge-style hinge analysis and Freudenthal-strip discretizations need when matching combinatorial cofactors to actual $3$-space angles. It does not itself invoke the forcing chain (T5-T8) or the mass ladder; it is pure Euclidean $3$-geometry feeding those discrete-gravity layers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.