Encyclopedia Cost Cost Aczel Proof Ode Neg Zero Uniqueness

ARTICLE 3 claims 3 theorems

Cost Aczel Proof Ode Neg Zero Uniqueness

A small lemma in a machine-checked proof says that the only twice-differentiable solution to a certain second-order differential equation with zero initial conditions is the zero function.

Verify this page

The zero solution

In the theory of differential equations, a standard question asks whether a function can be nonzero while satisfying a linear second-order equation and starting from rest. The declaration ode_neg_zero_uniqueness answers this for the equation f''(t) = -f(t), which is the harmonic oscillator equation. It proves that if a twice-differentiable function f satisfies this equation for all real t, and if both f(0) and its derivative f'(0) are zero, then f(t) must be zero for every t. This is a uniqueness statement: the zero function is the only solution with those initial conditions.

The proof works by a standard energy argument. Define the quantity E(t) = f(t)^2 + f'(t)^2. Differentiating E with respect to t and using the differential equation gives E'(t) = 0, so E is constant. Since E(0) = 0 by the initial conditions, E(t) = 0 for all t, which forces f(t) = 0 everywhere. This argument requires f to be twice differentiable, which is exactly the hypothesis of the theorem. The declaration is part of a larger machine-checked proof of Aczél's classification of solutions to the d'Alembert functional equation, where this uniqueness result selects the cosine solution from the three possible branches.

In Recognition Science, this lemma appears inside the derivation of the framework's cost function. The framework models recognition as a discrete record of events with a forced cost, and its central theorem states that any cost function satisfying five conditions must equal J(x) = (x + 1/x)/2 - 1. The proof of that theorem passes through the d'Alembert equation, and this uniqueness lemma is one of the steps that rules out extraneous solutions. The lemma itself is a classical fact about differential equations; the framework's contribution is to show that the equation arises from its axioms, not to change the mathematics of the lemma.

The declaration does not claim that every solution of f'' = -f is zero. It applies only under the specific initial conditions f(0) = 0 and f'(0) = 0. With different initial data, the general solution is f(t) = A cos(t) + B sin(t), which is nonzero for most choices of A and B. The lemma also does not assert anything about the cost function J itself, nor about the physical interpretation of the differential equation. It is a technical tool inside a longer proof, not a standalone result about recognition.

