dAlembert_to_ODE_of_contDiff
plain-language theorem explainer
A C² function satisfying the d'Alembert functional equation with second derivative normalized to one at the origin obeys the ODE H'' = H everywhere. Researchers reducing the T5 J-uniqueness step in Recognition Science cite this when converting functional equations to differential equations under smoothness. The proof applies the second-derivative identity at zero, substitutes the calibration hypothesis, and concludes by linear arithmetic.
Claim. Let $H:ℝ→ℝ$ be twice continuously differentiable and satisfy the d'Alembert equation $H(t+u)+H(t-u)=2H(t)H(u)$ for all real $t,u$, with $H''(0)=1$. Then $H''(t)=H(t)$ for all $t$.
background
This declaration belongs to the ContDiff Reduction module for T5, which removes explicit regularity seams from the J-uniqueness argument. The d'Alembert equation encodes the Recognition Composition Law for the cost function J. The upstream lemma dAlembert_second_deriv_at_zero_of_contDiff states that differentiation of the first-derivative identity at u=0 produces the relation 2 H''(t) = 2 H(t) H''(0) for all t.
proof idea
The proof introduces an arbitrary real t and applies the upstream lemma dAlembert_second_deriv_at_zero_of_contDiff to obtain 2 (H'')'(t) = 2 H(t) (H'')'(0). It rewrites the relation using the calibration hypothesis that the second derivative at zero equals one, then concludes by linear arithmetic that (H'')'(t) equals H(t).
why it matters
This theorem bridges an explicit C² hypothesis to the legacy ODE hypothesis used in earlier T5 arguments. It feeds the cosh solution theorem, which concludes that such functions equal cosh, and the interface packaging the ODE condition. In the Recognition framework it advances the T5 J-uniqueness step by showing that smoothness plus the functional equation plus calibration recover the differential equation whose solutions are the hyperbolic functions on the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.