dAlembert_to_ODE_general
plain-language theorem explainer
A smooth solution H to the d'Alembert equation H(t+u) + H(t-u) = 2 H(t) H(u) satisfies the linear ODE H''(t) = H''(0) H(t) for all t. Researchers classifying continuous solutions of functional equations or discharging axioms in the Recognition Science cost algebra cite this reduction to reach the explicit cosh, cos, and constant cases. The proof twice differentiates the functional equation in the second variable, evaluates at zero after fixing t, and equates the resulting expressions via the chain rule on translated arguments.
Claim. Let $H : ℝ → ℝ$ be infinitely differentiable and satisfy $H(t+u) + H(t-u) = 2 H(t) H(u)$ for all real $t,u$. Then $H''(t) = H''(0) · H(t)$ for every $t$.
background
The theorem belongs to the Aczél smoothness package for the d'Alembert equation, which descends from the Recognition Composition Law via the shifted cost H(x) = J(x) + 1. Phi is defined as the integral from 0 to t of H and supplies the representation formula that bootstraps continuity to C^∞. Upstream results include the composition of J-automorphisms and the definition of H in CostAlgebra, which convert the multiplicative RCL into the additive d'Alembert form shown in the hypothesis.
proof idea
The tactic proof first extracts C² regularity from the given C^∞ assumption via contDiff_infty. It constructs HasDerivAt lemmas for the translated maps t+u and t-u using the chain rule with explicit shift derivatives. Differentiating the left-hand side of the functional equation twice at u=0 yields 2 H''(t), while the right-hand side yields 2 H(t) H''(0); equating the two sides of the differentiated equation produces the ODE.
why it matters
This ODE bridge is invoked by dAlembert_classification in AczelProof and by aczel_kannappan_via_cases in the AxiomDischargePlan. It completes the step from C^∞ regularity to the explicit ODE H'' = c H whose solutions are cosh, cos, or constant, thereby discharging the former Aczel hypothesis in the Recognition Science foundation. The result aligns with T5 J-uniqueness and the Recognition Composition Law that originally forces the d'Alembert equation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.