genuineRegularFactorPhaseAt
plain-language theorem explainer
QuantitativeLocalFactorization supplies a uniform bound M on the logarithmic derivative of the regular factor g in a local meromorphic factorization together with the regime M R ≤ 1. genuineRegularFactorPhaseAt extracts the corresponding RegularFactorPhase at each positive integer level n by scaling the disk radius to R/(n+1) while retaining the same M. Researchers bounding phase perturbations on sampled circles around zeta zeros cite this object to obtain the level-dependent Lipschitz constant. The definition is realized as a direct wrapper to
Claim. Let $Q$ be a quantitative local factorization with log-derivative bound $M$ and radius $R$. For each positive integer $n$, the genuine regular factor phase at level $n$ is the phase object on the circle of radius $R/(n+1)$ whose log-derivative bound equals $M R/(n+1)$ and whose sample increments satisfy the arc-length estimate controlled by that constant.
background
QuantitativeLocalFactorization extends LocalMeromorphicWitness by adding a real number logDerivBound together with the positivity hypothesis and the perturbation regime condition logDerivBound times radius ≤ 1. This bound directly limits the phase perturbation contributed by the regular factor g on any circle of radius r by M times the arc length between adjacent eight-tick samples. The module MeromorphicCircleOrder adapts Mathlib meromorphic-order machinery to the Recognition Science annular-cost setting: a meromorphic function with order n at ρ factors locally as (z-ρ)^n g(z) with g holomorphic and non-vanishing at ρ, so the pole part carries phase charge -n while g contributes the controllable perturbation ε.
proof idea
The definition first casts 0 < n into the real inequalities 1 ≤ n and 0 < n+1 < n+2 via exact_mod_cast and linarith. It then invokes regularFactorPhaseFromWitness on qlf.toLocalMeromorphicWitness, the scaled radius qlf.radius/(n+1), the positivity proof div_pos, the strict inequality div_lt_self, and the pair (qlf.logDerivBound, qlf.logDerivBound_pos).
why it matters
This definition supplies the phase object required by epsilon_abs_bound, sum_epsilon_abs_bound, epsilon_log_phi_small and genuineZetaDerivedPhasePerturbationWitness. It converts the analytic input logDerivBound into the phase-level Lipschitz constant that discharges the linear-plus-quadratic error summability for RingPerturbationControl. In the Recognition framework it closes the regular-factor contribution to phi-cost control on the eight-tick octave, supporting the D=3 spatial structure and the alpha-band constants used in carrier-excess bounds for shared-circle pairs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.