Finite-Window Exponential Agreement

Abstract

Hyperbolic budget tubes force uniform exponential agreement on every fixed window.

Theorem 1.1 (Every fixed window agrees at the hyperbolic exponential rate).

$$\begin{array}{r}\forall a,R_{\ast },T\in \mathbb{R},\\ 0<a\wedge 0\le R_{\ast }\wedge 0\le T\wedge \mathrm{BoundedLocalCoshLaw}(a,R_{\ast })\Rightarrow \\ (\forall L,0<L,T<2\cdot L\Rightarrow \forall t,\left|t\right|\le T\Rightarrow \left|\mathrm{DeltaH}(L,t)\right|\le \frac{R_{\ast }}{\sinh (a\cdot L{)}^2}\cdot \cosh (a\cdot T))\wedge \\ (\exists C\ge 0,\mathrm{eventually}(L,\forall t,\left|t\right|\le T\Rightarrow \left|\mathrm{DeltaH}(L,t)\right|\le C\cdot \exp (-2\cdot a\cdot L)))\wedge (a=\frac{1}{2}\Rightarrow \exists C\ge 0,\mathrm{eventually}(L,\forall t,\left|t\right|\le T\Rightarrow \left|\mathrm{DeltaH}(L,t)\right|\le C\cdot \exp (-L))).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Weil/FiniteWindowExponentialAgreement.finite_window_exponential_agreement (✓ std3). ∎

Source. Repository-derived.

Commentary.

The hypotheses are the same bounded-correlation and local cosh difference law used by the frozen hyperbolic budget tube. Positivity of the scale and resolvent excludes the totalized sinh denominator at zero.

The two tube walls bound both signs of the budget deviation by R-star divided by sinh(aL) squared. Monotonicity of cosh in absolute value then makes the bound independent of time on the fixed window.

For sufficiently large L, exp(aL)/4 is at most sinh(aL). This gives one time-independent constant multiplying exp(-2aL); when a is one half, the exponent simplifies exactly to -L.

References

• Truth anchor: D5/S3/Weil/FiniteWindowExponentialAgreement.finite_window_exponential_agreement
• Dependency: D5/S3/Weil/Budget/ExplicitHyperbolicDegreeThreshold
• Dependency: D5/S3/Weil/ZetaGamma/HyperbolicBudgetTube