hasDerivAt_cm3_partial3
plain-language theorem explainer
The single-edge slice of the Cayley-Menger polynomial along squared edge (1,2) is differentiable at the base length, with derivative equal to the closed-form third partial. Anyone assembling first-order Regge variations or single-coordinate CM updates from the explicit gradient would cite it. The proof is a one-line specialization of the uniform coordinate-derivative theorem, rewriting the packaged gradient entry into the named partial.
Claim. For any assignment $a$ of six squared edge lengths of a tetrahedron, the map $t \mapsto \mathrm{CM}_3(a[3 \mapsto t])$ is differentiable at $t = a_3$, and its derivative equals the explicit partial $\partial \mathrm{CM}_3 / \partial a_3$ evaluated at $a$.
background
The Cayley-Menger polynomial $\mathrm{CM}_3$ is the explicit cubic in the six squared edge lengths of a tetrahedron whose vanishing is the classical $\mathbb{R}^3$-embeddability condition. Squared edges are typed as $\mathrm{Fin},6 \to \mathbb{R}$ with fixed indexing: edge $0=(0,1)$, $1=(0,2)$, $2=(0,3)$, $3=(1,2)$, $4=(1,3)$, $5=(2,3)$. This module supplies the six partials as closed-form polynomials and packages them as a gradient map $a \mapsto (\partial_i \mathrm{CM}_3(a))_i$.
The third partial (w.r.t. squared edge $(1,2)$) is the quadratic polynomial $2\bigl(a_2(a_0+a_1+a_4+a_5-a_2-a_3)-a_2 a_3+a_0 a_5+a_1 a_4-a_0 a_1-a_4 a_5\bigr)$. Formal $C^\infty$ smoothness of $\mathrm{CM}_3$ is already recorded in the polynomial module; the contribution here is the explicit first derivative under a single-coordinate update.
Upstream, the uniform theorem states that for every index $i$, $t \mapsto \mathrm{CM}_3(a.\mathrm{update}, i, t)$ has derivative equal to the $i$-th gradient entry at $t=a_i$.
proof idea
One-line wrapper. Instantiate the uniform result (derivative of any single-coordinate slice equals the corresponding gradient entry) at index $3$, then simpa unfolds the gradient match so the right-hand side becomes the named third partial.
why it matters
The module's purpose is to feed the Regge second-variation matrix $M_{ij}$, built from these partials by the chain rule through a conformal edge ansatz. Single-edge differentiability is the thin API between the closed-form gradient and any first-order variation argument.
This declaration is the coordinate-3 instance (edge $(1,2)$). The dependency graph currently shows no downstream users, but the sibling partials, the packaged gradient, and the polynomial Taylor identity sit beside it as the same API layer. In the Recognition geometry stack the target comparison is $M_{ij}$ versus face areas, a discrete-curvature step consistent with the forced spatial dimension $D=3$ (T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.