carrier_budget
plain-language theorem explainer
The carrier budget theorem states that any budgeted carrier has annular excess of its trace mesh bounded by a constant times the square of its log-derivative bound and radius, uniformly in mesh size N. Researchers establishing mesh-independent bounds for zero-charge holomorphic carriers in the RS cost-covering bridge would cite it. The proof is a direct one-line extraction of the pre-supplied budget constant and excess bound from the carrier structure.
Claim. For any budgeted carrier $C$, there exists $K : ℝ$ such that for all $N : ℕ$, annularExcess of the mesh-$N$ trace of $C$ satisfies annularExcess$(C.trace.mesh N) ≤ K · (C.logDerivBound)^2 · (C.radius)^2$.
background
The annular J-cost framework defines phiCost u := cosh((log φ)·u) − 1 = J(φ^u). AnnularSample consists of phase increments on concentric rings; Jensen-based coercivity shows nonzero winding forces Θ(m² log N) cost. Carrier budget asserts holomorphic nonvanishing implies O(R²) annular cost. A BudgetedCarrier extends RegularCarrier with a zero-charge annular trace, nonnegative budgetConstant, and an explicit excess_bound holding for every mesh size N. The module establishes the φ-weighted cost function and annular sampling machinery for the RS topological cost-covering bridge. Upstream results supply radius from cellular automata and various carrier frequency definitions, but the argument uses only the structure fields.
proof idea
The proof is a one-line wrapper that returns the pair consisting of the budgetConstant and the excess_bound field of the supplied BudgetedCarrier.
why it matters
This supplies the uniform bound required by the downstream excess_bounded theorem, which states annular cost minus topological floor equals O(R²) for fields F(s) = (s−ρ)^{−m} G(s) with G regular. It realizes the carrier-budget interface in the annular J-cost framework, bridging holomorphic nonvanishing to mesh-independent excess. In Recognition Science it supports the cost-covering bridge between topological floors and annular excesses; the specific carrier C(s) = det₂(I−A(s))² has finite M_C(σ₀) for σ₀ > 1/2. It touches the open question of constructing explicit trace families for analytic carriers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.