Foundation Dalembert Stability

Stability near the cost function

The d'Alembert functional equation, H(t+u) + H(t-u) = 2·H(t)·H(u), is a classical condition. It appears in probability and harmonic analysis. In 1747, Jean le Rond d'Alembert derived it while studying the vibrating string, and its solutions include the hyperbolic cosine, cosh(a·t). The equation says that the value at a sum and difference of two points relates to the product of the values at those points.

In the framework of Recognition Science, this equation is not an arbitrary starting point. The framework's central object is the cost, a function that measures the price of a recognition event, and the framework proves that any cost function satisfying five plain conditions must equal J(x) = (x + 1/x)/2 - 1. The d'Alembert equation enters because the cost function, after a logarithmic change of variables, satisfies a related identity. The module under discussion, d'Alembert stability, asks a sharper question: what happens if a function H only nearly satisfies the d'Alembert equation?

The answer is a stability theorem. The module defines a defect, Δ_H(t,u) = H(t+u) + H(t-u) - 2·H(t)·H(u), which measures exactly how far H is from solving the equation. Under mild conditions, namely H is C³ and even with H(0) = 1, and if the defect is bounded by a small number ε on a finite interval, then H must be close to cosh(√a·t), where a = H''(0) is positive. The closeness is quantitative: the error is bounded by an explicit expression involving ε, the interval size, and the curvature a.

This is not a vague approximation statement. The module proves a chain of results. A small defect implies that H approximately satisfies the ordinary differential equation H''(t) = a·H(t), which is the defining equation of the hyperbolic cosine. From that, a stability estimate follows, and then a transfer step converts the bound back to the cost function J(x). The final corollary, cost_stability_calibrated, states that if H is close to cosh in the d'Alembert sense, then after the logarithmic change of variables, H(log x) - 1 is close to the cost function J(x). The error term is proportional to J(x) itself, multiplied by a small factor that depends on ε.

The practical meaning is that the cost function J is stable. If a process almost satisfies the defining functional equation, its cost structure is almost forced to be the canonical one. The framework's library, a machine-checked collection of formal theorems, verifies each step. The theorems are not merely asserted; they are proved from the definitions. The result does not require the equation to hold exactly, only within a small error, and the conclusion degrades gracefully with that error.

This stability result matters because it separates the framework's core claim from a fragile idealization. Real systems are never exact. The theorem says that near-solutions of the d'Alembert equation are near the unique cost function, so the framework's predictions hold for approximate systems, not just perfect ones. The error bounds are explicit, so a user can compute how close a given approximate system must be to the ideal cost shape.

/-- **Theorem 7.1 (Complete Statement)** -/
theorem dAlembert_stability
    (H : ℝ → ℝ) (T : ℝ) (hyp : StabilityHypotheses H T) (bounds : StabilityBounds H T)
    (h_ode : ODEApproximationHypothesis H T hyp bounds)
    (h_stab : StabilityFromODEHypothesis H T hyp bounds) :
    StabilityEstimate H T hyp.curvature bounds := by
  have h_ode' := ode_approximation_from_defect H T hyp bounds h_ode
  exact stability_from_ode_approx H T hyp bounds h_ode' h_stab

theorem cost_stability_transfer
    (H : ℝ → ℝ) (T : ℝ) (hyp : StabilityHypotheses H T) (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 / hyp.curvature) *
      (Real.cosh (Real.sqrt hyp.curvature * |Real.log x|) - 1) := by
  exact h_transfer h_stab h hh_pos hh_le

/-- When a = 1 (standard RS calibration), the stability estimate simplifies. -/
theorem 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 : ℝ) (hh_pos : 0 < h) (hh_le : h ≤ T) :
    ∀ t : ℝ, |t| ≤ T - h →
    |H t - Real.cosh t| ≤ δ_error bounds.ε bounds.B bounds.K h * (Real.cosh |t| - 1) := by
  intro t ht
  have h_main := h_stab h hh_pos hh_le t ht
  simp only [h_a1, Real.sqrt_one, one_mul, div_one] at h_main
  exact h_main

What this page does not claim

The module does not prove that the d'Alembert equation itself is the unique source of the cost function. The stability bounds are not shown to be optimal; they are explicit but not claimed to be tight. The module does not address the stability of solutions to the full set of five cost conditions, only the d'Alembert equation.

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: