sampledBudgetedCarrier
plain-language theorem explainer
sampledBudgetedCarrier builds a BudgetedCarrier from a zero-winding certificate together with a positive log-derivative bound and radius. Researchers instantiating the Euler function cite it to obtain a carrier whose trace and charge derive from contour data rather than a synthetic zero-charge assumption. The definition populates the structure fields directly from sampledTraceToAnnularTrace and its zero-excess lemma, fixing the budget constant at zero.
Claim. Given a zero-winding certificate cert, a positive real M serving as logarithmic derivative bound, and positive radius R, the sampled budgeted carrier is the budgeted carrier structure with logarithmic derivative bound equal to M, radius equal to R, trace equal to the annular trace sampled from cert, charge zero, and budget constant zero.
background
The SampledTrace module bridges continuous contour-winding certificates to the discrete annular ring sample and mesh cost framework. A zero-winding certificate asserts vanishing winding number on the contour; sampledTraceToAnnularTrace converts it into an annular trace for cost calculations, while the companion lemma sampledTraceToAnnularTrace_charge_zero forces the charge to zero. The local setting uses rings with 8n equispaced angular samples at radii r_n = R n / (N+1), matching the annular mesh convention.
proof idea
The definition constructs the budgeted carrier structure by direct assignment of the input bound and radius, sets the trace via sampledTraceToAnnularTrace, the charge via its zero lemma, the budget constant to zero by reflexivity of le_refl, and the excess bound by rewriting with sampledTraceToAnnularTrace_excess_zero followed by norm_num.
why it matters
This definition supplies the concrete carrier used inside eulerSampledBudgetedCarrier, which packages the Euler function as a budgeted carrier for cost covering. It replaces the synthetic eulerBudgetedCarrier by deriving the zero-charge property from the actual zero-winding certificate supplied by EulerCarrierComplex. The construction thereby closes the bridge from contour winding to annular cost models in the sampled trace layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.