hasDerivAt_deriv_of_contDiffTwo
If a real-valued function Hf is twice continuously differentiable, then its first derivative is differentiable at every point x with derivative equal to the second derivative of Hf at x. Analysts reducing d'Alembert-type functional equations to ODEs under smoothness hypotheses cite this step when passing from C^2 assumptions to pointwise derivative identities. The proof is a one-line wrapper that invokes the differentiability of the derivative for C^2 functions.
claimLet $H_f : ℝ → ℝ$ be twice continuously differentiable. Then for every real number $x$, the derivative of $H_f'$ exists at $x$ and equals $H_f''(x)$.
background
The ContDiffReduction module removes explicit regularity seams from the T5 uniqueness argument. ContDiff ℝ 2 Hf denotes twice continuous differentiability of Hf. The upstream lemma contDiffTwo_differentiable_deriv shows that ContDiff ℝ 2 Hf implies Differentiable ℝ (deriv Hf) by rewriting the ContDiff condition as a successor and extracting the differentiability clause.
proof idea
One-line wrapper that applies contDiffTwo_differentiable_deriv to obtain Differentiable ℝ (deriv Hf), then uses the general fact that any differentiable map admits a derivative at each point.
why it matters in Recognition Science
This lemma supplies the differentiability step needed for dAlembert_second_deriv_at_zero_of_contDiff, which relates second derivatives under the d'Alembert identity. It advances the T5 J-uniqueness reduction by allowing the Recognition Composition Law plus normalization to force reciprocity on the C^2 surface without additional regularity hypotheses.
scope and limits
- Does not assume or prove any functional equation such as d'Alembert.
- Does not establish existence or uniqueness of solutions.
- Does not extend to functions with lower regularity than C^2.
- Does not address higher-order derivatives beyond the second.
formal statement (Lean)
38private lemma hasDerivAt_deriv_of_contDiffTwo {Hf : ℝ → ℝ}
39 (h_diff : ContDiff ℝ 2 Hf) (x : ℝ) :
40 HasDerivAt (deriv Hf) (deriv (deriv Hf) x) x := by
proof body
Term-mode proof.
41 exact (contDiffTwo_differentiable_deriv h_diff).differentiableAt.hasDerivAt
42
43/-- Differentiate the d'Alembert equation once in the second variable. -/