dAlembert_contDiff_top
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. Researchers in functional equations and Recognition Science cost algebra cite this to remove any smoothness hypothesis from the Aczél classification. The proof first obtains C^∞ regularity by bootstrap from continuity, derives the ODE H'' = c H, then classifies solutions by the sign of c = H''(0) and invokes uniqueness for the resulting differential equations.
Claim. Let $H : ℝ → ℝ$ be continuous with $H(0) = 1$ and satisfy $H(t+u) + H(t-u) = 2 H(t) H(u)$ for all real $t,u$. Then $H$ is infinitely differentiable.
background
In the cost algebra, H is the shifted cost function defined by H(x) = J(x) + 1, where J satisfies the Recognition Composition Law; this substitution converts the RCL into the additive d'Alembert equation H(t+u) + H(t-u) = 2 H(t) H(u). The module proves that every continuous solution with H(0)=1 is C^∞, recovering the three classical cases: the constant 1, cosh(λ t), and cos(λ t). Upstream results supply the initial smoothness bootstrap (dAlembert_contDiff_smooth) and the ODE derivation (dAlembert_to_ODE_general), which states that H''(t) = H''(0) · H(t) once H is C².
proof idea
The proof invokes dAlembert_contDiff_smooth to obtain ContDiff ℝ smooth H, extracts a C² version, and applies dAlembert_to_ODE_general to reach the ODE with constant c = H''(0). It then branches on the sign of c. For c > 0 a rescaled function g satisfies g'' = g and is identified with cosh by ode_cosh_uniqueness_contdiff. For c < 0 the rescaled equation becomes g'' = -g and is identified with cos by ode_cos_uniqueness. The remaining case c = 0 yields the constant solution 1, which is smooth.
why it matters
This declaration supplies the final step that turns the Aczél classification into an unconditional theorem, feeding directly into h_aczel_classification_proved which asserts H_AczelClassification without axioms. It closes the last foundation gap in the IndisputableMonolith codebase and aligns with the cost-algebra origin of H from J. The result matches the 1966 Aczél reference cited in the module and supports the smoothness presupposed by the phi-ladder and mass formulas in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.