THEOREM ode_neg_zero_uniqueness · IndisputableMonolith/Cost/AczelProof.lean
ode_neg_zero_uniqueness · IndisputableMonolith/Cost/AczelProof.lean:229 
private theorem ode_neg_zero_uniqueness (f : ℝ → ℝ)
    (h_diff2 : ContDiff ℝ 2 f)
    (h_ode : ∀ t, deriv (deriv f) t = -(f t))
    (h_f0 : f 0 = 0) (h_f'0 : deriv f 0 = 0) :
    ∀ t, f t = 0 := by
  have h_d1 : Differentiable ℝ f := h_diff2.differentiable (by decide : (2 : WithTop ℕ∞) ≠ 0)
  have hCD1 : ContDiff ℝ 1 (deriv f) := by
    rw [show (2 : WithTop ℕ∞) = 1 + 1 from rfl] at h_diff2
    rw [contDiff_succ_iff_deriv] at h_diff2; exact h_diff2.2.2
  have h_dd : Differentiable ℝ (deriv f) := hCD1.differentiable (by decide : (1 : WithTop ℕ∞) ≠ 0)
  -- Energy E(t) = f(t)² + f'(t)² has E' = 2f'(f + f'') = 2f'(f - f) = 0
  -- So E is constant = E(0) = 0, giving f(t)² ≤ 0, hence f = 0.
  have hE_deriv_zero : ∀ s, deriv (fun t => f t ^ 2 + deriv f t ^ 2) s = 0 := by
    intro s
    have h1 : HasDerivAt (fun x => f x ^ 2 + deriv f x ^ 2)
        (↑2 * f s ^ (2 - 1) * deriv f s + ↑2 * deriv f s ^ (2 - 1) * deriv (deriv f) s) s :=
      ((h_d1 s).hasDerivAt.pow 2).add ((h_dd s).hasDerivAt.pow 2)
    have h2 := h1.deriv; rw [h_ode s] at h2; push_cast at h2; simp only [pow_one] at h2
    linarith
  have hE_eq := is_const_of_deriv_eq_zero
    (show Differentiable ℝ (fun t => f t ^ 2 + deriv f t ^ 2) from
      (h_d1.pow 2).add (h_dd.pow 2))
    hE_deriv_zero
  intro t
  have hE0 : f 0 ^ 2 + deriv f 0 ^ 2 = 0 := by rw [h_f0, h_f'0]; ring
  have hEt := hE_eq t 0; simp only [hE0] at hEt
  nlinarith [sq_nonneg (f t), sq_nonneg (deriv f t)]
THEOREM ode_neg_zero_uniqueness · IndisputableMonolith/Cost/AczelProof.lean
ode_neg_zero_uniqueness · IndisputableMonolith/Cost/AczelProof.lean:229 
private theorem ode_neg_zero_uniqueness (f : ℝ → ℝ)
    (h_diff2 : ContDiff ℝ 2 f)
    (h_ode : ∀ t, deriv (deriv f) t = -(f t))
    (h_f0 : f 0 = 0) (h_f'0 : deriv f 0 = 0) :
    ∀ t, f t = 0 := by
  have h_d1 : Differentiable ℝ f := h_diff2.differentiable (by decide : (2 : WithTop ℕ∞) ≠ 0)
  have hCD1 : ContDiff ℝ 1 (deriv f) := by
    rw [show (2 : WithTop ℕ∞) = 1 + 1 from rfl] at h_diff2
    rw [contDiff_succ_iff_deriv] at h_diff2; exact h_diff2.2.2
  have h_dd : Differentiable ℝ (deriv f) := hCD1.differentiable (by decide : (1 : WithTop ℕ∞) ≠ 0)
  -- Energy E(t) = f(t)² + f'(t)² has E' = 2f'(f + f'') = 2f'(f - f) = 0
  -- So E is constant = E(0) = 0, giving f(t)² ≤ 0, hence f = 0.
  have hE_deriv_zero : ∀ s, deriv (fun t => f t ^ 2 + deriv f t ^ 2) s = 0 := by
    intro s
    have h1 : HasDerivAt (fun x => f x ^ 2 + deriv f x ^ 2)
        (↑2 * f s ^ (2 - 1) * deriv f s + ↑2 * deriv f s ^ (2 - 1) * deriv (deriv f) s) s :=
      ((h_d1 s).hasDerivAt.pow 2).add ((h_dd s).hasDerivAt.pow 2)
    have h2 := h1.deriv; rw [h_ode s] at h2; push_cast at h2; simp only [pow_one] at h2
    linarith
  have hE_eq := is_const_of_deriv_eq_zero
    (show Differentiable ℝ (fun t => f t ^ 2 + deriv f t ^ 2) from
      (h_d1.pow 2).add (h_dd.pow 2))
    hE_deriv_zero
  intro t
  have hE0 : f 0 ^ 2 + deriv f 0 ^ 2 = 0 := by rw [h_f0, h_f'0]; ring
  have hEt := hE_eq t 0; simp only [hE0] at hEt
  nlinarith [sq_nonneg (f t), sq_nonneg (deriv f t)]
THEOREM dAlembert_classification · IndisputableMonolith/Cost/AczelProof.lean
dAlembert_classification · IndisputableMonolith/Cost/AczelProof.lean:291 
/-- **Aczél–Kannappan classification of the d'Alembert functional equation.**

Any continuous H : ℝ → ℝ with H(0) = 1 satisfying
  H(t+u) + H(t−u) = 2·H(t)·H(u)
is exactly one of:
* the constant 1,
* `Real.cosh (α·)` for some α ∈ ℝ, or
* `Real.cos  (α·)` for some α ∈ ℝ.

Proof: continuity ⇒ C^∞ via the integration bootstrap (`dAlembert_contDiff_smooth`);
C² + d'Alembert ⇒ H'' = c·H with c = H''(0) (`dAlembert_to_ODE_general`);
ODE uniqueness in each branch of the trichotomy on c gives the explicit formula. -/
theorem dAlembert_classification (H : ℝ → ℝ)
    (h_one : H 0 = 1) (h_cont : Continuous H)
    (h_dAl : ∀ t u, H (t + u) + H (t - u) = 2 * H t * H u) :
    (∀ x, H x = 1) ∨
    (∃ α : ℝ, ∀ x, H x = Real.cosh (α * x)) ∨
    (∃ α : ℝ, ∀ x, H x = Real.cos (α * x)) := by
  have h_sm : ContDiff ℝ smooth H := dAlembert_contDiff_smooth H h_one h_cont h_dAl
  have h2 : ContDiff ℝ 2 H := by exact_mod_cast (contDiff_infty.mp h_sm) 2
  have hDiff : Differentiable ℝ H := h2.differentiable (by decide : (2 : WithTop ℕ∞) ≠ 0)
  have h_H'0 : deriv H 0 = 0 :=
    even_deriv_at_zero H (dAlembert_even H h_one h_dAl) hDiff.differentiableAt
  have h_ode := dAlembert_to_ODE_general H h_sm h_dAl
  set c := deriv (deriv H) 0 with hc_def
  have hDD : Differentiable ℝ (deriv H) := by
    rw [show (2 : WithTop ℕ∞) = 1 + 1 from rfl] at h2
    exact (contDiff_succ_iff_deriv.mp h2).2.2.differentiable (by decide : (1 : WithTop ℕ∞) ≠ 0)
  by_cases hc_pos : 0 < c
  · -- c > 0: H = cosh(√c · t)
    right; left; refine ⟨Real.sqrt c, ?_⟩
    have hsc_ne : Real.sqrt c ≠ 0 := ne_of_gt (Real.sqrt_pos.mpr hc_pos)
    let g : ℝ → ℝ := fun s => H (s / Real.sqrt c)
    have h_div : ∀ s, HasDerivAt (fun x => x / Real.sqrt c) (Real.sqrt c)⁻¹ s := fun s => by
      have := (hasDerivAt_id s).div_const (Real.sqrt c); simp only [id, one_div] at this; exact this
    have hg_d : ∀ s, HasDerivAt g (deriv H (s / Real.sqrt c) * (Real.sqrt c)⁻¹) s :=
      fun s => (hDiff _).hasDerivAt.comp s (h_div s)
    have hg_ode : ∀ t, deriv (deriv g) t = g t := by
      intro s
      have hg1 : deriv g = fun s => deriv H (s / Real.sqrt c) * (Real.sqrt c)⁻¹ :=
        funext fun s => (hg_d s).deriv
      have h_dd_g : HasDerivAt (deriv g)
          ((deriv (deriv H) (s / Real.sqrt c) * (Real.sqrt c)⁻¹) * (Real.sqrt c)⁻¹) s := by
        rw [hg1]
        exact ((hDD (s / Real.sqrt c)).hasDerivAt.comp s (h_div s)).mul_const _
      rw [h_dd_g.deriv, h_ode (s / Real.sqrt c)]
      simp only [g]
      rw [show c * H (s / Real.sqrt c) * (Real.sqrt c)⁻¹ * (Real.sqrt c)⁻¹ =
          H (s / Real.sqrt c) * (c * ((Real.sqrt c)⁻¹ * (Real.sqrt c)⁻¹)) from by ring,
          show (Real.sqrt c)⁻¹ * (Real.sqrt c)⁻¹ = (Real.sqrt c * Real.sqrt c)⁻¹ from
            (mul_inv_rev _ _).symm,
          Real.mul_self_sqrt (le_of_lt hc_pos),
          mul_inv_cancel₀ (ne_of_gt hc_pos), mul_one]
    intro t
    have := ode_cosh_uniqueness_contdiff g (h2.comp (contDiff_id.div_const _))
      hg_ode (by simp [g, h_one]) (by rw [(hg_d 0).deriv]; simp [h_H'0])
      (Real.sqrt c * t)
    simp only [g, mul_div_cancel_left₀ _ hsc_ne] at this; exact this
  · by_cases hc_neg : c < 0
    · -- c < 0: H = cos(√(−c) · t)
      right; right; refine ⟨Real.sqrt (-c), ?_⟩
      set c' := -c
      have hsc_ne : Real.sqrt c' ≠ 0 := ne_of_gt (Real.sqrt_pos.mpr (neg_pos.mpr hc_neg))
      let g : ℝ → ℝ := fun s => H (s / Real.sqrt c')
      have h_div : ∀ s, HasDerivAt (fun x => x / Real.sqrt c') (Real.sqrt c')⁻¹ s := fun s => by
        have := (hasDerivAt_id s).div_const (Real.sqrt c'); simp only [id, one_div] at this; exact this
      have hg_d : ∀ s, HasDerivAt g (deriv H (s / Real.sqrt c') * (Real.sqrt c')⁻¹) s :=
        fun s => (hDiff _).hasDerivAt.comp s (h_div s)
      have hg_ode : ∀ t, deriv (deriv g) t = -(g t) := by
        intro s
        have hg1 : deriv g = fun s => deriv H (s / Real.sqrt c') * (Real.sqrt c')⁻¹ :=
          funext fun s => (hg_d s).deriv
        have h_dd_g : HasDerivAt (deriv g)
            ((deriv (deriv H) (s / Real.sqrt c') * (Real.sqrt c')⁻¹) * (Real.sqrt c')⁻¹) s := by
          rw [hg1]
          exact ((hDD (s / Real.sqrt c')).hasDerivAt.comp s (h_div s)).mul_const _
        rw [h_dd_g.deriv, h_ode (s / Real.sqrt c')]
        simp only [g, c']
        rw [show c * H (s / Real.sqrt (-c)) * (Real.sqrt (-c))⁻¹ * (Real.sqrt (-c))⁻¹ =
            H (s / Real.sqrt (-c)) * (c * ((Real.sqrt (-c))⁻¹ * (Real.sqrt (-c))⁻¹)) from by ring,
            show (Real.sqrt (-c))⁻¹ * (Real.sqrt (-c))⁻¹ = (Real.sqrt (-c) * Real.sqrt (-c))⁻¹ from
              (mul_inv_rev _ _).symm,
            Real.mul_self_sqrt (le_of_lt (neg_pos.mpr hc_neg)),
            show c * (-c)⁻¹ = -(1 : ℝ) from by
              have hc_ne : c ≠ 0 := ne_of_lt hc_neg
              field_simp]
        ring
      intro t
      have := ode_cos_uniqueness g (h2.comp (contDiff_id.div_const _))
        hg_ode (by simp [g, h_one]) (by rw [(hg_d 0).deriv]; simp [h_H'0])
        (Real.sqrt c' * t)
      simp only [g, mul_div_cancel_left₀ _ hsc_ne] at this; exact this
    · -- c = 0: H ≡ 1
      left
      have hc0 : c = 0 := le_antisymm (not_lt.mp hc_pos) (not_lt.mp hc_neg)
      have h_H'_zero : ∀ t, deriv H t = 0 := by
        have := is_const_of_deriv_eq_zero hDD (fun t => by rw [h_ode t, hc0, zero_mul])
        intro t; have := this t 0; simp [h_H'0] at this; exact this
      intro t
      have := is_const_of_deriv_eq_zero hDiff h_H'_zero t 0
      simp [h_one] at this; exact this

What this page does not claim

The lemma does not apply to solutions with nonzero initial conditions. The lemma says nothing about the cost function J or its physical meaning. The lemma is not a statement about recognition events themselves.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Cost/AczelProof.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND