holomorphic_nonvanishing_zero_charge
plain-language theorem explainer
A holomorphic function without zeros on a closed disk admits a continuous phase lift on the boundary circle with zero total winding. Analysts using the argument principle to bound charges in annular cost models would cite this when establishing zero-charge regular factors. The proof invokes mkRegularFactorPhase on a halved radius and directly assembles the ContinuousPhaseData structure with charge zero.
Claim. If $f : ℂ → ℂ$ is differentiable on the closed disk of radius $R > 0$ centered at $c ∈ ℂ$ and $f(z) ≠ 0$ for all $z$ in the disk, then there exists a ContinuousPhaseData record with center $c$, radius $R$, and charge $0$.
background
The CirclePhaseLift module supplies continuous phase data for nonvanishing functions on circles, bridging complex analysis to the annular cost framework of AnnularRingSample. ContinuousPhaseData packages a continuous real-valued phase function Θ : ℝ → ℝ together with an integer charge satisfying Θ(2π) − Θ(0) = −2π·charge. RegularFactorPhase extends ContinuousPhaseData by a log-derivative Lipschitz bound and records that charge equals zero whenever the underlying function is holomorphic and nonvanishing on a disk containing the circle, by the argument principle.
proof idea
The proof first obtains strict inequalities for the halved radius R/2. It applies mkRegularFactorPhase to f, c, R and R/2 under the given differentiability and nonvanishing hypotheses. The resulting RegularFactorPhase supplies the phase function, its continuity, and the charge_zero fact; the theorem then constructs the ContinuousPhaseData instance by copying these fields and setting charge to zero, using the charge_zero property to discharge the winding equation.
why it matters
This result establishes that holomorphic nonvanishing functions induce zero-charge phases, a foundational step in the phase-lift infrastructure. It supports the subsequent explicit charge calculations for z-powers and additive properties under multiplication. In the Recognition framework it aligns with the eight-tick phase sampling and the requirement that regular factors contribute zero winding to the annular cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.