ODEFoundationCert
plain-language theorem explainer
Packages two ODE facts that underwrite cosh uniqueness for the Recognition cost: twice-differentiable solutions of f''=f with zero initial data vanish identically, and any even H differentiable at 0 has H'(0)=0. Cited by the ODE-foundation verification layer feeding the cosh uniqueness argument. The top-level check is a two-branch constructor applying ode_zero_uniqueness and even_deriv_at_zero.
Claim. An empty certificate type whose verification predicate is the conjunction of: (i) every $C^2$ map $f:\mathbb{R}\to\mathbb{R}$ with $f''=f$, $f(0)=0$, and $f'(0)=0$ satisfies $f\equiv 0$; (ii) every even $H:\mathbb{R}\to\mathbb{R}$ differentiable at $0$ has $H'(0)=0$. Every inhabitant of the certificate type satisfies the predicate.
background
This module sits in the Verification layer and packages the ODE lemmas that make the cosh uniqueness theorem for the Recognition cost go through. The shifted cost $H(x)=J(x)+1=\frac12(x+x^{-1})$ converts the Recognition Composition Law into the d'Alembert form $H(xy)+H(x/y)=2H(x)H(y)$. In log-coordinates the same $H$ is even, so symmetry alone forces the first derivative at the origin to vanish.
The companion fact is homogeneous uniqueness for $f''=f$: zero Cauchy data at $0$ imply $f\equiv 0$. The module doc records the diagonalization used upstream: the combinations $f'-f$ and $f'+f$ satisfy first-order equations $g'=-g$ and $h'=h$, each of which is killed by a multiplying factor $e^{\pm t}$ when the initial value is zero. Together these supply the initial condition and the uniqueness step in the comparison $H-\cosh$.
proof idea
The structure itself carries no fields (only Repr). Its verification predicate is literally the conjunction of the two target statements. The theorem that every certificate verifies is a two-goal constructor: the first goal is discharged by ode_zero_uniqueness on the given $C^2$ data and zero initial conditions; the second by even_deriv_at_zero on the evenness and differentiability hypotheses. No further rewriting or analysis is performed at this layer.
why it matters
These two facts are the ODE core of the cosh uniqueness argument for the cost, which is the analytic half of T5 J-uniqueness ($J(x)=\frac12(x+x^{-1})-1$, equivalently $\cosh(\log x)-1$). Evenness of $H$ in log-coordinates yields $H'(0)=0$; zero uniqueness then shows that any candidate satisfying the same second-order ODE and initial data as $\cosh$ must coincide with it. The certificate is a verification wrapper: it freezes the two lemmas into a single checkable Prop so downstream certificate chains can assert the ODE foundation without reopening the analysis. No further used-by edges are recorded yet; the intended consumer is the cosh-uniqueness certificate in the FunctionalEquation development.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.