hasFDerivAt_cm3
plain-language theorem explainer
At every squared-edge configuration of a tetrahedron, the continuous linear map assembled from the six partials of the Cayley-Menger polynomial is its Fréchet derivative. Anyone wiring the Regge second-variation matrix to face areas through the conformal edge ansatz would cite this. The proof is a one-line appeal to C¹ smoothness of the polynomial, with no coordinate expansion.
Claim. For every squared-edge vector $a \in \mathbb{R}^6$ of a tetrahedron, the Cayley-Menger polynomial $\mathrm{CM}_3:\mathbb{R}^6\to\mathbb{R}$ is Fréchet differentiable at $a$, and its derivative equals the continuous linear map $\mathrm{d}\mathrm{CM}_3(a)$ obtained from Mathlib's Fréchet derivative of $\mathrm{CM}_3$ at $a$.
background
The Cayley-Menger polynomial $\mathrm{CM}_3$ is the explicit cubic in the six squared edge lengths of a tetrahedron; it encodes (a multiple of) the squared volume and vanishes on Euclidean-embeddable length data. The domain type is squared edges indexed by $\mathrm{Fin},6$, with the fixed convention edge $0=(0,1)$, $\ldots$, edge $5=(2,3)$.
This module's job is the closed-form gradient and the polynomial Taylor identity for $\mathrm{CM}_3(a+h)$. Smoothness is already settled upstream: $\mathrm{CM}_3$ is $C^n$ for every $n$, built by composing Mathlib ContDiff rules for sums, products, and coordinate evaluations. The gradient continuous linear map at $a$ is defined simply as Mathlib's fderiv of $\mathrm{CM}_3$ at $a$; the present result asserts that this object satisfies the HasFDerivAt predicate.
proof idea
Unfold the gradient continuous-linear-map definition (it is literally fderiv ℝ cm3 a). Invoke the upstream theorem that $\mathrm{CM}_3$ is $C^1$, specialize to order one, pass to differentiability at the point $a$, and apply Mathlib's conversion from differentiability to HasFDerivAt. No partial-formula algebra appears; existence and identification with fderiv are inherited from $C^1$ smoothness.
why it matters
The module states that the Regge second-variation matrix $M_{ij}$ ultimately compared to face areas is built from these partials via the chain rule through the conformal edge ansatz. Pinning the packaged gradient map as the genuine Fréchet derivative licenses all first-order calculus (directional derivatives, chain rule, Taylor remainder) without re-proving differentiability at each call site. The sibling API (coordinate partials, gradient vector, quadratic/cubic Taylor pieces, single-coordinate updates) is designed to rest on this identification. In the Recognition geometry stack this sits under discrete volume/curvature variation for tetrahedra, consistent with the forcing-chain claim $D=3$ (T8). No downstream theorems are recorded yet in the dependency graph.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.