dihedralCofactorProductPoly
plain-language theorem explainer
Defines the product of the two diagonal Cayley–Menger cofactor polynomials opposite a chosen tetrahedral edge. That product is the radicand of the dihedral-cosine denominator in squared-edge coordinates. Anyone working dihedral angles, Schläfli identities, or Regge calculus on a nondegenerate tet cites it. The body is a three-line unpack of opposite vertices times the two matching cofactor polynomials.
Claim. For squared edge lengths $a : \mathrm{Fin}\,6 \to \mathbb{R}$ and an edge index $e \in \mathrm{Fin}\,6$, let $(p,q)$ be the pair of Cayley–Menger vertex indices opposite $e$. The dihedral cofactor product is $C_p(a)\,C_q(a)$, where $C_r$ denotes the diagonal Cayley–Menger cofactor polynomial at vertex index $r$.
background
The module supplies derivative hooks for Cayley–Menger cofactors and the dihedral cofactor ratio, so the calculus layer is explicit even while hard symbolic simplifications sit downstream.
Squared edge lengths of a tetrahedron are packaged as $a : \mathrm{Fin},6 \to \mathbb{R}$. For each edge $e$, oppositeCMVertices returns the two Cayley–Menger matrix vertex indices opposite that edge (e.g. edge $(0,1)$ pairs with vertices $2,3$). The cofactor polynomials cmCofactor3Poly r c a are the explicit polynomial normal forms of the $5\times 5$ Cayley–Menger cofactors in those six squared lengths; the diagonal entries $r=c$ enter the classical dihedral-cosine formulae.
Classically, $\cos\theta_e$ for the dihedral angle at edge $e$ is a ratio whose denominator involves $\sqrt{C_p C_q}$. This definition isolates that product as a pure polynomial in $a$, before taking square roots or forming the cosine ratio.
proof idea
Definitional, not a proof. Unpack the opposite-vertex pair $(p,q)$ for edge $e$, then multiply the two diagonal cofactor polynomials cmCofactor3Poly p p a and cmCofactor3Poly q q a. No lemmas are applied; the value is exactly that product in $\mathbb{R}$.
why it matters
This is the shared radicand underneath the polynomial dihedral denominator and the radical-free $1-\cos^2$ identities in the same module. Downstream positivity (dihedralCofactorProductPoly_pos_of_nonDegenerate and the nonneg/ne-zero corollaries) guarantees the product is strictly positive on nondegenerate tetrahedra, so the square-root denominator dihedralDenom3Poly is well-defined and positive, and dihedralDenom3Poly_sq recovers the product. Those facts feed one_sub_dihedralCos3SqPoly_sq_eq, the closed derivative interfaces for dihedral cosines, and the Schläfli summand non-vanishing lemma in SchlaefliTetrahedronProof.
In the Recognition geometry stack this is scaffolding for rigorous Regge/Schläfli calculus on tetrahedra (edge-length variations of dihedral angles), not a forcing-chain step (T0–T8). It closes the gap between symbolic Cayley–Menger cofactors and differentiable dihedral data used by volume and curvature identities.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.