cm3_linear
plain-language theorem explainer
Defines the first-order (linear-in-h) term of the Cayley–Menger polynomial CM₃ on six squared edge lengths: the Euclidean pairing of the explicit gradient with a perturbation h. Anyone expanding CM₃(a+h) or building the Regge second-variation matrix cites it. The body is the plain six-term sum of the closed-form partials times the components of h.
Claim. For squared-edge vectors $a,h\in\mathbb{R}^6$, the linear term is $\mathrm{CM}_3^{\mathrm{lin}}(a,h)=\sum_{i=0}^{5}(\partial_i\mathrm{CM}_3)(a)\,h_i$, i.e. the pairing $\langle\nabla\mathrm{CM}_3(a),h\rangle$ with the six explicit partial derivatives of the Cayley–Menger polynomial.
background
The module works with the Cayley–Menger polynomial $\mathrm{CM}_3$ of a tetrahedron, written as an explicit cubic polynomial in the six squared edge lengths $a_0,\ldots,a_5$ under the fixed edge labeling $(0,1),(0,2),(0,3),(1,2),(1,3),(2,3)$. Formal $C^\infty$ differentiability of $\mathrm{CM}_3$ is already available; this file supplies the closed-form partials.
Each $\partial_i\mathrm{CM}_3$ is itself a quadratic polynomial in the $a_j$ (e.g. the $a_0$-partial is $2(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)$). The linear term packages those six partials into the directional first-order piece of the algebraic Taylor expansion of $\mathrm{CM}_3(a+h)$.
Sibling pieces are the quadratic form in $(a,h)$ and a pure cubic remainder in $h$ alone; together they give an exact polynomial identity, not an asymptotic expansion.
proof idea
Pure definition: the value is the sum of the six already-defined partials evaluated at $a$, each multiplied by the matching component of $h$. No tactics or lemmas are invoked; it is the coordinate expression of the gradient pairing.
why it matters
This is the gradient term in the polynomial Taylor identity $\mathrm{CM}_3(a+h)=\mathrm{CM}_3(a)+\mathrm{CM}_3^{\mathrm{lin}}(a,h)+\mathrm{CM}_3^{\mathrm{quad}}(a,h)+\mathrm{CM}_3^{\mathrm{cub}}(h)$, which is the central theorem of the module. The single-coordinate update corollary restricts the same linear piece to a one-edge perturbation and feeds the six per-edge partial-derivative theorems.
Downstream, the Regge rigorous-foundation certificate records that $\mathrm{CM}3$ is fully explicit and that the conformal edge ansatz is smooth; the second-variation matrix $M{ij}$ compared to face areas is built from these partials via the chain rule. In the Recognition geometry stack this supplies the concrete differential calculus needed for discrete curvature and rigidity statements on tetrahedra, without leaving the polynomial algebra of squared lengths.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.