Foundation Axiom Discharge Plan Ode Cos Unit Uniqueness

The uniqueness of cosine

The cosine function is one of the most familiar objects in mathematics, but pinning it down precisely requires more than a graph or a table of values. A standard way to define it exactly is through a differential equation: the function whose second derivative is its own negative, which starts at 1 with an initial slope of 0. The declaration ode_cos_unit_uniqueness establishes that this description is complete: any twice-differentiable function satisfying f''(t) = -f(t), with f(0) = 1 and f'(0) = 0, must be exactly cos(t) for every real number t.

This is a uniqueness theorem, not a new definition of cosine. It says that the differential equation has only one solution under those starting conditions, so the familiar cosine is the unique function that fits the description. The proof uses the standard energy method: it defines a quantity E(t) = f(t)² + f'(t)², shows this quantity stays constant, and then uses the initial conditions to show the constant is 1, which forces f to be cosine. The declaration is part of a larger effort in the machine-checked library of formal theorems to replace previously assumed classical results with fully verified statements, and this particular theorem closes a gap by handling the cosine case directly.

In Recognition Science, this theorem serves a specific role in the framework's development. The framework models reality as maintaining a discrete record of recognition events, and from that starting point it derives a cost function and a chain of consequences. Along the way, it needs to classify solutions to a functional equation known as the d'Alembert equation, and that classification splits into three cases: constant, hyperbolic cosine, and cosine. The ode_cos_unit_uniqueness theorem provides the rigorous foundation for the cosine case, ensuring that the classification is complete and rests on verified mathematics rather than on an unexamined assumption.

The theorem does not claim anything about the physical meaning of cosine or about the framework's broader conclusions. It is a purely mathematical statement about a differential equation, and its proof is self-contained. It does not assert that the framework's derivation of physical constants is correct, nor does it address the empirical checks of those constants against measured values. The declaration is a precise mathematical tool, and its value lies in the fact that it is verified, not in any direct physical interpretation.

What this means for the framework is that one more piece of its foundation is now on solid ground. The classification of d'Alembert solutions no longer depends on an opaque assumption; instead, each case, including the cosine case, is backed by a theorem that has been checked by a machine. This is a step toward the framework's goal of deriving its structure from explicit, verified starting points, and it shows how a classical mathematical result can be integrated into a larger formal system.

/-- **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]

/-- **Zero uniqueness for `f'' = -f`**: if `f(0)=0` and `f'(0)=0`,
then `f ≡ 0`. Proof by conservation of the energy
`E(t) = f(t)^2 + f'(t)^2`. -/
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)
  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)]

What this page does not claim

This theorem does not assign any physical meaning to the cosine function. It does not assert that the framework's derivation of physical constants is correct. It does not address the empirical checks of the framework's constants against measured values.

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: