ode_zero_uniqueness_neg
The theorem proves that the zero function is the unique twice continuously differentiable solution to the differential equation f'' = -f satisfying the initial conditions f(0) = 0 and f'(0) = 0. Researchers establishing the cosine solution branch in the d'Alembert functional equation for angle coupling functions would cite this result. The proof is a short tactic sequence that invokes the energy conservation identity and applies non-negativity together with linear arithmetic to force the function and its derivative to vanish.
claimLet $f : ℝ → ℝ$ be twice continuously differentiable. If $f''(t) = -f(t)$ for all real $t$, with $f(0) = 0$ and $f'(0) = 0$, then $f(t) = 0$ for all $t$.
background
This result belongs to the cosine branch of the d'Alembert functional equation in the Recognition Angle module. The module develops uniqueness for functions satisfying H(t+u) + H(t-u) = 2 H(t) H(u) with negative curvature calibration H''(0) = -1, selecting the cosine solution. Twice continuous differentiability is denoted ContDiff ℝ 2 f. The key upstream result is ode_neg_energy_constant, which states that for solutions of f'' = -f the quantity f(t)^2 + (f'(t))^2 is constant and equal to its value at zero. The module mirrors the cosh uniqueness proof in Cost.FunctionalEquation but with opposite sign.
proof idea
The proof begins by specializing the energy conservation theorem ode_neg_energy_constant at the given point t. This yields f(t)^2 + (deriv f t)^2 = f(0)^2 + (deriv f 0)^2. Substituting the initial conditions f(0) = 0 and deriv f 0 = 0 produces the sum of squares equal to zero. Non-negativity of each square term together with linarith and nlinarith then forces each square to be individually zero, hence f(t) = 0.
why it matters in Recognition Science
This lemma supplies the zero-initial-condition case needed to complete the uniqueness argument for the cosine solution in ode_cos_uniqueness_contdiff. It fills the T5 step for the angle branch of the forcing chain, where the negative curvature selects cos rather than cosh. The result supports the master theorem THEOREM_angle_coupling_rigidity that packages axioms Aθ1–Aθ4 into H = cos. It touches the open question of extending the uniqueness from C^2 to weaker regularity classes.
scope and limits
- Does not prove uniqueness for solutions lacking twice continuous differentiability.
- Does not address the d'Alembert functional equation directly, only the derived ODE.
- Does not apply when the initial conditions differ from zero.
- Does not establish existence of non-trivial solutions.
formal statement (Lean)
102theorem ode_zero_uniqueness_neg (f : ℝ → ℝ)
103 (h_diff2 : ContDiff ℝ 2 f)
104 (h_ode : ∀ t, deriv (deriv f) t = -f t)
105 (h_f0 : f 0 = 0)
106 (h_f'0 : deriv f 0 = 0) :
107 ∀ t, f t = 0 := by
proof body
Tactic-mode proof.
108 intro t
109 have hE := ode_neg_energy_constant f h_diff2 h_ode t
110 have hzero : f t ^ 2 + (deriv f t) ^ 2 = 0 := by
111 simpa [h_f0, h_f'0] using hE
112 have hsq_nonneg : 0 ≤ f t ^ 2 := sq_nonneg (f t)
113 have hderivsq_nonneg : 0 ≤ (deriv f t) ^ 2 := sq_nonneg (deriv f t)
114 have hsq_zero : f t ^ 2 = 0 := by linarith
115 nlinarith [hsq_zero]
116
117/-- cos satisfies the ODE cos'' = -cos. -/