regularFactor_continuousPhase_exists
plain-language theorem explainer
The theorem asserts existence of a continuous real phase function on the circle with zero net change over a full 2π period, for any differentiable nonvanishing g on a closed disk. Constructions of regular factor phases in the annular cost framework cite this result to obtain the required zero-winding witness. The proof is a direct term that instantiates the constant zero function and verifies continuity plus endpoint equality by simplification.
Claim. Let $g : ℂ → ℂ$ be differentiable on the closed disk of radius $R$ centered at $c ∈ ℂ$, with $0 < r < R$, and suppose $g(z) ≠ 0$ for all $z$ in that disk. Then there exists a continuous function $ϕ : ℝ → ℝ$ such that $ϕ ≡ 0$ and $ϕ(2π) − ϕ(0) = 0$.
background
The Circle Phase Lift module supplies continuous-phase infrastructure that bridges Mathlib complex analysis to the discrete AnnularRingSample and AnnularMesh cost framework. A continuous phase Θ : ℝ → ℝ is a real lift whose total change Θ(2π) − Θ(0) = −2π m encodes the winding number m; sampling at 8n equispaced angles produces increments satisfying the winding_constraint of AnnularRingSample. The module relies on Mathlib primitives such as circleMap, circleIntegral_eq_zero_of_differentiable_on_off_countable, and IsCoveringMap.liftPath.
proof idea
The proof is a term-mode one-line wrapper. It refines the existential with the constant-zero function, reflexivity for the definitional equality, simpa to confirm continuity of the constant map, and simp to obtain the zero difference at the endpoints.
why it matters
This supplies the zero-winding witness required by mkRegularFactorPhase to build a RegularFactorPhase with explicit log-derivative bound. It implements the module interface that needs only some continuous phase with zero total change, without a representation theorem tying the phase to g. The result supports the transition from holomorphic nonvanishing functions (holomorphic_nonvanishing_zero_charge) to discrete phase sampling in annular costs, consistent with the eight-tick octave and zero-charge condition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.