Encyclopedia Foundation Foundation Axiom Discharge Plan

ARTICLE 4 claims 4 theorems

Foundation Axiom Discharge Plan

A classical equation from 1968, once assumed as an axiom, is now proved from simpler pieces inside the Recognition Science framework.

Verify this page

The discharge plan

The plan concerns the d'Alembert functional equation, a classical relation that asks for functions H satisfying H(x + y) + H(x − y) = 2H(x)H(y). Its continuous solutions were classified in 1968 by János Aczél and Pl. Kannappan: the solutions are the constant 1, the hyperbolic cosine cosh(αx), and the cosine cos(βx). This classification is a standard result in functional equations, and Recognition Science's machine-checked library of formal theorems had previously recorded it as a named classical input, an axiom rather than a proved statement.

The discharge plan is the work of replacing that axiom with a proof. The key observation is that a smooth solution H with H(0) = 1 satisfies the ordinary differential equation H''(t) = H''(0)·H(t), a bridge proved in the framework's cost functional equation module. The sign of H''(0) then decides the solution family: zero gives the constant 1, positive gives cosh, negative gives cosine. Each case reduces to a standard uniqueness theorem for a linear ODE with prescribed initial conditions. For example, a C² function f satisfying f'' = −f with f(0) = 1 and f'(0) = 0 must be exactly cos(t), proved by an energy method. The cosine case rescales to this unit-frequency result, and the cosh case rescales to the already-proved cosh solution theorem.

In Recognition Science, this discharge matters because the framework's central result, the forced cost function J(x) = (x + 1/x)/2 − 1, relies on the d'Alembert classification. The plan turns a borrowed classical theorem into a proved consequence of the framework's own structure. The module AxiomDischargePlan contains the four proved theorems: ode_constant_case, ode_cosine_case, cosh_rescaling_lemma, and aczel_kannappan_via_cases, each with no sorry or local axiom declarations. The original opaque axiom is now a corollary of these pieces plus the framework's existing smoothness lifting.

The practical upshot is a cleaner foundation. Where the framework once leaned on an unproved classical input, it now derives the same result from a finite, concrete combination of ODE uniqueness theorems. This is part of a broader program to reduce every external assumption to proved statements, making the framework's logical spine more transparent and self-contained.

THEOREM dAlembert_to_ODE_general · IndisputableMonolith/Foundation/AxiomDischargePlan.lean
dAlembert_to_ODE_general · IndisputableMonolith/Foundation/AxiomDischargePlan.lean:316 
/-- **General ODE bridge (proved in `Cost.FunctionalEquation`)**: a smooth
d'Alembert solution `H` with `H(0) = 1` satisfies `H''(t) = H''(0) · H(t)`
for every `t`. This is the universal form of the existing
`dAlembert_to_ODE_theorem`, which only states the special case
`H''(0) = 1`. The general statement follows from the same calculation
with no normalization. -/
theorem dAlembert_to_ODE_general
    (H : ℝ → ℝ) (h_smooth : ContDiff ℝ ⊤ H)
    (h_dAlembert : ∀ x y, H (x + y) + H (x - y) = 2 * H x * H y) :
    ∀ t, deriv (deriv H) t = (deriv (deriv H) 0) * H t :=
  dAlembert_to_ODE_general_theorem H h_smooth h_dAlembert
THEOREM ode_neg_zero_uniqueness · IndisputableMonolith/Foundation/AxiomDischargePlan.lean
ode_neg_zero_uniqueness · IndisputableMonolith/Foundation/AxiomDischargePlan.lean:73 
/-- **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)]
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 discharge plan does not prove the full Aczél–Kannappan classification without the smoothness assumption; it relies on the framework's AczelSmoothnessPackage. This module does not derive the cost function J itself; it only discharges a classical input used in that derivation. The plan does not claim the original axiom was false, only that it is now redundant.

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