ode_neg_zero_uniqueness
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prove uniqueness without the C^2 regularity hypothesis.
- Does not apply when initial conditions are nonzero.
- Does not treat nonlinear or higher-order oscillator equations.
- Does not establish existence of nontrivial solutions.
formal statement (Lean)
76theorem ode_neg_zero_uniqueness (f : ℝ → ℝ)
77 (h_diff2 : ContDiff ℝ 2 f)
78 (h_ode : ∀ t, deriv (deriv f) t = -(f t))
79 (h_f0 : f 0 = 0) (h_f'0 : deriv f 0 = 0) :
80 ∀ t, f t = 0 := by
proof body
Tactic-mode proof.
81 have h_d1 : Differentiable ℝ f := h_diff2.differentiable (by decide : (2 : WithTop ℕ∞) ≠ 0)
82 have hCD1 : ContDiff ℝ 1 (deriv f) := by
83 rw [show (2 : WithTop ℕ∞) = 1 + 1 from rfl] at h_diff2
84 rw [contDiff_succ_iff_deriv] at h_diff2
85 exact h_diff2.2.2
86 have h_dd : Differentiable ℝ (deriv f) :=
87 hCD1.differentiable (by decide : (1 : WithTop ℕ∞) ≠ 0)
88 have hE_deriv_zero : ∀ s, deriv (fun t => f t ^ 2 + deriv f t ^ 2) s = 0 := by
89 intro s
90 have h1 : HasDerivAt (fun x => f x ^ 2 + deriv f x ^ 2)
91 (↑2 * f s ^ (2 - 1) * deriv f s + ↑2 * deriv f s ^ (2 - 1) * deriv (deriv f) s) s :=
92 ((h_d1 s).hasDerivAt.pow 2).add ((h_dd s).hasDerivAt.pow 2)
93 have h2 := h1.deriv
94 rw [h_ode s] at h2
95 push_cast at h2
96 simp only [pow_one] at h2
97 linarith
98 have hE_eq := is_const_of_deriv_eq_zero
99 (show Differentiable ℝ (fun t => f t ^ 2 + deriv f t ^ 2) from
100 (h_d1.pow 2).add (h_dd.pow 2))
101 hE_deriv_zero
102 intro t
103 have hE0 : f 0 ^ 2 + deriv f 0 ^ 2 = 0 := by rw [h_f0, h_f'0]; ring
104 have hEt := hE_eq t 0
105 simp only [hE0] at hEt
106 nlinarith [sq_nonneg (f t), sq_nonneg (deriv f t)]
107
108/-- **Unit-frequency cosine uniqueness**: a C² solution of `f'' = -f`
109with `f(0)=1` and `f'(0)=0` is `cos`. -/