Encyclopedia Cost Cost Aczel Theorem D Alembert Double Angle

ARTICLE 3 claims 3 theorems

Cost Aczel Theorem D Alembert Double Angle

A single equation from 1747 about waves and vibrating strings turns out to force every smooth solution into one of three familiar shapes.

Verify this page

The double-angle identity

The d'Alembert equation, written H(t+u) + H(t-u) = 2·H(t)·H(u) with H(0) = 1, is a functional equation: it constrains a function's values at sums and differences of its inputs. Jean le Rond d'Alembert introduced it in 1747 while studying the vibrating string, and it appears across physics wherever waves add and cancel. The equation's solutions are exactly the ordinary hyperbolic and circular functions: H(t) = 1, H(t) = cosh(λt), and H(t) = cos(λt), up to a scale factor λ. This classification, due to János Aczél in 1966, is a standard result in functional equations.

The double-angle identity is a simple consequence of the d'Alembert equation. Set u = t in the defining equation: H(2t) + H(0) = 2·H(t)², and since H(0) = 1, this gives H(2t) = 2·H(t)² − 1. This is the same identity that cos(2θ) = 2cos²θ − 1 satisfies, and it holds for every solution of the d'Alembert equation, not just the trigonometric ones. The Recognition Science library proves this as a theorem: any function H satisfying the d'Alembert equation with H(0) = 1 must satisfy the double-angle identity for all real t.

In Recognition Science, this identity is a stepping stone in a larger proof. The framework's library, a machine-checked collection of formal theorems, uses the double-angle identity to establish that every continuous solution of the d'Alembert equation is infinitely differentiable, and then classifies all such solutions as exactly the three families above. This classification removes the last unproved assumption from the framework's foundation, replacing it with a proved theorem. The double-angle identity itself is the first step in that chain: it gives a concrete algebraic relation that any solution must obey, which the framework then uses to bootstrap smoothness and derive the classification.

What the declaration does not claim is equally precise. It does not assert that the double-angle identity holds for every function, only for those satisfying the d'Alembert equation with H(0) = 1. It does not claim that the identity alone classifies solutions; the classification requires continuity and the full d'Alembert equation, not just the double-angle consequence. And it does not claim that the d'Alembert equation itself is derived from Recognition Science principles; the equation is a classical object that the framework takes as given and then analyzes.

THEOREM dAlembert_double_angle · IndisputableMonolith/Cost/AczelTheorem.lean
dAlembert_double_angle · IndisputableMonolith/Cost/AczelTheorem.lean:66 
/-- H3: d'Alembert + H(0)=1 implies H(2t) = 2H(t)² − 1. -/
theorem dAlembert_double_angle (H : ℝ → ℝ)
    (h_one : H 0 = 1)
    (h_dAlembert : ∀ t u, H (t + u) + H (t - u) = 2 * H t * H u) :
    ∀ t, H (2 * t) = 2 * H t ^ 2 - 1 := by
  intro t
  have h := h_dAlembert t t
  have : t + t = 2 * t := by ring
  rw [this] at h
  have : t - t = 0 := by ring
  rw [this, h_one] at h
  nlinarith [sq (H t)]
THEOREM dAlembert_contDiff_top · IndisputableMonolith/Cost/AczelTheorem.lean
dAlembert_contDiff_top · IndisputableMonolith/Cost/AczelTheorem.lean:351 
/-- The full Aczél classification theorem. Continuous d'Alembert with H(0) = 1
    implies H ∈ {cosh(λ·), cos(λ·), 1}, all of which are C^∞. -/
private theorem dAlembert_contDiff_top (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 ℝ ⊤ H := 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
  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
  · -- Case c > 0: H = cosh(√c · t)
    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]
    have h_eq : ∀ t, H t = Real.cosh (Real.sqrt c * t) := fun t => by
      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
    rw [show H = fun t => Real.cosh (Real.sqrt c * t) from funext h_eq]
    exact Real.contDiff_cosh.comp (contDiff_const.mul contDiff_id)
  · by_cases hc_neg : c < 0
    · -- Case c < 0: H = cos(√|c| · t)
      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
      have h_eq : ∀ t, H t = Real.cos (Real.sqrt c' * t) := fun t => by
        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
      rw [show H = fun t => Real.cos (Real.sqrt c' * t) from funext h_eq]
      exact Real.contDiff_cos.comp (contDiff_const.mul contDiff_id)
    · -- Case c = 0: H = 1
      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
      rw [show H = fun _ => (1 : ℝ) from funext fun t => by
        have := is_const_of_deriv_eq_zero hDiff h_H'_zero t 0
        simp [h_one] at this; exact this]
      exact contDiff_const
THEOREM h_aczel_classification_proved · IndisputableMonolith/Cost/AczelTheorem.lean
h_aczel_classification_proved · IndisputableMonolith/Cost/AczelTheorem.lean:450 
/-- **THEOREM (Aczél, PROVED)**: `H_AczelClassification` holds unconditionally.
    This eliminates the sole remaining foundation axiom. -/
theorem h_aczel_classification_proved : H_AczelClassification :=
  fun H h_one h_cont h_dAlembert => dAlembert_contDiff_top H h_one h_cont h_dAlembert

-- The typeclass-parameterized `aczel_dAlembert_smooth` lives in
-- `IndisputableMonolith.Cost.AczelClass` and is satisfied by the
-- `AczelSmoothnessPackage` instance in `IndisputableMonolith.Cost.AczelProof`,
-- which delegates to `dAlembert_contDiff_top` above.

What this page does not claim

The double-angle identity alone does not classify d'Alembert solutions; continuity and the full equation are required. The d'Alembert equation is not derived from Recognition Science principles; it is a classical object the framework analyzes. The classification does not cover discontinuous solutions, which may 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/AczelTheorem.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