dAlembert_to_ODE_theorem
plain-language theorem explainer
Any infinitely differentiable real function H obeying the d'Alembert identity H(t+u)+H(t-u)=2 H(t) H(u) together with H''(0)=1 must satisfy the ODE H''(t)=H(t) at every point. Workers on the T5 J-uniqueness step cite the result to convert the Recognition Composition Law into a differential equation whose solutions are cosh. The argument fixes t, equates the second derivatives at zero of the translated functional equation and its scaled counterpart, then extracts the common factor 2 by explicit chain-rule differentiation of the shift maps.
Claim. If $H:ℝ→ℝ$ is infinitely differentiable, satisfies $H(t+u)+H(t-u)=2H(t)H(u)$ for all real $t,u$, and $H''(0)=1$, then $H''(t)=H(t)$ for every real $t$.
background
The module supplies functional-equation tools for the T5 uniqueness argument. H is the shifted cost reparametrization H(t)=G(t)+1; under this change the Recognition Composition Law becomes the additive d'Alembert equation shown in the hypothesis. Upstream CostAlgebra records the corresponding definition H(x)=J(x)+1=½(x+x⁻¹) and notes that the composition law takes exactly this d'Alembert form. The sibling definition ode_regularity_continuous_hypothesis encodes the converse implication from the ODE to continuity, which the present theorem helps close in the forward direction.
proof idea
The tactic proof first reduces ContDiff ⊤ to ContDiff 2 and obtains differentiability of H and of H'. It builds constant-shift maps whose derivatives are +1 and -1. For fixed t it equates the two sides of the d'Alembert identity after translation by t, differentiates both twice, and evaluates at zero. The left-hand side yields 2 H''(t) via chain rule on the translated arguments; the right-hand side yields 2 H(t) H''(0). The normalization H''(0)=1 forces the ODE.
why it matters
The lemma is invoked by dAlembert_cosh_solution_aczel and aczelRegularityKernel to reach the conclusion that smooth d'Alembert solutions are cosh. It supplies the ODE step inside the T5 forcing chain that identifies J with the unique self-similar fixed point. The same result appears in AczelClassification and AxiomDischargePlan, closing the regularity gap between the functional equation and the explicit cosh form required for the mass ladder and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.