winding_integral_simple_pole
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.
claimIf $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 in Recognition Science
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.
scope and limits
- Does not evaluate the integral when the pole lies on or outside the contour.
- Does not treat higher-order poles or essential singularities.
- Does not apply to non-circular contours.
formal statement (Lean)
313theorem winding_integral_simple_pole (c w : ℂ) (R : ℝ) (hw : w ∈ Metric.ball c R) :
314 (∮ z in C(c, R), (z - w)⁻¹) = 2 * ↑π * Complex.I :=
proof body
Term-mode proof.
315 circleIntegral.integral_sub_inv_of_mem_ball hw
316
317/-- Cauchy–Goursat for the circle: if `f` is holomorphic on the closed disk
318(possibly off a countable set), the contour integral vanishes. -/