geometricDihedralCos_edge5_eq_cmCofactorRatio
plain-language theorem explainer
For a realized tetrahedron, the geometric dihedral cosine at edge 5 equals the Cayley–Menger cofactor ratio on its squared edge lengths at that edge. Anyone assembling Berger’s full six-edge identification cites this case. The proof unfolds both sides, rewrites via two edge-5 cofactor identities, and finishes with field simplification.
Claim. For every realized tetrahedron $T$, the cosine of the dihedral angle at edge $5$ (normalized inner product of the two adjacent face normals) equals the Cayley–Menger cofactor ratio $C_{1,2}/\sqrt{C_{1,1}C_{2,2}}$ formed from the squared edge lengths of $T$.
background
This module builds the Euclidean side of tetrahedral dihedral cosines: face normals via cross products of edge vectors, then the normalized inner product of the two normals meeting at a chosen edge. That quantity is the geometric dihedral cosine.
On the algebraic side, the Cayley–Menger matrix of squared edge lengths supplies cofactors $C_{r,c}$. The CM dihedral cosine at an edge is the off-diagonal cofactor of the two opposite vertices, divided by the square root of the product of the corresponding diagonal cofactors. For edge index $5$ those opposite vertices are $(1,2)$.
The module’s target is Berger’s cofactor formula: equality of the geometric cosine with the CM ratio on every edge of a realized tetrahedron. This declaration is the edge-$5$ case of that identification.
proof idea
Term-mode proof. Unfold the geometric cosine, the CM cosine, and the CM denominator, then change both sides into explicit quotients: geometric numerator over sqrt of geometric denom-square versus $C_{1,2}/\sqrt{C_{1,1}C_{2,2}}$.
Rewrite with the two edge-5 bridge lemmas: the CM off-diagonal cofactor equals four times the geometric numerator, and the sqrt of the CM diagonal product matches the geometric denom sqrt (up to the same constant factor). field_simp cancels the common factors and closes the equality.
why it matters
Feeds the parent theorem geometricDihedralCos_eq_cmCofactorRatio, Berger’s cofactor formula for all six tetrahedral edges, which dispatches by fin_cases and invokes one lemma per edge. Without the edge-$5$ case the full identification is incomplete.
In the Recognition geometry stack this pins the Euclidean dihedral cosine (cross-product normals) to the Cayley–Menger cofactor calculus used for non-coordinate tetrahedra. It is pure 3D Euclidean geometry supporting later discrete-curvature and forcing-chain geometry, not a physics constant claim by itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.