zeroWindingData
plain-language theorem explainer
zeroWindingData constructs the zero-charge instance of WindingData for any complex center and positive radius. Researchers handling contour integrals or carrier certificates in Recognition Science cite it as the base case for zero-holonomy. The definition is a direct record constructor that hard-codes the charge field to zero.
Claim. For complex center $c$ and positive real radius $r>0$, the zero-winding datum is the record with center $c$, radius $r$, and integer charge $0$.
background
WindingData is the structure that packages a complex center, positive radius, and integer winding charge; it is the continuous-side counterpart to discrete annular sampling. The ContourWinding module shows that holomorphic nonvanishing functions have zero winding around every interior circle by applying the Cauchy integral theorem to $f'/f$. zeroWindingData supplies the charge-zero case of this structure.
proof idea
The definition is a direct record constructor that populates the four fields of WindingData, taking center and radius from the arguments, inheriting the positivity proof, and setting charge to zero.
why it matters
It supplies the zero base case consumed by zeroWindingFromCert, which bridges ZeroWindingCert to the discrete layer. The definition anchors the module's zero-holonomy result obtained from the Cauchy integral theorem and supports the subsequent additive and defect-charge identifications. It aligns with the framework's treatment of phase increments on the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.