deriv_differentiableAt_of_contDiffAt_top
plain-language theorem explainer
If a real function is C^∞ at a point, its first derivative is differentiable there. Analysts working the nonlinear Regge second-variation chain cite this to pass ContDiffAt ⊤ down to DifferentiableAt on the scalar derivative. The proof is a short Mathlib chain-rule: ContDiffAt.fderiv_right, then ContinuousLinearMap.apply composed with the Fréchet derivative.
Claim. Let $f:\mathbb{R}\to\mathbb{R}$ and $x\in\mathbb{R}$. If $f$ is $C^\infty$ at $x$ (i.e. $\mathrm{ContDiffAt}\,\mathbb{R}\,\top\,f\,x$), then the map $y\mapsto f'(y)$ is differentiable at $x$.
background
The ambient module isolates the hard endpoint of the nonlinear Regge calculation: the second directional derivative of the Regge action at a flat vertex potential must equal the canonical incidence Hessian. Once that identity is in hand, the existing second-variation input package follows at once.
This lemma is pure real analysis scaffolding for that chain. Smoothness at a point (ContDiffAt of order $\top$) is stronger than mere differentiability: it supplies Fréchet derivatives of all orders in a neighborhood sense. The scalar derivative deriv f is the evaluation of the Fréchet derivative fderiv f on the unit direction $1\in\mathbb{R}$, so differentiability of deriv f reduces to differentiability of fderiv f composed with a continuous linear map.
No Recognition-specific cost or ladder structure enters here; the lemma is a reusable calculus fact used when deficit angles along a potential line must be differentiated twice at the flat point.
proof idea
First record the elementary inequality $1+1\le\top$ in WithTop ℕ∞ via WithTop.coe_le_coe and le_top. Apply ContDiffAt.fderiv_right to the given $C^\infty$ hypothesis to obtain ContDiffAt of order $1$ for fderiv ℝ f at $x$. Drop to DifferentiableAt of fderiv ℝ f by ContDiffAt.differentiableAt (order $1\ge 1$). Rewrite the goal as differentiability of $y\mapsto(\mathrm{fderiv},f,y),1$, then compose the continuous linear map ContinuousLinearMap.apply ℝ ℝ 1 (which is everywhere differentiable) with that Fréchet derivative.
why it matters
Downstream, deficitLineDeriv_differentiableAt_zero_of_flatConfiguration invokes this fact so that the first $t$-derivative of each edge deficit along a potential line is itself differentiable at $t=0$ when the background configuration is flat. That differentiability is a prerequisite for forming the second directional derivative of the nonlinear Regge action and matching it to the canonical incidence Hessian.
In the module's own framing, the target is not a new physical hypothesis but the exact endpoint of the second chain-rule calculation on the Regge action. This lemma is the calculus hinge that lets ContDiffAt smoothness of the action-along-a-line pass down to DifferentiableAt on the first deficit derivative, closing one technical gap in the nonlinear Hessian interface.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.