zeroWindingFromCert_charge
plain-language theorem explainer
zeroWindingFromCert_charge shows that the integer charge extracted from any zero-winding certificate is identically zero inside the certified radius. Researchers modeling holomorphic carriers in the Recognition Science contour analysis cite it to separate carrier and defect contributions before applying cost bounds. The proof is a one-line reflexivity that unfolds the definition of zeroWindingFromCert.
Claim. Let cert be a zero-winding certificate with radius R. For any real r satisfying 0 < r < R, the charge component of the winding data returned by zeroWindingFromCert(cert, r) equals zero.
background
The ContourWinding module defines WindingData as a record containing a center, radius, and integer winding charge. zeroWindingFromCert constructs such data from a ZeroWindingCert that certifies a function is holomorphic and nonvanishing inside the disk. The module's local setting is zero-holonomy: holomorphic nonvanishing functions have vanishing contour winding around every interior circle, proved via the Cauchy integral theorem applied to f'/f.
proof idea
The declaration is a term-mode proof consisting of a single reflexivity. It holds because zeroWindingFromCert is defined to return data whose charge field is exactly zero.
why it matters
The result is invoked by carrier_trace_charge_zero to establish that the sampled carrier trace carries zero charge. This zero-charge property bounds the annular excess cost and forces the defect index m to vanish in the factorization argument. It supplies the zero-holonomy step required for the additive winding decomposition that links to the Recognition Composition Law and the J-cost functional equation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.