defectPhasePureIncrement
plain-language theorem explainer
The definition supplies the exact pure winding phase increment for each sampled ring in a defect phase family of fixed charge m. Researchers separating topological winding from regular-factor perturbations in the annular-cost attack on the Riemann hypothesis would cite it. It is realized by the direct formula that scales the total phase charge by the 8-tick period and the ring index.
Claim. For a defect phase family with fixed sensor charge $m$, the pure winding increment on the $n$th sampled ring is $-(2 m) / (8 n)$ (in units where the full circle is $2π$).
background
In the Meromorphic Circle Order module a DefectPhaseFamily is a structure carrying a DefectSensor (with integer charge $m$), a positive witness radius, and a family of ContinuousPhaseData objects whose charge is required to equal $m$ at every level. The construction extracts the genuine local meromorphic factorization of a function such as $ζ^{-1}$ near a zero of multiplicity $m$, so that the pole factor $(z-ρ)^{-m}$ supplies the full phase charge while the regular holomorphic factor contributes zero charge. Upstream, the eight-tick phase structure supplies the discrete sampling on $8n$ points per ring and the defect functional identifies cost with the J-functional.
proof idea
The definition is a direct one-line formula that extracts the sensor charge, multiplies by $2π$, divides by the 8-tick octave length $8n$, and attaches the conventional negative sign for winding direction.
why it matters
This definition supplies the exact topological floor for the phase increments inside the DefectPhasePerturbationWitness structure. It is invoked by phaseFamily_ringPerturbationControl and canonicalDefectSampledFamily_ringPerturbationControl to isolate the regular perturbation $ε_j$ whose phiCost bounds are then controlled. In the Recognition framework it realizes the eight-tick octave contribution to the phase charge that matches the defect charge in the meromorphic factorization of $ζ^{-1}$, closing the separation between pure winding and regular factor needed for the RingPerturbationControl witness.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.