dihedralCofactorNumeratorPoly
plain-language theorem explainer
Defines the numerator of the dihedral cosine as the Cayley–Menger 3-cofactor polynomial at the two vertices opposite a chosen tetrahedral edge. Anyone working with polynomial (determinant-free) dihedral cosines or their derivatives cites this. The body is a thin selector: map the edge to opposite CM indices, then evaluate the explicit cofactor polynomial.
Claim. Given 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 dihedral cofactor numerator is the explicit degree-4 Cayley–Menger cofactor polynomial $C_{p,q}(a)\in\mathbb{R}$.
background
This module supplies calculus hooks for Cayley–Menger cofactors and the dihedral cofactor ratio, so derivatives need not stay implicit. Squared edge data live in SqEdges ($\mathrm{Fin},6\to\mathbb{R}$): the six squared lengths of a tetrahedron.
Cayley–Menger geometry packages volumes and angles via a bordered Gram-type matrix. The cofactor $C_{r,c}$ at matrix indices $(r,c)$ has an explicit polynomial normal form in the six squared edges (the upstream cofactor polynomial). For each tetrahedral edge $e$, the opposite-vertex map returns the unique pair of Cayley–Menger indices not incident to that edge; those indices label the cofactor that enters the classical cosine-of-dihedral formula.
The numerator here is that cofactor in polynomial form, so later ratios and derivatives avoid raw determinant normalization.
proof idea
Definition only: unpack the opposite Cayley–Menger vertex pair $(p,q)$ for edge $e$, then return the explicit cofactor polynomial $C_{p,q}(a)$. No proof obligations; the content is the composition of the opposite-vertex lookup with the cofactor polynomial table.
why it matters
This is the numerator half of the polynomial dihedral cosine $C_{p,q}(a)/D_e(a)$. Downstream, the squared cosine is defined as that ratio, and a comparison theorem shows the classical cofactor cosine equals the polynomial form. Positivity of cofactor products on nondegenerate tetrahedra and the radical-free identity for $1-\cos^2$ both thread through this numerator.
In the gravity layer it feeds exact local dihedral cosines of the canonical Freudenthal tetrahedron (six-tet cubic Dirichlet data). Within Recognition geometry, clean polynomial cofactors keep dihedral angle calculus algebraic on the edge-length cone, which is the setting for discrete curvature and Regge-type assemblies rather than a forcing-chain (T0–T8) step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.