hasDerivAt_cm3_partial5
plain-language theorem explainer
Specializes the uniform one-coordinate derivative of the Cayley–Menger polynomial to the fifth squared-edge slot (edge (2,3)). Anyone needing formal differentiability of CM₃ in ν = a₅ cites this. The proof is a one-line specialization of the packaged gradient derivative theorem.
Claim. For any assignment $a$ of six squared edge lengths, the real map $t \mapsto \mathrm{CM}_3(a[5\mapsto t])$ is differentiable at $t=a_5$, and its derivative equals the closed-form partial $\partial\mathrm{CM}_3/\partial a_5$ evaluated at $a$.
background
The Cayley–Menger polynomial $\mathrm{CM}_3$ is the explicit degree-3 polynomial in the six squared edge lengths of a tetrahedron that vanishes precisely when the four points embed isometrically in Euclidean 3-space. Coordinates follow the fixed edge convention: index 5 is the squared length of edge (2,3).
This module supplies closed-form partials $\partial\mathrm{CM}_3/\partial a_i$ and packages them as a gradient map. The fifth partial is the explicit quadratic polynomial $2\bigl(a_0(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_2-a_3 a_4\bigr)$.
Upstream, the uniform statement already proves that $t\mapsto\mathrm{CM}_3(a[i\mapsto t])$ has derivative equal to the $i$th gradient entry at $t=a_i$, via the single-coordinate Taylor expansion (linear term plus quadratic coefficient plus cubic remainder).
proof idea
One-line wrapper. Apply the uniform theorem hasDerivAt_cm3_grad at basepoint $a$ and coordinate index 5; then simpa rewrites the gradient component cm3_grad a 5 into the named fifth partial. No fresh calculus is performed.
why it matters
The module exists to feed the Regge second-variation matrix $M_{ij}$, which is assembled from these partials by the chain rule through the conformal edge ansatz. Formal $C^\infty$ smoothness of $\mathrm{CM}_3$ is already known; the contribution here is the explicit closed-form gradient API. This lemma is the coordinate-5 instance of that API, so downstream Hessian or single-perturbation arguments can cite a named partial rather than an opaque gradient lookup. No downstream consumers are wired yet in the graph, but the sibling Taylor and quadratic-coefficient material sits immediately above the second-derivative (Hessian diagonal) layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.