mkRegularFactorPhase
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not prove existence of the continuous phase lift.
- Does not supply an explicit formula for the phase function.
- Does not apply when zeros lie inside the disk.
- Does not bound charge for meromorphic functions.
Lean usage
mkRegularFactorPhase w.regularFactor w.center w.radius r hr hrw M hMformal statement (Lean)
167noncomputable def mkRegularFactorPhase
168 (g : ℂ → ℂ) (c : ℂ) (R r : ℝ) (hR : 0 < R) (hr : 0 < r) (hrR : r < R)
169 (hg_diff : DifferentiableOn ℂ g (Metric.closedBall c R))
170 (hg_nz : ∀ z ∈ Metric.closedBall c R, g z ≠ 0)
171 (M : ℝ) (hM : 0 < M) :
172 RegularFactorPhase := by
proof body
Definition body.
173 have hex := regularFactor_continuousPhase_exists g c R r hR hr hrR hg_diff hg_nz
174 exact {
175 center := c
176 radius := r
177 radius_pos := hr
178 phase := hex.choose
179 phase_continuous := hex.choose_spec.2.1
180 charge := 0
181 phase_winding := by simp [hex.choose_spec.2.2]
182 logDerivBound := M * r
183 logDerivBound_pos := mul_pos hM hr
184 phase_lipschitz := regularFactor_phase_lipschitz g c R r hR hr hrR
185 hg_diff hg_nz M hM hex.choose hex.choose_spec.1
186 charge_zero := rfl
187 }
188
189/-! ### §3a. Zero charge for holomorphic nonvanishing functions -/
190
191/-- A holomorphic nonvanishing function on a closed disk has zero winding
192on the boundary circle.
193
194**Proof**: constructs a `RegularFactorPhase`, then extracts the
195`ContinuousPhaseData` with charge `0`. -/