dAlembert_to_ODE_general
plain-language theorem explainer
A smooth function H satisfying the d'Alembert equation H(x+y) + H(x-y) = 2 H(x) H(y) obeys the linear ODE H''(t) = H''(0) H(t) for every real t. Researchers reducing the Aczél–Kannappan classification to ODE uniqueness or discharging axioms in Recognition Science would cite this bridge. The proof is a one-line wrapper that invokes the general theorem already established in Cost.FunctionalEquation.
Claim. If $H : {R} {to} {R}$ is $C^infty$ and satisfies $H(x + y) + H(x - y) = 2 H(x) H(y)$ for all real $x, y$, then $H''(t) = H''(0) cdot H(t)$ for all real $t$.
background
The shifted cost is defined by $H(x) = J(x) + 1$, where $J$ is the cost function whose Recognition Composition Law rearranges directly into the displayed d'Alembert equation. Module AxiomDischargePlan reduces the classical aczel_kannappan_continuous_dAlembert axiom to the already-discharged cosh case plus ODE uniqueness for the constant and cosine cases. Upstream, dAlembert_to_ODE_general_theorem in Cost.FunctionalEquation supplies the ODE reduction for $C^infty$ functions, while AczelTheorem provides the smoothness bootstrap from continuity.
proof idea
The declaration is a one-line wrapper that applies dAlembert_to_ODE_general_theorem H h_smooth h_dAlembert from the Cost.FunctionalEquation module.
why it matters
This reduction supplies the ODE form required by dAlembert_classification and aczel_kannappan_via_cases, completing discharge of the aczel_kannappan_continuous_dAlembert axiom. It converts the Recognition Composition Law into the differential equation whose solutions are the cosh and cos functions used in the eight-tick octave and the phi-ladder mass formula. The step closes the analytic gap after T5 J-uniqueness and before explicit classification for D = 3 and the alpha band.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.
papers checked against this theorem (showing 1 of 1)
-
Closed-form oscillators replace ODE solvers for irregular time series
"We model keys and values as damped, driven oscillators... closed-form solution... resonance phenomenon... H(ω) = β/(ω_i² - ω² + 2iγ_iω)"