Foundation Dalembert Proof D Alembert Solution Even

The evenness lemma

The d'Alembert functional equation is a classical object in mathematics, studied since the 18th century. It asks for functions H that satisfy H(t+u) + H(t-u) = 2H(t)H(u) for all real numbers t and u, together with the normalization H(0) = 1. This equation appears across analysis, from trigonometric identities to the theory of group representations. The standard continuous solutions are exactly the constant function 1, the cosine functions cos(αt), and the hyperbolic cosine functions cosh(αt), a classification due to János Aczél in his 1966 monograph on functional equations.

One structural property follows immediately from the equation itself, with no continuity or differentiability assumptions: every solution is even, meaning H(-t) = H(t) for every t. The proof is a one-line calculation. Set u = 0 in the equation. The left side becomes H(t) + H(-t). The right side becomes 2H(t)H(0), which equals 2H(t) because H(0) = 1. Hence H(-t) = H(t). This is the content of the machine-checked theorem dAlembert_solution_even in the framework's library, a collection of formal theorems verified by computer. The theorem states: if H is a solution of the d'Alembert equation with H(0) = 1, then H is even.

A second, related property holds when H is differentiable at 0: the derivative H'(0) must be 0. This follows from evenness, since the derivative of an even function at the origin vanishes. The library records this as dAlembert_solution_deriv_zero. Both results are elementary consequences of the defining equation, not of any deeper regularity assumption.

In Recognition Science, the framework models cost functions as solutions to a shifted version of this equation. The framework's central object is a cost function J(x) = (x + 1/x)/2 - 1, which arises from a functional equation of the form F(xy) + F(x/y) = 2F(x) + 2F(y) + 2F(x)F(y). After a logarithmic change of variables, H(t) = F(e^t) + 1 satisfies the standard d'Alembert equation. The evenness lemma then translates into the symmetry F(x) = F(1/x), a property the framework's cost function indeed possesses. The evenness lemma is a small but load-bearing step in this chain: it guarantees the symmetry that the framework's uniqueness proof relies on.

The theorem does not claim that all solutions are even in any stronger sense, nor does it identify which solution the framework selects. It says only that evenness is necessary for any solution. The classification of all continuous solutions, and the calibration H''(0) = 1 that selects the hyperbolic cosine, are separate theorems in the library. The evenness lemma is a necessary condition, not a sufficient one.

/-- 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 theorem does not classify all solutions; it only establishes a necessary symmetry condition. The theorem does not assert that every even function satisfying the normalization is a solution. The theorem does not prove the uniqueness of the cost function J; that is a separate result in the library.

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: