zeroWindingData
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not apply when the underlying function has nonzero winding.
- Does not verify holomorphicity or zero-freeness of the carrier.
- Does not handle negative radii or annular regions.
- Does not compute explicit contour integrals.
formal statement (Lean)
56def zeroWindingData (c : ℂ) (r : ℝ) (hr : 0 < r) : WindingData where
57 center := c
proof body
Definition body.
58 radius := r
59 radius_pos := hr
60 charge := 0
61
62/-! ### §2. Zero winding from carrier certificate -/
63
64/-- Given a `ZeroWindingCert`, produce zero `WindingData` at any interior radius.
65This is the bridge from the complex carrier certificate to the discrete sampling
66layer: the carrier has zero winding, so any sampling of it will produce zero
67net phase increment. -/