Encyclopedia Foundation Foundation Axiom Discharge Plan Ode Cosine Case

ARTICLE 3 claims 3 theorems

Foundation Axiom Discharge Plan Ode Cosine Case

A machine-checked theorem pins down the only smooth function that solves a simple second-order equation with given starting values: the cosine.

Verify this page

The cosine uniqueness theorem

The cosine is the familiar wave that repeats every 2π and starts at its maximum value 1. This page concerns a precise uniqueness statement about it. The statement is one of the standard facts of calculus: if a twice-differentiable function f satisfies f''(t) = -f(t) for all t, with f(0) = 1 and f'(0) = 0, then f is exactly the cosine function. The Recognition Science framework's library of formal theorems contains a machine-checked proof of this fact, under the name ode_cos_unit_uniqueness.

The framework's declaration ode_cosine_case extends that unit-frequency result to a general frequency. It states: if a twice-differentiable function H satisfies H''(x) = -β²·H(x) for all x, with H(0) = 1 and H'(0) = 0, and β is a positive real number, then H(x) = cos(β·x) for every x. The proof rescales the input by setting H_β(t) = H(t/β), which turns the general equation into the unit-frequency one, then applies the already-proved unit-frequency uniqueness theorem.

This theorem is not an isolated curiosity. It is one of the residual analytic inputs in a larger reduction plan. The framework previously relied on a named classical axiom, the Aczél–Kannappan continuous d'Alembert classification, which describes all continuous solutions of the functional equation H(x+y) + H(x-y) = 2H(x)H(y). That classification has three cases: the constant solution, the hyperbolic cosine (cosh) solution, and the cosine solution. The framework had already proved the cosh case. The declaration ode_cosine_case, together with a companion constant-case theorem, discharges the remaining two cases by reducing them to standard ODE uniqueness results. The original axiom is thereby replaced by a finite combination of proved theorems, with no unproved assumptions left in the chain.

In Recognition Science, this matters because the d'Alembert equation is a structural constraint that appears in the framework's derivation of the cost function J(x) = (x + 1/x)/2 - 1, the golden ratio, and related constants. The cosine case is the oscillatory branch of that classification. The theorem does not claim that the cosine itself is derived from the framework's axioms; it takes the cosine as a known classical function and proves a uniqueness property about it. The framework's contribution is the reduction: it shows that a previously assumed classical input can be proved from more basic principles, strengthening the axiom audit of the whole derivation chain.

