bergerCofactorFormula3
plain-language theorem explainer
For every realized tetrahedron and each of its six edges, the geometric dihedral cosine built from face normals equals the Cayley-Menger cofactor ratio of squared edge lengths. Anyone matching Euclidean tetrahedra to pure edge-length data (Regge-style or RS hinge data) would cite this packaging. The proof is a one-line term that names the already-proved edgewise identity as the discharged Berger target.
Claim. For every realized tetrahedron $T$ and every edge index $e\in\{0,\ldots,5\}$, the geometric dihedral cosine of $T$ at $e$ equals the Cayley-Menger cofactor ratio of the squared edge lengths of $T$.
background
This module builds the Euclidean side of the tetrahedral dihedral cosine: edge vectors in coordinates, face normals via cross products, and the normalized inner product of the two normals meeting an edge. That quantity is the geometric dihedral cosine.
The combinatorial counterpart is the Cayley-Menger cofactor ratio of squared edge lengths (the squared-edge form of the classical Berger formula). The named target packages the claim that, for every realized tetrahedron and every one of the six edges, these two cosines agree.
Upstream, the edgewise theorem already proves the identity by fin_cases on the six edges, each reduced to a specialized lemma. The present declaration simply records that result as the discharged Berger cofactor target for realized tetrahedra.
proof idea
One-line term proof. The declaration's type is the Prop asserting equality of geometric dihedral cosine and Cayley-Menger cofactor ratio for all realized tetrahedra and all six edges. The proof term is exactly the upstream theorem that already states and proves that universal quantification (via case split on the edge index and six specialized edge lemmas). No new algebra is done here.
why it matters
This closes the remaining theorem of the Berger cofactor module: the geometric (cross-product) dihedral cosine is identified with the Cayley-Menger cofactor ratio on squared edges. That bridge lets later work pass between coordinate realizations and pure edge-length hinge data (dihedral cosines and areas-squared), the same hinge data used in discrete gravity and Wick-action continuations.
No downstream consumers are wired in the current graph, so the declaration is an export point rather than an intermediate lemma. In the broader Recognition framework it supports geometric consistency of discrete 3-space structures, in line with the forced spatial dimension $D=3$ (T8) and tetrahedral building blocks of the eight-tick octave geometry. A sibling comment flags the natural next bound: cofactor-defined cosines of realized tetrahedra lie in $[-1,1]$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.