contDiffTwo_differentiable
plain-language theorem explainer
A real function that is twice continuously differentiable is differentiable. Workers on the T5 J-uniqueness step cite this when they reduce regularity assumptions inside the d'Alembert equation to reach the cosh form. The proof is a one-line wrapper that extracts differentiability directly from the ContDiff hypothesis.
Claim. If $f : ℝ → ℝ$ is twice continuously differentiable, then $f$ is differentiable.
background
The ContDiffReduction module removes explicit regularity seams from the T5 step of the forcing chain. ContDiff ℝ 2 means the function admits two continuous derivatives. The module shows that any such function obeying the d'Alembert relation satisfies the ODE H'' = H and therefore equals cosh after calibration.
proof idea
One-line wrapper that applies the differentiability extraction from ContDiff ℝ 2, using exact on h_diff.differentiable together with a decidable check that the order 2 is nonzero in the extended naturals.
why it matters
The lemma is invoked by dAlembert_cosh_solution_of_contDiff, which states that C² d'Alembert solutions are determined by calibration and equal cosh, and by dAlembert_first_deriv_of_contDiff. It therefore supplies the minimal regularity needed to advance T5 J-uniqueness (J(x) = cosh(log x) - 1) on the ContDiff surface using only normalization, the Recognition Composition Law, and calibration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.