dihedralCos3SqClosedFormDeriv_eq_poly
plain-language theorem explainer
The closed-form partial of the squared dihedral cofactor-cosine, taken with respect to any squared edge length of a tetrahedron, equals the same expression written entirely in Cayley–Menger polynomials. Anyone differentiating dihedral angles in the Schläfli identity or auditing Regge Jacobian entries cites this bridge. The proof unfolds both quotient-rule forms and rewrites denominator and cofactor pieces via the existing poly equalities.
Claim. For squared edge lengths $a:\{0,\ldots,5\}\to\mathbb{R}$ and indices $e,k\in\{0,\ldots,5\}$, the closed-form coordinate derivative of the cofactor-ratio cosine along edge $e$ in direction $k$ equals its polynomial-cofactor counterpart: both are the quotient-rule expression $(N'_k D - C\, D'_k)/D^2$, with $C$ the opposite-vertex Cayley–Menger cofactor, $D$ the dihedral denominator, and primes the corresponding partials in $a_k$.
background
The module supplies derivative hooks for Cayley–Menger cofactors and the dihedral cofactor ratio, so calculus on tetrahedra is explicit rather than implicit. Squared edge lengths live in SqEdges ($\mathrm{Fin},6\to\mathbb{R}$). Opposite vertices of an edge determine a CM cofactor $C$ and a positive denominator $D$ built from diagonal cofactors; the squared cosine of the dihedral is the ratio $C^2/D$ (up to sign conventions fixed upstream).
The closed-form derivative dihedralCos3SqClosedFormDeriv is the ordinary quotient rule on that ratio, with numerator partial dihedralNumeratorClosedDeriv equal to the CM cofactor partial. The poly twin replaces every cofactor by its explicit polynomial in the six squared lengths. Upstream equalities already identify the denominator and its closed derivative with their poly versions, and cmCofactor3_eq_poly identifies the cofactors themselves.
proof idea
Term-style tactic proof. Unfold both sides of the claimed equality together with the shared numerator derivative definition, exposing identical quotient-rule skeletons. Rewrite the ordinary denominator and its closed derivative by dihedralDenom3_eq_poly and dihedralDenom3ClosedDerivValue_eq_poly. Finish with simp_rw [cmCofactor3_eq_poly], which replaces the remaining cofactor occurrences by polynomials and makes the two expressions definitionally equal.
why it matters
This is the last identification step that lets dihedral angle derivatives be computed entirely inside the polynomial CM ring. Downstream, dihedralClosedDerivSq_eq_poly in the Schläfli tetrahedron proof lifts the equality to squared closed-form angle derivatives on nondegenerate tetrahedra. The Regge TT Bloch audit uses it directly in worstRadical_flatAngleJacobian_value to evaluate a flat-angle Jacobian entry as $-\sqrt{2}/4$ after cancelling a radical denominator, separating genuine radical coefficients at the raw Jacobian layer from still-open rationality claims at bucket-fiber aggregation. In the broader geometry stack it keeps the calculus layer of the eight-tick / $D=3$ discrete geometry honest: derivatives of dihedral data stay algebraic until a deliberate radical appears.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.