zeroWindingFromCert
plain-language theorem explainer
zeroWindingFromCert builds winding data with charge zero from a zero-winding certificate at any interior radius. It supplies the interface between the holomorphic carrier certificate and the discrete sampling layer. The definition is a direct record construction that inherits the center and radius while fixing the charge at zero.
Claim. Let cert be a zero-winding certificate and let r be a real number satisfying 0 < r < radius of cert. The winding data is the record with center taken from cert, radius equal to r, a proof that r is positive, and charge equal to zero.
background
WindingData packages a complex center, positive real radius, and integer charge for a contour. The module establishes that holomorphic nonvanishing functions have zero winding around every interior circle by applying the Cauchy integral theorem to f'/f, so that the normalized contour integral equals zero. The upstream ZeroWindingCert from EulerCarrierComplex certifies that the carrier itself has this zero-winding property. The module doc notes that the carrier contour winding is zero and that winding is additive under products, with the link to discrete sampling handled in SampledTrace.lean.
proof idea
The definition is a direct record construction. It copies the center from the certificate, substitutes the supplied radius, attaches the given positivity proof, and sets the charge field to zero. No auxiliary lemmas are invoked.
why it matters
This definition supplies the zero-charge data consumed by carrier_trace_charge_zero, which shows the carrier trace has charge zero and thereby bounds the defect floor, forcing mode number m to zero in the cost-covering argument. It completes the bridge step in the zero-holonomy section, connecting the holomorphic certificate to the annular cost layer. The parent theorem carrier_trace_charge_zero applies it directly to obtain the zero-charge conclusion.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.