regularFactor_phase_lipschitz
plain-language theorem explainer
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.
Claim. Let 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.