pureDefectPhaseData
plain-language theorem explainer
pureDefectPhaseData assembles a fixed-radius continuous phase package whose winding slope equals the negative of the supplied defect charge. Researchers constructing the unperturbed base case for zeta-derived phase families in the Recognition Science annular-cost setting cite this definition. The body is a direct record construction that copies the sensor's realPart and charge, sets radius to 1, and discharges continuity and winding by the continuity tactic together with simp and ring.
Claim. Given a defect sensor carrying real location $r$ and integer charge $c$, the function maps each natural number $n>0$ to the continuous phase data record with center $r$, radius $1$, phase function $θ ↦ -c θ$, and the same charge $c$.
background
The MeromorphicCircleOrder module connects Mathlib meromorphic-order factorization to the Recognition Science annular-cost framework. A meromorphic function of order $n$ at $ρ$ factors locally as $(z-ρ)^n g(z)$ with $g$ holomorphic and non-vanishing at $ρ$; the pole factor contributes phase charge $-n$ while the regular factor contributes charge $0$. DefectSensor (imported from CostCoveringBridge) packages a real location together with an integer charge that matches the multiplicity-derived charge of $ζ^{-1}$ at a zero of $ζ$. ContinuousPhaseData (imported from CirclePhaseLift) is the record type that stores center, radius, phase function, charge, and the winding proof required by the downstream perturbation witnesses.
proof idea
The definition is a direct lambda that, for each $n>0$, builds the ContinuousPhaseData record by setting center to sensor.realPart, radius to 1, phase to the linear map with slope equal to minus the sensor charge, and charge copied from the sensor. Radius positivity is discharged by norm_num; phase continuity by the continuity tactic; the winding identity by simp followed by ring.
why it matters
This definition supplies the pure-winding instance used by trivialDefectPhaseFamily and trivialDefectPhasePerturbationWitness, which in turn feed genuineZetaDerivedPhasePerturbationWitness. It realizes the exact phase-charge contribution of the $(z-ρ)^n$ factor when the regular holomorphic increment is set to zero, matching the charge $m$ required for $ζ^{-1}$ at a zero of multiplicity $m$. The construction therefore closes the base case of the perturbation decomposition needed for the phiCost bounds in the RingPerturbationControl development.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.