BergerCofactorFormula3
plain-language theorem explainer
Defines the Berger cofactor target: for every realized tetrahedron and each of its six edges, the geometric dihedral cosine (normalized inner product of adjacent face normals) equals the Cayley–Menger cofactor cosine on squared edge lengths. Geometers and RS geometry auditors cite it as the Prop that the main identification theorem must discharge. It is a pure Prop abbreviation, not a proved statement.
Claim. For every realized tetrahedron $T$ and every edge index $e\in\{0,\ldots,5\}$, the geometric dihedral cosine of $T$ at $e$ (normalized inner product of the two adjacent face normals) equals the Cayley–Menger cofactor ratio cosine computed from the six squared edge lengths of $T$ at $e$.
background
This module builds the Euclidean side of tetrahedral dihedral angles. Adjacent faces determine normals via cross products of edge vectors; the geometric dihedral cosine is the normalized inner product of those two normals (sign convention fixed by orientation of the shared edge).
On the algebraic side, dihedralCos3Sq in DihedralCayleyMenger expresses the same cosine as a ratio of $5\times5$ Cayley–Menger cofactors of the squared-edge Gram data: numerator is the cofactor for the pair of vertices opposite the shared edge, denominator the product of face-area cofactors. A realized tetrahedron supplies an embedded point configuration in $\mathbb{R}^3$ whose squared pairwise distances feed that cofactor formula.
The module doc states the remaining goal explicitly: identify the geometric cosine with the Cayley–Menger cofactor ratio. The present declaration packages that identification as a single universal Prop over all six edges.
proof idea
No proof: the declaration is a def of a Prop. Its body is the universal statement equating geometricDihedralCos T e with dihedralCos3Sq (sqEdgeOfPoints T) e for all realized tetrahedra $T$ and all six edge indices. Downstream, the theorem bergerCofactorFormula3 discharges this Prop by applying the already-proved pointwise identity geometricDihedralCos_eq_cmCofactorRatio.
why it matters
This Prop is the named target for Berger’s cofactor formula inside the RS geometry stack. The parent theorem bergerCofactorFormula3 has type exactly this Prop and is proved by the geometric-to-cofactor identity; once discharged, cofactor-defined dihedral cosines of realized tetrahedra are known to lie in $[-1,1]$ and match the Euclidean normals construction.
In the broader framework the match matters because tetrahedral dihedral data feed discrete curvature and interface geometry on the recognition lattice (eight-tick / $D=3$ forcing chain). Without equating face-normal cosines to Cayley–Menger cofactors, length-only combinatorial models cannot inherit classical dihedral bounds. The definition closes the interface between GramCayleyMenger / DihedralCayleyMenger and the cross-product geometry developed in this file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.