Encyclopedia Cost Cost Aczel Proof D Alembert Classification

ARTICLE 1 claim 1 theorem

Cost Aczel Proof D Alembert Classification

A single functional equation, with only continuity assumed, forces its solutions to be exactly three familiar families: constant, hyperbolic cosine, or cosine.

Verify this page

The classification theorem

The d'Alembert functional equation is a classical object. It asks for functions H that satisfy H(t + u) + H(t − u) = 2·H(t)·H(u). This is a kind of addition law: it says the value at a sum and a difference combine in a way governed only by the values at the two inputs. The equation appears across mathematics, most famously in the theory of trigonometric functions, where both cosine and hyperbolic cosine obey it.

The classical classification, due to Jean le Rond d'Alembert in the 18th century and refined by János Aczél in his 1966 Lectures on Functional Equations, is a striking rigidity result. If a function H from the real line to itself satisfies the equation, has H(0) = 1, and is merely continuous, then it must be exactly one of three things: the constant function 1, a hyperbolic cosine H(x) = cosh(αx), or a cosine H(x) = cos(αx), for some real number α. Continuity alone, with no differentiability assumed, forces the solution into these smooth families. The proof proceeds by an integration bootstrap: continuity lets one construct an antiderivative, which is differentiable; the equation then upgrades differentiability to smoothness, and the smooth function satisfies the ordinary differential equation H'' = c·H. Solving that ODE gives the three families.

In Recognition Science, the framework's machine-checked library of formal theorems proves this classification in full. The declaration dAlembert_classification is a theorem: for any continuous H with H(0) = 1 satisfying the equation, the conclusion is a disjunction of the three explicit forms. The proof is fully formalized, from the integration bootstrap through the ODE uniqueness arguments, with no gaps. This matters for the framework because the d'Alembert equation is a cousin of the cost equation, the function J(x) = (x + 1/x)/2 − 1 that the framework derives from five plain conditions. The classification shows that the cost equation's smoothness is not an extra assumption but a consequence of its structure.

What the theorem does not claim is as important as what it proves. It does not assert that every solution of the d'Alembert equation is the cost function J; the three families are far more general. It does not identify which α corresponds to any physical constant or framework parameter. It does not prove that the cost equation itself has a unique solution; that is a separate theorem. And it does not say anything about discontinuous solutions, which exist in abundance once continuity is dropped. The theorem is a classification of continuous solutions only, and it is that classification, not a uniqueness result, that the framework's library establishes.

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 theorem does not identify the cost function J as a solution of the d'Alembert equation. The theorem does not prove uniqueness of solutions to the cost equation. The theorem says nothing about discontinuous solutions, which exist without the continuity assumption.

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