defectWindingData
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.
claimLet 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 in Recognition Science
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.
scope and limits
- Does not evaluate any contour integral.
- Does not check holomorphicity of the underlying function.
- Does not produce discrete annular samples.
- Does not enforce the eight-tick periodicity or phi-ladder constraints.
formal statement (Lean)
114def defectWindingData (sensor : DefectSensor) (r : ℝ) (hr : 0 < r) :
115 WindingData where
116 center := ⟨sensor.realPart, 0⟩
proof body
Definition body.
117 radius := r
118 radius_pos := hr
119 charge := sensor.charge
120
121/-- The defect winding charge equals the sensor charge. -/