phi_differentiable
plain-language theorem explainer
Continuous functions H admit an antiderivative Phi that is differentiable on the reals. Analysts performing regularity bootstrap for d'Alembert solutions in the Recognition Science cost setting cite this step. The proof is a one-line term that extracts differentiability from the HasDerivAt property of the integral.
Claim. If $H : ℝ → ℝ$ is continuous, then the antiderivative $Φ(t) := ∫_0^t H(s) ds$ is differentiable on $ℝ$.
background
The module establishes that every continuous solution of the d'Alembert equation $H(t+u) + H(t-u) = 2 H(t) H(u)$ with $H(0) = 1$ is $C^∞$. Phi is the antiderivative $Φ(t) := ∫_0^t H(s) ds$. Upstream, the shifted cost $H(x) = J(x) + 1 = ½(x + x^{-1})$ converts the Recognition Composition Law into this d'Alembert form. The companion lemma phi_hasDerivAt states that HasDerivAt (Phi H) (H t) t holds by the fundamental theorem for interval integrals.
proof idea
One-line term wrapper: for each t the expression (phi_hasDerivAt H h_cont t).differentiableAt directly yields the Differentiable predicate from the HasDerivAt fact already proved for the integral.
why it matters
The lemma supplies the first regularity lift in the bootstrap chain that removes the former H_AczelClassification axiom. It is invoked by phi_contDiff_succ to obtain ContDiff of order n+1 for Phi and by exists_integral_ne_zero to locate a nonzero integral value. The step sits inside the cost-algebra setting where H derives from the J-cost and supports the full Aczél classification into cosh, cos, or constant solutions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.