hasDerivAt_cmCofactor3_along_coord
plain-language theorem explainer
Every Cayley-Menger cofactor C_{r,c} of a tetrahedron, as a real function of one squared edge length with the other five fixed, is differentiable, and its derivative equals the named partial polynomial. Dihedral-angle and Schläfli calculus cite this to replace opaque fderiv terms by closed forms. The proof is a one-line transfer from the polynomial derivative via the cofactor-equals-polynomial identity.
Claim. Fix cofactor indices $r,c \in \{0,\ldots,4\}$, an edge index $k \in \{0,\ldots,5\}$, and squared edge lengths $a \in \mathbb{R}^6$. The map $t \mapsto C_{r,c}(a[k \mapsto t])$ is differentiable at $t = a_k$, and its derivative equals the explicit partial polynomial $\partial_k C_{r,c}(a)$.
background
The module expands every tetrahedral Cayley-Menger cofactor into an explicit polynomial in the six squared edge coordinates. Downstream dihedral-angle calculus can then name polynomial partials instead of opaque Fréchet derivatives.
Squared edge data live in SqEdges ($\mathrm{Fin},6 \to \mathbb{R}$). The cofactor $C_{r,c}$ is the signed $4\times 4$ minor of the $5\times 5$ Cayley-Menger matrix built from those edges. The sibling identity cmCofactor3_eq_poly asserts that this determinant-defined cofactor equals a concrete multivariate polynomial cmCofactor3Poly. The named partial cmCofactorPartial r c k a is the formal $\partial/\partial a_k$ of that polynomial, evaluated at $a$.
The upstream polynomial derivative theorem already proves HasDerivAt for the polynomial presentation; the present result only renames the object back to the geometric cofactor.
proof idea
One-line wrapper. Rewrite the target function via cmCofactor3_eq_poly (cofactor equals its explicit polynomial), then apply hasDerivAt_cmCofactor3Poly_along_coord at the same indices and point. simpa discharges the rewritten goal.
why it matters
This is the bridge from determinant geometry to coordinate calculus on tetrahedra. The sole recorded consumer is hasDerivAt_dihedralCos3Sq_explicit, which differentiates the squared cofactor-cosine used for dihedral angles; that theorem needs a closed-form $\partial_k C_{r,c}$ under a non-vanishing product hypothesis on the opposite-vertex cofactors.
In the broader Recognition geometry stack, explicit cofactor derivatives feed the algebraic identity $C_{pp}C_{qq}-C_{pq}^2 = 2\cdot\mathrm{CM}\cdot a_e$ (the cofactor discriminant for a tetrahedral edge). That identity converts the arccos denominator into the common volume factor appearing in Schläfli-type variation formulas. The module is the cofactor analogue of CayleyMengerDerivatives: once partials are named polynomials, volume and angle forcing arguments stay inside elementary real analysis rather than abstract fderiv.
No forcing-chain landmark (T5–T8) is proved here; the result is pure Euclidean infrastructure that those geometric arguments rely on when they differentiate tetrahedral data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.