qlf_regularFactorPhase
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.
claimGiven 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 in Recognition Science
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.
scope and limits
- Does not compute an explicit closed-form expression for the phase.
- Does not apply when $n=0$.
- Does not relax the regime condition $M·r≤1$.
- Does not extend beyond the disk of the supplied witness.
formal statement (Lean)
457noncomputable def qlf_regularFactorPhase
458 (qlf : QuantitativeLocalFactorization) (n : ℕ) (hn : 0 < n) :
459 RegularFactorPhase := by
proof body
Definition body.
460 have hnR : (1 : ℝ) ≤ (n : ℝ) := by exact_mod_cast hn
461 have hd : (0 : ℝ) < ↑n + 1 := by linarith
462 have hgt1 : (1 : ℝ) < ↑n + 1 := by linarith
463 exact regularFactorPhaseFromWitness qlf.toLocalMeromorphicWitness
464 (qlf.radius / (↑n + 1)) (div_pos qlf.radius_pos hd) (div_lt_self qlf.radius_pos hgt1)
465 qlf.logDerivBound qlf.logDerivBound_pos
466
467/-- A defect phase family using genuine regular-factor phase data.
468Each level carries non-trivial perturbation from the regular factor's
469Lipschitz-controlled phase, unlike the synthetic `zetaDerivedPhaseFamily`
470which has identically zero perturbation. -/