dihedralCos3SqClosedFormDeriv_eq_generic
plain-language theorem explainer
The closed-form partial of the squared dihedral cosine (Cayley-Menger cofactor ratio) equals the generic quotient-rule derivative once the explicit numerator and denominator cofactor partials are substituted. Anyone differentiating tetrahedron dihedral data along squared-edge coordinates would cite this identification. The proof is a pure unfold-and-simp definitional match.
Claim. For squared edge lengths $a:\{0,\ldots,5\}\to\mathbb{R}$ of a tetrahedron and indices $e,k\in\{0,\ldots,5\}$, the closed-form coordinate derivative of the squared dihedral cosine at $(a,e,k)$ equals the generic quotient derivative of that cofactor ratio, evaluated on the constant path $t\mapsto a$ at $t=0$, after inserting the closed-form numerator partial and the closed-form three-denominator partial.
background
The module supplies derivative hooks for Cayley-Menger cofactors and the dihedral cofactor ratio on a tetrahedron. Squared edge lengths live in SqEdges ($\mathrm{Fin},6\to\mathbb{R}$). The squared dihedral cosine is realized as a ratio of CM cofactors: a numerator cofactor against a three-factor denominator built from diagonal cofactors of opposite vertex pairs.
Two parallel derivative interfaces exist. The closed-form side (dihedralCos3SqClosedFormDeriv) writes the quotient rule with explicit partials of the numerator and of the three-denominator. The generic side (dihedralCos3SqDerivValue) is the abstract quotient derivative value along a path in edge space, taking numerator and denominator derivatives as parameters. This theorem asserts they agree after the closed-form partials are plugged in.
Upstream geometry supplies the cofactor polynomials and the opposite-vertex pairing that indexes the dihedral edge; the calculus layer only packages their first derivatives.
proof idea
One-line definitional identification. Unfold the closed-form cosine derivative and the generic quotient derivative value; both expand to the same quotient-rule expression
$(N' D - N D')/D^2$
with $N'$ the closed numerator partial and $D'$ the closed three-denominator partial. simp discharges the residual definitional equalities. No analytic lemmas are invoked.
why it matters
Closes the bridge between the hand-written closed-form dihedral cosine derivative and the generic pathwise quotient interface in the Cayley-Menger calculus layer. The module doc states that hard symbolic simplifications remain downstream; this equality lets those later simplifications work against either interface without double bookkeeping.
No downstream consumers are wired yet (used_by is empty), so the result is infrastructure rather than a forcing-chain step. It does not touch T5-T8, RCL, or the phi ladder; it is pure tetrahedron geometry supporting later realisability and curvature work that may feed Recognition geometry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.