StabilityEstimate
plain-language theorem explainer
StabilityEstimate defines the target inequality asserting that an even C³ function H with H(0)=1 stays within an explicit multiple of (cosh(√a |t|)-1) of cosh(√a t) on compact intervals when its d'Alembert defect is controlled. Analysts deriving the Recognition cost functional or proving stability of functional equations cite this bound when passing from defect size to concrete approximation error. The definition assembles the error term directly from the three uniform constants packaged in StabilityBounds.
Claim. Let $H:ℝ→ℝ$, $T>0$, $a>0$, and let bounds be a StabilityBounds record supplying defect supremum $ε$, function supremum $B$, and third-derivative supremum $K$. Then StabilityEstimate asserts that 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)$, where $δ(h)=ε/h²+(1+B)Kh/3$.
background
The d'Alembert equation $H(t+u)+H(t-u)=2H(t)H(u)$ is the image of the Recognition Composition Law under the change of variables $H(x)=J(x)+1$, where $J$ is the cost function. StabilityBounds collects the three uniform controls needed for the estimate: the defect supremum $ε$, the range bound $B$, and the third-derivative bound $K$. The module develops quantitative stability for near-solutions of this equation on symmetric intervals, following the development in Washburn & Zlatanović.
proof idea
This is a definition that directly encodes the target inequality of Theorem 7.1. It constructs the error function δ_error from the three fields of the StabilityBounds structure and inserts it into the stated bound; no lemmas or tactics are invoked inside the definition itself.
why it matters
StabilityEstimate supplies the core quantitative statement invoked by dAlembert_stability to conclude the full theorem from the ODE approximation hypothesis. It is also used by cost_stability_calibrated and cost_stability_transfer to move the bound onto the cost functional via $F(x)=H(log x)-1$. In the Recognition framework this step converts the Recognition Composition Law into explicit control on the cost near the identity, supporting the phi-ladder and the derivation of spatial dimension three.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.