geometricDihedralCos_edge2_eq_cmCofactorRatio
plain-language theorem explainer
For a realized tetrahedron, the geometric dihedral cosine at edge 2 equals the Cayley-Menger cofactor ratio built from its squared edge lengths. Cite this when assembling Berger's formula edge by edge. The proof unfolds both cosines, rewrites via two edge-2 cofactor identities (numerator and diagonal product), and cancels the common factor of 4 by field simplification.
Claim. Let $T$ be a realized tetrahedron in Euclidean space. Then the geometric dihedral cosine at edge index $2$ (normalized inner product of the two adjacent face normals) equals the Cayley-Menger dihedral cosine of the squared-edge data of $T$ at the same edge: $\cos^{\mathrm{geom}}_2(T)=C_{2,3}/\sqrt{C_{2,2}C_{3,3}}$, where $C_{r,c}$ are the Cayley-Menger cofactors of those squared lengths.
background
This module supplies the Euclidean geometric side of tetrahedral dihedral cosines: edge vectors from the four embedded vertices, face normals as cross products, and the geometric cosine as the normalized inner product of the two normals meeting at a chosen edge. The module target is Berger's cofactor formula, equating that geometric cosine to a pure distance expression.
On the algebraic side, the Cayley-Menger matrix of squared edge lengths yields cofactors $C_{r,c}$. The CM dihedral cosine at an edge is the off-diagonal cofactor of the opposite vertex pair divided by $\sqrt{C_{pp}C_{qq}}$. For edge index 2 the opposite pair is $(2,3)$ in the Fin-5 cofactor indexing.
Two prior lemmas already pin the edge-2 case: the off-diagonal cofactor equals four times the geometric numerator, and the CM diagonal product under a square root matches the geometric denominator factor (up to that same scaling).
proof idea
Unfold the geometric cosine and the CM cosine (including its denominator) so both sides are explicit quotients. A change aligns the goal with
$N_{\mathrm{geom}}/\sqrt{D_{\mathrm{geom}}}$ versus $C_{2,3}/\sqrt{C_{2,2}C_{3,3}}$.
Rewrite the numerator by cmCofactor3_edge2_eq_four_geometricNumerator ($C_{2,3}=4N_{\mathrm{geom}}$) and the denominator by cmCofactor3_edge2_sqrt_diag_product. The shared factor of 4 cancels under field_simp, finishing the equality.
why it matters
This is the edge-2 case of the six specialized identities that feed Berger's full cofactor formula geometricDihedralCos_eq_cmCofactorRatio, which dispatches on Fin 6 by fin_cases and quotes each edge lemma. The module doc names that identification as the remaining theorem of the file.
Closing the geometric-to-CM bridge lets dihedral data of a realized tet be read from squared edge lengths alone, without retaining coordinates or explicit normals. Downstream geometry that works only with Cayley-Menger or Gram data can therefore import dihedral cosines as cofactor ratios. In the broader Recognition geometry stack this is bookkeeping infrastructure for tetrahedral angle content from distance data, not a forcing-chain step (T0-T8) itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.