winding_reciprocal
plain-language theorem explainer
For winding data w with center c, radius r and integer charge m, there exists w' with the same center and radius but charge -m. Researchers analyzing contour integrals or defect charges in Recognition Science cite this when handling reciprocal functions or poles. The proof is a direct term-mode record update that negates the charge field and confirms the other components by reflexivity.
Claim. Let $w$ be winding data with center $c$, radius $r>0$ and integer charge $m$. Then there exists winding data $w'$ such that the charge of $w'$ equals $-m$, the center of $w'$ equals $c$, and the radius of $w'$ equals $r$.
background
WindingData is the structure that packages an integer winding charge of a function around a circle of given center and radius; it is the continuous counterpart to discrete annular sampling. The module defines contour winding numbers on disks and proves that holomorphic nonvanishing functions have zero winding around every interior circle by applying the Cauchy integral theorem to $f'/f$. The present theorem records the sign change under reciprocals, which matches the argument principle: a zero of multiplicity $m$ produces a pole of order $m$ whose winding is $-m$.
proof idea
The proof is a one-line term-mode construction. It forms a new WindingData record by replacing the charge field with its negation and applies reflexivity to verify that center and radius are unchanged.
why it matters
The result supports the module's identification of defect winding with sensor charge and the zero-holonomy properties of carriers. It supplies the sign-flip step needed for the argument principle in the contour setting, which in turn feeds the connection between continuous integrals and discrete phase sampling. In the Recognition Science framework it contributes to the treatment of defects and the zero-winding certificates that appear in the phi-ladder analysis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.