dAlembert_contDiff_nat
plain-language theorem explainer
Continuous solutions H to the d'Alembert equation H(t+u) + H(t-u) = 2 H(t) H(u) with H(0)=1 belong to C^n for every natural number n. Analysts working on functional equations cite this bootstrap when lifting regularity. The argument obtains a nonzero integral shift δ, invokes the representation formula expressing H via its antiderivative Phi, and lifts differentiability order by induction using composition and subtraction.
Claim. Let $H : ℝ → ℝ$ be continuous, satisfy $H(0) = 1$, and obey the d'Alembert equation $H(t+u) + H(t-u) = 2 H(t) H(u)$ for all real $t,u$. Then for every natural number $n$, $H$ is of class $C^n$.
background
In the Cost.AczelProof module the d'Alembert equation arises as the image of the Recognition Composition Law under the shifted cost map H(x) = J(x) + 1 from CostAlgebra. The auxiliary antiderivative Phi(H,t) is the definite integral from 0 to t of H(s) ds. The supporting lemma exists_integral_ne_zero produces a δ > 0 with Phi(H,δ) ≠ 0, while representation_formula recovers the explicit formula H(t) = (Phi(t+δ) - Phi(t-δ)) / (2 Phi(δ)). The companion lemma phi_contDiff_succ states that if H is C^n then Phi(H) is C^{n+1}. The module_doc frames this as Phase 1 of Aczél's smoothness theorem: continuous solutions are shown to be C^∞ before the ODE H'' = c H is derived.
proof idea
The term proof first obtains δ and the representation formula via exists_integral_ne_zero and representation_formula. It then performs induction on n. The base case n=0 invokes contDiff_zero from the given continuity. In the successor step phi_contDiff_succ supplies C^{n+1} regularity for Phi(H); the proof composes with the translations t ↦ t+δ and t ↦ t-δ, subtracts the two results, and divides by the nonzero constant 2 Phi(δ) to recover the required C^{n+1} class for H.
why it matters
This finite-order bootstrap feeds directly into dAlembert_contDiff_smooth, which concludes ContDiff ℝ smooth H, and is re-used in the AczelTheorem module for the same purpose. It supplies the integration step of Aczél's theorem referenced in the module_doc, ensuring that any continuous H arising from the J-cost via the Recognition Composition Law is regular enough for the subsequent ODE derivation H'' = c H. In the broader Recognition Science setting the result guarantees that the eight-tick octave and phi-ladder constructions rest on sufficiently smooth functions before mass formulas or the alpha band are extracted.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.