contDiffTwo_differentiable_deriv
plain-language theorem explainer
A map from the reals to the reals that is twice continuously differentiable has a differentiable first derivative. Workers reducing the T5 regularity seam in the Recognition cost functional cite this to justify passing differentiability through the derivative operator before invoking the d'Alembert ODE. The proof is a short term-mode reduction that rewrites the ContDiff 2 hypothesis via the successor relation and extracts the required differentiability component from Mathlib's contDiff_succ_iff_deriv.
Claim. If a function $Hf : ℝ → ℝ$ is twice continuously differentiable, then its first derivative is differentiable.
background
The module ContDiffReduction removes a central portion of the explicit T5 regularity seam. Its main advances are that a ContDiff ℝ 2 d'Alembert solution satisfies the ODE H'' = H, that the Recognition Composition Law plus normalization already force reciprocity, and that on the ContDiff surface the canonical reciprocal cost follows from normalization, composition, and calibration alone.
proof idea
The term proof copies the ContDiff hypothesis, rewrites 2 as 1 + 1, applies contDiff_succ_iff_deriv to unpack the structure, and extracts the differentiability of the derivative from the resulting components using the fact that 1 ≠ 0.
why it matters
This lemma is invoked directly by hasDerivAt_deriv_of_contDiffTwo, whose doc-comment states it differentiates the d'Alembert equation once in the second variable. It therefore participates in the ContDiff reduction for T5 described in the module documentation and supports the step from the Recognition Composition Law to the ODE H'' = H that precedes the J-uniqueness claim in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.