contDiffTwo_differentiable_deriv
If a real-valued function on the reals is twice continuously differentiable, then its first derivative is differentiable. Workers reducing explicit regularity seams in the T5 J-uniqueness step of the forcing chain cite this when passing from ContDiff ℝ 2 to the existence of the second derivative. The argument is a direct unwinding of the successor characterization of ContDiff classes.
claimIf $Hf : ℝ → ℝ$ is $C^2$, then the derivative $Hf'$ is differentiable.
background
The ContDiffReduction module removes a central portion of the explicit T5 regularity seam. It establishes that a ContDiff ℝ 2 d'Alembert solution satisfies the ODE H'' = H, after which the Recognition Composition Law plus normalization force reciprocity. The upstream theorem from PrimitiveDistinction converts seven independent axioms into four substantive structural conditions plus three definitional facts that the functional equation must obey. ContDiff ℝ 2 Hf asserts that Hf admits a continuous second derivative on the reals.
proof idea
The term proof copies the hypothesis, rewrites the index 2 as 1 + 1, applies the Mathlib lemma contDiff_succ_iff_deriv to obtain that the first derivative is ContDiff 1, and extracts differentiability of that derivative from the resulting structure via the second projection and the non-zero check on the index.
why it matters in Recognition Science
This lemma supplies the differentiability of the first derivative required by hasDerivAt_deriv_of_contDiffTwo, which differentiates the d'Alembert equation once in the second variable. It therefore contributes to the module claim that on the ContDiff surface the canonical reciprocal cost follows from normalization, composition, and calibration alone. In the framework it closes part of the T5 J-uniqueness seam (T5) by removing an explicit regularity hypothesis before the eight-tick octave and D = 3 are forced.
scope and limits
- Does not establish existence of the second derivative without the ContDiff ℝ 2 hypothesis.
- Does not extend the result to higher orders of differentiability.
- Does not address the functional equation or the J-cost itself.
- Does not apply to functions on domains other than the reals.
Lean usage
example {Hf : ℝ → ℝ} (h : ContDiff ℝ 2 Hf) : Differentiable ℝ (deriv Hf) := contDiffTwo_differentiable_deriv hformal statement (Lean)
31private lemma contDiffTwo_differentiable_deriv {Hf : ℝ → ℝ}
32 (h_diff : ContDiff ℝ 2 Hf) : Differentiable ℝ (deriv Hf) := by
proof body
Term-mode proof.
33 have h_diff' := h_diff
34 rw [show (2 : WithTop ℕ∞) = 1 + 1 from rfl] at h_diff'
35 rw [contDiff_succ_iff_deriv] at h_diff'
36 exact h_diff'.2.2.differentiable (by decide : (1 : WithTop ℕ∞) ≠ 0)
37