cm3_taylor
plain-language theorem explainer
The Cayley-Menger polynomial CM₃ on six squared edge lengths expands exactly as value plus linear form plus quadratic form plus cubic remainder under an arbitrary edge perturbation. Anyone assembling the Regge second-variation matrix or single-edge update formulas cites this algebraic identity. The proof unfolds the explicit polynomial definitions of the gradient pairing, quadratic piece, and cubic remainder, then closes by ring arithmetic.
Claim. For squared-edge vectors $a,h\in\mathbb{R}^6$, the Cayley-Menger polynomial satisfies $\mathrm{CM}_3(a+h)=\mathrm{CM}_3(a)+L_a(h)+Q_a(h)+C(h)$, where $L_a(h)=\sum_{i=0}^{5}(\partial_i\mathrm{CM}_3)(a)\,h_i$ is the gradient pairing, $Q_a$ is the quadratic form in $h$ with coefficients depending on $a$, and $C$ is the cubic form depending only on $h$.
background
This module works in the six-dimensional space of squared edge lengths of a tetrahedron (type SqEdges), with the fixed edge indexing of CayleyMengerPolynomial: edges 0–2 from vertex 0 to 1,2,3 and edges 3–5 the opposite face. The scalar cm3 is the classical Cayley-Menger polynomial whose vanishing (with sign) encodes tetrahedron volume.
The six partials cm3_partial0–cm3_partial5 are written as explicit cubic polynomials in those squared lengths; their pairing against a perturbation $h$ is cm3_linear. The quadratic and cubic pieces cm3_quadratic and cm3_cubic complete the homogeneous decomposition of the degree-3 polynomial. Formal $C^\infty$ differentiability of cm3 is already available upstream as cm3_contDiff; the present module supplies the closed-form gradient and the exact Taylor identity rather than an abstract remainder.
The local goal is the algebraic expansion that later feeds the conformal-edge chain rule into the Regge second-variation matrix $M_{ij}$.
proof idea
Purely algebraic one-shot proof. Unfold cm3 together with the six partials, the linear pairing, the quadratic form, and the cubic remainder into their explicit polynomial expressions in the six coordinates of $a$ and $h$. The resulting equality of two multivariate polynomials is discharged by the ring tactic; no analytic remainder estimate or induction is required because cm3 is globally cubic.
why it matters
This is the central theorem of the module: the polynomial Taylor identity that exposes gradient, quadratic term, and cubic remainder of CM₃ directly. Downstream, cm3_update_taylor specialises it to a single-coordinate bump singlePerturb i t, which is exactly the 1-D restriction used to certify the six per-edge partial-derivative theorems.
It is also wired into the certificate reggeRigorousFoundationCert as the field cm3_taylor_identity, alongside smoothness (cm3_contDiff) and the explicit polynomial form. That certificate is the formal backbone for comparing the Regge second-variation matrix $M_{ij}$ to face areas under the conformal edge ansatz. In the broader Recognition chain the ambient dimension is forced to $D=3$ (T8) with the eight-tick octave (T7), so tetrahedral Cayley-Menger geometry is the native spatial setting; this identity is the concrete calculus step that makes the Regge Hessian computable inside that setting.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.