mkRegularFactorPhase
plain-language theorem explainer
mkRegularFactorPhase assembles a RegularFactorPhase record for a holomorphic nonvanishing function g on a disk by calling the continuous phase existence result and inserting an explicit log-derivative bound M r. Researchers building annular cost models or phase perturbation witnesses cite it when they need a concrete zero-charge witness with controlled Lipschitz constant. The definition proceeds by direct structure construction after one invocation of the existence lemma and one application of the Lipschitz lemma.
Claim. Let $g:ℂ→ℂ$ be differentiable on the closed disk of radius $R$ centered at $c∈ℂ$ and nonvanishing there. For $0<r<R$ and positive real $M$, the construction produces a RegularFactorPhase with center $c$, radius $r$, charge zero, continuous phase lift, and Lipschitz constant $Mr$ on the phase function.
background
RegularFactorPhase extends ContinuousPhaseData by adding a log-derivative bound, its positivity, a Lipschitz condition on the phase, and the assertion charge=0. The module supplies continuous-phase infrastructure that connects Mathlib complex analysis (circle integrals, covering lifts) to the discrete AnnularRingSample and AnnularMesh cost framework. Upstream results guarantee a continuous zero-winding phase via the existence lemma and establish the Lipschitz property from the supplied bound M on |g'/g|.
proof idea
The definition calls regularFactor_continuousPhase_exists to obtain the phase and its zero-winding property, then builds the record by setting center, radius, phase, charge=0, logDerivBound=M*r, and applying regularFactor_phase_lipschitz to the chosen phase. The charge_zero field is discharged by reflexivity.
why it matters
This definition supplies the zero-charge phase witness required by holomorphic_nonvanishing_zero_charge and regularFactorPhaseFromWitness. It is invoked in mkSharedCirclePair_carrier_excess_bounded to control carrier excess and in genuineZetaDerivedPhasePerturbationWitness for perturbation estimates. It realizes the zero-winding property for holomorphic factors, enabling phase sampling that feeds the eight-tick octave and annular cost calculations in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.