phi_contDiff_succ
plain-language theorem explainer
The lemma shows that if a continuous real function H is C^n then its antiderivative Phi(H) is C^{n+1}. It is invoked in the inductive step of the bootstrap that upgrades continuous solutions of d'Alembert's equation to C^infty. The proof reduces the claim via contDiff_succ_iff_deriv, invokes phi_differentiable for the base differentiability, and substitutes the explicit derivative supplied by deriv_phi_eq.
Claim. If $H : ℝ → ℝ$ is continuous and of class $C^n$, then the antiderivative $Φ(H)$ defined by $Φ(H)(t) = ∫_0^t H(s) ds$ is of class $C^{n+1}$.
background
The module establishes Aczél's smoothness theorem: any continuous solution of the d'Alembert equation $H(t+u) + H(t-u) = 2 H(t) H(u)$ with $H(0)=1$ is real analytic. Phi is the antiderivative operator $Φ(H)(t) := ∫_0^t H(s) ds$. Upstream, H is the shifted cost function $H(x) = J(x) + 1$ that converts the Recognition Composition Law into the standard d'Alembert form. The sibling lemmas phi_differentiable and deriv_phi_eq supply the facts that Phi(H) is differentiable with derivative exactly H when H is merely continuous.
proof idea
The tactic proof first rewrites the target via contDiff_succ_iff_deriv. It then supplies the three conjuncts: phi_differentiable gives differentiability of Phi(H), an absurd rules out the WithTop top case, and rwa substitutes the derivative identity from deriv_phi_eq.
why it matters
This supplies the inductive step inside dAlembert_contDiff_nat (both the proof and theorem versions), which upgrades continuous d'Alembert solutions to C^n for every finite n. The result therefore closes the integration-bootstrap half of Aczél's theorem as described in the module documentation. Within Recognition Science it underwrites the C^infty regularity presupposed by the phi-ladder mass formula and the eight-tick octave construction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.