regularFactorPhaseFromWitness
plain-language theorem explainer
regularFactorPhaseFromWitness supplies the RegularFactorPhase data structure for any LocalMeromorphicWitness by feeding its regular factor, center, radius and positivity proofs into the standard constructor together with a user-supplied bound M on the logarithmic derivative. Workers constructing genuine zeta-derived phase families or shared-circle carrier pairs cite it to obtain the charge-zero regular-factor component. The implementation is a direct one-line wrapper around mkRegularFactorPhase.
Claim. Let $w$ be a local meromorphic witness (center $c$, radius $R>0$, regular factor $g$ analytic and non-vanishing on the closed ball of radius $R$). For $0<r<R$ and $M>0$, define the regular-factor phase data by applying the constructor mkRegularFactorPhase to $g$, $c$, $R$, $r$, the positivity and differentiability witnesses from $w$, and the bound $M$; the resulting log-derivative bound equals $M r$.
background
LocalMeromorphicWitness is the structure that packages a meromorphic factorization datum: center $c$, integer order, radius $R>0$, the regular factor $g$ (analytic at $c$ and non-vanishing on the closed ball), together with the corresponding analyticity, differentiability-on-ball and non-vanishing proofs. The module MeromorphicCircleOrder uses this structure to bridge Mathlib meromorphic-order machinery to the RS annular-cost framework. On a circle around a zero of multiplicity $m$, the pole factor carries charge $-m$ while the regular factor carries charge 0; their sum is obtained by the charge_additive theorem.
proof idea
One-line wrapper that applies mkRegularFactorPhase, passing w.regularFactor, w.center, w.radius, the radius-positivity and radius-strict-inequality proofs, w.regularFactor_diff, w.regularFactor_nz, and the supplied bound M.
why it matters
The definition is the entry point for all genuine (non-synthetic) regular-factor phases used by genuineRegularFactorPhaseAt, genuineZetaDerivedPhaseData and genuineZetaDerivedPhasePerturbationWitness. These feed mkSharedCirclePair and the carrier-excess-bounded theorem in CarrierBudgetComparison, supplying the charge-zero Lipschitz-controlled component required for the annular-perturbation estimates in the RS zeta application. It directly implements the regular-factor half of the phase-charge decomposition described in the module doc-comment.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.