contDiffTwo_differentiable
A real-valued function that is twice continuously differentiable is differentiable. Researchers reducing regularity assumptions in d'Alembert solutions for Recognition Science T5 J-uniqueness cite this when stripping explicit C² seams. The proof is a one-line wrapper that extracts differentiability directly from the ContDiff hypothesis.
claimIf $f : ℝ → ℝ$ is twice continuously differentiable, then $f$ is differentiable.
background
The ContDiffReduction module removes a central portion of the explicit T5 regularity seam. It shows that a ContDiff ℝ 2 d'Alembert solution satisfies the ODE H'' = H, with the Recognition Composition Law plus normalization forcing reciprocity. ContDiff ℝ 2 Hf denotes twice continuous differentiability of Hf : ℝ → ℝ.
proof idea
The proof is a one-line wrapper that applies the differentiability extraction from ContDiff ℝ 2 via h_diff.differentiable, using a decidable check that the order 2 is nonzero.
why it matters in Recognition Science
This lemma feeds dAlembert_cosh_solution_of_contDiff (C² d'Alembert solutions equal cosh by calibration) and dAlembert_first_deriv_of_contDiff. It advances the T5 forcing chain by removing regularity seams, consistent with J-uniqueness and the eight-tick octave.
scope and limits
- Does not establish differentiability for functions below C² regularity.
- Does not supply explicit derivative expressions or higher-order results.
- Does not address domains other than the reals.
Lean usage
have h_diff : Differentiable ℝ Hf := contDiffTwo_differentiable h_contDiffformal statement (Lean)
27private lemma contDiffTwo_differentiable {Hf : ℝ → ℝ}
28 (h_diff : ContDiff ℝ 2 Hf) : Differentiable ℝ Hf := by
proof body
One-line wrapper that applies exact.
29 exact h_diff.differentiable (by decide : (2 : WithTop ℕ∞) ≠ 0)
30