ode_cosh_uniqueness
plain-language theorem explainer
The uniqueness theorem for the second-order ODE H'' = H with initial conditions H(0) = 1 and H'(0) = 0 asserts that any solution satisfying the listed regularity hypotheses must coincide with the hyperbolic cosine. Analysts working on the Recognition Science T5 J-uniqueness step or on d'Alembert equations would cite this result when converting the cost functional equation into explicit cosh form. The proof is a one-line wrapper that extracts continuity, differentiability, and C² smoothness from the three regularity hypotheses before delegating.
Claim. Let $H : ℝ → ℝ$ satisfy $H''(t) = H(t)$ for all real $t$, with initial conditions $H(0) = 1$ and $H'(0) = 0$, together with the regularity hypotheses that guarantee continuity, differentiability, and twice continuous differentiability of $H$. Then $H(t) = cosh(t)$ for all real $t$.
background
The Cost.FunctionalEquation module supplies lemmas for the T5 cost uniqueness proof. Here H is the shifted cost defined by H_F(t) = G_F(t) + 1, where G reparametrizes the J-cost. Upstream, the CostAlgebra definition states that H(x) = J(x) + 1 = ½(x + x^{-1}), so that the Recognition Composition Law reduces to the d'Alembert equation H(xy) + H(x/y) = 2 H(x) H(y). The module imports derivative and Taylor tools from Mathlib to treat the ODE form of this equation.
proof idea
The proof first applies the three regularity hypotheses (ode_regularity_continuous_hypothesis, ode_regularity_differentiable_hypothesis, ode_linear_regularity_bootstrap_hypothesis) to the given ODE to obtain that H is continuous, differentiable, and ContDiff ℝ 2. It then invokes the core theorem ode_cosh_uniqueness_contdiff on these strengthened assumptions to conclude that H equals the hyperbolic cosine everywhere.
why it matters
This result closes the ODE analysis step inside the T5 J-uniqueness chain by confirming that solutions to the derived differential equation are precisely the cosh functions, which correspond to the explicit form J(x) = cosh(log x) - 1. It is used by the downstream theorem dAlembert_cosh_solution, which combines the d'Alembert functional equation with the ODE to recover the cosh solution. In the Recognition Science framework it supports identification of the self-similar fixed point phi and the eight-tick octave by fixing the functional form of the cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.