hyperbolic_ode_unique
plain-language theorem explainer
The uniqueness theorem for the hyperbolic ODE asserts that any C² function G satisfying G''(t) = G(t) + 1 together with G(0) = G'(0) = 0 must equal cosh(t) - 1. Analysts working on the d'Alembert bridge in Recognition Science cite it to identify the log-reparametrized interaction function with the J-cost. The proof reduces the inhomogeneous equation to the homogeneous oscillator via a shift by cosh, verifies the zero initial data, and applies the zero-uniqueness lemma for f'' = f.
Claim. The unique twice continuously differentiable function $G : ℝ → ℝ$ satisfying the hyperbolic ordinary differential equation $G''(t) = G(t) + 1$ for all $t$, together with the initial conditions $G(0) = 0$ and $G'(0) = 0$, is $G(t) = cosh t - 1$.
background
In the Analytic Bridge module the log-lift $G(t) = F(e^t)$ converts the multiplicative consistency equation into an additive functional equation whose second derivative yields the hyperbolic ODE. SatisfiesHyperbolicODE G encodes the condition $deriv(deriv G) t = G t + 1$. The upstream lemma ode_zero_uniqueness states that the unique C² solution to $f'' = f$ with $f(0) = f'(0) = 0$ is $f = 0$. This local setting sits inside the larger strategy of showing that interaction forces the d'Alembert structure rather than the additive one.
proof idea
The tactic proof introduces G, assumes the ODE, zero initial data and C² smoothness. It defines y(t) := G(t) + 1 and f(t) := y(t) - cosh(t), establishes f(0) = 0 and f'(0) = 0 by direct computation, and derives the homogeneous ODE f'' = f from the given hyperbolic condition. An energy E(t) := (f'(t))² - (f(t))² is shown to have vanishing derivative and therefore to be constant; since E(0) = 0 it vanishes everywhere. The proof then invokes Cost.FunctionalEquation.ode_zero_uniqueness on f to conclude f ≡ 0, which immediately yields the claimed form for G.
why it matters
This result supplies the explicit solution needed in the chain F_forced_to_Jcost, where hyperbolic ODE plus boundary conditions imply G = cosh - 1 and therefore F(x) = Jcost(x). It also supports the converse verification Jcost_satisfies_dAlembert. Within the Recognition framework it realizes the T5 J-uniqueness step by showing that the forced hyperbolic solution coincides with the self-similar fixed point J(x) = (x + x^{-1})/2 - 1. The declaration closes one link in the forcing chain from interaction to the explicit J-cost form.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.