phaseIncrementEpsilonBound
plain-language theorem explainer
The definition supplies an explicit upper bound on each phase perturbation ε_j from the regular factor g in a meromorphic factorization sampled on a circle of radius r. Workers on ring perturbation control and defect sampling in the Recognition Science annular cost framework cite it to control total error across refinement depth n. It is realized by a direct arithmetic expression that multiplies the supplied log-derivative bound M by the arc length 2πr/(8n).
Claim. Let $M$ be the uniform bound on $|g'/g|$ supplied by a quantitative local factorization of a meromorphic function on a disk. For a circle of radius $r$ centered at the singularity and refinement parameter $n$, the phase perturbation bound is $M · (2πr)/(8n)$.
background
QuantitativeLocalFactorization extends LocalMeromorphicWitness by adjoining a positive real logDerivBound $M$ together with the perturbation regime condition $M · radius ≤ 1$. This structure encodes the analytic control on the regular factor $g$ after the local factorization $f(z) = (z - ρ)^n g(z)$ guaranteed by meromorphicOrderAt_eq_int_iff. The module bridges Mathlib meromorphic-order machinery to the RS annular cost framework, where each sampled increment decomposes as Δ_j = pure_winding_increment + ε_j and the ε_j must be small in the log φ scale. Upstream, CirclePhaseLift.and supplies an explicit log-derivative bound M that becomes the angular Lipschitz constant on the circle via the chain rule.
proof idea
One-line definition that multiplies the logDerivBound field of the QuantitativeLocalFactorization by the arc length 2πr/(8n).
why it matters
The definition is invoked by phaseIncrementEpsilonBound_decreasing (which obtains the O(1/n²) decay needed for summability of perturbations across rings) and by phaseIncrementEpsilonBound_nonneg. It is also used in pureVectorCDoublingData_offline_example inside VectorCSymmetryOnlyNoGo. It supplies the concrete ε bound required for canonicalDefectSampledFamily_ringPerturbationControl and thereby closes the analytic input for phase-charge calculations in the meromorphic-order setting of the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.