cm3_update_hessianForm
plain-language theorem explainer
One-coordinate update of the Cayley-Menger polynomial is exactly quadratic: base value plus gradient entry times t plus half the Hessian diagonal times t squared. Anyone packaging second variations of tetrahedral volume for Regge-type comparisons would cite this form. The proof rewrites the known single-coordinate polynomial Taylor identity, unfolds the Hessian diagonal and the vanishing cubic coefficient, then closes by ring.
Claim. For squared edge lengths $a$ of a tetrahedron, edge index $i\in\{0,\ldots,5\}$, and real $t$, $$\mathrm{CM}_3(a[i\mapsto a_i+t])=\mathrm{CM}_3(a)+(\nabla\mathrm{CM}_3(a))_i\,t+\tfrac12 H_{ii}(a)\,t^2,$$ where $H_{ii}(a)$ is the pure second partial of $\mathrm{CM}_3$ in the $i$-th squared edge. The cubic term in $t$ is identically zero.
background
The Cayley-Menger polynomial $\mathrm{CM}_3$ is the explicit polynomial in the six squared edge lengths of a tetrahedron whose vanishing encodes coplanarity (equivalently, zero volume). Squared edges are indexed by $\mathrm{Fin},6$ with the fixed convention edge $0=(0,1)$, $1=(0,2)$, $2=(0,3)$, $3=(1,2)$, $4=(1,3)$, $5=(2,3)$.
This module computes the six partials of $\mathrm{CM}3$ as closed-form polynomials and packages the single-coordinate Taylor identity. The gradient is the map sending each basepoint to its six partials. The Hessian diagonal is defined by $H{ii}(a)=2q_i(a)$, where $q_i$ is the quadratic coefficient of the one-variable expansion along coordinate $i$. Because $\mathrm{CM}_3$ is only degree two in each individual squared-edge coordinate, the cubic coefficient along any pure update is the zero function.
Upstream, the polynomial form already states $\mathrm{CM}_3(a.update,i,(a_i+t))=\mathrm{CM}_3(a)+(\nabla\mathrm{CM}_3)_i t+q_i t^2+c_i t^3$ with $c_i\equiv 0$.
proof idea
Algebraic repackaging of the single-coordinate polynomial Taylor identity. Rewrite via that identity, unfold the Hessian diagonal (twice the quadratic coefficient) and the cubic coefficient (identically zero), then finish with ring, which inserts the factor $1/2$ and drops the zero cubic term. No case split on the edge index is needed.
why it matters
The module exists to supply the explicit gradient and second-derivative data that feed the Regge second-variation matrix $M_{ij}$, later compared to face areas through the conformal edge ansatz. Formal $C^\infty$ differentiability of $\mathrm{CM}_3$ is already established elsewhere; the contribution here is the closed-form one-coordinate calculus. Hessian form is the natural packaging for second-variation work: the pure second partial along an edge is exactly what appears on the diagonal of a discrete Hessian. No downstream dependents are recorded yet, so the declaration sits at the tip of the derivative API, ready for the second-variation comparison. It does not itself touch the forcing chain (T0–T8) or the Recognition Composition Law; it is pure tetrahedral geometry infrastructure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.