phi_contDiff_succ
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.
claimIf $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 in Recognition Science
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.
scope and limits
- Does not assume the d'Alembert functional equation holds for H.
- Does not establish infinite differentiability or analyticity.
- Does not apply when H fails to be continuous.
- Does not produce explicit higher-order derivatives of Phi(H).
formal statement (Lean)
139private lemma phi_contDiff_succ (H : ℝ → ℝ) (h_cont : Continuous H) {n : ℕ}
140 (h : ContDiff ℝ (n : ℕ∞) H) : ContDiff ℝ ((n + 1 : ℕ) : ℕ∞) (Phi H) := by
proof body
Tactic-mode proof.
141 suffices ContDiff ℝ ((n : ℕ∞) + 1) (Phi H) by exact_mod_cast this
142 rw [contDiff_succ_iff_deriv]
143 exact ⟨phi_differentiable H h_cont,
144 fun h_omega => absurd h_omega (by exact_mod_cast WithTop.coe_ne_top),
145 by rwa [deriv_phi_eq H h_cont]⟩
146