ode_zero_uniqueness
plain-language theorem explainer
The theorem asserts that the only C² solution to the ODE f'' = f on the reals with vanishing initial conditions f(0) = f'(0) = 0 is the zero function. It is invoked inside the T5 cost-uniqueness argument and the hyperbolic ODE bridge to rule out the homogeneous trivial solution. The proof diagonalizes the second-order equation into a pair of first-order linear ODEs and applies the two zero-uniqueness lemmas already established for those equations.
Claim. Let $f : ℝ → ℝ$ be twice continuously differentiable. If $f''(t) = f(t)$ for all $t ∈ ℝ$ and the initial conditions $f(0) = 0$, $f'(0) = 0$ hold, then $f(t) = 0$ for every $t$.
background
The module supplies auxiliary results for the T5 cost-uniqueness proof. The ODE f'' = f is the linear equation satisfied by the J-cost function after the Recognition Composition Law is rewritten in exponential coordinates. Upstream, ode_diagonalization decomposes any C² solution of f'' = f into the pair of first-order equations satisfied by (f' − f) and (f' + f). The lemmas deriv_neg_self_zero and deriv_pos_self_zero then give uniqueness for each of those first-order problems when the initial value is zero.
proof idea
Apply ode_diagonalization to obtain the two first-order relations. Define g := deriv f − f and hf := deriv f + f; both are differentiable, satisfy g' = −g and hf' = hf, and vanish at zero. Invoke deriv_neg_self_zero on g and deriv_pos_self_zero on hf to conclude both are identically zero. Subtracting the two identities forces f = 0.
why it matters
The result is used by ode_cosh_uniqueness_contdiff to identify the unique C² solution with H(0) = 1, H'(0) = 0 as cosh, and by hyperbolic_ode_unique to conclude that the only solution of G'' = G + 1 with G(0) = G'(0) = 0 is cosh(t) − 1. It therefore supplies the homogeneous uniqueness step required for the identification J(x) = cosh(log x) − 1 in the T5 forcing-chain argument.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.