dAlembert_to_ODE_hypothesis
plain-language theorem explainer
The d'Alembert to ODE hypothesis packages the conditions under which a continuous real function H with H(0)=1, H''(0)=1 and satisfying the addition formula H(t+u)+H(t-u)=2 H(t) H(u) for all real t,u must obey the differential equation H''=H everywhere. Researchers proving T5 uniqueness of the cost algebra cite this packaging when they reduce the Recognition Composition Law to its ODE form. The declaration is a direct definition that bundles the four antecedents into a single Prop for use in downstream uniqueness and classification arguments.
Claim. Let $H : ℝ → ℝ$. The hypothesis asserts that if $H(0)=1$, $H$ is continuous, $H(t+u)+H(t-u)=2 H(t) H(u)$ holds for all real $t,u$, and the second derivative satisfies $H''(0)=1$, then $H''(t)=H(t)$ for every real $t$.
background
The Cost.FunctionalEquation module supplies helper lemmas for the T5 cost uniqueness proof. The shifted cost is introduced by the sibling definition H(t) := G(t) + 1, where G is the reparametrized cost function. Upstream, the CostAlgebra module defines the same H(x) = J(x) + 1 = ½(x + x^{-1}), under which the Recognition Composition Law reduces exactly to the d'Alembert equation H(xy) + H(x/y) = 2 H(x) H(y).
proof idea
This is a definition that directly encodes the implication from the d'Alembert functional equation plus continuity and the calibration H''(0)=1 to the ODE H''=H. No tactics or lemmas are applied inside the body; the declaration simply names the four-antecedent Prop for reuse.
why it matters
It supplies the ODE hypothesis required by the canonical cost algebra uniqueness theorem cost_algebra_unique, which establishes that any CostAlgebraData obeying the axioms and the calibration J''(1)=1 must coincide with the J function of T5. The declaration is also invoked by the AczelRegularityKernel structure and by the cosh solution theorems that verify the hypothesis for the explicit cosh case.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.