zpow_phase_charge
plain-language theorem explainer
The map z ↦ (z − c)^n carries winding charge −n on any circle of radius R centered at c. Complex analysts and Recognition Science modelers cite this result to obtain explicit phase data for monomials before invoking winding integrals or meromorphic factorization. The proof is an explicit construction: define the phase function Θ(θ) = n θ on [0, 2π], verify continuity by multiplication of continuous maps, and confirm the winding identity by direct arithmetic.
Claim. For any $c ∈ ℂ$, $R > 0$, and $n ∈ ℤ$, the function $f(z) = (z - c)^n$ admits a continuous phase lift Θ : ℝ → ℝ on the circle $|z - c| = R$ whose total change satisfies Θ(2π) − Θ(0) = −2π(−n).
background
ContinuousPhaseData packages a continuous real function Θ together with an integer charge m such that Θ(2π) − Θ(0) = −2π m; the charge is the winding number of the underlying nonvanishing function along the circle. The module CirclePhaseLift supplies the bridge from Mathlib complex analysis to the discrete annular-cost framework by sampling such phases at 8n equispaced points. The upstream result holomorphic_nonvanishing_zero_charge shows that analytic nonvanishing functions have charge zero, so the present theorem supplies the complementary nonzero-charge case for pure powers.
proof idea
The proof is a direct construction. It builds a ContinuousPhaseData record with center c, radius R, phase function λ θ, (n : ℝ) * θ, and charge −n. Continuity of the phase follows from the product of the constant n and the identity map. The winding identity phase(2π) − phase(0) = −2π(−n) is discharged by simp and ring after rewriting the negation.
why it matters
This theorem supplies the explicit phase data required by zpow_charge_eq_winding_integral, which equates the constructed charge to the contour-integral winding number, and by meromorphic_phase_charge, which lifts local meromorphic orders to ContinuousPhaseData. It therefore closes the link between the algebraic power (z − c)^n and the Recognition Science phase-charge accounting used in annular sampling and EightTick periodicity. No open scaffolding remains; the result is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.