carrier_trace_charge_zero
plain-language theorem explainer
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.
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.