phaseIncrementEpsilonBound_nonneg
plain-language theorem explainer
The theorem proves nonnegativity of the phase increment epsilon bound for any quantitative local factorization when radius r is nonnegative and sample count n is positive. Analysts controlling phase perturbations on sampled circles in the Recognition Science annular cost framework would cite it to keep error terms valid for summability arguments. The proof is a direct term-mode reduction that unfolds the bound and applies real nonnegativity lemmas for division and multiplication.
Claim. Let $M > 0$ be the logarithmic derivative bound of a quantitative local factorization. For $r ≥ 0$ and $n > 0$, the phase increment epsilon bound satisfies $0 ≤ (M · 2π r) / (8n)$.
background
QuantitativeLocalFactorization extends a local meromorphic witness by a uniform bound $M$ on the logarithmic derivative $|g'/g|$ of the regular factor together with the regime condition $M · radius ≤ 1$. This supplies the analytic control on phase perturbations $ε_j$ that arise when sampling a meromorphic function on circles around a pole or zero. The module sets up the bridge from Mathlib meromorphic order to the RS annular cost framework: a function with order $n$ factors locally as $(z − ρ)^n · g(z)$, the pole part contributes exact phase charge $-n$, and the regular factor $g$ contributes a small perturbation $ε_j$ bounded by $M · 2π r / (8n)$ on each sampled arc.
proof idea
The term proof unfolds the definition of phaseIncrementEpsilonBound and applies div_nonneg. The numerator is shown nonnegative by mul_nonneg applied to the positive logDerivBound, the constant 2, π, and the given nonnegative radius r; the denominator is dispatched by positivity.
why it matters
The result supplies the nonnegativity step required for the perturbation lemmas that feed canonicalDefectSampledFamily_ringPerturbationControl. It guarantees that the ε terms remain controllable in the log φ scale, allowing the linear-plus-quadratic error to be summed uniformly across refinement depth N in the meromorphic circle order construction. The module documentation explicitly ties this bound to the phase-charge additivity and to the summability needed for DefectPhaseFamily and regular_perturbation lemmas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.