cm3_update_taylor
plain-language theorem explainer
When a single squared edge length of a tetrahedron is shifted by t, the Cayley–Menger value expands exactly as value plus gradient component times t, plus the quadratic and cubic forms of that one-edge perturbation. Anyone deriving the six closed-form partials ∂CM₃/∂aᵢ cites this. The proof specialises the full multivariable Taylor identity by identifying the update with a singlePerturb vector and collapsing the linear term to the i-th gradient entry.
Claim. Let $a \in \mathbb{R}^6$ be the six squared edge lengths of a tetrahedron and fix an edge index $i \in \{0,\ldots,5\}$ and a real shift $t$. Writing $a^{(i,t)}$ for the vector that equals $a$ except at coordinate $i$, where it is $a_i+t$, one has $$\mathrm{CM}_3(a^{(i,t)}) = \mathrm{CM}_3(a) + (\nabla\mathrm{CM}_3(a))_i\, t + Q(a; e_i t) + C(e_i t),$$ where $Q$ and $C$ are the quadratic and cubic homogeneous parts of the Cayley–Menger polynomial and $e_i t$ is the perturbation supported only on edge $i$.
background
The Cayley–Menger polynomial $\mathrm{CM}_3$ is a cubic polynomial in the six squared edge lengths of a tetrahedron; its vanishing (up to a constant factor) characterises flat embedding in $\mathbb{R}^3$. Edges are indexed as in the companion polynomial module: $0=(0,1)$, $1=(0,2)$, $2=(0,3)$, $3=(1,2)$, $4=(1,3)$, $5=(2,3)$. The ambient type SqEdges is simply $\mathrm{Fin},6\to\mathbb{R}$.
This module’s job is the explicit gradient $\partial\mathrm{CM}3/\partial a_i$ as polynomial functions of those lengths. Formal $C^\infty$ differentiability is already known; here one needs closed forms because the Regge second-variation matrix $M{ij}$ is built from these partials via the chain rule through a conformal edge ansatz.
The parent identity is the full multivariable Taylor expansion of $\mathrm{CM}_3(a+h)$ into constant, linear (gradient), quadratic, and cubic pieces. The present statement is the one-dimensional restriction of that expansion along a single coordinate axis.
proof idea
First prove that adding the sparse vector singlePerturb i t (value $t$ at index $i$, zero elsewhere) is definitionally the same as Function.update a i (a i + t), by a pointwise case split on whether the coordinate equals $i$.
Apply the full Taylor identity cm3_taylor a (singlePerturb i t) and transport along that equality. It remains only to identify the linear form: unfold cm3_linear, cm3_grad, and singlePerturb, then fin_cases on the six values of $i$ and simplify against the six explicit partial polynomials. A final linarith absorbs the rewritten linear term into the claimed right-hand side.
why it matters
This is the bridge from the abstract multivariable Taylor identity to the concrete one-edge update used everywhere downstream. Its sole direct consumer is cm3_update_polyform, which rewrites the quadratic-plus-cubic remainder as $\alpha(a,i),t^2+\beta(i),t^3$ with explicit coefficient polynomials; those coefficients then yield the six partial-derivative theorems uniformly.
In the broader Recognition geometry stack, the partials feed the Regge second-variation matrix that is compared to face areas under the conformal edge ansatz. That comparison sits inside the discrete-geometry side of the forcing chain (spatial dimension $D=3$ already forced at T8), so closed-form control of $\nabla\mathrm{CM}_3$ is load-bearing rather than decorative. The declaration itself is fully proved; it closes no scaffold, but it is the last algebraic step before the per-edge partial API.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.