regularFactorPhaseFromWitness
Constructs a RegularFactorPhase instance from a LocalMeromorphicWitness by feeding its analytic regular factor, center, radius, and a caller-supplied bound M on |g'/g| into the covering-space lift constructor. Researchers modeling zeta-derived phase perturbations and annular cost bounds in the Recognition Science framework cite this to obtain charge-zero phase data with explicit log-derivative control. The definition is a direct one-line wrapper around mkRegularFactorPhase that threads the witness fields and radius inequalities.
claimLet $w$ be a local meromorphic witness with center $c$, radius $R>0$, and regular factor $g$ analytic and non-vanishing on the closed disk of radius $R$. For $0<r<R$ and $M>0$, the regular factor phase is the phase data with center $c$, radius $r$, charge $0$, phase given by the covering-space lift of $g$, and logarithmic derivative bound $Mr$.
background
The module MeromorphicCircleOrder bridges Mathlib meromorphic-order machinery to the RS annular-cost framework. A meromorphic function admits the local factorization $f(z)=(z-ρ)^n g(z)$ with $g$ analytic and $g(ρ)≠0$; the pole factor carries phase charge $-n$ while the regular factor carries charge $0$, and charge_additive combines them on a common circle. LocalMeromorphicWitness packages the center, order, radius, the regularFactor function together with its analyticity at the center, differentiability on the closed ball, and strict non-vanishing on that ball.
proof idea
This definition is a one-line wrapper that applies mkRegularFactorPhase to the witness regularFactor, center, radius, the supplied $r$ with the two radius inequalities, the differentiability and non-vanishing fields of the witness, and the bound $M$.
why it matters in Recognition Science
The definition supplies the genuine regular-factor phase used by genuineZetaDerivedPhaseData, genuineZetaDerivedPhasePerturbationWitness, and qlf_regularFactorPhase to produce non-synthetic perturbation data for zeta-derived phases. It is invoked by mkSharedCirclePair and mkSharedCirclePair_carrier_excess_bounded in CarrierBudgetComparison to equip the charge-zero carrier family with Lipschitz-controlled excess bounds. In the Recognition framework it realizes the regular-factor contribution to phase-charge additivity on meromorphic circles, feeding the annular-cost bounds required for defect sampling around zeros.
scope and limits
- Does not establish existence of a regular factor for an arbitrary meromorphic function.
- Does not compute or bound the numerical value of $M$; the caller supplies it.
- Does not evaluate explicit phase values on the circle; it only assembles the data structure.
- Does not extend beyond the local disk of the witness to global meromorphic continuation.
formal statement (Lean)
402noncomputable def regularFactorPhaseFromWitness
403 (w : LocalMeromorphicWitness) (r : ℝ) (hr : 0 < r) (hrw : r < w.radius)
404 (M : ℝ) (hM : 0 < M) :
405 RegularFactorPhase :=
proof body
Definition body.
406 mkRegularFactorPhase
407 w.regularFactor w.center w.radius r
408 w.radius_pos hr hrw
409 w.regularFactor_diff w.regularFactor_nz
410 M hM
411
412/-- Phase data using the genuine regular factor phase: combines pole winding
413with the Lipschitz-controlled regular-factor phase from the covering-space
414lift, producing non-trivial perturbation data.
415
416Unlike `zetaDerivedPhaseDataBundle` (which uses synthetic linear phase),
417this construction passes through `charge_additive` to combine:
418- pole factor: charge = -order, phase = order * θ
419- regular factor: charge = 0, phase = genuine covering-space lift -/