pith. sign in
theorem

cost_stability_transfer

proved
show as:
module
IndisputableMonolith.Foundation.DAlembert.Stability
domain
Foundation
line
287 · github
papers citing
none yet

plain-language theorem explainer

The cost stability transfer theorem shows that a quantitative stability bound for near-solutions H of the d'Alembert equation implies a corresponding bound on the deviation of the associated cost function from the J-cost. Researchers deriving error estimates for the reciprocal cost in Recognition Science would cite this when moving from the functional equation to explicit uniqueness bounds. The proof is a direct invocation of the CostStabilityTransferHypothesis after assuming the d'Alembert stability estimate.

Claim. Let $H:ℝ→ℝ$ be $C^3$, even, with $H(0)=1$ and curvature $a=H''(0)>0$, and let $ε, B, K$ be the uniform defect, function, and third-derivative bounds on $[-T,T]$. Suppose the d'Alembert stability estimate holds: for $0<h≤T$ and $|t|≤T-h$, $|H(t)-cosh(√a t)|≤(δ_error(ε,B,K,h)/a)(cosh(√a |t|)-1)$. Then for $0<h≤T$ and $e^{-(T-h)}<x<e^{T-h}$, $|H(log x)-1-J(x)|≤(δ_error(ε,B,K,h)/a)(cosh(√a |log x|)-1)$, where $J(x)=(x+x^{-1})/2-1$.

background

The module formalizes stability estimates for near-solutions of the d'Alembert equation $H(t+u)+H(t-u)=2H(t)H(u)$, with defect $Δ_H(t,u)=H(t+u)+H(t-u)-2H(t)H(u)$. StabilityHypotheses requires $H$ to be $C^3$ and even with $H(0)=1$ and positive curvature $a=H''(0)$. StabilityBounds collects the uniform defect bound $ε$, the sup-norm $B$ on $H$, and the bound $K$ on $|H'''|$. StabilityEstimate is the quantitative bound showing $H$ is close to $cosh(√a t)$ with error controlled by $δ_error(ε,B,K,h)/a$ times $(cosh(√a |t|)-1)$ for $|t|≤T-h$ (equation 7.3 in the paper).

proof idea

The proof is a one-line wrapper that applies the CostStabilityTransferHypothesis. It invokes the hypothesis with the assumed StabilityEstimate h_stab together with the step size $h$ and the conditions $0<h≤T$ to obtain the stated bound on $|H(log x)-1-Jcost x|$.

why it matters

This result transfers the d'Alembert stability theorem to the cost functional, feeding directly into the cost stability corollary cost_stability_calibrated (when curvature equals 1). It fills the Cost Stability Corollary (Corollary 7.1) in the paper on uniqueness of the canonical reciprocal cost. In the Recognition Science framework it supports quantitative uniqueness statements for the J-cost consistent with T5 J-uniqueness and the Recognition Composition Law.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.