geometricDihedralCos_edge0_eq_cofactorRatio_of_sqrt
plain-language theorem explainer
For a realized tetrahedron, the Euclidean dihedral cosine on edge 0 equals the Cayley–Menger cofactor ratio once a single square-root scaling identity is assumed. Anyone proving Berger’s cofactor formula for tetrahedra will cite this reduction. The proof unfolds both cosines, substitutes the fourfold numerator identity, applies the scaling hypothesis, and finishes by field simplification.
Claim. Let $T$ be a realized tetrahedron. Write $a$ for its squared edge lengths. Suppose $\sqrt{C_{3,3}(a)\,C_{4,4}(a)}=4\sqrt{D_0(T)}$, where $C_{r,c}$ are Cayley–Menger cofactors and $D_0(T)$ is the squared geometric denominator on edge $0$. Then the geometric dihedral cosine on edge $0$ equals the Cayley–Menger dihedral cosine: $N_0(T)/\sqrt{D_0(T)}=C_{3,4}(a)/\sqrt{C_{3,3}(a)\,C_{4,4}(a)}$.
background
This module builds the Euclidean side of the tetrahedral dihedral cosine: face normals via cross products of edge vectors, and the cosine as their normalized inner product. The target is Berger’s cofactor formula, equating that geometric cosine to the Cayley–Menger cofactor ratio from DihedralCayleyMenger.
On the Cayley–Menger side, cmCofactor3 is the signed $3\times3$ minor of the $5\times5$ Cayley–Menger matrix of squared edge lengths. The CM dihedral cosine on an edge is $C_{p,q}/\sqrt{C_{p,p}C_{q,q}}$ for the two vertices opposite that edge; for edge $0$ those indices are $3$ and $4$. The geometric numerator is (a multiple of) the inner product of the two adjacent face normals; the geometric denominator square is the product of the squared normal lengths.
An upstream identity already shows $C_{3,4}(a)=4$ times the geometric numerator on edge $0$. What remains is matching the two square-root denominators up to that same factor of $4$.
proof idea
Term-mode proof by definitional reduction. Unfold the geometric cosine and the CM cosine (and its denominator) so both sides become an explicit quotient. The goal is then geometric-numerator over geometric-sqrt-denom versus $C_{3,4}$ over $\sqrt{C_{3,3}C_{4,4}}$. Rewrite the numerator via cmCofactor3_edge0_eq_four_geometricNumerator and the denominator via the assumed scaling hsqrt. A single field_simp cancels the common factor of $4$ and equates the quotients.
why it matters
This is the last algebraic step before Berger’s cofactor formula is closed for edge $0$. The immediate parent geometricDihedralCos_edge0_eq_cmCofactorRatio simply feeds in the discharged square-root identity cmCofactor3_edge0_sqrt_diag_product and obtains the unconditional equality of geometric and CM dihedral cosines on edge $0$ (doc: “Edge 0: Berger's cofactor formula is fully proved”).
In the Recognition geometry stack, matching the cross-product normal cosine to the Cayley–Menger cofactor ratio is the bridge from realized point configurations to pure edge-length data. That bridge is needed wherever dihedral angles enter discrete curvature or volume constraints built from the Gram/Cayley–Menger pipeline. The module then proceeds edge-by-edge (edge $1$ starts immediately after the parent theorem).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.