phaseIncrementEpsilonBound_decreasing
plain-language theorem explainer
The theorem shows that for a quantitative local factorization with log-derivative bound M, the phase perturbation epsilon bound on the circle of radius r₀/(n+1) with n+1 samples equals exactly M · 2π r₀ / (8 (n+1)²). Workers on meromorphic factorizations for annular cost models cite it to confirm O(1/n²) decay of per-ring errors. The argument unfolds the bound definition then reduces the resulting rational expression by field simplification and ring normalization.
Claim. Let $M > 0$ be the logarithmic derivative bound of the regular factor in a quantitative local factorization. For $r_0 > 0$ and $n$ a natural number, the phase increment epsilon bound at radius $r_0/(n+1)$ with $n+1$ sample points satisfies $M · (2π r_0) / (8 (n+1)^2)$.
background
QuantitativeLocalFactorization extends LocalMeromorphicWitness by adding a uniform bound M on |g'/g| of the regular analytic factor g over the disk, together with the regime condition M · radius ≤ 1. This bound directly controls the phase perturbation ε_j on sampled points of a circle: each |ε_j| ≤ M · (2π r / (8n)) where the arc length between adjacent 8-tick samples is 2π r / (8n). The module bridges Mathlib meromorphic-order machinery to the Recognition Science annular cost framework, showing that a meromorphic function with order n at ρ factors locally as (z−ρ)^n · g(z) with g(ρ) ≠ 0, so the phase charge of the pole part is −n while the regular part contributes zero charge.
proof idea
Unfolds the definition of phaseIncrementEpsilonBound. Establishes positivity of (n : ℝ) + 1. Applies field_simp to clear the denominator, ring_nf to normalize, simp on Nat.cast_add and Nat.cast_one, then finishes with ring.
why it matters
Supplies the explicit O(1/n²) decay of the per-sample epsilon bound, so that the total perturbation sum over the 8(n+1) samples on ring n is O(1/n). This is the analytic input required for the perturbation lemmas that feed canonicalDefectSampledFamily_ringPerturbationControl and the zeta-derived phase family. It closes the control of regular-factor errors in the meromorphic circle order setting, ensuring the phase charge extracted from meromorphic_phase_charge remains compatible with DefectSensor.charge after perturbation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.