Foundation Dalembert Stability Zero Defect Calibrated Implies Cosh

The zero-defect theorem

The d'Alembert functional equation, named for Jean le Rond d'Alembert's 1747 work on vibrating strings, asks for functions H that satisfy H(t+u) + H(t-u) = 2·H(t)·H(u). The classical smooth solutions are the hyperbolic cosine, H(t) = cosh(a·t), and the ordinary cosine, H(t) = cos(a·t), distinguished by the sign of the curvature a = H''(0). The equation encodes a deep symmetry: the value at the midpoint of an interval, in a certain sense, is the product of the values at the endpoints.

The Recognition Science library formalizes a stability version of this equation. The defect, the amount by which a function fails the identity, is defined as Δ_H(t,u) := H(t+u) + H(t-u) - 2·H(t)·H(u). A theorem in the machine-checked library of formal theorems proves that if H is C³, even, has H(0) = 1, and its defect is exactly zero on a symmetric interval, then H must equal cosh(√a·t) on that interval. The proof does not rely on solving a differential equation; it follows directly from the functional equation and the regularity assumptions.

The declaration zero_defect_calibrated_implies_cosh is a corollary that adds one calibration step. If the curvature a is set to 1, then the conclusion simplifies to H(t) = cosh(t) for all |t| ≤ T. This is the hyperbolic cosine with no scaling parameter left free. The theorem is a precise statement: it holds on the bounded interval [-T, T], not on the whole real line, and it requires the defect to vanish identically there, not merely to be small.

The theorem does not claim that any function with a small but nonzero defect is exactly cosh. The stability theory in the same module gives quantitative bounds for that case: if the defect is bounded by ε, then H is close to cosh with an explicit error bound involving ε, the interval length, and bounds on H and its derivatives. The zero-defect result is the sharp limit of that stability estimate, not a separate claim about approximate solutions.

Within the Recognition Science framework, this theorem matters because the cost function J(x) = (x + 1/x)/2 - 1, which the framework derives from five plain conditions, is related to cosh through a logarithmic change of variables. The zero-defect theorem provides a rigidity result: a function that exactly satisfies the d'Alembert symmetry on an interval, with unit curvature, is forced to be cosh, and therefore the associated cost is forced to be J. The theorem does not by itself derive J; it is one link in a chain that the framework's library checks.

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

/-- Zero defect + calibration a = 1 gives H = cosh exactly. -/
theorem zero_defect_calibrated_implies_cosh
    (H : ℝ → ℝ) (T : ℝ) (hyp : StabilityHypotheses H T)
    (h_a1 : hyp.curvature = 1)
    (h_zero : UniformDefectBound H T 0)
    (h_zero_hyp : ZeroDefectImpliesCoshHypothesis H T hyp) :
    ∀ t : ℝ, |t| ≤ T → H t = Real.cosh t := by
  intro t ht
  have h := zero_defect_implies_cosh H T hyp h_zero h_zero_hyp t ht
  simp only [h_a1, Real.sqrt_one, one_mul] at h
  exact h

/-- Zero defect + calibration a = 1 gives H = cosh exactly. -/
theorem zero_defect_calibrated_implies_cosh
    (H : ℝ → ℝ) (T : ℝ) (hyp : StabilityHypotheses H T)
    (h_a1 : hyp.curvature = 1)
    (h_zero : UniformDefectBound H T 0)
    (h_zero_hyp : ZeroDefectImpliesCoshHypothesis H T hyp) :
    ∀ t : ℝ, |t| ≤ T → H t = Real.cosh t := by
  intro t ht
  have h := zero_defect_implies_cosh H T hyp h_zero h_zero_hyp t ht
  simp only [h_a1, Real.sqrt_one, one_mul] at h
  exact h

/-- Zero defect + calibration a = 1 gives H = cosh exactly. -/
theorem zero_defect_calibrated_implies_cosh
    (H : ℝ → ℝ) (T : ℝ) (hyp : StabilityHypotheses H T)
    (h_a1 : hyp.curvature = 1)
    (h_zero : UniformDefectBound H T 0)
    (h_zero_hyp : ZeroDefectImpliesCoshHypothesis H T hyp) :
    ∀ t : ℝ, |t| ≤ T → H t = Real.cosh t := by
  intro t ht
  have h := zero_defect_implies_cosh H T hyp h_zero h_zero_hyp t ht
  simp only [h_a1, Real.sqrt_one, one_mul] at h
  exact h

/-- **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)

What this page does not claim

The theorem does not claim that any function with a small but nonzero defect is exactly cosh. The theorem does not claim that the d'Alembert equation has no cosine solutions; the zero-defect result with curvature = 1 selects cosh, not cos. The theorem does not by itself derive the cost function J from the five plain conditions; it is one link in a chain.

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: