Encyclopedia Cost Cost Aczel Proof D Alembert Cont Diff Nat

ARTICLE 3 claims 3 theorems

Cost Aczel Proof D Alembert Cont Diff Nat

A famous functional equation has a hidden regularity property: any continuous solution is automatically infinitely differentiable.

Verify this page

The smoothness theorem

The d'Alembert functional equation, H(t + u) + H(t − u) = 2·H(t)·H(u), is a classical object in analysis. It asks for functions H from the real line to itself whose value at a sum and difference of two inputs relates to the product of their individual values. The equation appears in geometry, probability, and the study of trigonometric functions; the familiar identities for cosine and hyperbolic cosine are its best-known solutions.

A theorem of J. Aczél, published in his 1966 Lectures on Functional Equations, states a striking regularity result: if a solution H is merely continuous and satisfies H(0) = 1, then H is not just continuous but infinitely differentiable, in fact real analytic. The proof proceeds by a bootstrap argument. First, one represents H as a derivative of an antiderivative, which shows that continuity implies differentiability. Repeating this argument shows that H is C∞. Then the functional equation itself forces a second-order ordinary differential equation, H'' = c·H, with c = H''(0). Solving this ODE gives the classification: H is either the constant 1, a hyperbolic cosine cosh(α·t), or a cosine cos(α·t) for some real α. Each of these is real analytic, so the conclusion follows.

The Recognition Science framework's machine-checked library of formal theorems contains a proof of this classical result. The declaration dAlembert_contDiff_nat establishes the smoothness claim for every finite order of differentiability: for any natural number n, the solution H is n-times continuously differentiable. A companion declaration dAlembert_contDiff_smooth extends this to the full C∞ statement, and dAlembert_classification gives the explicit trichotomy into constant, cosh, and cos. These are formal theorems, checked by a proof assistant, with no additional axioms beyond the standard logical ones.

What the declaration does not claim is just as important. It does not assert that every solution of the equation is of the form cosh or cos; that requires the continuity assumption, and without it there exist wild, non-continuous solutions. It does not say anything about the specific value of the constant c = H''(0), which is left as a parameter that determines which of the three solution families appears. And it does not, by itself, connect the functional equation to the Recognition Science framework's cost function J(x) = (x + 1/x)/2 − 1; that connection is a separate theorem in the library. The smoothness theorem is a piece of classical analysis, formalized, not a claim about the framework's own objects.

The practical consequence is that the framework's library can rely on the full power of calculus when working with solutions of the d'Alembert equation. Any continuous solution is smooth enough for differentiation, integration, and power series expansions, which makes the later classification and uniqueness arguments rigorous. For a reader, the theorem is a bridge: a classical result, proved in a modern formal system, that shows how the framework builds on standard mathematics rather than replacing it.

THEOREM dAlembert_contDiff_smooth · IndisputableMonolith/Cost/AczelProof.lean
dAlembert_contDiff_smooth · IndisputableMonolith/Cost/AczelProof.lean:165 
private theorem dAlembert_contDiff_smooth (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 ℝ smooth H :=
  contDiff_infty.mpr (dAlembert_contDiff_nat H h_one h_cont h_dAl)
THEOREM dAlembert_to_ODE_general · IndisputableMonolith/Cost/AczelProof.lean
dAlembert_to_ODE_general · IndisputableMonolith/Cost/AczelProof.lean:172 
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 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 apply to discontinuous solutions, which can behave pathologically. It does not specify the value of c = H''(0), which is a free parameter. It does not by itself connect the equation to the Recognition Science cost function J.

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