dihedralCos3SqPoly
plain-language theorem explainer
Defines the squared-edge dihedral cosine of a tetrahedron as a pure cofactor ratio: numerator cofactor over the geometric mean of the two face-diagonal cofactors. Geometers and discrete-gravity workers cite it when they need a determinant-free cosine that still matches the classical Cayley–Menger angle. The body is a one-line quotient of two already-defined polynomial cofactors.
Claim. For squared edge lengths $a:\{0,\ldots,5\}\to\mathbb{R}$ and an edge index $e$, the polynomial-cofactor dihedral cosine is $\mathrm{num}(a,e)/\mathrm{den}(a,e)$, where $\mathrm{num}$ is the off-diagonal Cayley–Menger $3$-cofactor of the two vertices opposite $e$, and $\mathrm{den}=\sqrt{C_{pp}(a)\,C_{qq}(a)}$ is the geometric mean of the corresponding diagonal cofactors.
background
The module supplies derivative hooks for Cayley–Menger cofactors and the dihedral cofactor ratio, so that later symbolic derivative work can sit on an explicit calculus layer rather than an implicit one.
SqEdges is simply a map from the six edges of a tetrahedron to squared lengths. The numerator dihedralCofactorNumeratorPoly is the off-diagonal $3$-cofactor $C_{pq}(a)$ of the two Cayley–Menger vertices opposite the chosen edge. The denominator dihedralDenom3Poly is $\sqrt{C_{pp}(a)C_{qq}(a)}$; it is definitionally lighter than the classical normalized determinant form because it never divides by the full Cayley–Menger determinant.
Together these give a cosine that is algebraically identical to the usual dihedral cosine whenever the configuration is nondegenerate, but is written entirely in polynomial cofactors.
proof idea
Pure definition: the value is the quotient of the two upstream polynomial-cofactor maps already introduced in the same module. No tactic proof, no lemmas applied beyond the definitions of the numerator and denominator.
why it matters
This is the preferred algebraic stand-in for the classical dihedral cosine in the cofactor calculus pipeline. Downstream, dihedralCos3Sq_eq_poly proves it equals the determinant-normalized cosine; one_sub_dihedralCos3SqPoly_sq_eq and its square-root sibling turn $1-\cos^2$ into a radical-free cofactor discriminant, which feeds the arccos chain rule.
In SchlaefliTetrahedronProof, dihedralClosedDerivSqPoly builds the squared-edge Schläfli derivative from this cosine and its closed-form derivative, the preferred target for the six algebraic Schläfli identities. The same cosine appears in the Freudenthal six-tetrahedron cubic instance when exact local dihedral cosines of the canonical triangulation are recorded.
Within Recognition geometry this keeps discrete curvature and hinge angles on a polynomial footing, avoiding determinant normalizations that obstruct later differentiation and exact evaluation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.