The generalized winding number of a circle: 1 at the centre, 0 outside

For the counterclockwise circle circleMap c R traversed over [0, 2π], this file evaluates the generalized winding number TauCeti.Contour.windingNumber (Hungerbühler–Wasem Def 2.1) at two kinds of points:

• at every interior point w — one with dist w c < R — the winding number is 1 (windingNumber_circleMap_eq_one_of_dist_lt), in particular at the centre c (windingNumber_circleMap_center_eq_one), and
• at every exterior point w — one with R < dist w c — it is 0 (windingNumber_circleMap_eq_zero_of_lt_dist).

Together these are the roadmap's n_c(circle) = 1 normalization and its companion "n is 0 outside" (ContourIntegration/README.md, the worked examples). They upgrade the raw-index-integral raw index-integral value windingNumber_circle to statements about the windingNumber definition, connecting the principal-value packaging to the elementary circle computation and to Mathlib's disc Cauchy theory.

The exterior value rests on a fact Mathlib records as missing: the Cauchy-kernel integral ∮_{C(c,R)} dz/(z − w) for w outside the closed disc is not among the explicit circleIntegral.integral_sub_* formulas (its docstring notes the case |w − c| > R is deferred to Cauchy's theorem). We supply it here as circleIntegral_sub_inv_eq_zero_of_lt_dist, obtained from DiffContOnCl.circleIntegral_eq_zero: for w off the closed disc, z ↦ (z − w)⁻¹ is holomorphic across the whole disc, so its circle integral vanishes.

Main results

• TauCeti.Contour.circleIntegral_sub_inv_eq_zero_of_lt_dist — the exterior Cauchy-kernel circle integral ∮_{C(c,R)} (z − w)⁻¹ = 0 for R < dist w c.
• TauCeti.Contour.windingNumber_circleMap_eq_circleIntegral — off the circle, the generalized winding number is (2πi)⁻¹ times the ordinary Cauchy-kernel circle integral.
• TauCeti.Contour.windingNumber_circleMap_eq_one_of_dist_lt — n_w(circle) = 1 for any w inside the disc.
• TauCeti.Contour.indexIntegral_arc_interval and TauCeti.Contour.indexIntegral_arc — the normalized index integral of a circular arc about its centre, (b − a) / 2π and α / 2π, with the specialization windingNumber_circle (the full circle, 1). The two values the valence formula names by their points, windingNumber_at_i and windingNumber_at_rho, are in ModelSector/Winding.lean.
• TauCeti.Contour.cauchyPVExistsAt_circleMap_comp_affine — the index principal value of an affinely reparametrised circle exists.
• TauCeti.Contour.windingNumber_circleMap_center — an arc about its own centre has winding (b − a) / 2π, its angular extent, with the two specializations TauCeti.Contour.windingNumber_circleMap_center_eq_one (n_c(circle) = 1, over [0, 2π]) and TauCeti.Contour.windingNumber_circleMap_center_eq_half (n_c(semicircle) = ½, over [0, π]).
• TauCeti.Contour.windingNumber_circleMap_eq_zero_of_lt_dist — n_w(circle) = 0 for w outside the disc.

This is a Layer-1 acceptance criterion of the Hungerbühler–Wasem generalized residue theorem (HW Thm 3.3).

Provenance

The arc index-integral material (indexIntegral_arc_interval, indexIntegral_arc and their specialization windingNumber_circle) was migrated and adapted from the AINTLIB LeanModularForms project (ForMathlib/HungerbuhlerWasem/Crossing.lean), specialised to the raw-function (γ : ℝ → ℂ on [a, b]) design of the contour-integration roadmap.

References

• N. Hungerbühler, M. Wasem, Non-integer valued winding numbers and a generalized Residue Theorem, arXiv:1808.00997.

theorem TauCeti.Contour.indexIntegral_arc_interval {z₀ : ℂ} {r : ℝ} (hr : r ≠ 0) (a b : ℝ) : (2 * ↑Real.pi * Complex.I)⁻¹ * ∫ (θ : ℝ) in a..b, deriv (circleMap z₀ r) θ / (circleMap z₀ r θ - z₀) = ↑(b - a) / (2 * ↑Real.pi)

The circular-arc index integral (Hungerbühler–Wasem (2.4)), on an arbitrary angular interval. For the circular arc γ θ = z₀ + r·e^{iθ} about its centre z₀, traversed over [a, b], the normalized index integral is the signed angular extent over 2π: (2πi)⁻¹ ∫_a^b (γ̇ / (γ − z₀)) dθ = (b − a) / 2π. The centre is off the arc, so the integrand γ̇ / (γ − z₀) is constantly i and the value is elementary. This is the general arbitrary-interval statement; indexIntegral_arc (a = 0) and windingNumber_circle are derived from it.

@[deprecated TauCeti.Contour.indexIntegral_arc_interval (since := "2026-07-29")]

theorem TauCeti.Contour.windingNumber_modelSector_interval {z₀ : ℂ} {r : ℝ} (hr : r ≠ 0) (a b : ℝ) : (2 * ↑Real.pi * Complex.I)⁻¹ * ∫ (θ : ℝ) in a..b, deriv (circleMap z₀ r) θ / (circleMap z₀ r θ - z₀) = ↑(b - a) / (2 * ↑Real.pi)

Alias of TauCeti.Contour.indexIntegral_arc_interval.

---

The circular-arc index integral (Hungerbühler–Wasem (2.4)), on an arbitrary angular interval. For the circular arc γ θ = z₀ + r·e^{iθ} about its centre z₀, traversed over [a, b], the normalized index integral is the signed angular extent over 2π: (2πi)⁻¹ ∫_a^b (γ̇ / (γ − z₀)) dθ = (b − a) / 2π. The centre is off the arc, so the integrand γ̇ / (γ − z₀) is constantly i and the value is elementary. This is the general arbitrary-interval statement; indexIntegral_arc (a = 0) and windingNumber_circle are derived from it.

theorem TauCeti.Contour.indexIntegral_arc {z₀ : ℂ} {r : ℝ} (hr : r ≠ 0) (α : ℝ) : (2 * ↑Real.pi * Complex.I)⁻¹ * ∫ (θ : ℝ) in 0..α, deriv (circleMap z₀ r) θ / (circleMap z₀ r θ - z₀) = ↑α / (2 * ↑Real.pi)

The normalized index integral of a circular arc (Hungerbühler–Wasem (2.4)). The arc γ θ = z₀ + r·e^{iθ} about its centre z₀, traversed over [0, α], has normalized index integral (2πi)⁻¹ ∫_0^α (γ̇ / (γ − z₀)) dθ = α / 2π: an arc of signed angular extent α contributes generalized winding number α/2π. For 0 ≤ α the traversal is counterclockwise; for α < 0 the interval [0, α] is reversed, the arc runs clockwise, and the contribution is negative.

The α = 2π specialization is windingNumber_circle; the α = π and α = π/3 values the valence formula names by their points are windingNumber_at_i and windingNumber_at_rho, in ModelSector/Winding.lean.

ContourIntegration/Suggested.lean lists this statement as windingNumber_modelSector, which is retained below as a deprecated alias. The closed model-sector curve — a different statement — is TauCeti.Contour.windingNumber_closedModelSector in ModelSector/Closed.lean.

@[deprecated TauCeti.Contour.indexIntegral_arc (since := "2026-07-29")]

theorem TauCeti.Contour.windingNumber_modelSector {z₀ : ℂ} {r : ℝ} (hr : r ≠ 0) (α : ℝ) : (2 * ↑Real.pi * Complex.I)⁻¹ * ∫ (θ : ℝ) in 0..α, deriv (circleMap z₀ r) θ / (circleMap z₀ r θ - z₀) = ↑α / (2 * ↑Real.pi)

Alias of TauCeti.Contour.indexIntegral_arc.

---

The normalized index integral of a circular arc (Hungerbühler–Wasem (2.4)). The arc γ θ = z₀ + r·e^{iθ} about its centre z₀, traversed over [0, α], has normalized index integral (2πi)⁻¹ ∫_0^α (γ̇ / (γ − z₀)) dθ = α / 2π: an arc of signed angular extent α contributes generalized winding number α/2π. For 0 ≤ α the traversal is counterclockwise; for α < 0 the interval [0, α] is reversed, the arc runs clockwise, and the contribution is negative.

The α = 2π specialization is windingNumber_circle; the α = π and α = π/3 values the valence formula names by their points are windingNumber_at_i and windingNumber_at_rho, in ModelSector/Winding.lean.

ContourIntegration/Suggested.lean lists this statement as windingNumber_modelSector, which is retained below as a deprecated alias. The closed model-sector curve — a different statement — is TauCeti.Contour.windingNumber_closedModelSector in ModelSector/Closed.lean.

theorem TauCeti.Contour.windingNumber_circle {c : ℂ} {r : ℝ} (hr : r ≠ 0) : (2 * ↑Real.pi * Complex.I)⁻¹ * ∫ (θ : ℝ) in 0..2 * Real.pi, deriv (circleMap c r) θ / (circleMap c r θ - c) = 1

A full circle ([0, 2π]) has winding number 1 — the closed-curve normalization, the [0, 2π] specialization of indexIntegral_arc (2π / 2π = 1). Its value also follows from Mathlib's circleIntegral.integral_sub_center_inv; this is the raw-index-integral form of that normalization used as a Layer-1 target.

theorem TauCeti.Contour.circleIntegral_sub_inv_eq_zero_of_lt_dist {c w : ℂ} {R : ℝ} (hR : 0 ≤ R) (hw : R < dist w c) : ∮ (z : ℂ) in C(c, R), (z - w)⁻¹ = 0

The exterior Cauchy-kernel circle integral vanishes. For a point w strictly outside the closed disc of radius R ≥ 0 about c (R < dist w c), the integral of the Cauchy kernel (z − w)⁻¹ around the circle is 0. On the closed disc the kernel is holomorphic (its only singularity w lies outside), so DiffContOnCl.circleIntegral_eq_zero applies. Mathlib's circleIntegral.integral_sub_inv_of_mem_ball covers the interior case (value 2πi) but leaves this exterior case to Cauchy's theorem, which is exactly this argument.

theorem TauCeti.Contour.windingNumber_circleMap_eq_circleIntegral {c w : ℂ} {R : ℝ} (havoid : ∀ (θ : ℝ), circleMap c R θ ≠ w) : windingNumber (circleMap c R) 0 (2 * Real.pi) w = (2 * ↑Real.pi * Complex.I)⁻¹ * ∮ (z : ℂ) in C(c, R), (z - w)⁻¹

Off the circle, the generalized winding number of circleMap c R over [0, 2π] about w is the ordinary Cauchy-kernel circle integral, normalized by (2πi)⁻¹. The avoidance hypothesis (circleMap c R θ ≠ w for all θ) collapses the principal value in windingNumber to the ordinary integral, which is ∮_{C(c,R)} (z − w)⁻¹ up to the commutativity of the integrand's product.

theorem TauCeti.Contour.windingNumber_circleMap_eq_one_of_dist_lt {c w : ℂ} {R : ℝ} (hw : dist w c < R) : windingNumber (circleMap c R) 0 (2 * Real.pi) w = 1

n_w(circle) = 1 inside the disc — the interior value at an arbitrary point. For a point w strictly inside the disc (dist w c < R, so 0 < R), the generalized winding number of the counterclockwise circle circleMap c R over [0, 2π] about w is 1: the kernel integral ∮_{C(c,R)} (z − w)⁻¹ is 2πi by circleIntegral.integral_sub_inv_of_mem_ball, and the (2πi)⁻¹ normalization of windingNumber_circleMap_eq_circleIntegral cancels it to 1.

theorem TauCeti.Contour.cauchyPVExistsAt_circleMap_comp_affine {c : ℂ} {R : ℝ} (m s a b : ℝ) : CauchyPVExistsAt (circleMap c R ∘ fun (t : ℝ) => m * t + s) a b (fun (z : ℂ) => (z - c)⁻¹) c

The index principal value of an affinely reparametrised circle exists. The curve t ↦ circleMap c R (m t + s) stays at distance |R| from c, so for R ≠ 0 the principal value about c is the ordinary integral. At R = 0 the curve is constant at c, every truncated integrand is identically zero, and the principal value exists (and is 0) for that reason instead. This is the shared construction behind the arc pieces of the model sector and of the half-disc worked example.

@[simp]

theorem TauCeti.Contour.windingNumber_circleMap_center {c : ℂ} {R : ℝ} (hR : R ≠ 0) (a b : ℝ) : windingNumber (circleMap c R) a b c = ↑(b - a) / (2 * ↑Real.pi)

The winding number of a circular arc about its own centre is its angular extent over 2π. For R ≠ 0, the generalized winding number of circleMap c R over [a, b] about c is (b - a) / 2π. The curve misses its centre (circleMap_ne_center), so the principal value in windingNumber collapses to the ordinary index integral, which is indexIntegral_arc_interval. This is the windingNumber-definition form of that raw index-integral computation.

theorem TauCeti.Contour.windingNumber_circleMap_center_eq_one {c : ℂ} {R : ℝ} (hR : R ≠ 0) : windingNumber (circleMap c R) 0 (2 * Real.pi) c = 1

n_c(circle) = 1 — the closed-curve normalization at the centre. The generalized winding number of the counterclockwise circle circleMap c R (R ≠ 0) over [0, 2π] about its centre c is 1, the interior value. This is the [0, 2π] specialization of windingNumber_circleMap_center (2π / 2π = 1); it reconciles with circleIntegral.integral_sub_center_inv. Unlike windingNumber_circleMap_eq_one_of_dist_lt, this covers a negative radius R as well.

theorem TauCeti.Contour.windingNumber_circleMap_center_eq_half {c : ℂ} {R : ℝ} (hR : R ≠ 0) : windingNumber (circleMap c R) 0 Real.pi c = 1 / 2

n_c(semicircle) = ½ at the centre, the [0, π] specialization of windingNumber_circleMap_center.

This is one of the two ingredients of a half-disc contour computation: the arc about the point supplies ½, and windingNumber_eq_zero_segment supplies 0 for a diameter through it. The combined contour, and the additivity argument assembling the two, are not established here.

theorem TauCeti.Contour.windingNumber_circleMap_eq_zero_of_lt_dist {c w : ℂ} {R : ℝ} (hR : 0 ≤ R) (hw : R < dist w c) : windingNumber (circleMap c R) 0 (2 * Real.pi) w = 0

n_w(circle) = 0 outside the disc — the roadmap's "n is 0 outside" companion to the centre normalization. For a point w strictly outside the closed disc (R < dist w c, with R ≥ 0), the generalized winding number of circleMap c R over [0, 2π] about w vanishes: the kernel is holomorphic across the disc, so the Cauchy-kernel circle integral is 0.