cm3GradientCLM
plain-language theorem explainer
Packages the Fréchet derivative of the tetrahedron Cayley-Menger polynomial CM₃ at a squared-edge point a as Mathlib's continuous linear map ℝ⁶ →L ℝ. Anyone assembling the Regge second-variation matrix from edge lengths cites this object. The body is the one-line Mathlib fderiv of CM₃ at a; coordinate partials elsewhere identify its directional pieces.
Claim. For squared edge lengths $a \in \mathbb{R}^{6}$ of a tetrahedron, let $\mathrm{CM}_{3}:\mathbb{R}^{6}\to\mathbb{R}$ be the Cayley-Menger polynomial. Define the continuous linear map $D\mathrm{CM}_{3}(a):\mathbb{R}^{6}\to\mathbb{R}$ to be the Fréchet derivative of $\mathrm{CM}_{3}$ at $a$.
background
Squared edge lengths of a tetrahedron are an element $a$ of $\mathrm{SqEdges}:=\mathrm{Fin},6\to\mathbb{R}$, with the fixed edge order $(0,1),(0,2),(0,3),(1,2),(1,3),(2,3)$. The scalar $\mathrm{CM}_{3}(a)$ is the explicit Cayley-Menger polynomial in those six squared lengths (the usual $288V^{2}$ determinant expanded as a cubic polynomial).
This module's job is the closed-form gradient of that polynomial: six partials $\partial\mathrm{CM}{3}/\partial a{i}$ as polynomials, plus the Taylor identity for $\mathrm{CM}{3}(a+h)$. Formal $C^{\infty}$ regularity of $\mathrm{CM}{3}$ is already in cm3_contDiff upstream; here one needs the derivative as a Mathlib continuous linear map so chain-rule and HasFDerivAt APIs apply.
The intended physics use is the Regge second-variation matrix $M_{ij}$, built from these partials via the chain rule through a conformal edge ansatz and compared to face areas.
proof idea
One-line definition: the value is Mathlib's fderiv ℝ cm3 a, i.e. the unique continuous linear map that is the Fréchet derivative of the polynomial map $\mathrm{CM}_{3}$ at the point $a$. No algebraic expansion is performed here; the six coordinate partials and the Taylor identity live in sibling definitions and supply the concrete action of this CLM on basis directions.
why it matters
Downstream, hasFDerivAt_cm3 unfolds this definition and quotes differentiability from cm3_contDiff to certify that the packaged map really is the Fréchet derivative. That certificate is the bridge from the explicit polynomial gradient to Mathlib's calculus stack.
In the broader Recognition geometry pipeline, the Regge Hessian that is later matched to area weights is assembled from $\partial\mathrm{CM}{3}/\partial a{i}$ by the chain rule on the conformal edge ansatz. Without a named continuous-linear-map derivative, those second-variation identities cannot be stated in the HasFDerivAt language already used for continuum limits on the lattice. The object is pure differential geometry scaffolding for the discrete-gravity side; it does not itself invoke the forcing chain (T5–T8) or the J-cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.