dAlembert_contDiff_smooth
plain-language theorem explainer
Any continuous real-valued function H with H(0) equal to one that satisfies the d'Alembert addition formula is infinitely differentiable. Analysts classifying functional-equation solutions or physicists tracing wave equations back to a cost function would cite this intermediate step. The proof is a one-line wrapper that lifts the finite-order differentiability result to C^∞ via the definition of smoothness as the limit over all orders.
Claim. Suppose $H:ℝ→ℝ$ is continuous, satisfies $H(0)=1$, and obeys the d'Alembert equation $H(t+u)+H(t-u)=2H(t)H(u)$ for all real $t,u$. Then $H$ is infinitely differentiable.
background
The module proves Aczél's smoothness theorem: every continuous solution to the d'Alembert equation with value one at zero is real analytic. The function H is the shifted cost H(x)=J(x)+1, where J satisfies the Recognition Composition Law; under this shift the law becomes the stated d'Alembert equation. The upstream result on finite differentiability orders establishes by induction and an integral representation that such an H is differentiable to every finite order.
proof idea
The argument is a one-line wrapper that applies the theorem establishing differentiability of every natural order and then uses the equivalence of infinite differentiability with the limit of all finite orders.
why it matters
This step supplies the infinite-differentiability ingredient required by the classification theorem that identifies all solutions as the constant one, a hyperbolic cosine, or a cosine, and by the top-level smoothness theorem. It completes the bootstrap phase described in the module documentation, which cites Aczél's 1966 lectures. In Recognition Science the analyticity of the cost-derived H supports the forcing chain from the functional equation to the eight-tick octave and three spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.