cost_stability_calibrated
plain-language theorem explainer
cost_stability_calibrated establishes that when curvature equals 1, the shifted function H(log x) - 1 deviates from the canonical Jcost by at most δ_error times Jcost itself, for x inside the symmetric exponential interval around 1. Researchers deriving error-controlled approximations to the Recognition cost functional from d'Alembert near-solutions would cite this corollary. The proof is a short tactic sequence that applies the transfer hypothesis, cancels the curvature factor via the a=1 assumption, and substitutes the cosh representation ofJ
Claim. Let $H:ℝ→ℝ$ be $C^3$, even, with $H(0)=1$ and curvature $a=H''(0)=1$. Let $T>0$ and $0<h≤T$. Suppose the defect, function, and derivative bounds hold and the d'Alembert stability estimate is satisfied. Then for all $x$ satisfying $e^{-(T-h)}<x<e^{T-h}$, $|H(ℝ.log x)-1-J(x)|≤δ_error(ε,B,K,h)·J(x)$, where $J(x)$ denotes the canonical cost function.
background
The module formalizes quantitative stability for near-solutions of the d'Alembert equation $H(t+u)+H(t-u)=2H(t)H(u)$. StabilityHypotheses bundles the regularity, evenness, normalization $H(0)=1$, and positive curvature $a=H''(0)$. StabilityBounds packages the uniform defect $ε$, the sup-norm $B$ on $H$, and the third-derivative bound $K$. StabilityEstimate then asserts that $H(t)$ stays within an explicit multiple of $(cosh(√a|t|)-1)$ of the exact cosh solution. CostStabilityTransferHypothesis re-expresses the same estimate on the multiplicative side via $F(x)=H(log x)-1$ and the canonical $J$. Upstream, CostAlgebra.H defines the shifted cost $H(x)=J(x)+1$, while the lemma Jcost_exp_cosh states $J(exp t)=cosh t-1$.
proof idea
The tactic proof introduces $x$ in the open interval, applies the cost_stability_transfer lemma (the concrete instance of the transfer hypothesis), then simplifies the resulting expression by substituting $a=1$ (which removes the division by $a$ and sets $√a=1$). It next invokes Jcost_exp_cosh on the positive argument $log x$ to replace the cosh term by Jcost, uses symmetry to align the two sides, and finishes with simpa.
why it matters
This corollary specializes the general d'Alembert stability transfer to the curvature-1 case that matches the J-uniqueness fixed point (T5) in the forcing chain. It directly supports the Cost Stability Corollary listed in the module header and supplies the error control needed when the Recognition cost functional is approximated by solutions of the d'Alembert equation. Because the used_by list is currently empty, the result sits ready for insertion into mass-ladder or alpha-band derivations that rely on calibrated Jcost bounds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.