ode_neg_zero_uniqueness
plain-language theorem explainer
Uniqueness of the zero solution to the harmonic oscillator ODE f'' + f = 0 under zero initial data. Analysts classifying continuous d'Alembert solutions cite it to isolate the trivial case before extracting cosine or hyperbolic forms. The argument shows that the energy E(t) = f(t)^2 + (f'(t))^2 is constant by direct differentiation and the ODE, then concludes from E(0) = 0 that f vanishes identically.
Claim. Let $f:ℝ→ℝ$ be twice continuously differentiable and satisfy $f''(t)=-f(t)$ for all real $t$, together with the initial conditions $f(0)=0$ and $f'(0)=0$. Then $f(t)=0$ for every real $t$.
background
In the Aczél theorem module every continuous solution of the d'Alembert equation H(t+u)+H(t-u)=2H(t)H(u) with H(0)=1 is shown to be C^∞ by an integration bootstrap that produces the representation formula via the antiderivative Phi. The ODE derivation step then yields H''=cH with c=H''(0). The present lemma handles the c=0 case under zero initial data. The upstream result in AxiomDischargePlan states: 'Zero uniqueness for f''=-f: if f(0)=0 and f'(0)=0, then f≡0. Proof by conservation of the energy E(t)=f(t)^2+f'(t)^2.'
proof idea
The tactic proof first extracts differentiability of f and of f' from the C² hypothesis. It computes the derivative of the energy functional E(t)=f(t)²+(f'(t))², substitutes the ODE to obtain E'(t)=0, and invokes is_const_of_deriv_eq_zero to conclude that E is constant. The initial conditions give E(0)=0, so E(t)=0 everywhere; non-negativity of the squares then forces f(t)=0 and f'(t)=0 for all t.
why it matters
This result closes the c=0 case inside the Aczél classification of d'Alembert solutions and feeds directly into ode_cos_uniqueness (which subtracts the unit cosine and applies the zero theorem to the difference) as well as the axiom-discharge plan. It completes the passage from C^∞ regularity to the explicit forms 1, cos(λt), cosh(λt) without external hypotheses. The module documentation records that the lemma eliminates the former H_AczelClassification axiom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.