ODECoshUniqueCert
plain-language theorem explainer
Packages four ODE facts into one certificate: the zero solution of f''=f is unique under C² and zero data; cosh satisfies cosh''=cosh with cosh(0)=1, cosh'(0)=0; and any C² solution with those initials equals cosh. Cited by anyone closing the T5 cost-uniqueness chain via the log-coordinate identification Jlog=cosh−1. The top theorem is a four-way constructor that applies named uniqueness and derivative lemmas.
Claim. A certificate object whose verification predicate is the conjunction of: (i) every $C^2$ map $f:\mathbb{R}\to\mathbb{R}$ with $f''=f$, $f(0)=0$, $f'(0)=0$ is identically zero; (ii) $\cosh''=\cosh$ pointwise; (iii) $\cosh(0)=1$ and $\cosh'(0)=0$; (iv) every $C^2$ map $H$ with $H''=H$, $H(0)=1$, $H'(0)=0$ equals $\cosh$. The certificate always verifies.
background
In Recognition Science the cost $J$ is forced by the Recognition Composition Law. The shifted function $H(x)=J(x)+1=\frac12(x+x^{-1})$ converts that law into d'Alembert's equation $H(xy)+H(x/y)=2H(x)H(y)$. In log coordinates the natural candidate is $H(t)=\cosh t$, equivalently $J_{\log}(t)=\cosh t-1$.
The module packages the classical second-order uniqueness statement that pins this candidate: among $C^2$ real functions, $H''=H$ with $H(0)=1$ and $H'(0)=0$ has only the solution $\cosh$. A companion zero-data statement ($f(0)=f'(0)=0$) yields only the zero solution, which is the linear-algebraic engine behind uniqueness.
Upstream, ode_cosh_uniqueness_contdiff states exactly that uniqueness theorem; cosh_second_deriv_eq records $\cosh''=\cosh$ from the Mathlib derivative rules $\cosh'=\sinh$ and $\sinh'=\cosh$; ode_zero_uniqueness handles the homogeneous zero-initial-value case.
proof idea
The structure itself is empty (a tag type). The content lives in the verification predicate, a four-fold conjunction, and in verified_any, which discharges it by constructor four times.
First conjunct: apply ode_zero_uniqueness to the given $C^2$ $f$ with $f''=f$ and zero initial data. Second: apply cosh_second_deriv_eq. Third: Real.cosh_zero for the value, and Real.deriv_cosh rewritten with Real.sinh_zero for the derivative. Fourth: apply ode_cosh_uniqueness_contdiff to the given $C^2$ $H$ with matching ODE and initials.
No new analysis is done here; the certificate is a thin assembly layer over the FunctionalEquation lemmas.
why it matters
This sits on the T5 J-uniqueness path in the forcing chain. Once the d'Alembert form of the RCL plus regularity produce the ODE $H''=H$, the certificate removes all free parameters: the solution is exactly $\cosh$, so $J_{\log}=\cosh-1$ (equivalently $J(x)=\frac12(x+x^{-1})-1$) is forced. That is the analytic content of T5.
The module doc states the role explicitly: uniqueness means $J_{\log}$ is uniquely determined up to the constant shift already fixed by $H=J+1$, and "there are no parameters to tune." Downstream graph edges are empty in the current mirror, but the certificate is the verification-layer handle for those FunctionalEquation theorems inside the broader cost-uniqueness argument.
It does not itself derive the ODE from the functional equation; that step lives upstream. Its job is to freeze the solution once the ODE and initials are on the table.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.