hasDerivAt_deriv_of_contDiffTwo
plain-language theorem explainer
A twice continuously differentiable real-valued function has a first derivative that is itself differentiable at every point, with the derivative of the first derivative equaling the second derivative. Researchers reducing the d'Alembert equation to an ODE under C² regularity cite this step to justify passing differentiability through the first derivative operator. The proof is a one-line wrapper applying the upstream fact that ContDiff ℝ 2 implies differentiability of the first derivative.
Claim. Let $f : ℝ → ℝ$ be twice continuously differentiable. Then for every $x ∈ ℝ$, the derivative $f'$ is differentiable at $x$ with $(f')'(x) = f''(x)$.
background
The module ContDiff Reduction for T5 removes an explicit regularity seam in the T5 J-uniqueness argument. It shows that any ContDiff ℝ 2 solution to 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 states that ContDiff ℝ 2 Hf implies Differentiable ℝ (deriv Hf), obtained by rewriting the ContDiff condition via 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 any differentiable function is differentiable at a point to conclude HasDerivAt (deriv Hf) (deriv (deriv Hf) x) x.
why it matters
This lemma feeds the theorem dAlembert_second_deriv_at_zero_of_contDiff, which differentiates the first-derivative identity at u = 0 to relate H''(t) to H''(0). It advances the T5 reduction by removing the regularity seam, so that the Recognition Composition Law plus normalization alone force the reciprocal cost on the ContDiff surface. The step sits between the forcing chain T5 J-uniqueness and the eight-tick octave calibration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.