BudgetedCarrier
plain-language theorem explainer
BudgetedCarrier augments a RegularCarrier with a zero-charge AnnularTrace and a nonnegative budgetConstant that bounds annularExcess uniformly over all mesh refinements N. Researchers formalizing the RS cost-covering bridge cite this interface to replace synthetic-mesh quantification with a concrete trace witness. The declaration is a structure extension that directly encodes the trace family and the excess inequality as additional fields.
Claim. A structure extending RegularCarrier (holomorphic nonvanishing disk carrier of radius $r>0$ with logarithmic derivative bounded by $M>0$) by an AnnularTrace of charge zero together with $B≥0$ such that annularExcess(trace.mesh $N$) ≤ $B·M^2·r^2$ for every $N∈ℕ$.
background
Module AnnularCost supplies the φ-weighted J-cost and annular sampling machinery for the RS topological cost-covering bridge. RegularCarrier is a holomorphic nonvanishing carrier on a disk with bounded logarithmic derivative. AnnularTrace is a refinement family of annular samples carrying a fixed integer charge. annularExcess(mesh) is defined as annularCost(mesh) minus the topological floor for that charge. The module states that holomorphic nonvanishing carriers yield O(R²) annular cost above the floor.
proof idea
Structure definition extending RegularCarrier; the five new fields directly record the zero-charge trace, its charge specification, the budget scalar, its nonnegativity, and the uniform excess bound.
why it matters
BudgetedCarrier supplies the carrier type required by CostCoveringPackage and is the explicit witness used by carrier_budget and excess_bounded. It realizes the mesh-independent budget claim needed for the annular layer of the Recognition Science cost-covering bridge, closing the interface between holomorphic carriers and the J-cost topological floor.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.