phi_contDiff_succ
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not derive the explicit closed-form solutions (constant, cosh, or cos).
- Does not apply when H fails to be continuous.
- Does not treat vector-valued or higher-dimensional analogues of the equation.
- Does not supply explicit derivative bounds or growth estimates.
formal statement (Lean)
197private lemma phi_contDiff_succ (H : ℝ → ℝ) (h_cont : Continuous H) {n : ℕ}
198 (h : ContDiff ℝ (n : ℕ∞) H) : ContDiff ℝ ((n + 1 : ℕ) : ℕ∞) (Phi H) := by
proof body
Tactic-mode proof.
199 suffices ContDiff ℝ ((n : ℕ∞) + 1) (Phi H) by exact_mod_cast this
200 rw [contDiff_succ_iff_deriv]
201 exact ⟨phi_differentiable H h_cont,
202 fun h_omega => absurd h_omega (by exact_mod_cast WithTop.coe_ne_top),
203 by rwa [deriv_phi_eq H h_cont]⟩
204
205/-- Core bootstrap: continuous d'Alembert → C^n for all n. -/