Hyperbolic Budget Tubes

Abstract

Local correlation bounds confine completion budgets and their extremal profiles.

Theorem 1.1 (The hyperbolic budget tube).

$$\forall Completion\in Type,L\in \mathrm{Real}\left(\right),a\in \mathrm{Real}\left(\right),budget\in Completion\to \mathrm{Real}\left(\right),correlation\in Completion\to \left(\mathrm{Real}\left(\right)\to \mathrm{Real}\left(\right)\right),globalCompletion\in Completion,localCompletion\in Completion,\left(0<L\wedge \left(0<a\wedge \left(\left(\forall completion\in Completion,t\in \mathrm{Real}\left(\right),\left|\mathrm{apply}\left(correlation,completion,t\right)\right|\le \mathrm{apply}\left(budget,completion\right)\right)\wedge \left(\forall t\in \mathrm{Real}\left(\right),\left|t\right|<\mathrm{mul}\left(2,L\right)\Rightarrow \mathrm{sub}\left(\mathrm{apply}\left(correlation,localCompletion,t\right),\mathrm{apply}\left(correlation,globalCompletion,t\right)\right)=\mathrm{mul}\left(\mathrm{sub}\left(\mathrm{apply}\left(budget,localCompletion\right),\mathrm{apply}\left(budget,globalCompletion\right)\right),\cosh \left(\mathrm{mul}\left(a,t\right)\right)\right)\right)\right)\right)\right)\Rightarrow \left(\mathrm{mul}\left(\mathrm{apply}\left(budget,globalCompletion\right),\mathrm{pow}\left(\tanh \left(\mathrm{mul}\left(a,L\right)\right),2\right)\right)\le \mathrm{apply}\left(budget,localCompletion\right)\wedge \mathrm{apply}\left(budget,localCompletion\right)\le \mathrm{mul}\left(\mathrm{apply}\left(budget,globalCompletion\right),\mathrm{pow}\left(\mathrm{div}\left(\cosh \left(\mathrm{mul}\left(a,L\right)\right),\sinh \left(\mathrm{mul}\left(a,L\right)\right)\right),2\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Weil/ZetaGamma/HyperbolicBudgetTube.hyperbolic_budget_tube (✓ std3). ∎

Source. Repository-derived.

Commentary.

The endpoint estimate is obtained from the local correlation law by closedness at the edge of the observation window. The two signs of the budget difference give the lower and upper walls separately.

Theorem 1.2 (Natural-budget profile and exponential width bounds).

$$\forall Completion\in \mathrm{Real}\left(\right)\to Type,lambdaOne\in \mathrm{Real}\left(\right),budget\in \mathrm{Pi}\left(\mathrm{typed}\left(L,\mathrm{Real}\left(\right)\right),\mathrm{apply}\left(Completion,L\right)\to \mathrm{Real}\left(\right)\right),correlation\in \mathrm{Pi}\left(\mathrm{typed}\left(L,\mathrm{Real}\left(\right)\right),\mathrm{apply}\left(Completion,L\right)\to \left(\mathrm{Real}\left(\right)\to \mathrm{Real}\left(\right)\right)\right),naturalCompletion\in \mathrm{Pi}\left(\mathrm{typed}\left(L,\mathrm{Real}\left(\right)\right),\mathrm{apply}\left(Completion,L\right)\right),\left(0<lambdaOne\wedge \left(\left(\forall L\in \mathrm{Real}\left(\right),\mathrm{apply}\left(budget,L,\mathrm{apply}\left(naturalCompletion,L\right)\right)=\mathrm{mul}\left(2,lambdaOne\right)\right)\wedge \left(\left(\forall L\in \mathrm{Real}\left(\right),completion\in \mathrm{apply}\left(Completion,L\right),t\in \mathrm{Real}\left(\right),\left|\mathrm{apply}\left(correlation,L,completion,t\right)\right|\le \mathrm{apply}\left(budget,L,completion\right)\right)\wedge \left(\forall L\in \mathrm{Real}\left(\right),completion\in \mathrm{apply}\left(Completion,L\right),t\in \mathrm{Real}\left(\right),\left|t\right|<\mathrm{mul}\left(2,L\right)\Rightarrow \mathrm{sub}\left(\mathrm{apply}\left(correlation,L,completion,t\right),\mathrm{apply}\left(correlation,L,\mathrm{apply}\left(naturalCompletion,L\right),t\right)\right)=\mathrm{mul}\left(\mathrm{sub}\left(\mathrm{apply}\left(budget,L,completion\right),\mathrm{apply}\left(budget,L,\mathrm{apply}\left(naturalCompletion,L\right)\right)\right),\cosh \left(\mathrm{div}\left(t,2\right)\right)\right)\right)\right)\right)\right)\Rightarrow \mathrm{let}lowerBudget=\mathrm{lambda}\left(\mathrm{typed}\left(L,\mathrm{Real}\left(\right)\right),\mathrm{sInf}\left(\mathrm{range}\left(\mathrm{apply}\left(budget,L\right)\right)\right)\right),\mathrm{let}upperBudget=\mathrm{lambda}\left(\mathrm{typed}\left(L,\mathrm{Real}\left(\right)\right),\mathrm{sSup}\left(\mathrm{range}\left(\mathrm{apply}\left(budget,L\right)\right)\right)\right),\mathrm{let}budgetWidth=\mathrm{lambda}\left(\mathrm{typed}\left(L,\mathrm{Real}\left(\right)\right),\mathrm{sub}\left(\mathrm{apply}\left(upperBudget,L\right),\mathrm{apply}\left(lowerBudget,L\right)\right)\right),\left(\forall L\in \mathrm{Real}\left(\right),0<L\Rightarrow \left(\forall completion\in \mathrm{apply}\left(Completion,L\right),\mathrm{mul}\left(\mathrm{mul}\left(2,lambdaOne\right),\mathrm{pow}\left(\tanh \left(\mathrm{div}\left(L,2\right)\right),2\right)\right)\le \mathrm{apply}\left(budget,L,completion\right)\wedge \mathrm{apply}\left(budget,L,completion\right)\le \mathrm{mul}\left(\mathrm{mul}\left(2,lambdaOne\right),\mathrm{pow}\left(\mathrm{div}\left(\cosh \left(\mathrm{div}\left(L,2\right)\right),\sinh \left(\mathrm{div}\left(L,2\right)\right)\right),2\right)\right)\right)\right)\wedge \left(\left(\forall L\in \mathrm{Real}\left(\right),0<L\Rightarrow \left(0\le \mathrm{sub}\left(\mathrm{mul}\left(2,lambdaOne\right),\mathrm{apply}\left(lowerBudget,L\right)\right)\wedge \mathrm{sub}\left(\mathrm{mul}\left(2,lambdaOne\right),\mathrm{apply}\left(lowerBudget,L\right)\right)\le \mathrm{div}\left(\mathrm{mul}\left(2,lambdaOne\right),\mathrm{pow}\left(\cosh \left(\mathrm{div}\left(L,2\right)\right),2\right)\right)\right)\right)\wedge \left(\left(\forall L\in \mathrm{Real}\left(\right),0<L\Rightarrow \left(0\le \mathrm{sub}\left(\mathrm{apply}\left(upperBudget,L\right),\mathrm{mul}\left(2,lambdaOne\right)\right)\wedge \mathrm{sub}\left(\mathrm{apply}\left(upperBudget,L\right),\mathrm{mul}\left(2,lambdaOne\right)\right)\le \mathrm{div}\left(\mathrm{mul}\left(2,lambdaOne\right),\mathrm{pow}\left(\sinh \left(\mathrm{div}\left(L,2\right)\right),2\right)\right)\right)\right)\wedge \left(\mathrm{IsBigO}\left(\mathrm{lambda}\left(\mathrm{typed}\left(L,\mathrm{Real}\left(\right)\right),\mathrm{sub}\left(\mathrm{mul}\left(2,lambdaOne\right),\mathrm{apply}\left(lowerBudget,L\right)\right)\right),atTop,\mathrm{lambda}\left(\mathrm{typed}\left(L,\mathrm{Real}\left(\right)\right),\exp \left(\mathrm{neg}\left(L\right)\right)\right)\right)\wedge \left(\mathrm{IsBigO}\left(\mathrm{lambda}\left(\mathrm{typed}\left(L,\mathrm{Real}\left(\right)\right),\mathrm{sub}\left(\mathrm{apply}\left(upperBudget,L\right),\mathrm{mul}\left(2,lambdaOne\right)\right)\right),atTop,\mathrm{lambda}\left(\mathrm{typed}\left(L,\mathrm{Real}\left(\right)\right),\exp \left(\mathrm{neg}\left(L\right)\right)\right)\right)\wedge \left(\mathrm{IsBigO}\left(budgetWidth,atTop,\mathrm{lambda}\left(\mathrm{typed}\left(L,\mathrm{Real}\left(\right)\right),\exp \left(\mathrm{neg}\left(L\right)\right)\right)\right)\wedge \left(\mathrm{IsBigO}\left(\mathrm{lambda}\left(\mathrm{typed}\left(L,\mathrm{Real}\left(\right)\right),\max \left(0,\mathrm{sub}\left(\mathrm{sub}\left(\mathrm{mul}\left(2,lambdaOne\right),\mathrm{apply}\left(lowerBudget,L\right)\right),\mathrm{mul}\left(8,lambdaOne,\exp \left(\mathrm{neg}\left(L\right)\right)\right)\right)\right)\right),atTop,\mathrm{lambda}\left(\mathrm{typed}\left(L,\mathrm{Real}\left(\right)\right),\exp \left(\mathrm{neg}\left(\mathrm{mul}\left(2,L\right)\right)\right)\right)\right)\wedge \left(\mathrm{IsBigO}\left(\mathrm{lambda}\left(\mathrm{typed}\left(L,\mathrm{Real}\left(\right)\right),\max \left(0,\mathrm{sub}\left(\mathrm{sub}\left(\mathrm{apply}\left(upperBudget,L\right),\mathrm{mul}\left(2,lambdaOne\right)\right),\mathrm{mul}\left(8,lambdaOne,\exp \left(\mathrm{neg}\left(L\right)\right)\right)\right)\right)\right),atTop,\mathrm{lambda}\left(\mathrm{typed}\left(L,\mathrm{Real}\left(\right)\right),\exp \left(\mathrm{neg}\left(\mathrm{mul}\left(2,L\right)\right)\right)\right)\right)\wedge \mathrm{IsBigO}\left(\mathrm{lambda}\left(\mathrm{typed}\left(L,\mathrm{Real}\left(\right)\right),\max \left(0,\mathrm{sub}\left(\mathrm{apply}\left(budgetWidth,L\right),\mathrm{mul}\left(16,lambdaOne,\exp \left(\mathrm{neg}\left(L\right)\right)\right)\right)\right)\right),atTop,\mathrm{lambda}\left(\mathrm{typed}\left(L,\mathrm{Real}\left(\right)\right),\exp \left(\mathrm{neg}\left(\mathrm{mul}\left(2,L\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Weil/ZetaGamma/HyperbolicBudgetTube.riemann_budget_tube (✓ std3). ∎

Source. Repository-derived.

Commentary.

The lower and upper profiles are the infimum and supremum of the actual completion-budget range at each scale. Their exact hyperbolic errors give the three leading exponential estimates and the three refined second-order positive-excess bounds.

References

• Truth anchor: D5/S3/Weil/ZetaGamma/HyperbolicBudgetTube.hyperbolic_budget_tube
• Truth anchor: D5/S3/Weil/ZetaGamma/HyperbolicBudgetTube.riemann_budget_tube