CostStabilityTransferHypothesis
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prove the StabilityEstimate itself.
- Does not fix the curvature value.
- Does not apply outside the interval (exp(-(T-h)), exp(T-h)).
- Does not quantify explicit T-dependence of the constants.
falsifier
A C³ even function H with H(0)=1, positive curvature, and small uniform defect on [-T,T] that violates the cosh-weighted bound on |H(log x)-1-J(x)| for some x in the allowed interval.
formal statement (Lean)
278def CostStabilityTransferHypothesis
279 (H : ℝ → ℝ) (T : ℝ) (hyp : StabilityHypotheses H T) (bounds : StabilityBounds H T) : Prop :=
proof body
Definition body.
280 StabilityEstimate H T hyp.curvature bounds →
281 ∀ (h : ℝ) (hh_pos : 0 < h) (hh_le : h ≤ T),
282 ∀ x : ℝ, Real.exp (-(T - h)) < x → x < Real.exp (T - h) →
283 |H (Real.log x) - 1 - Cost.Jcost x| ≤
284 (δ_error bounds.ε bounds.B bounds.K h / hyp.curvature) *
285 (Real.cosh (Real.sqrt hyp.curvature * |Real.log x|) - 1)
286