ode_neg_energy_constant
plain-language theorem explainer
The theorem shows that any twice continuously differentiable solution f to f'' = -f conserves the quantity f(t)^2 + (f'(t))^2. Researchers proving uniqueness for the cosine branch of d'Alembert's equation in Recognition Science would cite this conservation law. The proof defines an auxiliary energy E(t) = f(t)^2 + (f'(t))^2, shows its derivative vanishes by the product rule and ODE substitution, then applies is_const_of_deriv_eq_zero to obtain constancy.
Claim. Let $f : ℝ → ℝ$ be twice continuously differentiable. If $f''(t) = -f(t)$ for all real $t$, then $f(t)^2 + (f'(t))^2 = f(0)^2 + (f'(0))^2$ for all $t$.
background
This result sits in the module on the cosine branch of the angle functional equation, which mirrors the cosh branch for the cost functional J in Cost.FunctionalEquation. The module derives uniqueness of the cosine solution to d'Alembert's equation H(t+u) + H(t-u) = 2 H(t) H(u) under the calibration H''(0) = -1, as part of the forcing chain for recognition angle (Aθ1–Aθ4).
proof idea
The proof defines E(s) := f(s)^2 + (deriv f s)^2. It extracts differentiability of f and deriv f from the ContDiff ℝ 2 hypothesis. It computes deriv E t by the product rule on each summand, substitutes the ODE into the second-derivative terms, and simplifies via ring to zero. It then calls is_const_of_deriv_eq_zero on the differentiable E to conclude E(t) = E(0) for all t.
why it matters
This conservation law is invoked directly by the downstream theorem ode_zero_uniqueness_neg, which proves that the only solution with zero initial data is the zero function. In the Recognition Science framework it supports the angle T5 result by enabling uniqueness for the cosine solution under negative curvature, paralleling J-uniqueness in the cosh branch. It supplies the energy method needed for the d'Alembert cosine calibration in the eight-tick octave construction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.