dAlembert_to_ODE_general
plain-language theorem explainer
Smooth functions H satisfying the d'Alembert equation H(t + u) + H(t - u) = 2 H(t) H(u) obey the ODE H''(t) = H''(0) H(t) for all t. Analysts reducing such equations to differential form cite this result. The proof twice differentiates the functional equation, computes the second derivatives of each side at zero using the chain rule on shifted arguments, and equates them.
Claim. Suppose $H : ℝ → ℝ$ is $C^∞$ and obeys $H(t+u) + H(t-u) = 2 H(t) H(u)$ for all $t, u ∈ ℝ$. Then $H''(t) = H''(0) ⋅ H(t)$ holds for every real $t$.
background
The shifted cost function is defined by H(x) = J(x) + 1, converting the Recognition Composition Law into the displayed d'Alembert equation. The module proves Aczél's theorem that continuous solutions with H(0) = 1 are real analytic, proceeding in three phases: bootstrap to smoothness, derivation of the ODE, and classification of solutions. Upstream, the result dAlembert_contDiff_nat establishes C^n regularity for all n from continuity alone. The present theorem specializes that regularity to the smooth case and extracts the differential consequence.
proof idea
After casting the ContDiff ⊤ hypothesis to C^2 regularity and establishing differentiability of H and H', the proof constructs HasDerivAt facts for the maps u ↦ t + u and u ↦ t - u. It rewrites the functional equation as an equality of functions and equates their second derivatives evaluated at zero. Separate calculations show the left side equals 2 H''(t) and the right side equals 2 H(t) H''(0); linarith then yields the ODE.
why it matters
This supplies the ODE bridge used by dAlembert_classification to identify solutions as cosh, cos, or constant, and by dAlembert_contDiff_top to conclude full smoothness. It implements the second phase of the Aczél proof described in the module documentation. Within Recognition Science the step translates the algebraic structure of the J-cost into a linear ODE whose solutions underpin the phi-ladder mass formula and the eight-tick periodicity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.