ode_neg_zero_uniqueness
plain-language theorem explainer
The theorem states that the only twice continuously differentiable solution to the linear ODE f'' + f = 0 with initial conditions f(0) = 0 and f'(0) = 0 is the zero function. Researchers reducing the Aczél–Kannappan classification of continuous d'Alembert solutions cite it to handle the trivial case inside the Recognition Science axiom discharge plan. The proof conserves the quadratic energy E(t) = f(t)^2 + (f'(t))^2, shows its derivative vanishes by the ODE, and concludes E is identically zero from its value at t = 0.
Claim. Let $f : {R} {to} {R}$ be twice continuously differentiable and satisfy $f''(t) = -f(t)$ for all real $t$, with $f(0) = 0$ and $f'(0) = 0$. Then $f(t) = 0$ for all $t$.
background
The AxiomDischargePlan module reduces the classical continuous d'Alembert functional equation to three ODE cases: constant, cosine, and the zero solution handled here. Upstream results establish that continuous solutions are automatically C^infty, supplying the ContDiff hypothesis. The energy functional E(t) = f(t)^2 + (f'(t))^2 is the standard conserved quantity for the harmonic oscillator equation f'' + f = 0.
proof idea
Differentiability of f and f' follows from the C^2 assumption. The derivative of E is computed term-by-term and the ODE is substituted to obtain E' = 0 everywhere. The lemma is_const_of_deriv_eq_zero then yields that E is constant. Evaluation at t = 0 gives E(0) = 0, so E(t) = 0 for all t. Non-negativity of squares forces f(t) = f'(t) = 0.
why it matters
This discharges the zero case required by the reduction plan for aczel_kannappan_continuous_dAlembert, feeding directly into ode_cos_uniqueness (both in AczelProof and AczelTheorem) and ode_cos_unit_uniqueness in the same module. It removes a named classical input, advancing the Recognition Science program of replacing external axioms with theorems derived from the J-functional equation and the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.