cm3_partial1
plain-language theorem explainer
Closed-form partial of the tetrahedron Cayley–Menger polynomial CM₃ with respect to the squared length of edge (0,2). Anyone assembling the CM₃ gradient, the linear pairing in the polynomial Taylor identity, or a one-edge HasDerivAt statement cites this. The body is the explicit cubic polynomial obtained by differentiating CM₃ in that coordinate.
Claim. Let $a:\{0,\ldots,5\}\to\mathbb{R}$ be the six squared edge lengths of a tetrahedron, with $a_1$ the squared length of edge $(0,2)$. Then $\partial\mathrm{CM}_3/\partial a_1$ is the real number $2\bigl(a_4(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_3-a_2 a_5\bigr)$.
background
The ambient object is the Cayley–Menger polynomial CM₃ in six squared edge lengths. In this codebase those lengths are packaged as SqEdges (maps Fin 6 → ℝ). The edge index convention is fixed: edge 0 = (0,1), 1 = (0,2), 2 = (0,3), 3 = (1,2), 4 = (1,3), 5 = (2,3). Upstream, CM₃ itself is the explicit cubic
$2\bigl(a_0 a_5(a_1+a_2+a_3+a_4-a_0-a_5)+a_1 a_4(a_0+a_2+a_3+a_5-a_1-a_4)+a_2 a_3(a_0+a_1+a_4+a_5-a_2-a_3)-\cdots\bigr)$.
This module’s job is not existence of derivatives (already in cm3_contDiff) but the six closed-form partials. Those partials feed the Regge second-variation comparison: the matrix $M_{ij}$ is built from them by the chain rule through a conformal edge ansatz.
proof idea
Definition, not a proved theorem. The right-hand side is the formal partial derivative of the cubic polynomial CM₃ with respect to coordinate $a_1$, written out after collecting like terms. No tactic proof; the expression is the content. Sibling definitions supply the other five partials by the same algebraic differentiation.
why it matters
This is the $i=1$ slot of the packaged gradient: cm3_grad a returns this value at index 1. It appears in the linear pairing cm3_linear a h = Σ (∂CM₃/∂a_i) h_i, which is the first-order term in the algebraic Taylor identity
cm3(a+h) = cm3 a + cm3_linear a h + cm3_quadratic a h + cm3_cubic h.
That identity specializes to the single-coordinate update formula used by the six HasDerivAt theorems; in particular hasDerivAt_cm3_partial1 states that the map $t \mapsto \mathrm{CM}_3(a[1\mapsto t])$ has derivative equal to this partial at $t=a_1$. Downstream, those derivatives are the raw material for the Regge Hessian comparison to face areas. No Recognition forcing-chain landmark (T5–T8, RCL, φ) is invoked here; the link is geometric, through discrete gravity / Regge calculus scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.