hasDerivAt_deriv_of_contDiffTwo
plain-language theorem explainer
If a map Hf from the reals to the reals is twice continuously differentiable, then its first derivative is differentiable at every point x with derivative value equal to the second derivative of Hf at x. Analysts reducing d'Alembert-type equations to ODEs under C^2 assumptions would cite this step in the T5 regularity reduction. The argument is a one-line wrapper that invokes differentiability of the first derivative from the ContDiff 2 hypothesis.
Claim. If $Hf : ℝ → ℝ$ is $C^2$, then for every $x ∈ ℝ$ the derivative map $Hf'$ is differentiable at $x$ and $(Hf')'(x) = Hf''(x)$.
background
The module ContDiffReduction removes an explicit regularity seam in the T5 J-uniqueness step of the forcing chain. It shows that any ContDiff ℝ 2 solution of the d'Alembert equation satisfies the ODE H'' = H, after which the Recognition Composition Law and normalization force reciprocity. The upstream lemma contDiffTwo_differentiable_deriv proves that ContDiff ℝ 2 Hf implies Differentiable ℝ (deriv Hf) by rewriting the ContDiff condition as contDiff_succ_iff_deriv and extracting the differentiability clause.
proof idea
One-line wrapper that applies contDiffTwo_differentiable_deriv h_diff to obtain Differentiable ℝ (deriv Hf), then uses the fact that every differentiable map is differentiable in the HasDerivAt sense at every point.
why it matters
The lemma supplies the differentiability step needed to differentiate the d'Alembert identity once more, feeding directly into the downstream theorem dAlembert_second_deriv_at_zero_of_contDiff. It advances the T5 reduction by letting the composition law and normalization alone produce the reciprocal cost on the ContDiff surface, closing one part of the regularity seam in the eight-tick octave construction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.