carrierBudgetScale
plain-language theorem explainer
The carrier budget scale extracts the explicit scaling factor for annular excess from a budgeted carrier. Researchers on the RS cost-covering bridge to the Riemann hypothesis cite it when controlling the topological floor via uniform bounds. The definition is a direct field product of the budget constant, squared log-derivative bound, and squared radius.
Claim. Let $C$ be a budgeted carrier with budget constant $b$, logarithmic derivative bound $L$, and radius $R$. The carrier budget scale is $b L^2 R^2$.
background
The annular J-cost framework defines phiCost u as cosh((log phi) u) - 1, which equals J(phi^u), and equips carriers with annular traces to obtain Jensen-based coercivity bounds. A BudgetedCarrier extends RegularCarrier by a zero-charge AnnularTrace together with a nonnegative budgetConstant and an explicit excess_bound that caps annularExcess above the topological floor by budgetConstant times logDerivBound squared times radius squared. Upstream results supply the radius definition from cellular automata and scaling functions from large-scale structure, which populate the carrier fields.
proof idea
This is a one-line definition that unfolds the BudgetedCarrier structure and returns the product of its budgetConstant field, the square of its logDerivBound field, and the square of its radius field.
why it matters
It supplies the scalar bound required by DefectTopologicalFloorCovered and is invoked directly in rh_from_cost_covering, the main theorem that derives the Riemann hypothesis from the RS cost-covering axiom. The definition closes the interface between sampled trace constructions (which achieve scale zero) and the uniform control of the topological floor in the annular layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.