CostStabilityEstimate
CostStabilityEstimate defines the predicate asserting that a perturbed cost functional F stays within a scaled cosh error of the canonical J-cost on the logarithmic interval (e^{-T}, e^T). Researchers deriving mass spectra or applying functional-equation stability in Recognition Science would cite this corollary when moving from d'Alembert bounds on H to explicit control on F. The definition is a direct transcription of the error estimate supplied by the upstream stability theorem after the substitution F(x) = H(log x) - 1.
claimLet $F : (0,∞) → ℝ$ be given by $F(x) = H(ℝlog x) - 1$ where $H$ satisfies the d'Alembert stability hypotheses with second derivative $a$ at zero and defect bounded by $δ$. The predicate holds if and only if, for every $x$ with $e^{-T} < x < e^{T}$, $|F(x) - J(x)| ≤ (δ/a) (cosh(√a |log x|) - 1)$, where $J(x) = cosh(log x) - 1$.
background
The module formalizes stability for near-solutions of the d'Alembert equation $H(t+u) + H(t-u) = 2 H(t) H(u)$. The defect is defined as $Δ_H(t,u) := H(t+u) + H(t-u) - 2 H(t) H(u)$. Upstream CostAlgebra.H supplies the shifted cost $H(x) = J(x) + 1$ with $J$ obeying the Recognition Composition Law; the module doc states that if $H$ is $C^3$, even, $H(0)=1$, the defect is bounded by $ε$ on $[-T,T]^2$ and $H''(0)=a>0$, then $H$ lies close to $cosh(√a t)$ with explicit bounds. CostStabilityEstimate transfers this closeness to the cost functional on the positive reals.
proof idea
The definition is a direct transcription of the stability bound after the change of variables $x = e^t$. It substitutes the upstream identification $H = J + 1$ and replaces the cosh approximation for the canonical $J$ inside the given interval determined by $T$.
why it matters in Recognition Science
This corollary completes the transfer from the d'Alembert stability theorem (Theorem 7.1) to the cost functional, supplying the explicit error control needed for mass-ladder constructions and phi-weighted derivations in Recognition Science. It sits downstream of J-uniqueness (T5) and the forcing chain by furnishing quantitative closeness to the canonical $J$ when the defect is small. The supplied material flags no open questions.
scope and limits
- Does not prove existence of an H satisfying the stability hypotheses.
- Does not quantify the size of δ required for a given a.
- Does not extend the bound outside the interval (e^{-T}, e^T).
- Does not address global behavior or higher derivatives of F.
formal statement (Lean)
273def CostStabilityEstimate (F : ℝ → ℝ) (T a : ℝ) (δ : ℝ) : Prop :=
proof body
Definition body.
274 ∀ x : ℝ, Real.exp (-(T)) < x → x < Real.exp T →
275 |F x - Cost.Jcost x| ≤ (δ / a) * (Real.cosh (Real.sqrt a * |Real.log x|) - 1)
276
277/-- Transfer stability from H to F via F(x) = H(log x) - 1. -/