dAlembert_to_ODE_theorem
plain-language theorem explainer
Any infinitely differentiable real function H satisfying the d'Alembert equation H(t+u) + H(t-u) = 2 H(t) H(u) for all t and u, together with the normalization H''(0) = 1, must obey the ordinary differential equation H''(t) = H(t) for every t. Workers on functional equations in the Recognition Science cost algebra would invoke this result to close the uniqueness argument for the shifted J-cost. The proof fixes an arbitrary t, equates the second derivatives at zero of the two sides of the functional equation after a translation, and reduces the
Claim. If $H : ℝ → ℝ$ is infinitely differentiable, satisfies $H(t + u) + H(t - u) = 2 H(t) H(u)$ for all real $t, u$, and $H''(0) = 1$, then $H''(t) = H(t)$ for all real $t$.
background
The module isolates Aczél-dependent closure theorems for functional equation uniqueness, separate from the axiom-free core. The shifted cost is defined by $H(x) = J(x) + 1 = ½(x + x^{-1})$, where $J$ is the J-cost function; under this reparametrization the Recognition Composition Law becomes the d'Alembert equation $H(xy) + H(x/y) = 2 H(x) H(y)$. Upstream results supply the definition of $H$ in CostAlgebra and the composition of J-automorphisms that preserve the multiplicative structure.
proof idea
The tactic proof first extracts second-order differentiability and differentiability of the derivative from the $C^∞$ hypothesis. It builds HasDerivAt lemmas for the translated addition and subtraction maps. For fixed $t$ the functional equation is rewritten as an equality of functions; their second derivatives at zero are equated by congruence. The left-hand side reduces to $2 H''(t)$ via chain-rule applications on the sum, while the right-hand side reduces to $2 H(t)$ using the normalization at zero.
why it matters
This result is used by aczelRegularityKernel, dAlembert_cosh_solution_aczel, and cosh_rescaling_lemma in the Aczél classification and axiom discharge plan. It completes the ODE step that identifies solutions with the hyperbolic cosine, supporting J-uniqueness (T5) and the self-similar fixed point (T6) in the forcing chain. The theorem bridges the functional equation to the differential equation whose solutions appear in the Recognition Science mass ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.