THEOREM ode_cosine_case · IndisputableMonolith/Foundation/AxiomDischargePlan.lean
ode_cosine_case · IndisputableMonolith/Foundation/AxiomDischargePlan.lean:148 
/-- **Cosine case (proved)**: a smooth function with `H(0) = 1`,
`H'(0) = 0`, and `H''(x) = -β² · H(x)` is `cos(β·)`. We rescale
`H_β(t) := H(t/β)` to reduce to the unit-frequency cosine uniqueness
theorem. -/
theorem ode_cosine_case
    (H : ℝ → ℝ) (h_smooth : ContDiff ℝ 2 H)
    (h_one : H 0 = 1) (h_deriv0 : deriv H 0 = 0)
    {β : ℝ} (hβ : 0 < β)
    (h_d2 : ∀ x, deriv (deriv H) x = -β ^ 2 * H x) :
    ∀ x, H x = Real.cos (β * x) := by
  have hβ_ne : (β : ℝ) ≠ 0 := ne_of_gt hβ
  let Hβ : ℝ → ℝ := fun t => H (t / β)
  have hβ_smooth : ContDiff ℝ 2 Hβ := by
    have hlin : ContDiff ℝ 2 (fun t : ℝ => t / β) := contDiff_id.div_const β
    exact h_smooth.comp hlin
  have hβ_one : Hβ 0 = 1 := by
    show H (0 / β) = 1
    rw [zero_div, h_one]
  have h_diff_H : Differentiable ℝ H :=
    h_smooth.differentiable (by decide : (2 : WithTop ℕ∞) ≠ 0)
  have hC2 : ContDiff ℝ 2 H := h_smooth
  have hC2eq : (2 : WithTop ℕ∞) = 1 + 1 := rfl
  rw [hC2eq] at hC2
  rw [contDiff_succ_iff_deriv] at hC2
  have h_diff_H' : Differentiable ℝ (deriv H) :=
    hC2.2.2.differentiable (by decide : (1 : WithTop ℕ∞) ≠ 0)
  have h_diff_phi : ∀ t, DifferentiableAt ℝ (fun x : ℝ => x / β) t :=
    fun t => (differentiableAt_id).div_const β
  have h_dHβ : ∀ t, deriv Hβ t = deriv H (t / β) / β := by
    intro t
    change deriv (fun s => H (s / β)) t = deriv H (t / β) / β
    have hcomp : (fun s => H (s / β)) = H ∘ (fun s => s / β) := rfl
    rw [hcomp, deriv_comp t (h_diff_H _) (h_diff_phi _)]
    rw [show deriv (fun s : ℝ => s / β) t = 1 / β from by
          rw [deriv_div_const]; simp]
    ring
  have hβ_deriv0 : deriv Hβ 0 = 0 := by
    rw [h_dHβ 0, zero_div, h_deriv0, zero_div]
  have h_d2Hβ : ∀ t, deriv (deriv Hβ) t = deriv (deriv H) (t / β) / β ^ 2 := by
    intro t
    have h_eq : deriv Hβ = fun t => deriv H (t / β) / β := by
      funext t
      exact h_dHβ t
    rw [h_eq]
    change deriv (fun s => deriv H (s / β) / β) t = deriv (deriv H) (t / β) / β ^ 2
    rw [deriv_div_const]
    change deriv (fun s => deriv H (s / β)) t / β
          = deriv (deriv H) (t / β) / β ^ 2
    have hcomp : (fun s => deriv H (s / β)) = (deriv H) ∘ (fun s => s / β) := rfl
    rw [hcomp, deriv_comp t (h_diff_H' _) (h_diff_phi _)]
    rw [show deriv (fun s : ℝ => s / β) t = 1 / β from by
          rw [deriv_div_const]; simp]
    field_simp
  have hβ_ode : ∀ t, deriv (deriv Hβ) t = -(Hβ t) := by
    intro t
    rw [h_d2Hβ, h_d2 (t / β)]
    field_simp
    ring
  have hunit := ode_cos_unit_uniqueness Hβ hβ_smooth hβ_ode hβ_one hβ_deriv0
  intro x
  have hkey : H (β * x / β) = Real.cos (β * x) := hunit (β * x)
  have hcancel : β * x / β = x := by field_simp
  rw [hcancel] at hkey
  exact hkey
THEOREM ode_cos_unit_uniqueness · IndisputableMonolith/Foundation/AxiomDischargePlan.lean
ode_cos_unit_uniqueness · IndisputableMonolith/Foundation/AxiomDischargePlan.lean:108 
/-- **Unit-frequency cosine uniqueness**: a C² solution of `f'' = -f`
with `f(0)=1` and `f'(0)=0` is `cos`. -/
theorem ode_cos_unit_uniqueness (f : ℝ → ℝ)
    (h_diff : ContDiff ℝ 2 f)
    (h_ode : ∀ t, deriv (deriv f) t = -(f t))
    (h_f0 : f 0 = 1) (h_f'0 : deriv f 0 = 0) :
    ∀ t, f t = Real.cos t := by
  let g := fun t => f t - Real.cos t
  have hg_diff : ContDiff ℝ 2 g := h_diff.sub Real.contDiff_cos
  have hDf : Differentiable ℝ f :=
    h_diff.differentiable (by decide : (2 : WithTop ℕ∞) ≠ 0)
  have hg_ode : ∀ t, deriv (deriv g) t = -(g t) := by
    intro t
    have h1 : deriv g = fun s => deriv f s - deriv Real.cos s :=
      funext fun s => deriv_sub hDf.differentiableAt Real.differentiable_cos.differentiableAt
    have hDf1 : ContDiff ℝ 1 (deriv f) := by
      rw [show (2 : WithTop ℕ∞) = 1 + 1 from rfl] at h_diff
      exact (contDiff_succ_iff_deriv.mp h_diff).2.2
    have hDcos1 : ContDiff ℝ 1 (deriv Real.cos) := by
      rw [Real.deriv_cos']; exact Real.contDiff_sin.neg
    have h2 : deriv (deriv g) t = deriv (deriv f) t - deriv (deriv Real.cos) t := by
      rw [h1]
      exact deriv_sub
        (hDf1.differentiable (by decide : (1 : WithTop ℕ∞) ≠ 0) |>.differentiableAt)
        (hDcos1.differentiable (by decide : (1 : WithTop ℕ∞) ≠ 0) |>.differentiableAt)
    rw [h2, h_ode t]
    have : deriv (deriv Real.cos) t = -(Real.cos t) := by
      have h_dcos : deriv Real.cos = fun x => -Real.sin x := Real.deriv_cos'
      rw [h_dcos]
      exact (Real.hasDerivAt_sin t).neg.deriv
    rw [this]
    ring
  have hg0 : g 0 = 0 := by simp [g, h_f0, Real.cos_zero]
  have hg'0 : deriv g 0 = 0 := by
    have : deriv g 0 = deriv f 0 - deriv Real.cos 0 :=
      deriv_sub hDf.differentiableAt Real.differentiable_cos.differentiableAt
    rw [this, h_f'0, Real.deriv_cos, Real.sin_zero, neg_zero, sub_zero]
  intro t
  linarith [ode_neg_zero_uniqueness g hg_diff hg_ode hg0 hg'0 t]
THEOREM aczel_kannappan_via_cases · IndisputableMonolith/Foundation/AxiomDischargePlan.lean
aczel_kannappan_via_cases · IndisputableMonolith/Foundation/AxiomDischargePlan.lean:328 
/-- **Aczél–Kannappan via the explicit reduction**: the discharge
puts the three cases together. We retain the conclusion's form to
match the original axiom. -/
theorem aczel_kannappan_via_cases
    [AczelSmoothnessPackage]
    (H : ℝ → ℝ) (h_cont : Continuous H) (h_one : H 0 = 1)
    (h_dAlembert : ∀ x y, H (x + y) + H (x - y) = 2 * H x * H y)
    (h_smooth : ContDiff ℝ ⊤ H) (h_deriv0 : deriv H 0 = 0)
    (h_classification : (deriv (deriv H) 0 = 0)
                       ∨ (∃ α : ℝ, 0 < α ∧ deriv (deriv H) 0 = α ^ 2)
                       ∨ (∃ β : ℝ, 0 < β ∧ deriv (deriv H) 0 = -β ^ 2)) :
    (∀ x, H x = 1) ∨
    (∃ α : ℝ, ∀ x, H x = Real.cosh (α * x)) ∨
    (∃ β : ℝ, ∀ x, H x = Real.cos (β * x)) := by
  have h_smooth2 : ContDiff ℝ 2 H := h_smooth.of_le le_top
  rcases h_classification with h0 | ⟨α, hα, hα2⟩ | ⟨β, hβ, hβ2⟩
  · left
    intro x
    exact ode_constant_case H h_smooth2 h_one h_deriv0
      (by
        intro y
        have hb := dAlembert_to_ODE_general H h_smooth h_dAlembert y
        rw [h0] at hb; simpa using hb) x
  · right; left
    refine ⟨α, ?_⟩
    intro x
    exact cosh_rescaling_lemma H h_one h_cont h_dAlembert hα hα2 x
  · right; right
    refine ⟨β, ?_⟩
    intro x
    have h_bridge : ∀ y, deriv (deriv H) y = -β ^ 2 * H y := by
      intro y
      have hb := dAlembert_to_ODE_general H h_smooth h_dAlembert y
      rw [hb, hβ2]
    exact ode_cosine_case H h_smooth2 h_one h_deriv0 hβ h_bridge x

What this page does not claim

The cosine function itself is not derived from the framework's axioms; it is a known classical function whose uniqueness property is proved. The theorem does not cover the case where β is zero or negative; those are handled separately or excluded by the hypothesis. The declaration does not prove the full Aczél–Kannappan classification from scratch; it proves the cosine case and relies on the existing cosh theorem for the other branch.

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/Foundation/AxiomDischargePlan.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