phaseIncrementEpsilonBound
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
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prove existence of the local meromorphic factorization.
- Does not bound the summed perturbation over all samples on one ring.
- Does not control behavior outside the local disk of the factorization.
- Does not incorporate quadratic or higher terms in the phase expansion.
Lean usage
theorem use_in_decreasing (qlf : QuantitativeLocalFactorization) {r0 : ℝ} (hr0 : 0 < r0) (n : ℕ) : phaseIncrementEpsilonBound qlf (r0 / (n + 1)) (n + 1) = qlf.logDerivBound * (2 * Real.pi * r0) / (8 * (n + 1)^2) := by unfold phaseIncrementEpsilonBoundformal statement (Lean)
278noncomputable def phaseIncrementEpsilonBound
279 (qlf : QuantitativeLocalFactorization) (r : ℝ) (n : ℕ) : ℝ :=
proof body
Definition body.
280 qlf.logDerivBound * (2 * Real.pi * r) / (8 * n)
281
282/-- The ε bound is nonneg when r and n are positive. -/