qlf_regularFactorPhase
plain-language theorem explainer
This definition constructs a RegularFactorPhase from a QuantitativeLocalFactorization at positive integer level n, supplying the Lipschitz-controlled phase of the regular factor on the nth circle. Workers on annular cost bounds or RingPerturbationControl cite it when replacing synthetic phase families with genuine meromorphic data. The construction is a one-line wrapper that invokes regularFactorPhaseFromWitness after casting the level bound and confirming the scaled radius remains positive and strictly smaller than the original.
Claim. Given a quantitative local factorization $qlf$ (a local meromorphic witness equipped with a uniform bound $M$ on $|g'/g|$ of the regular factor) and a positive integer $n$, the regular factor phase at level $n$ is the RegularFactorPhase obtained by feeding the witness, the scaled radius $r/(n+1)$, the positivity and strict inequality of that radius, and the logarithmic derivative bound $M$ into the witness constructor.
background
The module bridges Mathlib meromorphic-order machinery to the RS annular cost framework. A meromorphic function with order $n$ at a point admits the local factorization $f(z)=(z-ρ)^n g(z)$ with $g$ holomorphic and non-vanishing at $ρ$; the pole part contributes phase charge $-n$ while the regular factor $g$ contributes zero charge. QuantitativeLocalFactorization extends the basic LocalMeromorphicWitness by adding a uniform bound $M$ on the logarithmic derivative $|g'/g|$ together with the regime condition $M·r≤1$, which controls the size of phase perturbations $ε_j$ sampled on circles around $ρ$ (see the sibling doc-comment on arc-length separation). Upstream results supply the eight-tick phase definition, the defect functional $J$, and the active-edge count $A$ used in the surrounding φ-ladder arithmetic.
proof idea
The definition proceeds by three short linear-arithmetic facts establishing that the scaled radius $r/(n+1)$ is positive and strictly less than $r$, followed by a direct application of regularFactorPhaseFromWitness to the underlying LocalMeromorphicWitness, the scaled radius, the two radius inequalities, and the logarithmic derivative bound together with its positivity.
why it matters
It supplies the genuine Lipschitz-controlled phase data required by the perturbation lemmas that feed canonicalDefectSampledFamily_ringPerturbationControl, replacing the identically zero perturbation of the synthetic zetaDerivedPhaseFamily. The construction therefore closes the analytic input gap between meromorphic factorization (phase charge $-n$ from the pole part plus controlled $ε_j$ from $g$) and the RS annular cost framework, directly supporting the RingPerturbationControl step that bounds linear-plus-quadratic error uniformly in refinement depth.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.