dihedralNumeratorClosedDeriv
plain-language theorem explainer
Gives the explicit partial of the Cayley–Menger numerator cofactor for a tetrahedral edge, with respect to one squared-edge coordinate. Anyone differentiating dihedral cosines via cofactor ratios cites this value. It is a thin naming layer: opposite vertices of the edge, then the matching cofactor partial polynomial.
Claim. For squared edge lengths $a\colon\{0,\ldots,5\}\to\mathbb{R}$, tetrahedral edge $e$, and coordinate index $k$, if $(p,q)$ are the two Cayley–Menger vertex indices opposite $e$, the closed-form numerator derivative is the explicit partial $\partial_{a_k}C_{pq}(a)$ of the $(p,q)$-cofactor polynomial.
background
The module supplies calculus hooks for Cayley–Menger cofactors and the dihedral cofactor ratio on a tetrahedron. Squared edge lengths live in six real coordinates (SqEdges). The classical Cayley–Menger matrix is $5\times 5$; its cofactors encode volumes and face data used to form dihedral cosines.
For each of the six edges, a fixed pair of matrix indices marks the two vertices opposite that edge. The numerator of the squared-cosine cofactor ratio is the off-diagonal cofactor $C_{pq}$ at that pair. Upstream, cmCofactorPartial is the fully expanded multilinear polynomial for $\partial/\partial a_k$ of any such cofactor entry (case-split on row, column, and edge index).
Local setting: symbolic derivative simplifications remain downstream; this file only makes the derivative interface explicit rather than implicit in later gravity or Regge analysis.
proof idea
Definition, not a proof. Unpack the opposite Cayley–Menger vertex pair $(p,q)$ for edge $e$, then return the already-expanded partial cmCofactorPartial p q k a. No further algebraic reduction occurs here; the value is exactly that polynomial specialization.
why it matters
Feeds the closed-form coordinate derivative of the cofactor-ratio cosine: the quotient rule needs this numerator partial together with the denominator derivative. Equality lemmas identify that closed form with the generic quotient derivative and with a pure polynomial presentation. The explicit HasDerivAt theorem for the dihedral cosine along a squared-edge coordinate also consumes it (under a non-vanishing face-cofactor product).
In the broader Recognition geometry stack this is infrastructure for differentiating dihedral data built from Cayley–Menger determinants, not a forcing-chain step (T5–T8) or an RCL identity. It closes the gap noted in the module header: calculus on cofactor ratios is no longer only implicit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.