Foundation Dalembert Proof Is Dalembert Solution

The d'Alembert equation

The d'Alembert functional equation is a classical object in mathematics. It asks for functions H such that H(t+u) + H(t-u) = 2 H(t) H(u) for all real numbers t and u, with the normalization H(0) = 1. Its continuous solutions were classified by János Aczél in 1966: they are the constant function 1, the cosine functions cos(αt), and the hyperbolic cosine functions cosh(αt). The equation appears in geometry and physics wherever a quantity must combine symmetrically under addition and subtraction, such as the addition formulas for trigonometric functions.

In the Recognition Science framework, this equation is not an arbitrary axiom. The framework's library contains a definition, called IsDAlembertSolution, which states that a function H from real numbers to real numbers satisfies exactly the two conditions H(0) = 1 and H(t+u) + H(t-u) = 2 H(t) H(u) for all t and u. The library proves, as a formal theorem, that any such solution must be an even function: H(-t) = H(t) for all t. It also proves that if such a solution is differentiable at zero, its derivative there is zero. These are immediate consequences of the defining equation.

The framework shows that this equation is forced. Starting from a cost functional F that measures the price of recognition, and requiring symmetry, normalization, and a multiplicative consistency condition, the framework derives the d'Alembert form. The proof transforms to logarithmic coordinates, constrains the combining function Φ by evenness and symmetry, and then applies Aczél's classification. With the additional calibration condition H''(0) = 1, only the hyperbolic cosine solution survives, giving H(t) = cosh(t). This is the unique smooth solution under those hypotheses.

What the declaration does not claim is important. The definition itself only states the equation; it does not assert that every solution is cosh. The classification theorem requires additional regularity hypotheses: continuity, the calibration condition, and several smoothness assumptions. Without those, the equation admits the constant solution H(t) = 1 and the cosine family. The full uniqueness result, that the cost must be J(x) = (x + 1/x)/2 - 1, lives in a separate module and depends on the complete forcing chain, not on this definition alone.

/-- D'Alembert solutions are even. -/
theorem dAlembert_solution_even (H : ℝ → ℝ) (h : IsDAlembertSolution H) :
    Function.Even H := by
  have h0 := h.1
  have heq := h.2
  intro u
  have := heq 0 u
  simp only [zero_add, zero_sub, h0, two_mul] at this
  linarith

/-- The classification theorem for d'Alembert equation (Aczél).

Continuous solutions to H(t+u) + H(t-u) = 2·H(t)·H(u) with H(0) = 1 are:
1. H(t) = 1 (constant)
2. H(t) = cos(αt) for some α ∈ ℂ
3. H(t) = cosh(αt) for some α ∈ ℝ

With the calibration H''(0) = 1, only H = cosh survives. -/
theorem dAlembert_classification (H : ℝ → ℝ)
    (h : IsDAlembertSolution H)
    (hCont : Continuous H)
    (hCalib : deriv (deriv H) 0 = 1)
    -- Regularity hypotheses (from Aczél theory)
    (hSmooth : dAlembert_continuous_implies_smooth_hypothesis H)
    (hODE : dAlembert_to_ODE_hypothesis H)
    (hODECont : ode_regularity_continuous_hypothesis H)
    (hODEDiff : ode_regularity_differentiable_hypothesis H)
    (hBoot : ode_linear_regularity_bootstrap_hypothesis H) :
    ∀ t, H t = cosh t :=
  dAlembert_cosh_solution H h.1 hCont h.2 hCalib hSmooth hODE hODECont hODEDiff hBoot

/-- D'Alembert solutions satisfy H'(0) = 0 if differentiable. -/
theorem dAlembert_solution_deriv_zero (H : ℝ → ℝ) (h : IsDAlembertSolution H)
    (hDiff : DifferentiableAt ℝ H 0) :
    deriv H 0 = 0 := by
  have hEven := dAlembert_solution_even H h
  exact even_deriv_at_zero H hEven hDiff

What this page does not claim

The definition alone does not classify all solutions; the cosine and constant solutions remain valid without the calibration condition. The full uniqueness of the cost functional J is not established in this module; it lives in Cost.FunctionalEquation. The polynomial-combiner uniqueness argument is a scoped sketch, not a formal theorem in this file.

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/DAlembert/Proof.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: