zpow_charge_eq_winding_integral
plain-language theorem explainer
The theorem equates the integer charge of the continuous phase datum for the monomial (z-c)^n on a circle of radius R to the negative real part of the normalized contour integral of n/(z-c) dz. Researchers bridging holomorphic functions to discrete annular sampling costs would cite this link. The proof is a term-mode wrapper that obtains the explicit phase record from zpow_phase_charge and substitutes the known simple-pole integral value.
Claim. For $c ∈ ℂ$, $R > 0$, and $n ∈ ℤ$, there exists a continuous phase datum with center $c$, radius $R$, and charge $-n$ such that this charge equals $-Re((1/(2πi)) · n · ∮_{C(c,R)} (z-c)^{-1} dz)$.
background
ContinuousPhaseData packages a continuous real-valued phase function Θ : ℝ → ℝ on the circle together with its integer winding charge, defined by the condition Θ(2π) − Θ(0) = −2π · charge. The CirclePhaseLift module supplies the infrastructure that lifts nonvanishing holomorphic functions on an annulus to such phase data while satisfying the winding constraint of AnnularRingSample in the cost framework.
proof idea
The proof is a term-mode wrapper. It obtains the ContinuousPhaseData record from zpow_phase_charge, refines the existential by rewriting the charge field, and invokes winding_integral_simple_pole at the center. Algebraic simplification then cancels the 2πi factor and extracts the real part, confirming the integral equals n and the charges match.
why it matters
This declaration closes the explicit verification that the phase charge for monomials coincides with the classical winding number from contour integration. It sits inside the CirclePhaseLift module whose purpose is to embed Mathlib complex analysis into the Recognition Science annular cost model. No downstream uses are recorded yet, but the equality supplies the concrete link between the discrete charge integer and the continuous integral appearing in the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.