geometricDihedralNumerator
plain-language theorem explainer
Defines the unnormalized numerator of the Euclidean dihedral cosine at a tetrahedron edge: the inner product of the two adjacent face normals built from cross products of edge vectors. Anyone proving the Berger cofactor identity or strict interior bounds on dihedral cosines cites it. The body is a direct let-binding composition of edge endpoints, opposite vertices, and face-normal dots.
Claim. For a tetrahedron $T$ realized by four affinely independent points in $\mathbb{R}^3$ and an edge index $e\in\{0,\ldots,5\}$, let $(i,j)$ be the endpoints of $e$ and let $(k,\ell)$ be the two opposite vertices of the faces meeting at $e$. The geometric dihedral numerator is $N(T,e)=n_{ijk}\cdot n_{ij\ell}$, where each face normal is the cross product of the two edge vectors from a common vertex on that face.
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 on faces adjacent to a shared edge. The target is Berger's cofactor formula, equating that geometric cosine to a Cayley-Menger cofactor ratio.
A RealizedTet is four points in Euclidean 3-space with an affine-independence hypothesis. Edges are indexed by Fin 6; edgeVertices3 sends each index to its endpoint pair in Fin 4. For edge $(i,j)$, adjacentFaceOppositeVertices returns the two remaining vertices $(k,\ell)$, so the adjacent faces are triangles $ijk$ and $ij\ell$.
A face normal faceNormal T a b c is the coordinate cross product of the edge vectors from $a$ to $b$ and from $a$ to $c$ in $\mathbb{R}^3$. The numerator defined here is simply the ordinary dot product of those two normals, before any normalization by their lengths.
proof idea
Pure definition, not a proof. Unpack the edge index to endpoints via edgeVertices3, read the two opposite vertices from adjacentFaceOppositeVertices, form each adjacent face normal with faceNormal, and return their Euclidean dot product. No lemmas are applied; the value is the raw bilinear form that later theorems relate to Cayley-Menger cofactors and to the normalized cosine.
why it matters
This is the geometric half of the Berger cofactor pipeline. Downstream, six edgewise theorems (cmCofactor3_edge0_eq_four_geometricNumerator through edge 5) prove that the corresponding Cayley-Menger 3-cofactor equals four times this numerator, which is the algebraic bridge to the cofactor-ratio form of the dihedral cosine in DihedralCayleyMenger.
It is also the numerator inside geometricDihedralCos, and feeds the strict-interior theorem geometricDihedralCos_strict_interior_of_faceNormals_independent: when the two face normals are linearly independent, the normalized cosine lies in $(-1,1)$. In the broader Recognition geometry stack this supplies the Euclidean dihedral data needed for Regge-style hinge analysis and tetrahedral gluing, sitting under the $D=3$ spatial forcing (T8) that makes cross-product normals well-defined in three dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.