defectWindingData
plain-language theorem explainer
defectWindingData converts a DefectSensor (real part ρ and integer charge m) into WindingData by placing the center at ρ on the real axis, adopting the supplied positive radius r, and retaining charge m. Researchers applying the argument principle to holomorphic functions in the critical strip cite it to translate pole orders into contour winding objects. The definition is a direct structure constructor that performs only field assignment.
Claim. Let sensor be a DefectSensor with real part ρ and charge m. For r > 0 the associated WindingData object has center ρ, radius r, and charge m.
background
WindingData is the structure that packages a center in the complex plane, a positive radius, and an integer winding charge; it serves as the continuous counterpart to discrete annular sampling. DefectSensor records the multiplicity m of a zero (equivalently the order of the pole of the reciprocal) together with its real part inside the critical strip. The module ContourWinding establishes that holomorphic non-vanishing functions have zero winding around interior circles via the Cauchy integral theorem applied to f'/f.
proof idea
This is a direct structure constructor. It sets center to the complex number formed from the sensor's realPart and zero imaginary part, radius to the input r, radius_pos to the supplied positivity witness hr, and charge to the sensor's charge field.
why it matters
The definition supplies the WindingData object consumed by the downstream theorem defect_winding_eq_charge, which asserts equality between the constructed charge and the sensor charge. It realizes the link, stated in the module doc-comment, between the defect sensor and the argument principle inside the Recognition Science contour-winding development. The construction sits between the discrete defect functional and the continuous winding data used for zero-holonomy arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.