WindingData
plain-language theorem explainer
WindingData packages a complex center, positive real radius, and integer charge to represent the winding number of a function around a circle. Number theorists working on contour integrals and zero-holonomy in Recognition Science cite it to bridge continuous phase data to discrete annular samples. The definition is a direct record constructor with four fields and no proof obligations.
Claim. A winding datum consists of a center $c$ in the complex plane, a radius $r > 0$, and an integer charge $m$ that records the net winding of a function around the circle of radius $r$ centered at $c$.
background
The ContourWinding module defines contour winding numbers for functions on disks and proves that holomorphic nonvanishing functions have zero winding around every interior circle. WindingData is the continuous-side object that packages center, radius, and integer charge; its discrete counterpart is the sampled AnnularRingSample. The module uses the Cauchy integral theorem from Mathlib applied to $f'/f$ for zero-free holomorphic $f$, so that the normalized contour integral equals the winding number and is therefore zero.
proof idea
This is a direct structure definition. It declares the four fields center : ℂ, radius : ℝ with radius_pos : 0 < radius, and charge : ℤ, with no computational content or lemmas applied.
why it matters
WindingData is the base type for all winding results in the module. It is instantiated by defectWindingData to set charge equal to the sensor charge, by zeroWindingFromCert to produce zero-charge data from a ZeroWindingCert, and by the additive and reciprocal theorems. These feed the key claim that the carrier's contour winding is zero, closing the link from continuous complex analysis to the discrete sampling layer used for masses and defects.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.