phaseIncrementEpsilonBound
plain-language theorem explainer
This definition supplies the explicit upper bound on each phase perturbation ε_j from the regular factor g in a local meromorphic factorization, given by M times the arc length between adjacent samples spaced at 2π/(8n) on a circle of radius r. Researchers controlling sampled phase increments around zeros in the Recognition Science annular cost framework would cite it when establishing summability of errors under radial refinement. The definition is a direct algebraic formula obtained by scaling the supplied log-derivative bound M by the factor
Claim. Let $M > 0$ be the uniform bound on $|g'/g|$ for the regular factor $g$ in a quantitative local factorization of a meromorphic function. On a circle of radius $r > 0$ with refinement parameter $n$, the phase increment epsilon bound is $M · 2πr / (8n)$.
background
In the Meromorphic Circle Order module, a meromorphic function admits a local factorization $f(z) = (z - ρ)^n g(z)$ with $g$ holomorphic and nonvanishing at ρ. The pole or zero part contributes a fixed phase charge, while the regular factor $g$ produces small phase perturbations ε_j when the function is sampled on circles around ρ. QuantitativeLocalFactorization extends the basic local witness by adding a positive real $M$ that bounds $|g'/g|$ uniformly on the disk together with the regime condition $M · radius ≤ 1$ that keeps perturbations controlled.
proof idea
The definition is a one-line algebraic expression that multiplies the log-derivative bound by the arc length $2πr$ and divides by the sample count $8n$. No auxiliary lemmas are invoked; the formula follows at once from the chain-rule interpretation of $M$ as an angular Lipschitz constant and the fixed angular spacing $2π/(8n)$.
why it matters
This bound supplies the analytic control needed for ring perturbation lemmas that feed canonicalDefectSampledFamily_ringPerturbationControl. It is invoked to prove the decreasing property under radial refinement (phaseIncrementEpsilonBound_decreasing) and nonnegativity (phaseIncrementEpsilonBound_nonneg), which together guarantee that summed perturbations remain $O(1/n)$ across refinement levels. The construction aligns sampled phase charges of ζ^{-1} with defect-sensor requirements in the eight-tick structure and is used in the offline example of pure vector C doubling data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.