dihedralDenom3Poly
plain-language theorem explainer
Defines the polynomial form of the dihedral-cosine denominator for a tetrahedron: the square root of the product of the two opposite diagonal Cayley–Menger cofactors, written as explicit polynomials in the six squared edge lengths. Anyone differentiating dihedral cosines or comparing cofactor ratios to determinant-normalized forms cites it. The body is a three-line construction via opposite vertices and the cofactor polynomial table.
Claim. For squared edge lengths $a:\{0,\ldots,5\}\to\mathbb{R}$ of a tetrahedron and an edge index $e$, let $(p,q)$ be the two Cayley–Menger vertex indices opposite $e$. The polynomial dihedral denominator is $\sqrt{C_{pp}(a)\,C_{qq}(a)}$, where $C_{rc}(a)$ denotes the explicit degree-four Cayley–Menger cofactor polynomial in row $r$ and column $c$.
background
The module supplies derivative hooks for Cayley–Menger cofactors and the dihedral cofactor ratio, so that calculus on tetrahedral geometry is explicit rather than buried in determinants.
Squared edge lengths of a tetrahedron are packaged as SqEdges ($\mathrm{Fin},6\to\mathbb{R}$). Each Cayley–Menger cofactor has an explicit polynomial normal form $C_{rc}(a)$ (the table cmCofactor3Poly), avoiding adjugate-of-determinant presentation. For each of the six edges, oppositeCMVertices returns the pair of CM matrix indices opposite that edge (e.g. edge $(0,1)$ opposite vertices $2,3$).
Classically the dihedral cosine along an edge is a ratio whose denominator is $\sqrt{C_{pp}C_{qq}}$ for those opposite indices. The present definition is that denominator written entirely in the polynomial cofactors, so it is definitionally lighter than the determinant-normalized twin.
proof idea
Pure definition, no proof obligations. Unpack the opposite-vertex pair $(p,q)$ for the given edge, evaluate the two diagonal cofactor polynomials $C_{pp}(a)$ and $C_{qq}(a)$, and take the real square root of their product. Downstream lemmas later identify this with the determinant form and differentiate under the square root.
why it matters
This is the denominator half of the polynomial cofactor cosine used throughout the geometry calculus layer. It feeds the cosine ratio itself, the closed-form derivative of that ratio (quotient rule with the closed derivative of the sqrt denominator), the equality theorem linking determinant and polynomial denominators, positivity and non-vanishing on non-degenerate tetrahedra, and several algebraic identities (square of the denominator, $1-\cos^2$ expansions).
In the broader Recognition stack these hooks support Regge-style hinge analysis and zero-mode work on tetrahedral complexes: dihedral angles must be differentiable in edge lengths with controlled denominators. The definition does not itself force $D=3$ or the eight-tick structure; it is infrastructure for the geometric side of that program.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.