dAlembert_contDiff_smooth
plain-language theorem explainer
Continuous solutions to the d'Alembert equation H(t+u) + H(t-u) = 2 H(t) H(u) with H(0)=1 are infinitely differentiable. Analysts classifying functional equations or deriving ODEs in Recognition Science cost models cite this to justify C^∞ assumptions. The proof is a one-line wrapper that lifts the finite-order result via contDiff_infty.
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 $H$ is $C^∞$.
background
The module proves every continuous solution of the d'Alembert equation with H(0)=1 is C^∞, completing the Aczél classification into the constant 1, cosh(λt), or cos(λt). H here is the shifted cost H(x) = J(x) + 1, where the Recognition Composition Law reduces to this equation. Upstream dAlembert_contDiff_nat establishes C^n for every finite n via induction on the representation formula obtained from the antiderivative Φ and the fundamental theorem of calculus.
proof idea
One-line wrapper that applies dAlembert_contDiff_nat to obtain ∀n ContDiff n and then invokes contDiff_infty.mpr.
why it matters
It supplies the smoothness step for dAlembert_contDiff_top and dAlembert_classification. This closes the former H_AczelClassification hypothesis, confirming the 1966 Aczél result that all such H are C^∞. In the Recognition framework it ensures the cost function is smooth, supporting ODE derivations and the phi-ladder constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.