The real bounded-integrand formula for the winding number (Hungerbühler–Wasem Prop 2.3)

For a closed piecewise-C¹ curve γ that avoids a point w, Hungerbühler–Wasem Prop 2.3 evaluates the generalized winding number by the real integral

n_w(γ) = (1 / 2π) ∫_a^b (x ẏ − y ẋ) / (x² + y²) dt,

where x + i y = γ − w. Writing γ − w = x + i y and γ' = ẋ + i ẏ, the winding integrand (γ − w)⁻¹ · γ' has imaginary part exactly (x ẏ − y ẋ) / (x² + y²) (the real integrand above, here with denominator Complex.normSq (γ − w) = x² + y²); this pointwise piece is realWindingIntegrand_eq_div. For a point off the curve the winding number is a genuine integer (exists_int_windingNumber_of_closed), hence real, so the ordinary index integral (2πi)⁻¹ ∮_γ dz/(z − w) is purely imaginary: its real part vanishes and its imaginary part is the real integral above. This is the off-curve (no principal-value) case of the real formula — the computational workhorse of Layer 1; the on-curve bounded-integrand form and the ½·k·|Λ̇| crossing value need the immersion geometry and stay separate.

Main results

• TauCeti.Contour.windingNumber_eq_real_integral_of_closed — the winding number of a closed curve off w equals the real bounded integral (1 / 2π) ∫ (x ẏ − y ẋ) / (x² + y²).

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

References

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

Provenance

The pointwise imaginary-part decomposition and the real winding formula are migrated and cleaned from the AINTLIB LeanModularForms generalized-winding-number development, restated here for a raw γ : ℝ → ℂ on an oriented interval in the vocabulary the roadmap fixes.

theorem TauCeti.Contour.windingNumber_eq_real_integral_of_closed {γ : ℝ → ℂ} {w : ℂ} {a b : ℝ} {P : Set ℝ} (hclosed : γ a = γ b) (hP : P.Countable) (hγ_cont : ContinuousOn γ (Set.uIcc a b)) (hγ_diff : ∀ t ∈ Set.Ioo (min a b) (max a b) \ P, DifferentiableAt ℝ γ t) (h_avoid : ∀ t ∈ Set.uIcc a b, γ t ≠ w) (h_int : IntervalIntegrable (fun (t : ℝ) => (γ t - w)⁻¹ * deriv γ t) MeasureTheory.volume a b) : windingNumber γ a b w = ↑(1 / (2 * Real.pi) * ∫ (t : ℝ) in a..b, realWindingIntegrand (γ t - w) (deriv γ t))

The real bounded-integrand formula for the winding number (Hungerbühler–Wasem Prop 2.3, off-curve case). For a curve γ on the oriented interval with endpoints a, b that returns to its start (γ a = γ b), is continuous on Set.uIcc a b, differentiable off a countable set P, avoids w throughout, and has an interval-integrable index integrand, the generalized winding number about w is the real integral

n_w(γ) = (1 / 2π) ∫_a^b (x ẏ − y ẋ) / (x² + y²) dt, x + i y = γ − w,

with bounded real integrand and no principal value. The winding number is a genuine integer here (exists_int_windingNumber_of_closed), so the index integral is purely imaginary; its imaginary part is this real integral (realWindingIntegrand_eq_div), while its real part — the increment of log ‖γ − w‖ — vanishes by closedness.