phi_contDiff_succ
plain-language theorem explainer
The lemma shows that if a continuous real-valued function H is of class C^n then its antiderivative Phi(H) is of class C^{n+1}. Analysts proving regularity bootstrap for continuous solutions of d'Alembert's functional equation cite this inductive step. The proof is a short tactic sequence that invokes the standard criterion contDiff_succ_iff_deriv together with the explicit derivative formula for Phi.
Claim. Let $H : ℝ → ℝ$ be continuous and of class $C^n$. Then the antiderivative defined by $Φ(H)(t) := ∫_0^t H(s) ds$ is of class $C^{n+1}$.
background
In the Aczél theorem module the auxiliary function Phi is defined by integration: Phi(H)(t) := ∫ from 0 to t of H(s) ds. The module proves 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^∞, via a regularity bootstrap that lifts continuity to C^1, then C^2, and so on. The present lemma supplies the inductive step of that bootstrap. It depends on the upstream fact that the derivative of Phi(H) equals H exactly (deriv_phi_eq) and on the differentiability of Phi under the continuity assumption on H.
proof idea
The tactic proof first rewrites the target via contDiff_succ_iff_deriv, reducing C^{n+1} to the existence of a continuous derivative. It supplies the required derivative by calling phi_differentiable (which uses the continuity of H) and then rewrites that derivative via deriv_phi_eq to recover the induction hypothesis that H itself is C^n. The remaining absurd branch disposes of the WithTop.coe_ne_top case.
why it matters
This lemma is invoked inside the induction of dAlembert_contDiff_nat, the theorem that converts a continuous d'Alembert solution into a C^n function for every finite n and therefore into a C^∞ function. It thereby completes the regularity half of the Aczél classification inside the Recognition Science cost algebra, where H is obtained from the J-cost by the shift H(x) = J(x) + 1. The result removes the former external hypothesis H_AczelClassification and supports the smoothness required for the phi-ladder mass formulas and the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.