ode_cosh_uniqueness_contdiff
plain-language theorem explainer
The unique C² solution to the ODE H'' = H with H(0)=1 and H'(0)=0 is the hyperbolic cosine. Recognition Science researchers working on T5 cost uniqueness cite this to complete the regularity bootstrap inside the d'Alembert classification. The proof subtracts the known cosh solution from H to obtain a homogeneous problem with zero initial data and invokes the prior zero-uniqueness lemma for the same ODE.
Claim. Suppose a function $H:ℝ→ℝ$ is twice continuously differentiable and satisfies $H''(t)=H(t)$ for all real $t$, together with the initial conditions $H(0)=1$ and $H'(0)=0$. Then $H(t)=cosh(t)$ for all real $t$.
background
The module supplies lemmas for the T5 cost uniqueness proof in Recognition Science. The symbol H denotes the shifted cost reparametrization H(t)=G(t)+1, which converts the Recognition Composition Law into the d'Alembert equation. Upstream results include the ODE Zero Uniqueness theorem stating that the unique C² solution to f''=f with f(0)=f'(0)=0 is the zero function, and the identity that the second derivative of cosh recovers cosh itself.
proof idea
Define g(t):=H(t)−cosh(t). C² regularity of g follows by subtraction from the given ContDiff assumption on H and the known smoothness of cosh. Direct computation of derivatives, using the second-derivative identity for cosh, shows g obeys the same ODE with vanishing initial data. The conclusion follows by applying the zero-uniqueness theorem to g.
why it matters
This result is invoked by the d'Alembert classification theorem and the Aczél-form cosh solution theorem to identify regular solutions with hyperbolic cosine. It thereby supports the explicit form required for J-uniqueness in the forcing chain, where the cost is expressed via cosh(log x)−1. The declaration closes the regularity step that lets the framework pass from the abstract Recognition Composition Law to concrete constants such as the fine-structure interval.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.
papers checked against this theorem (showing 1 of 1)
-
Two axioms recover every geodesic current on a surface
"Theorem D (Hyperbolic metric case): λ(a)λ(b) = λ(ab) + λ(aB), where λ(g) := 2 cosh(f(g)/2). This identity comes from the hyperbolic parallelogram identity (Lemma A.2)."