regularFactor_phase_lipschitz
Constant zero phase satisfies the Lipschitz condition with bound M r for any positive M and r. Researchers building RegularFactorPhase witnesses for holomorphic nonvanishing functions with zero charge cite this auxiliary result. The tactic proof substitutes the constant-phase hypothesis and reduces the claim to nonnegativity of the bound via positivity and simplification.
claimLet phase : ℝ → ℝ be the constant zero function. Then for all real θ₁, θ₂, |phase(θ₂) − phase(θ₁)| ≤ (M r) |θ₂ − θ₁|, whenever M > 0, r > 0, and the standing data (g holomorphic and nonvanishing on the closed disk of radius R > r) are given.
background
The CirclePhaseLift module supplies continuous phase lifts for nonvanishing holomorphic functions on disks or annuli, bridging Mathlib complex analysis to the annular cost and 8-tick sampling framework. RegularFactorPhase (defined in the same module) extends ContinuousPhaseData by a positive logDerivBound together with the phase_lipschitz property and the assertion charge = 0; the latter follows from the argument principle once g is holomorphic and nonvanishing inside the circle. Upstream, EightTick.phase supplies the discrete 8-tick angles kπ/4, while the general phase here is the continuous real lift whose total change encodes winding number.
proof idea
The tactic proof introduces the two angles θ₁ and θ₂, substitutes the hypothesis that phase is identically zero, invokes the positivity tactic to obtain 0 ≤ (M r) |θ₂ − θ₁|, and finishes with simpa. No external lemmas are applied; the argument is a direct verification that the zero function meets the Lipschitz requirement for any positive constant.
why it matters in Recognition Science
The declaration is invoked inside mkRegularFactorPhase to discharge the phase_lipschitz field of RegularFactorPhase when the lift is trivial. This closes the zero-charge case for holomorphic nonvanishing g, which is guaranteed by the sibling result holomorphic_nonvanishing_zero_charge and aligns with the zero-winding constraint required by AnnularRingSample. It thereby completes one concrete instance of the continuous-to-discrete bridge that feeds the Recognition framework's annular mesh and the eight-tick octave structure.
scope and limits
- Does not establish a Lipschitz bound for any non-constant phase lift.
- Does not invoke differentiability or nonvanishing of g in the argument.
- Does not produce an explicit phase function or its derivative bound.
- Applies exclusively to the constant-zero phase supplied by the caller.
formal statement (Lean)
146theorem regularFactor_phase_lipschitz
147 (g : ℂ → ℂ) (c : ℂ) (R r : ℝ) (_hR : 0 < R) (_hr : 0 < r) (_hrR : r < R)
148 (_hg_diff : DifferentiableOn ℂ g (Metric.closedBall c R))
149 (_hg_nz : ∀ z ∈ Metric.closedBall c R, g z ≠ 0)
150 (M : ℝ) (hM : 0 < M)
151 (phase : ℝ → ℝ)
152 (hphase : phase = fun _ => 0) :
153 ∀ θ₁ θ₂ : ℝ, |phase θ₂ - phase θ₁| ≤ (M * r) * |θ₂ - θ₁| := by
proof body
Tactic-mode proof.
154 intro θ₁ θ₂
155 subst hphase
156 have hnonneg : 0 ≤ (M * r) * |θ₂ - θ₁| := by positivity
157 simpa using hnonneg
158
159/-- Build a `RegularFactorPhase` from the continuous-lift existence