hasDerivAt_cmCofactor3Poly_along_coord
plain-language theorem explainer
Along any single squared-edge coordinate, the explicit Cayley–Menger cofactor polynomial is differentiable, and its derivative equals the named partial polynomial. Anyone computing dihedral-angle or volume gradients from CM cofactors cites this. The proof rewrites the one-variable restriction as a shifted cubic (cubic coeff zero) and applies the generic shifted-cubic derivative lemma.
Claim. For every cofactor index pair $(r,c)\in\{0,\ldots,4\}^2$, every edge index $k\in\{0,\ldots,5\}$, and every squared-edge assignment $a:\{0,\ldots,5\}\to\mathbb{R}$, the map $t\mapsto P_{r,c}(a[k\mapsto t])$ is differentiable at $t=a_k$, with derivative equal to the explicit partial $\partial_k P_{r,c}(a)$. Here $P_{r,c}$ is the degree-$\le 2$ polynomial normal form of the $(r,c)$ Cayley–Menger cofactor in the six squared edge lengths.
background
The module expands every tetrahedral Cayley–Menger cofactor as an explicit polynomial in the six squared edge coordinates (SqEdges $:= \mathrm{Fin},6\to\mathbb{R}$). Downstream dihedral-angle calculus can then quote named polynomial partials instead of opaque Fréchet derivatives.
cmCofactor3Poly r c is that normal form: a concrete multivariate polynomial of total degree at most four, and of degree at most two in each individual coordinate. cmCofactorPartial r c k is the matching closed-form partial with respect to edge $k$. cmCofactorQuadraticCoeff records the quadratic coefficient of the one-coordinate restriction; the cubic coefficient is identically zero.
Upstream, cmCofactor3Poly_update_polyform gives the Taylor identity along one edge: after the update $a_k\mapsto a_k+t$, the cofactor equals constant + partial$\cdot t$ + quadratic$\cdot t^2$ + $0\cdot t^3$. The generic lemma hasDerivAt_shifted_cubic then supplies the derivative of any such shifted cubic at the base point.
proof idea
First prove functional equality: the path $t\mapsto$ cofactor-poly of $a$ with coordinate $k$ set to $t$ equals the shifted cubic
$A + B(t-a_k) + C(t-a_k)^2 + 0\cdot(t-a_k)^3$,
with $A$ the base cofactor, $B$ the named partial, and $C$ the quadratic coefficient. This is cmCofactor3Poly_update_polyform after the change of variable $t\mapsto t-a_k$ (and a one-line ring identity $a_k+(t-a_k)=t$).
Rewrite the goal along that equality, then apply hasDerivAt_shifted_cubic at base point $a_k$. That lemma differentiates $A+B(x-x_0)+C(x-x_0)^2+D(x-x_0)^3$ by the product/power rules and returns derivative $B$ at $x_0$; here $D=0$.
why it matters
This is the polynomial-side half of the closed-form coordinate derivative for every CM cofactor. Its sole direct consumer is hasDerivAt_cmCofactor3_along_coord, which transports the result across the identity cmCofactor3 = cmCofactor3Poly so that determinant-defined cofactors inherit the same named partial.
In the broader geometry stack, explicit cofactor derivatives feed dihedral-angle calculus (the cofactor analogue of CayleyMengerDerivatives). Recognition Science uses tetrahedral CM geometry when forcing $D=3$ spatial dimensions (forcing-chain T8) and when tracking edge-length variations on the recognition lattice; named partials keep those gradients algebraic rather than symbolic black boxes.
No scaffolding remains: the claim is fully proved, and the cubic coefficient vanishing is already baked into the polyform lemma.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.