Foundation Dalembert Stability Cost Stability Transfer

The stability transfer

The d'Alembert functional equation, H(t+u) + H(t-u) = 2·H(t)·H(u), is a classical object in mathematics, studied since the 18th century. Its smooth solutions are the hyperbolic cosine and cosine families, depending on the sign of the curvature at zero. The framework's library contains a machine-checked theorem, cost_stability_transfer, which concerns functions that only nearly solve this equation, not exactly. It states that if such a function H is smooth, even, and has a small defect (the amount by which the equation fails), then H, after a logarithmic change of variables, is close to the framework's canonical cost function J(x) = (x + 1/x)/2 - 1. The closeness is measured by an explicit error bound that depends on the size of the defect and the width of the interval.

The theorem is a stability result, a type of guarantee common in analysis: it says that a small perturbation of the equation's input leads to a small perturbation of the output. It does not say that any near-solution is exactly J, only that it is near J. The error bound involves a quantity called δ_error, which grows with the defect ε and shrinks as the interval length T grows. The theorem also requires a technical condition, the cost stability transfer hypothesis, which is a separate assumption in the library's formalization, not a consequence of the other hypotheses.

The practical meaning is a robustness claim for the framework's central object. The cost function J is not a fragile artifact that only exists under perfect, idealized conditions. The theorem shows that if the underlying recognition process is only approximately governed by the d'Alembert equation, the resulting cost function is still approximately J, with a quantifiable error. This is the kind of guarantee that makes a mathematical structure usable as a foundation: small deviations from the ideal do not produce wildly different conclusions.

In the framework's own account, this transfer is a step toward showing that the cost function is not just a convenient definition but a stable consequence of the forcing chain. The theorem is proved in the machine-checked library, meaning its logical validity is verified by a computer. It does not, however, assert anything about the physical world. It is a statement about functions on the real line, not about actual recognition events or measurements. The connection between this formal theorem and any physical process remains a separate, open question in the framework.

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

/-- Transfer stability from H to F via F(x) = H(log x) - 1. -/
def CostStabilityTransferHypothesis
    (H : ℝ → ℝ) (T : ℝ) (hyp : StabilityHypotheses H T) (bounds : StabilityBounds H T) : Prop :=
  StabilityEstimate H T hyp.curvature 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)

What this page does not claim

The theorem does not claim that any near-solution is exactly the cost function J. The theorem does not claim anything about physical recognition events or measurements. The theorem does not prove that the cost stability transfer hypothesis is satisfied by any particular function.

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: