Encyclopedia Cost Cost Aczel Proof D Alembert Cont Diff Smooth

ARTICLE 2 claims 2 theorems

Cost Aczel Proof D Alembert Cont Diff Smooth

A continuous solution to a classical functional equation is always a smooth, infinitely differentiable function, a fact proved by a machine-checked library.

Verify this page

The smoothness theorem

The d'Alembert functional equation is a classical object in mathematics, named after Jean le Rond d'Alembert, who studied it in the 18th century. It asks for functions H from the real numbers to themselves that satisfy the identity H(t + u) + H(t - u) = 2 · H(t) · H(u) for all real t and u, with the normalization H(0) = 1. The equation encodes a kind of symmetry: the average of the function at two points symmetric about t equals the product of the function's values at those points. A standard question is what regularity assumptions on H are needed to force it to be well-behaved. The answer, proved by János Aczél in his 1966 lectures, is that mere continuity is enough. Any continuous solution is automatically infinitely differentiable, indeed real analytic, meaning it can be represented by a convergent power series around every point. This is a striking bootstrap: a weak, pointwise condition on a function implies the strongest smoothness property imaginable.

The theorem's proof proceeds in three stages. First, one shows that a continuous solution is infinitely differentiable. This is done by integrating the function to define a new function Phi, whose derivative is the original H. Because H satisfies the d'Alembert equation, this integral representation can be used to show that H itself is differentiable, and then by induction that it has derivatives of all orders. Second, using this smoothness, one derives a simple ordinary differential equation: the second derivative of H is a constant multiple of H itself, where the constant is the second derivative at zero. Third, solving this ODE yields a complete classification. The only continuous solutions are the constant function 1, the hyperbolic cosine cosh(α·t), and the ordinary cosine cos(α·t), for some real parameter α. Each of these is visibly real analytic, so the classification completes the proof of analyticity.

In Recognition Science, this theorem is not merely a historical curiosity. The framework's central result, that any cost function satisfying five plain conditions must equal J(x) = (x + 1/x)/2 - 1, is proved in a machine-checked library of formal theorems. The d'Alembert equation appears in the proof of this uniqueness theorem, and the smoothness result is what allows the framework to pass from continuous solutions to the explicit formula. The declaration dAlembert_contDiff_smooth in the library's file IndisputableMonolith/Cost/AczelProof.lean is the formal statement of the first stage: it says that any continuous solution H with H(0) = 1 is infinitely differentiable. This is a theorem in the library, meaning it is proved from the axioms of the underlying type theory with no additional assumptions. The library also contains the full classification theorem, dAlembert_classification, which lists the three possible forms of the solution.

The theorem is a pure statement about real functions; it does not, by itself, say anything about the cost function J or about the physical world. It is a lemma in a larger proof. The classification theorem does not claim that every solution is of one of the three forms; it says that every continuous solution is one of them. The theorem does not assert that the parameter α is unique, nor does it provide a numerical value for it. The framework's application of this theorem to the cost function is a separate step, and the theorem does not by itself establish the uniqueness of J. The theorem is a tool, not a conclusion about physics.

What the theorem changes is the shape of the search for a cost function. If a candidate cost function is merely continuous, one does not need to check smoothness separately; smoothness is forced. This reduces the space of possible solutions dramatically and makes the subsequent classification tractable. The reader can now see why the framework's uniqueness proof can be so short: the hard analytic work is done once, in the abstract setting of the d'Alembert equation, and the result is then available for any application.

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_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 assert that the parameter α is unique or provide a numerical value for it. The theorem does not by itself establish the uniqueness of the cost function J; it is a lemma in a larger proof. The theorem makes no statement about the physical world or about the Recognition Science framework's empirical claims.

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