sampledBudgetedCarrier_scale_zero
plain-language theorem explainer
Zero-winding certificates produce sampled budgeted carriers whose budget scale is exactly zero. Researchers bridging contour winding data to annular mesh costs cite this when establishing that zero-winding inputs add no excess term. The proof is a direct simplification that unfolds the carrier constructor and the scale formula.
Claim. Let $C$ be the budgeted carrier obtained by sampling a zero-winding certificate with positive log-derivative bound $M$ and positive radius $R$. Then the budget scale of $C$ equals zero.
background
The SampledTrace module bridges continuous contour-winding certificates to the discrete AnnularRingSample and AnnularMesh cost framework. It constructs sampled rings from 8n equispaced points on concentric circles and proves the corresponding bridge theorems to the abstract cost layer. ZeroWindingCert is the structure that certifies a function has zero winding around every interior circle; it packages a center, positive radius, and a matching carrier certificate. The sampledBudgetedCarrier definition builds a BudgetedCarrier by installing the supplied log-derivative bound and setting the budget constant to zero precisely when the input certificate is zero-winding. carrierBudgetScale multiplies that constant by the square of the log-derivative bound and the square of the radius.
proof idea
The proof applies the simp tactic to the definitions of sampledBudgetedCarrier and carrierBudgetScale. Unfolding shows that the zero-winding construction forces the budget constant to zero, so the entire scale expression collapses to zero.
why it matters
This result closes the zero-winding case inside the sampled-trace bridge, ensuring that zero-winding certificates contribute no excess budget before the full trace-to-annular-trace theorems are applied. It supports the charge-zero statements for sampled meshes that appear later in the same module. In the Recognition Science setting it supplies the zero-excess step required when moving from contour certificates to the discrete cost-covering estimates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.