contDiffTwo_differentiable
plain-language theorem explainer
A twice continuously differentiable real-valued function is differentiable. Researchers reducing the T5 regularity seam for J-uniqueness in Recognition Science cite this to license differentiation of d'Alembert solutions. The proof is a one-line wrapper that extracts differentiability from the ContDiff hypothesis.
Claim. If $Hf : ℝ → ℝ$ is twice continuously differentiable, then $Hf$ is differentiable.
background
The module ContDiff Reduction for T5 removes a central portion of the explicit T5 regularity seam. Its main advances are that a C² d'Alembert solution satisfies the ODE H'' = H and that the Recognition Composition Law plus normalization already force reciprocity. ContDiff ℝ 2 is the standard predicate for twice continuous differentiability over the reals; this lemma supplies the basic differentiability step required before derivative extraction in the module's d'Alembert arguments.
proof idea
One-line wrapper that applies the differentiability extraction from ContDiff ℝ 2.
why it matters
This lemma feeds dAlembert_cosh_solution_of_contDiff (C² d'Alembert solutions equal cosh under calibration) and dAlembert_first_deriv_of_contDiff (first differentiation of the d'Alembert equation). It advances the ContDiff reduction for T5 J-uniqueness by removing an explicit regularity seam in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.