ode_zero_uniqueness
The theorem proves that the only C² solution to the ODE f'' = f with f(0) = f'(0) = 0 is the zero function. Analysts deriving uniqueness for hyperbolic cost functions in the Recognition Science T5 step would cite this result when showing that the J-cost is the sole solution compatible with the composition law and zero boundary data. The argument diagonalizes the second-order equation into a pair of first-order ODEs and applies separate zero-uniqueness lemmas for the negative and positive exponential cases.
claimLet $f : ℝ → ℝ$ be twice continuously differentiable. Suppose $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
This theorem sits inside the module of functional-equation helpers written for the T5 cost-uniqueness argument. The module supplies the analytic infrastructure needed to extract the unique solution of the Recognition Composition Law that is compatible with the self-similar fixed point. Upstream lemmas establish that any differentiable function obeying g' = -g with g(0) = 0 must vanish identically, and likewise for the equation h' = h with h(0) = 0; the present result reduces the second-order problem to those two first-order cases.
proof idea
The proof begins by calling ode_diagonalization to split the second-order ODE into the pair of first-order equations satisfied by g(t) := f'(t) - f(t) and h(t) := f'(t) + f(t). Differentiability of g and h follows from the assumed C² regularity of f. The initial conditions force g(0) = h(0) = 0. Separate invocations of deriv_neg_self_zero on g and deriv_pos_self_zero on h then show both auxiliaries are identically zero. Linear combination recovers f = 0.
why it matters in Recognition Science
The result is invoked directly by ode_cosh_uniqueness_contdiff to identify cosh as the unique solution with unit initial data, and by hyperbolic_ode_unique in the DAlembert analytic bridge to conclude that the J-cost equals cosh(t) - 1. Within the Recognition framework it supplies the uniqueness half of T5, confirming that the fixed point forced by the composition law is realized by the hyperbolic function whose series generates the phi-ladder. No scaffolding remains at this node.
scope and limits
- Does not establish existence of solutions to the ODE.
- Does not treat initial conditions at points other than zero.
- Does not extend to nonlinear or higher-order equations.
- Does not apply to functions lacking C² regularity.
- Does not address complex-valued or vector-valued solutions.
formal statement (Lean)
371theorem ode_zero_uniqueness (f : ℝ → ℝ)
372 (h_diff2 : ContDiff ℝ 2 f)
373 (h_ode : ∀ t, deriv (deriv f) t = f t)
374 (h_f0 : f 0 = 0)
375 (h_f'0 : deriv f 0 = 0) :
376 ∀ t, f t = 0 := by
proof body
Tactic-mode proof.
377 have ⟨h_minus, h_plus⟩ := ode_diagonalization f h_diff2 h_ode
378 have h_diff1 : Differentiable ℝ f := h_diff2.differentiable (by decide : (2 : WithTop ℕ∞) ≠ 0)
379 have h_deriv_contdiff : ContDiff ℝ 1 (deriv f) := by
380 rw [show (2 : WithTop ℕ∞) = 1 + 1 from rfl] at h_diff2
381 rw [contDiff_succ_iff_deriv] at h_diff2
382 exact h_diff2.2.2
383 have h_diff_deriv : Differentiable ℝ (deriv f) := h_deriv_contdiff.differentiable (by decide : (1 : WithTop ℕ∞) ≠ 0)
384 let g := fun s => deriv f s - f s
385 let hf := fun s => deriv f s + f s
386 have hg_diff : Differentiable ℝ g := h_diff_deriv.sub h_diff1
387 have hh_diff : Differentiable ℝ hf := h_diff_deriv.add h_diff1
388 have hg0 : g 0 = 0 := by simp [g, h_f0, h_f'0]
389 have hh0 : hf 0 = 0 := by simp [hf, h_f0, h_f'0]
390 have hg_deriv : ∀ t, deriv g t = -g t := h_minus
391 have hh_deriv : ∀ t, deriv hf t = hf t := h_plus
392 have hg_zero := deriv_neg_self_zero g hg_diff hg_deriv hg0
393 have hh_zero := deriv_pos_self_zero hf hh_diff hh_deriv hh0
394 intro t
395 have hgt := hg_zero t
396 have hht := hh_zero t
397 simp only [g, hf] at hgt hht
398 linarith
399