dAlembert_smooth_of_aczel
plain-language theorem explainer
Any real-valued function H satisfying H(0)=1, continuity, and the d'Alembert equation H(t+u)+H(t-u)=2H(t)H(u) is infinitely differentiable. Researchers deriving ODEs from the Recognition Composition Law in cost algebra would cite this to justify smoothness before passing to the cosh solutions. The proof is a one-line wrapper that invokes the Aczél smoothness package on the hypothesis predicate.
Claim. Every function $H:ℝ→ℝ$ with $H(0)=1$ that is continuous and satisfies the d'Alembert equation $H(t+u)+H(t-u)=2H(t)H(u)$ for all real $t,u$ is infinitely differentiable.
background
In the Recognition Science cost algebra the shifted function H(x)=J(x)+1, where J is the J-cost obeying the Recognition Composition Law, converts that law into the d'Alembert equation H(xy)+H(x/y)=2H(x)H(y). This compatibility module isolates legacy Aczél closure results so that callers needing classical smoothness can import them without touching the axiom-free core. Upstream the AczelClass theorem states that an AczelSmoothnessPackage instance yields ContDiff ℝ ⊤ H from the three hypotheses H(0)=1, continuity, and the d'Alembert equation; the hypothesis definition in FunctionalEquation encodes precisely this classical implication.
proof idea
The proof is a one-line wrapper that applies aczel_dAlembert_smooth from the AczelClass module, supplying the function H together with the three premises H(0)=1, continuity, and the functional equation.
why it matters
The declaration supplies the Aczél-dependent regularity kernel that feeds aczelRegularityKernel in AczelClassification and thereby the ODE derivation H''=H. It closes the legacy path from the Recognition Composition Law through continuous d'Alembert solutions to the cosh form used in the phi-ladder mass formula and the eight-tick octave. It touches the open question of fully axiom-free uniqueness by providing a drop-in closure for existing callers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.