Encyclopedia Cost Cost Aczel Theorem H Aczel Classification Proved

ARTICLE 3 claims 3 theorems

Cost Aczel Theorem H Aczel Classification Proved

A classical equation from 18th-century physics turns out to have only three possible solutions, and a machine-checked proof now shows that continuity alone forces them all to be perfectly smooth.

Verify this page

The smoothness theorem

The d'Alembert equation, H(t+u) + H(t-u) = 2·H(t)·H(u), with H(0) = 1, is a functional equation: it constrains a function's values at every pair of points. It first appeared in Jean le Rond d'Alembert's 1747 work on vibrating strings, where H described the shape of a plucked string at a fixed time. The equation is strong enough that its only continuous solutions are the constant function 1, the hyperbolic cosine cosh(λt), and the ordinary cosine cos(λt), where λ is any real number. This classification, due to János Aczél in his 1966 monograph, is a standard result in the theory of functional equations.

What the Recognition Science declaration h_aczel_classification_proved adds is a fully machine-checked proof of a stronger regularity statement. The theorem establishes that every continuous solution of the d'Alembert equation with H(0) = 1 is not merely continuous but infinitely differentiable, meaning it has derivatives of every order. The proof proceeds by an integration bootstrap: from continuity, one constructs an antiderivative, uses the functional equation to express H in terms of that antiderivative, and then iterates, showing that each new level of differentiability of the antiderivative implies one more level for H itself. This yields H'' = c·H for a constant c, and the classification follows by solving this ordinary differential equation.

The declaration therefore proves the Aczél classification unconditionally, with no axioms beyond the standard logical framework. In the Recognition Science framework, this result is significant because the d'Alembert equation is the composition law that forces the cost function J(x) = (x + 1/x)/2 − 1. The proof of h_aczel_classification_proved eliminates the last remaining foundation hypothesis, so the entire cost-function derivation now rests on proved theorems rather than on an assumed smoothness condition.

The theorem does not claim that the classification itself is new, nor does it derive the value of the constant λ. It also does not say that all solutions of the d'Alembert equation are smooth, only those that are continuous. Discontinuous solutions exist, though they are pathological and not relevant to the framework's applications. The result is a regularity theorem: it upgrades a continuity assumption to infinite differentiability, and it does so by a fully verified argument.

THEOREM dAlembert_contDiff_top · IndisputableMonolith/Cost/AczelTheorem.lean
dAlembert_contDiff_top · IndisputableMonolith/Cost/AczelTheorem.lean:351 
/-- The full Aczél classification theorem. Continuous d'Alembert with H(0) = 1
    implies H ∈ {cosh(λ·), cos(λ·), 1}, all of which are C^∞. -/
