cm3_partial0
plain-language theorem explainer
Explicit partial derivative of the Cayley-Menger cubic CM₃ with respect to the squared length of tetrahedron edge (0,1), written as a quadratic polynomial in the six squared edge lengths. Cited by anyone building the CM₃ gradient, the algebraic Taylor identity, or the Regge second-variation matrix via the conformal edge ansatz. The body is the closed-form result of differentiating the expanded CM₃ polynomial in the first coordinate.
Claim. For squared edge lengths $a=(a_0,\ldots,a_5)$ of a tetrahedron, $\partial\mathrm{CM}_3/\partial a_0$ equals $2\bigl(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\bigr)$, where $a_0$ is the squared length of edge $(0,1)$.
background
The Cayley-Menger polynomial $\mathrm{CM}_3$ is the explicit cubic in six squared edge lengths whose value is proportional to the squared volume of a tetrahedron. Squared edges are indexed on $\mathrm{Fin},6$ by the fixed convention edge $0=(0,1)$, $1=(0,2)$, $2=(0,3)$, $3=(1,2)$, $4=(1,3)$, $5=(2,3)$; the type of such assignments is abbreviated $\mathrm{SqEdges}$.
This module records the six partials $\partial\mathrm{CM}_3/\partial a_i$ as closed polynomial maps so that the gradient, the algebraic Taylor expansion $\mathrm{CM}_3(a+h)=\mathrm{CM}_3(a)+\langle\nabla\mathrm{CM}_3(a),h\rangle+Q+C$, and single-coordinate update formulae can be stated without on-the-fly symbolic differentiation. Upstream smoothness ($C^\infty$) of $\mathrm{CM}_3$ is already available; the contribution here is the explicit gradient.
The parent polynomial $\mathrm{cm3}$ expands as a sum of three cubic blocks minus four triple products; the present definition is the formal $\partial/\partial a_0$ of that expansion.
proof idea
Definition only: the right-hand side is the collected formal partial of the expanded $\mathrm{cm3}$ polynomial with respect to coordinate $a_0$. No tactics or lemmas are invoked; the expression is the closed form itself. Downstream theorems later certify that this formula coincides with the analytic derivative along the $0$-th edge update.
why it matters
Forms the $0$-component of the packaged gradient $\mathrm{cm3_grad}$, enters the linear pairing $\mathrm{cm3_linear}$, and is unfolded in the polynomial Taylor identity $\mathrm{cm3_taylor}$ and the single-coordinate corollary $\mathrm{cm3_update_taylor}$. Those identities power the uniform $\mathrm{HasDerivAt}$ statements (including the specialized $\mathrm{hasDerivAt_cm3_partial0}$) that certify the closed form is the true derivative of $t\mapsto\mathrm{CM}_3(a.update,0,t)$.
In the broader stack the gradient feeds the Regge second-variation matrix $M_{ij}$ compared to face areas through the conformal edge ansatz. That calculus layer sits under discrete-curvature and gluing analysis (including Gap-2 style edge complexes). The module doc states the point directly: formal differentiability is already known; this supplies the explicit closed-form gradient.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.