ode_diagonalization
plain-language theorem explainer
The lemma shows that any twice continuously differentiable solution f to the ODE f'' = f satisfies first-order equations for the combinations f' - f and f' + f, with derivatives equal to minus and plus the combinations themselves. Researchers proving uniqueness for the J-cost functional under T5 in Recognition Science cite this when reducing the second-order equation to independent exponential modes. The proof extracts differentiability from ContDiff 2, applies deriv_sub and deriv_add to each combination, substitutes the ODE, and simplifies by环
Claim. Let $f : ℝ → ℝ$ be twice continuously differentiable and satisfy $f''(t) = f(t)$ for all $t ∈ ℝ$. Then the combinations $g(t) := f'(t) - f(t)$ and $h(t) := f'(t) + f(t)$ obey $g'(t) = -g(t)$ and $h'(t) = h(t)$ for all $t$.
background
The module Cost.FunctionalEquation supplies lemmas for the T5 cost uniqueness proof. The local setting is the functional equation satisfied by the J-cost, where T5 asserts uniqueness of J(x) = (x + x^{-1})/2 - 1, also written cosh(log x) - 1. This lemma diagonalizes the linear ODE f'' = f that appears when analyzing critical points or uniqueness of that cost. Upstream results include the deriv_add theorem from Relativity.Fields.Scalar, which establishes linearity of the directional derivative in the field, together with foundational structural conditions from PrimitiveDistinction.
proof idea
The proof first derives differentiability of f and of deriv f from the ContDiff ℝ 2 hypothesis via contDiff_succ_iff_deriv. It splits into two conjuncts. For the minus combination it applies deriv_sub, rewrites the result using the ODE hypothesis, and simplifies with ring to obtain the claimed negative sign. The plus combination proceeds identically with deriv_add and ring.
why it matters
This lemma is invoked directly by the ODE zero uniqueness theorem, which concludes that the only solution to f'' = f with f(0) = f'(0) = 0 is f = 0. It supplies an intermediate reduction step in the T5 J-uniqueness argument of the Recognition Science forcing chain (T0 to T8), where the cost functional leads to this ODE whose solutions must match the self-similar fixed point phi. The diagonalization enables the exponential-mode analysis that closes the uniqueness claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.