cm3_update_polyform
plain-language theorem explainer
Single-coordinate update of the Cayley–Menger cubic on six squared edge lengths expands exactly as a cubic polynomial in the step t: value plus gradient entry times t, plus explicit quadratic and cubic coefficients. Regge and discrete-geometry workers cite it for closed-form one-edge variations. The proof rewrites the Taylor identity and specializes the quadratic and cubic remainder terms to a pure single-edge perturbation.
Claim. For any assignment $a$ of six squared edge lengths and any edge index $i\in\{0,\ldots,5\}$ and step $t\in\mathbb{R}$, if $a^{(i,t)}$ denotes $a$ with the $i$-th coordinate replaced by $a_i+t$, then $\mathrm{CM}_3(a^{(i,t)})=\mathrm{CM}_3(a)+(\nabla\mathrm{CM}_3(a))_i\,t+Q_i(a)\,t^2+C_i\,t^3$, where $Q_i(a)$ is the quadratic single-edge coefficient and $C_i$ is the cubic single-edge coefficient (identically zero).
background
The module works with the Cayley–Menger polynomial $\mathrm{CM}_3$ on six squared edge lengths of a tetrahedron (edges ordered $(0,1),(0,2),(0,3),(1,2),(1,3),(2,3)$). Formal $C^\infty$ smoothness of $\mathrm{CM}_3$ is already available; the point here is an explicit algebraic gradient and Taylor calculus in edge coordinates.
The gradient $\mathrm{cm3_grad}$ packages the six closed-form partials $\partial\mathrm{CM}_3/\partial a_i$. The cubic single-edge coefficient is defined to be identically zero, because $\mathrm{CM}_3$ is only degree two in each individual squared-edge variable. Upstream single-perturbation lemmas identify the quadratic and cubic pieces of the full Taylor remainder when the displacement is supported on one coordinate.
Locally this sits in the pipeline that feeds the Regge second-variation matrix through the conformal edge ansatz: explicit one-coordinate polynomials are the bridge from the algebraic $\mathrm{CM}_3$ to derivative and Hessian APIs.
proof idea
Term-mode rewrite proof. First apply the single-coordinate Taylor identity for $\mathrm{CM}_3$ under Function.update, which already writes the updated value as base value plus linear, quadratic, and cubic remainder terms in $t$. Then rewrite those remainder terms by the two specialization lemmas that evaluate the quadratic and cubic forms on a pure single-edge perturbation, replacing them by cm3_quadratic_coeff i a * t^2 and cm3_cubic_coeff i * t^3. No case split or ring work is needed at this layer.
why it matters
This is the uniform one-edge update formula the module advertises: every restriction of $\mathrm{CM}_3$ to a single squared-edge coordinate is an explicit shifted cubic (in fact quadratic, since the cubic coefficient vanishes). Downstream, cm3_update_hessianForm rewrites the same identity with the diagonal Hessian entry in place of the quadratic coefficient, and hasDerivAt_cm3_grad reads off the closed-form partial as the derivative of $t\mapsto\mathrm{CM}_3(a.update,i,t)$ at the base point.
It also appears in the Regge rigorous-foundation certificate bundle, which packages polynomial explicitness, smoothness, regularity, and the Taylor identity for the discrete-gravity comparison of the second-variation matrix to face areas. Within Recognition geometry this is infrastructure for $D=3$ simplicial calculus rather than a forcing-chain step, but it is the algebraic hinge between $\mathrm{CM}_3$ and the Regge Hessian.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.