geometricDihedralCos_edge0_eq_cmCofactorRatio
plain-language theorem explainer
For a realized tetrahedron, the geometric dihedral cosine at edge 0 equals the Cayley-Menger cofactor ratio on its squared edge lengths. Anyone citing Berger's cofactor formula for tetrahedra will use this edge case. The proof is a one-line application of the reduced cofactor identity, discharging the remaining square-root scaling by the diagonal-cofactor product theorem.
Claim. For every realized tetrahedron $T$, the internal geometric dihedral cosine at edge $0$ equals the Cayley-Menger dihedral cosine of the squared edge lengths of $T$ at edge $0$: $\cos\theta^{\mathrm{geom}}_0(T)=C_{pq}/D_0$, where $C_{pq}$ is the indicated $3\times 3$ Cayley-Menger cofactor and $D_0$ is the matching CM denominator.
background
This module builds the Euclidean geometric side of the tetrahedral dihedral cosine: face normals from cross products of edge vectors at a realized tetrahedron, and the normalized inner product of the two normals adjacent to a chosen edge. The geometric cosine is that signed numerator (internal Regge sign convention) over the square root of the product of the squared normal norms.
On the algebraic side, the Cayley-Menger dihedral cosine is the ratio of a $3\times 3$ CM cofactor to a denominator built from the six squared edge lengths. The module target is Berger's identification of the two expressions.
Upstream, a reduced form already equates the geometric cosine at edge 0 to the CM ratio once the square-root scaling $\sqrt{C_{33}C_{44}}=4\sqrt{\mathrm{denomSq}_0}$ holds, and that scaling is proved separately as the diagonal-cofactor product identity for edge 0.
proof idea
One-line term proof. It applies the reduced edge-0 identity, which states that the geometric cosine equals the CM cofactor ratio whenever $\sqrt{C_{33}C_{44}}=4\sqrt{\mathrm{denomSq}_0}$ holds, and discharges that hypothesis by the already-proved theorem that the product of the two diagonal CM cofactors under square root scales exactly to four times the geometric denominator square root at edge 0.
why it matters
Closes Berger's cofactor formula for edge 0 on a realized tetrahedron. The parent theorem equates geometric and CM dihedral cosines for all six edges by fin_cases, invoking this result as the edge-0 case. That global identification is the module's stated remaining theorem: linking cross-product face-normal geometry to the pure edge-length cofactor calculus used in discrete gravity and Regge calculus. Downstream work can therefore treat the geometric cosine and the CM ratio as interchangeable on realized tetrahedra, feeding any curvature or deficit constructions that consume dihedral data from either side.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.