hasDerivAt_deriv_of_contDiffTwo
plain-language theorem explainer
If Hf from reals to reals is twice continuously differentiable then its first derivative is differentiable at every real x with derivative equal to the second derivative of Hf at x. Analysts reducing d'Alembert equations under C2 assumptions cite this step when stripping explicit regularity from T5. The proof is a one-line wrapper that invokes the differentiability of the first derivative and applies the hasDerivAt property of differentiable maps.
Claim. If $Hf : ℝ → ℝ$ is $C^2$ then for every $x ∈ ℝ$ the map $Hf'$ is differentiable at $x$ and $(Hf')'(x) = Hf''(x)$.
background
The module ContDiffReduction removes an explicit regularity seam in the T5 step of the forcing chain. It shows that any $C^2$ solution of the d'Alembert equation satisfies the ODE $H'' = H$ and that the Recognition Composition Law plus normalization already force reciprocity. The upstream lemma contDiffTwo_differentiable_deriv states that ContDiff ℝ 2 Hf implies Differentiable ℝ (deriv Hf) by rewriting the ContDiff condition as ContDiff 1 of the first derivative and extracting the differentiability clause.
proof idea
One-line wrapper that applies contDiffTwo_differentiable_deriv to the ContDiff hypothesis, obtains Differentiable (deriv Hf), then uses the fact that every differentiable map has a derivative (differentiableAt.hasDerivAt).
why it matters
The lemma supplies the second-derivative existence needed by dAlembert_second_deriv_at_zero_of_contDiff, which differentiates the first-derivative identity at u=0. It therefore participates in the module's main advance: on the ContDiff surface the canonical reciprocal cost follows from normalization, composition, and calibration alone, closing part of the T5 J-uniqueness seam without additional regularity hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.