cm3_partial4
plain-language theorem explainer
Explicit partial of the Cayley–Menger cubic CM₃ with respect to the squared edge μ = ℓ₁₃² (index 4). Anyone building the CM gradient, the algebraic Taylor identity cm3(a+h), or per-edge HasDerivAt lemmas cites this closed form. It is a direct polynomial expression obtained by differentiating the expanded six-edge CM polynomial in a₄.
Claim. For squared edge lengths $a:\{0,\ldots,5\}\to\mathbb{R}$ of a tetrahedron, the partial $\partial\mathrm{CM}_3/\partial a_4$ is the quadratic polynomial $2\bigl(a_1(a_0+a_2+a_3+a_5-a_1-a_4)-a_1 a_4+a_0 a_5+a_2 a_3-a_0 a_2-a_3 a_5\bigr)$, where $a_4=\mu$ is the squared length of edge $(1,3)$.
background
The ambient object is the Cayley–Menger polynomial cm3 on six squared edge lengths of a tetrahedron. In RS geometry it is written as an explicit cubic in $a_0,\ldots,a_5$ and is proportional to $288 V^2$ for an embedded tetrahedron. Squared edges are packaged as SqEdges := Fin 6 → ℝ with the fixed labeling: edge 0=(0,1), 1=(0,2), 2=(0,3), 3=(1,2), 4=(1,3), 5=(2,3). Thus index 4 is μ = ℓ₁₃².
This module’s job is to expose the six partials ∂CM₃/∂aᵢ as closed polynomial maps, then assemble the gradient, the linear pairing ⟨∇cm3,h⟩, and the exact algebraic Taylor identity cm3(a+h)=cm3 a + linear + quadratic + cubic. Formal C^∞ differentiability of cm3 is already in cm3_contDiff; here one only needs the explicit formulae that feed the Regge second-variation matrix via the conformal edge ansatz.
proof idea
Pure definition, not a proved theorem. The body is the result of symbolically differentiating the expanded cubic cm3 with respect to the fourth coordinate a₄ and simplifying. No tactics or upstream lemmas are invoked at the definition site; correctness is discharged later when cm3_taylor unfolds all six partials and checks the polynomial identity by ring-style expansion, and when hasDerivAt_cm3_partial4 quotes the packaged gradient.
why it matters
This is one of the six coordinate partials that make the closed-form gradient cm3_grad and the linear term cm3_linear. Those feed the central algebraic Taylor identity cm3_taylor and its single-coordinate corollary cm3_update_taylor, which in turn power the six HasDerivAt lemmas (here hasDerivAt_cm3_partial4).
In the broader Recognition geometry stack the Regge second-variation matrix M_{ij} is built from these partials by the chain rule through the conformal edge ansatz; comparing M_{ij} to face areas is the geometric target of the module. The declaration is scaffolding for that comparison rather than a physics claim by itself: it supplies the μ-component of ∇CM₃ in D=3 tetrahedral geometry (T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.