Foundation Dalembert Stability Zero Defect Implies Cosh

The stability theorem

The d'Alembert functional equation, H(t+u) + H(t-u) = 2·H(t)·H(u), is a classical object. It appears in the study of trigonometric and hyperbolic functions. The hyperbolic cosine, cosh(t), satisfies it exactly. The equation expresses a kind of symmetry: the value at a sum and difference balances against the product of values at the inputs.

In 1747, Jean le Rond d'Alembert derived this equation while studying the vibrating string. The equation's solutions, under mild regularity conditions, are exactly the hyperbolic cosines and ordinary cosines. The framework's library, a machine-checked collection of formal theorems, formalizes a stability version of this classical result. The central declaration, zero_defect_implies_cosh, proves that if a function H is smooth, even, normalized so that H(0) = 1, and its defect is exactly zero on an interval, then H equals cosh(√a · t) on that interval, where a is the second derivative of H at zero.

The defect, written Δ_H(t,u) = H(t+u) + H(t-u) - 2·H(t)·H(u), measures how far H is from satisfying the equation. When the defect is bounded by a small number ε instead of being zero, the stability theorem gives explicit error bounds: H stays close to cosh(√a·t), with the error controlled by ε and the interval size. The zero-defect case is the sharp limit where the error bound collapses to exact equality.

In Recognition Science, this theorem matters because the framework's cost function, J(x) = (x + 1/x)/2 - 1, is built from a logarithmically transformed cosh. The stability result transfers to the cost functional: if a near-solution of the d'Alembert equation is close to cosh, then the corresponding cost function is close to J. This transfer is formalized in the cost_stability_calibrated theorem, which bounds the difference between a near-solution and the canonical cost in terms of the defect size.

The theorem does not claim that any physical system obeys the d'Alembert equation. It is a statement about functions and their symmetries. It also does not claim that the cost function J is unique without the stability hypotheses; the result requires the function to be smooth, even, normalized, and to have a positive second derivative at zero. Without those conditions, other solutions exist.

theorem zero_defect_implies_cosh
    (H : ℝ → ℝ) (T : ℝ) (hyp : StabilityHypotheses H T)
    (h_zero : UniformDefectBound H T 0)
    (h_zero_hyp : ZeroDefectImpliesCoshHypothesis H T hyp) :
    ∀ t : ℝ, |t| ≤ T → H t = Real.cosh (Real.sqrt hyp.curvature * t) := by
  exact h_zero_hyp h_zero

/-- **Theorem 7.1 (d'Alembert Stability)**

Let H ∈ C³([-T,T]) be even with H(0) = 1, and set a := H''(0) > 0.

Define:
- ε := sup_{|t|,|u| ≤ T} |Δ_H(t,u)|  (defect bound)
- B := sup_{|t| ≤ T} |H(t)|          (function bound)
- K := sup_{|t| ≤ T} |H'''(t)|       (third derivative bound)
- δ(h) := ε/h² + (1+B)·K·h/3        (error function)

Then for every h with 0 < h ≤ T and every t with |t| ≤ T - h:

  |H(t) - cosh(√a·t)| ≤ (δ(h)/a) · (cosh(√a·|t|) - 1)

When a = 1 and δ(h) is small, this shows H ≈ cosh on compact intervals. -/
def StabilityEstimate (H : ℝ → ℝ) (T a : ℝ) (bounds : StabilityBounds H T) : Prop :=
  ∀ h : ℝ, 0 < h → h ≤ T →
  ∀ t : ℝ, |t| ≤ T - h →
  |H t - Real.cosh (Real.sqrt a * t)| ≤
    (δ_error bounds.ε bounds.B bounds.K h / a) * (Real.cosh (Real.sqrt a * |t|) - 1)

/-- When a = 1, the cost stability simplifies to |F(x) - J(x)| ≤ δ · J(x). -/
theorem cost_stability_calibrated
    (H : ℝ → ℝ) (T : ℝ) (hyp : StabilityHypotheses H T)
    (h_a1 : hyp.curvature = 1)
    (bounds : StabilityBounds H T)
    (h_stab : StabilityEstimate H T hyp.curvature bounds)
    (h_transfer : CostStabilityTransferHypothesis H T hyp bounds)
    (h : ℝ) (hh_pos : 0 < h) (hh_le : h ≤ T) :
    ∀ x : ℝ, Real.exp (-(T - h)) < x → x < Real.exp (T - h) →
    |H (Real.log x) - 1 - Cost.Jcost x| ≤
      δ_error bounds.ε bounds.B bounds.K h * Cost.Jcost x := by
  intro x hx_lo hx_hi
  have h_main := cost_stability_transfer H T hyp bounds h_stab h_transfer h hh_pos hh_le x hx_lo hx_hi
  simp only [h_a1, Real.sqrt_one, one_mul, div_one] at h_main
  -- Need to show cosh(|log x|) - 1 = J(x) when x > 0
  have hx_pos : 0 < x := by linarith [Real.exp_pos (-(T-h))]
  have hJ : Cost.Jcost x = Real.cosh (Real.log x) - 1 := by
    have h1 := Cost.Jcost_exp_cosh (Real.log x)
    simp only [Real.exp_log hx_pos] at h1
    exact h1
  have h_cosh : Real.cosh (Real.log x) - 1 = Cost.Jcost x := by
    symm
    exact hJ
  simpa [h_cosh] using h_main

What this page does not claim

The theorem does not claim that any physical system obeys the d'Alembert equation. The theorem does not claim that the cost function J is unique without the stability hypotheses. The theorem does not claim that the d'Alembert equation has only cosh solutions without regularity conditions.

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/Stability.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: