hasDerivAt_cm3_partial0
plain-language theorem explainer
The closed-form partial of the Cayley–Menger polynomial in the first squared edge length is the genuine one-variable derivative of the single-coordinate update map. Anyone assembling the Regge second-variation matrix from explicit CM gradients would cite this. The proof is a one-line specialization of the uniform gradient derivative theorem at coordinate zero.
Claim. For every assignment $a$ of six squared edge lengths of a tetrahedron, the map $t \mapsto \mathrm{CM}_3(a[0\mapsto t])$ is differentiable at $t=a_0$, and its derivative equals the closed-form partial $\partial\mathrm{CM}_3/\partial a_0$ evaluated at $a$.
background
The Cayley–Menger polynomial $\mathrm{CM}_3$ is an explicit cubic in the six squared edge lengths of a tetrahedron. Lengths are indexed by $\mathrm{Fin},6$ under the fixed edge convention: $0=(0,1)$, $1=(0,2)$, $2=(0,3)$, $3=(1,2)$, $4=(1,3)$, $5=(2,3)$.
This module supplies the six closed-form partials and packages them as a gradient map $a\mapsto(\partial_i\mathrm{CM}_3(a))_i$. Smoothness of $\mathrm{CM}_3$ is already known; the contribution here is the algebraic gradient needed for the Regge second-variation matrix via the conformal edge ansatz.
The upstream uniform theorem states that for every coordinate $i$, the derivative of $t\mapsto\mathrm{CM}_3(a.\mathrm{update},i,t)$ at $t=a_i$ equals the $i$-th closed-form gradient entry. The partial for edge $0$ is the explicit quadratic polynomial $2(a_5(a_1+a_2+a_3+a_4-a_0-a_5)-a_0 a_5+a_1 a_4+a_2 a_3-a_1 a_3-a_2 a_4)$.
proof idea
One-line wrapper. Specialize the uniform one-coordinate derivative theorem to index $i=0$, then rewrite the resulting gradient entry by the packaging definition that sends coordinate $0$ to the closed-form first partial. simpa discharges the equality of the two presentations of that entry.
why it matters
The Regge second-variation matrix $M_{ij}$ is built from these partials through the chain rule on the conformal edge ansatz. The module's central Taylor identity already exposes gradient, quadratic, and cubic terms; this declaration (with its five siblings) turns the packaged gradient into a Mathlib-native single-coordinate HasDerivAt fact.
No downstream consumers are recorded yet in the dependency graph, but the API is the natural hook for later comparison of $M_{ij}$ against face areas. In Recognition Science geometry, explicit CM derivatives feed discrete curvature and volume-variation arguments that sit on the $D=3$ tetrahedral setting forced by the T8 step of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.