contDiffTwo_differentiable_deriv
plain-language theorem explainer
If a real function is twice continuously differentiable then its first derivative is differentiable. This supports the ContDiff reduction for T5 by stripping an explicit regularity seam before the d'Alembert-to-ODE step. The term proof rewrites ContDiff 2 via the Mathlib successor equivalence and extracts the differentiable part of the resulting C^1 structure.
Claim. If $f : ℝ → ℝ$ is twice continuously differentiable, then its derivative $f'$ is differentiable over $ℝ$.
background
The Cost.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 and that the Recognition Composition Law plus normalization already force reciprocity, so the canonical reciprocal cost follows from normalization, composition, and calibration alone. The upstream result from PrimitiveDistinction reduces seven independent axioms to four substantive structural conditions plus three definitional facts.
proof idea
Term-mode proof. It copies the hypothesis, rewrites the WithTop level 2 as 1 + 1, applies contDiff_succ_iff_deriv to obtain ContDiff 1 of the derivative, then extracts the differentiable component via the second projection and a decidable non-zero check.
why it matters
The lemma is used directly by hasDerivAt_deriv_of_contDiffTwo to obtain the first derivative of the derivative at a point, which in turn supports differentiation of the d'Alembert equation. It fills a step in the T5 J-uniqueness reduction inside the forcing chain (T5 to T8) by removing one regularity seam before the ODE and reciprocity arguments. No open scaffolding remains at this node.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.