geometricDihedralNumerator_edge2_gram
plain-language theorem explainer
For a realized Euclidean tetrahedron, the geometric dihedral numerator at edge 2 equals the Gram bilinear form G_{22}G_{01}-G_{21}G_{02}. Anyone matching face-normal geometry to Cayley-Menger cofactors cites this edge case. The proof rewrites via the cross-product expansion of the numerator, then simplifies edge and opposite-vertex data against the Gram matrix.
Claim. Let $T$ be a realized Euclidean tetrahedron with $3\times 3$ Gram matrix $G$ of its basis edge vectors. The geometric dihedral numerator at edge $2$ (the unnormalized inner product of the two adjacent face normals) equals $G_{22}G_{01}-G_{21}G_{02}$.
background
This module builds the Euclidean side of the tetrahedral dihedral cosine: face normals from cross products of edge vectors, and the normalized inner product of the two normals meeting an edge. The target is Berger's cofactor formula, equating that geometric cosine to a Cayley-Menger cofactor ratio.
The geometric dihedral numerator at edge $e$ is the raw dot product of the two face normals on the faces adjacent to $e$. Those faces are labeled by the opposite-vertex pair from adjacentFaceOppositeVertices (for edge 2, vertices 1 and 2). The expansion lemma geometricDihedralNumerator_cross rewrites that numerator via the vector identity for $\langle u\times v, u\times w\rangle$.
Coordinate edge vectors agree with Euclidean edge vectors under the real inner product (coordEdgeVector_dot_eq_inner). The Gram entries gram3 T i j are exactly those inner products of basis edge vectors, so the expanded numerator collapses to a $2\times 2$ Gram determinant expression once edge indices are fixed.
proof idea
One rewrite plus simplification. First apply geometricDihedralNumerator_cross, which expands the numerator as a product of edge-length squares and cross terms via cross_dot_cross. Then simp unfolds the edge-2 vertex table (edgeVertices3, adjacentFaceOppositeVertices, edgeVertices), replaces coordinate dots by Euclidean inners (coordEdgeVector_dot_eq_inner), and identifies those inners with Gram entries (gram3, basisEdgeVector, edgeVector). The residual algebra is the stated bilinear combination of Gram entries.
why it matters
This is the edge-2 Gram identity needed before matching Cayley-Menger cofactors to geometry. Its sole direct consumer is cmCofactor3_edge2_eq_four_geometricNumerator, which proves the CM cofactor at the corresponding minor equals four times this numerator. Parallel lemmas already exist for edges 0 and 1; together they feed the Berger cofactor identification of geometric dihedral cosine with the CM cofactor ratio in DihedralCayleyMenger.
In the broader Recognition geometry stack, realized tetrahedra and Gram/Cayley-Menger data underwrite discrete curvature and Regge-type edge lengths on the eight-tick / $D=3$ side of the forcing chain. Closing Berger edge-by-edge removes a scaffolding gap between pure Euclidean face-normal geometry and the combinatorial CM presentation used downstream.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.