sampledBudgetedCarrier_scale_zero
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not apply to carriers built from nonzero-winding certificates.
- Does not supply bounds or estimates when the winding is positive.
- Requires the input radius and log-derivative bound to be positive.
- Does not address non-circular sampling geometries.
formal statement (Lean)
183theorem sampledBudgetedCarrier_scale_zero
184 (cert : ZeroWindingCert)
185 (logDerivBound : ℝ) (hM : 0 < logDerivBound)
186 (R : ℝ) (hR : 0 < R) :
187 carrierBudgetScale (sampledBudgetedCarrier cert logDerivBound hM R hR) = 0 := by
proof body
Term-mode proof.
188 simp [sampledBudgetedCarrier, carrierBudgetScale]
189
190end
191
192end SampledTrace
193end NumberTheory
194end IndisputableMonolith