phi_contDiff_succ
plain-language theorem explainer
The lemma shows that the integral operator applied to a continuous C^n function H yields a C^{n+1} result. It is cited during the induction that lifts continuous d'Alembert solutions to arbitrary finite smoothness. The proof reduces the successor claim via the standard characterization of ContDiff and discharges the conditions with the known differentiability and derivative formula for the integral.
Claim. Let $H : ℝ → ℝ$ be continuous. If $H$ is of class $C^n$, then the function $t ↦ ∫_0^t H(s) ds$ is of class $C^{n+1}$.
background
The module proves Aczél's theorem: any continuous solution of the d'Alembert equation $H(t+u)+H(t-u)=2H(t)H(u)$ with $H(0)=1$ is real analytic. Phi is the antiderivative operator defined by $Phi(H)(t) := ∫_0^t H(s) ds$. Upstream lemmas establish that Phi H is differentiable with derivative exactly H whenever H is continuous, and that H itself arises as the shifted cost $H(x)=J(x)+1$ satisfying the d'Alembert equation via the Recognition Composition Law.
proof idea
The tactic proof begins with a suffices that adjusts the natural-number indexing of the smoothness order. It rewrites the goal with contDiff_succ_iff_deriv. The three resulting subgoals are discharged by phi_differentiable, an absurdity argument ruling out the top element, and a rewrite using deriv_phi_eq.
why it matters
The lemma supplies the inductive step inside dAlembert_contDiff_nat, which in turn feeds the classification of solutions as cosh, cos or constant. It realizes the integration-bootstrap phase of Aczél's argument quoted in the module documentation. In the Recognition framework the result confirms that the cost-derived function H is smooth before the ODE $H''=cH$ is derived and the eight-tick octave structure is imposed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.