cm3_grad
plain-language theorem explainer
Packages the six closed-form partials of the tetrahedron Cayley–Menger polynomial into one gradient map on squared edge lengths. Anyone citing the single-edge update Taylor formula, the Hessian diagonal, or the uniform HasDerivAt API needs this object. The body is a Fin-6 case split that returns the matching partial at each edge index.
Claim. Define the gradient of the Cayley–Menger polynomial $\mathrm{CM}_3$ on squared edge lengths $a\in\mathbb{R}^6$ by $(\nabla\mathrm{CM}_3)(a)_i=\partial\mathrm{CM}_3/\partial a_i$ for $i=0,\ldots,5$, using the six explicit partial polynomials already computed for the tetrahedron edge set.
background
This module works in the squared-edge coordinates of a 3-simplex. With spatial dimension forced to $D=3$ (T8), a tetrahedron has six edges, indexed as $(0,1)$, $(0,2)$, $(0,3)$, $(1,2)$, $(1,3)$, $(2,3)$. The type of squared edge lengths is therefore a 6-tuple, and $\mathrm{CM}_3$ is the classical Cayley–Menger determinant polynomial in those six variables (volume-squared data).
Formal $C^\infty$ differentiability of $\mathrm{CM}_3$ is already available from the companion polynomial module. What this file supplies is the explicit algebraic gradient: six closed-form partial polynomials, then this packaging map that returns them as a single vector field on squared-edge space.
The local goal is the polynomial Taylor identity $\mathrm{CM}_3(a+h)-\mathrm{CM}_3(a)=\langle\nabla\mathrm{CM}_3(a),h\rangle+Q(a,h)+C(h)$, with $Q$ quadratic and $C$ cubic in $h$. That identity is the bridge from closed-form partials to Fréchet derivatives and to the Regge second-variation matrix via the conformal edge ansatz.
proof idea
Definition by exhaustive match on the edge index $i\in{0,\ldots,5}$. Each branch returns the corresponding named partial polynomial evaluated at the basepoint $a$. The impossible residue $n+6$ is discharged by omega on the Fin bound. No algebraic simplification occurs here; the content lives in the six partial definitions this map selects.
why it matters
This is the closed-form gradient object the rest of the derivative API quotes by name. Downstream, the single-coordinate Taylor corollary writes the linear term as $(\nabla\mathrm{CM}_3(a))_i,t$; the combined polynomial update and its Hessian rewrite do the same; and the uniform HasDerivAt theorem states that $t\mapsto\mathrm{CM}_3(a[i\mapsto t])$ has derivative $(\nabla\mathrm{CM}_3(a))_i$ at $t=a_i$, with the six per-edge corollaries obtained by simp unfolding.
In the broader Recognition geometry chain, these partials feed the Regge second-variation matrix $M_{ij}$ that is compared to face areas under the conformal edge ansatz. Because $D=3$ is forced (T8), the six-edge tetrahedron is the elementary cell; packaging its gradient is the concrete calculus step that makes that comparison algebraic rather than abstract.
No open scaffold sits on this definition itself; it is pure packaging of already-written partials.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.