cm3_partial5
plain-language theorem explainer
Explicit closed form for the partial of the tetrahedron Cayley–Menger polynomial CM₃ with respect to the squared opposite edge ν = |e₂₃|². Anyone building the Regge second-variation matrix or a single-edge update of CM₃ cites this component. The body is a pure polynomial expression in the six squared lengths, obtained by symbolic differentiation of CM₃.
Claim. For squared edge lengths $a = (a_0,\ldots,a_5)\in\mathbb{R}^6$ of a tetrahedron, the partial derivative of the Cayley–Menger polynomial $\mathrm{CM}_3$ with respect to $a_5$ (the squared length of edge $(2,3)$) is $$\partial_{a_5}\mathrm{CM}_3(a) = 2\bigl(a_0(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_2-a_3 a_4\bigr).$$
background
The Cayley–Menger polynomial $\mathrm{CM}_3$ is a homogeneous cubic in the six squared edge lengths of a tetrahedron. Vanishing of $\mathrm{CM}_3$ is the classical embeddability condition in Euclidean 3-space; its value is proportional to $288 V^2$. Squared edges are packaged as a map $a:\mathrm{Fin},6\to\mathbb{R}$ with the fixed indexing edge $0=(0,1)$, $1=(0,2)$, $2=(0,3)$, $3=(1,2)$, $4=(1,3)$, $5=(2,3)$.
This module supplies the six partials $\partial\mathrm{CM}_3/\partial a_i$ as explicit polynomials. Formal $C^\infty$ differentiability of $\mathrm{CM}3$ is already in cm3_contDiff; the point here is the closed-form gradient that feeds the Regge second-variation matrix $M{ij}$ through the conformal edge ansatz and the chain rule.
Upstream, SqEdges is just the type of those six real coordinates. The continuum bridge and hinge-area structures later identify quadratic forms built from these partials with discrete Laplacians on the simplicial ledger.
proof idea
Definition, not a proof. The right-hand side is the result of differentiating the expanded Cayley–Menger polynomial in six variables with respect to the fifth coordinate and simplifying. No tactic or lemma is invoked; the expression is the closed form itself. Downstream theorems (Taylor identity, HasDerivAt for the single-coordinate slice) simply unfold this definition and match coefficients.
why it matters
This is the fifth component of the packaged gradient cm3_grad, and the $h_5$ term in the linear pairing cm3_linear. Both feed the algebraic Taylor identity
$$\mathrm{CM}_3(a+h)=\mathrm{CM}_3(a)+\langle\nabla\mathrm{CM}3(a),h\rangle+Q(a,h)+C(h),$$
which is the central theorem of the module. The single-coordinate corollary cm3_update_taylor and the calculus fact hasDerivAt_cm3_partial5 specialize that identity to edge 5, giving the exact first derivative used when only $\nu=|e{23}|^2$ is varied.
In the broader Recognition geometry stack these partials are the raw material for the Regge Hessian that is compared to face areas. Without the explicit $\partial/\partial a_5$ the chain-rule passage from edge conformal factors to second variation cannot be written as a closed polynomial. The declaration is pure scaffolding for that comparison; it does not itself assert any physical identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.