winding_integral_simple_pole
plain-language theorem explainer
Contour integration of the reciprocal difference over a circle yields exactly 2πi when the pole lies strictly inside the disk. Results that equate phase charges in continuous data structures to analytic winding numbers invoke this identity to close the link between holomorphic functions and discrete charges. The argument is a direct term application of the pre-verified Mathlib formula for the integral of 1/(z-w) inside the ball.
Claim. If $w$ lies inside the open disk of radius $R$ centered at $c$ in the complex plane, then the contour integral of $1/(z-w)$ over the circle $|z-c|=R$ equals $2πi$.
background
ContinuousPhaseData packages a continuous real-valued phase function Θ on the circle together with an integer charge that records the net winding: the change Θ(2π) − Θ(0) equals −2π times the charge. The Circle Phase Lift module supplies the analytic layer that converts such phase data into the cost functions required by annular ring sampling. The present result supplies the standard Cauchy integral for a simple pole, which is the Mathlib fact underlying the connection between zpow_phase_charge and the winding integral.
proof idea
The proof is a one-line term wrapper that applies the Mathlib lemma computing the integral of the reciprocal difference when the point lies inside the ball.
why it matters
The lemma is invoked by zpow_charge_eq_winding_integral to equate the charge of a power function with the normalized contour integral. It completes the analytic-to-discrete bridge inside the Circle Phase Lift module, supporting the phase data that feeds the Recognition Composition Law and the eight-tick octave structure. No open scaffolding remains at this step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.