carrier_trace_charge_zero
A zero-winding certificate forces the charge of the winding data sampled at any interior radius to equal zero. Researchers closing the cost-covering argument in Recognition Science cite this bridge when they bound annular excess and force the defect index m to vanish. The proof is a direct term application of the reflexivity lemma that sets the charge field of zeroWindingFromCert to zero.
claimLet $cert$ be a zero-winding certificate, $n$ a natural number, and $r$ a positive real number strictly less than the certificate radius. Then the charge of the winding data obtained from the zero-winding certificate at radius $r$ equals zero.
background
The ContourWinding module defines the contour winding number for functions on disks and proves that holomorphic nonvanishing functions have zero winding around every interior circle via the Cauchy integral theorem applied to $f'/f$. WindingData packages a center, radius, and integer winding charge. ZeroWindingCert is the structure that supplies a center, radius, and ComplexCarrierCert certifying zero winding on every interior circle. The upstream lemma zeroWindingFromCert constructs zero-charge WindingData from such a certificate at any interior radius, while zeroWindingFromCert_charge proves that this charge is identically zero by reflexivity.
proof idea
The proof is a one-line term wrapper that applies zeroWindingFromCert_charge directly to the supplied certificate and radius parameters. The natural-number parameter n is unused in the statement and plays no role in the reduction.
why it matters in Recognition Science
This declaration bridges the complex carrier certificate to the discrete sampling layer and supplies the zero-charge input required by the cost-covering argument. With carrier winding zero on every interior circle, the AnnularTrace has charge zero and bounded excess; the defect floor, which grows as $m^2 log N$ for $m ≠ 0$, then becomes unaffordable and forces $m = 0$. It completes the zero-holonomy step in the contour-winding development and connects directly to the AnnularCost and CostCoveringBridge modules.
scope and limits
- Does not establish winding numbers for functions possessing zeros inside the disk.
- Does not quantify approximation error between the continuous contour integral and discrete phase sampling.
- Does not apply when the radius lies outside the certificate bound.
- Does not treat non-circular contours or higher-dimensional domains.
formal statement (Lean)
132theorem carrier_trace_charge_zero (cert : ZeroWindingCert)
133 (n : ℕ) (r : ℝ) (hr : 0 < r) (hrR : r < cert.radius) :
134 (zeroWindingFromCert cert r hr hrR).charge = 0 :=
proof body
Term-mode proof.
135 zeroWindingFromCert_charge cert r hr hrR
136
137end
138
139end ContourWinding
140end NumberTheory
141end IndisputableMonolith