dAlembert_cosh_solution
plain-language theorem explainer
Any continuous real-valued function H satisfying the d'Alembert equation H(t+u) + H(t-u) = 2 H(t) H(u) with H(0)=1 and second derivative at zero equal to 1 must equal cosh(t). Researchers proving cost uniqueness in Recognition Science cite this to fix the explicit form of the shifted J-cost. The proof derives the ODE H''=H from the functional equation under supplied regularity hypotheses, confirms evenness and vanishing first derivative at zero, then invokes the ODE uniqueness lemma.
Claim. Let $H:ℝ→ℝ$ be continuous with $H(0)=1$, satisfying the d'Alembert equation $H(t+u)+H(t-u)=2H(t)H(u)$ for all real $t,u$, and with $H''(0)=1$. Under the regularity hypotheses that guarantee smoothness and ODE regularity, $H(t)=cosh(t)$ for all real $t$.
background
The function H reparametrizes the cost by H(t)=G(t)+1. Upstream, H is defined as J(x)+1=½(x+x^{-1}), under which the Recognition Composition Law becomes the d'Alembert equation H(xy)+H(x/y)=2H(x)H(y). The module supplies lemmas for the T5 cost uniqueness proof that derives all physics from one functional equation.
proof idea
The proof obtains the ODE deriv(deriv H)t = H t for all t directly from the dAlembert_to_ODE_hypothesis. It establishes evenness of H via dAlembert_even, then shows deriv H 0 = 0 by applying even_deriv_at_zero to the differentiability supplied by the smoothness hypothesis. It concludes by feeding these facts plus the remaining regularity hypotheses into ode_cosh_uniqueness.
why it matters
This result supplies the explicit cosh solution to the calibrated d'Alembert equation and feeds T5_uniqueness_complete together with washburn_uniqueness, which together establish J(x)=(x+x^{-1})/2-1 (equivalently cosh(log x)-1). It closes the step from the Recognition Composition Law to J-uniqueness in the T5 forcing chain, supporting later derivations of D=3 and the alpha band.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.