CostStabilityTransferHypothesis
plain-language theorem explainer
Posits transfer of d'Alembert stability bounds from H to the cost J via the reparametrization F(x) = H(log x) - 1. Recognition Science analysts cite it when controlling errors in the phi-ladder mass formula. The declaration is realized as the direct implication from the StabilityEstimate assumption to the explicit δ_error-scaled cosh bound on the logarithmic interval around 1.
Claim. Let $H:ℝ→ℝ$ satisfy the stability hypotheses with curvature $a>0$ and bounds $ε,B,K$ on $[-T,T]$. If the stability estimate holds, then for $0<h≤T$ and $x$ with $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$ is the canonical cost function.
background
The module formalizes stability for near-solutions of the d'Alembert equation $H(t+u)+H(t-u)=2H(t)H(u)$. The defect is $Δ_H(t,u)=H(t+u)+H(t-u)-2H(t)H(u)$. StabilityHypotheses bundles the requirements that $H$ is $C^3$ and even, $H(0)=1$, and $H''(0)=a>0$. StabilityBounds supplies the uniform defect bound $ε$, the bound $B$ on $|H|$, and the bound $K$ on $|H'''|$ over $[-T,T]$.
proof idea
The declaration is a one-line wrapper that defines the transfer hypothesis as the implication from StabilityEstimate H T hyp.curvature bounds to the stated pointwise bound on |H(log x)-1-J(x)| with the factor (δ_error bounds.ε bounds.B bounds.K h / hyp.curvature) times (cosh(√(hyp.curvature) |log x|)-1) for x in the exponential interval.
why it matters
This hypothesis feeds the downstream theorems cost_stability_transfer and cost_stability_calibrated (the latter specializing to curvature 1 and yielding |F(x)-J(x)|≤δ J(x)). It supplies the transfer step from the d'Alembert stability theorem to the cost functional in the Recognition framework, linking to the J-uniqueness result and the phi-ladder mass formula. It touches the question of constant tightness when T reaches the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.