private theorem dAlembert_contDiff_top (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) :
    ContDiff ℝ ⊤ H := 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
  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
  · -- Case c > 0: H = cosh(√c · t)
    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]
    have h_eq : ∀ t, H t = Real.cosh (Real.sqrt c * t) := fun t => by
      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
    rw [show H = fun t => Real.cosh (Real.sqrt c * t) from funext h_eq]
    exact Real.contDiff_cosh.comp (contDiff_const.mul contDiff_id)
  · by_cases hc_neg : c < 0
    · -- Case c < 0: H = cos(√|c| · t)
      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
      have h_eq : ∀ t, H t = Real.cos (Real.sqrt c' * t) := fun t => by
        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
      rw [show H = fun t => Real.cos (Real.sqrt c' * t) from funext h_eq]
      exact Real.contDiff_cos.comp (contDiff_const.mul contDiff_id)
    · -- Case c = 0: H = 1
      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
      rw [show H = fun _ => (1 : ℝ) from funext fun t => by
        have := is_const_of_deriv_eq_zero hDiff h_H'_zero t 0
        simp [h_one] at this; exact this]
      exact contDiff_const
THEOREM dAlembert_to_ODE_general · IndisputableMonolith/Cost/AczelTheorem.lean
dAlembert_to_ODE_general · IndisputableMonolith/Cost/AczelTheorem.lean:231 
private theorem dAlembert_to_ODE_general (H : ℝ → ℝ)
    (h_smooth : ContDiff ℝ smooth H)
    (h_dAl : ∀ t u, H (t + u) + H (t - u) = 2 * H t * H u) :
    ∀ t, deriv (deriv H) t = deriv (deriv H) 0 * H t := by
  have h2 : ContDiff ℝ 2 H := by exact_mod_cast (contDiff_infty.mp h_smooth) 2
  have hDiff : Differentiable ℝ H := h2.differentiable (by decide : (2 : WithTop ℕ∞) ≠ 0)
  have hCDiff1_H' : ContDiff ℝ 1 (deriv H) := by
    rw [show (2 : WithTop ℕ∞) = 1 + 1 from rfl] at h2
    rw [contDiff_succ_iff_deriv] at h2; exact h2.2.2
  have hDiffDeriv : Differentiable ℝ (deriv H) :=
    hCDiff1_H'.differentiable (by decide : (1 : WithTop ℕ∞) ≠ 0)
  have hsh_add : ∀ (s v : ℝ), HasDerivAt (fun u => s + u) (1 : ℝ) v := fun s v => by
    have h := (hasDerivAt_id v).add_const s; simp only [id] at h
    rwa [show (fun u : ℝ => u + s) = fun u => s + u from funext fun u => add_comm u s] at h
  have hsh_sub : ∀ (s v : ℝ), HasDerivAt (fun u => s - u) (-1 : ℝ) v := fun s v => by
    have h1 : HasDerivAt (fun u : ℝ => -u) (-1 : ℝ) v := by
      have := (hasDerivAt_id v).neg; simp only [id] at this; exact this
    have h2 := h1.const_add s
    rwa [show (fun u : ℝ => s + -u) = fun u => s - u from funext fun u => by ring] at h2
  intro t
  have h_feq : (fun u => H (t + u) + H (t - u)) = (fun u => 2 * H t * H u) :=
    funext (h_dAl t)
  have key : deriv (deriv (fun u => H (t + u) + H (t - u))) 0 =
             deriv (deriv (fun u => 2 * H t * H u)) 0 :=
    congr_arg (fun f => deriv (deriv f) 0) h_feq
  have lhs_eq : deriv (deriv (fun u => H (t + u) + H (t - u))) 0 =
      2 * deriv (deriv H) t := by
    have h_plus : ∀ v, HasDerivAt (fun u => H (t + u)) (deriv H (t + v)) v := fun v => by
      have h := ((hDiff (t + v)).hasDerivAt).comp v (hsh_add t v)
      simp only [mul_one, Function.comp_def] at h; exact h
    have h_minus : ∀ v, HasDerivAt (fun u => H (t - u)) (-deriv H (t - v)) v := fun v => by
      have hcomp := ((hDiff (t - v)).hasDerivAt).comp v (hsh_sub t v)
      simp only [mul_neg, mul_one, Function.comp_apply] at hcomp; exact hcomp
    have hfirst : deriv (fun u => H (t + u) + H (t - u)) =
        fun v => deriv H (t + v) - deriv H (t - v) := funext fun v => by
      have h12 := ((h_plus v).add (h_minus v)).deriv
      rw [show (fun u => H (t + u)) + (fun u => H (t - u)) =
          fun u => H (t + u) + H (t - u) from by ext u; rfl] at h12; linarith [h12]
    have hd2p : HasDerivAt (fun v => deriv H (t + v)) (deriv (deriv H) t) 0 := by
      have := ((hDiffDeriv (t + 0)).hasDerivAt).comp 0 (hsh_add t 0)
      simpa using this
    have hd2m : HasDerivAt (fun v => deriv H (t - v)) (-deriv (deriv H) t) 0 := by
      have := ((hDiffDeriv (t - 0)).hasDerivAt).comp 0 (hsh_sub t 0)
      simpa using this
    rw [congr_fun (congr_arg deriv hfirst) 0,
        show (fun v => deriv H (t + v) - deriv H (t - v)) =
          (fun v => deriv H (t + v)) - (fun v => deriv H (t - v)) from rfl]
    linarith [(hd2p.sub hd2m).deriv]
  have rhs_eq : deriv (deriv (fun u => 2 * H t * H u)) 0 =
      2 * H t * deriv (deriv H) 0 := by
    have hf : deriv (fun u => 2 * H t * H u) = fun v => 2 * H t * deriv H v :=
      funext fun v => ((hDiff v).hasDerivAt.const_mul (2 * H t)).deriv
    rw [congr_fun (congr_arg deriv hf) 0, ((hDiffDeriv 0).hasDerivAt.const_mul (2 * H t)).deriv]
  rw [lhs_eq, rhs_eq] at key; linarith
THEOREM h_aczel_classification_proved · IndisputableMonolith/Cost/AczelTheorem.lean
h_aczel_classification_proved · IndisputableMonolith/Cost/AczelTheorem.lean:450 
/-- **THEOREM (Aczél, PROVED)**: `H_AczelClassification` holds unconditionally.
    This eliminates the sole remaining foundation axiom. -/
theorem h_aczel_classification_proved : H_AczelClassification :=
  fun H h_one h_cont h_dAlembert => dAlembert_contDiff_top H h_one h_cont h_dAlembert

-- The typeclass-parameterized `aczel_dAlembert_smooth` lives in
-- `IndisputableMonolith.Cost.AczelClass` and is satisfied by the
-- `AczelSmoothnessPackage` instance in `IndisputableMonolith.Cost.AczelProof`,
-- which delegates to `dAlembert_contDiff_top` above.

What this page does not claim

The theorem does not claim that the classification is new. It does not claim that all solutions of the d'Alembert equation are smooth, only continuous ones. It does not claim to derive the value of the constant λ.

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/AczelTheorem.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