The winding number of a closed curve is an integer

For a curve γ on an interval that returns to its start (γ a = γ b), avoids a point w, and is regular enough — continuous, differentiable off a countable set, with an interval-integrable index integrand — its generalized winding number about w is an integer (see exists_int_windingNumber_of_closed for the exact hypotheses). This is the integrality step on the Hungerbühler–Wasem path (HW Thm 3.3): combined with continuity of the winding number in the point, it makes the winding number locally constant on the complement of the curve — the input to the homology form of Cauchy's theorem.

Closing the curve is the only thing used here: exp_two_pi_I_mul_windingNumber_of_avoidance evaluates exp (2πi · n_w(γ)) as the endpoint ratio (γ b - w) / (γ a - w) for any avoiding arc, and γ a = γ b makes that ratio 1.

Main results

• TauCeti.Contour.exists_int_windingNumber_of_closed — the generalized winding number of a closed curve is an integer.
• TauCeti.Contour.IsPiecewiseC1On.exists_int_windingNumber — the same for a closed piecewise-C¹ curve, whose regularity supplies the raw hypotheses on its own.

Provenance

Adapted from hasGeneralizedWindingNumber_integer_of_closed in WindingInteger.lean of the AINTLIB LeanModularForms development, restated for a raw γ : ℝ → ℂ on an oriented interval. The argument-lift computation that used to sit here now lives in Winding.EndpointRatio, which proves it for arcs that need not close up.

theorem TauCeti.Contour.exists_int_windingNumber_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) : ∃ (n : ℤ), windingNumber γ a b w = ↑n

The winding number of a closed curve is an integer. 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 Set.uIcc a b, and has an interval-integrable index integrand (γ · - w)⁻¹ * deriv γ, the generalized winding number windingNumber γ a b w is an integer.

theorem TauCeti.Contour.IsPiecewiseC1On.exists_int_windingNumber {γ : ℝ → ℂ} {a b : ℝ} {w : ℂ} (hγ : IsPiecewiseC1On γ a b) (hclosed : γ a = γ b) (h_avoid : ∀ t ∈ Set.uIcc a b, γ t ≠ w) : ∃ (n : ℤ), windingNumber γ a b w = ↑n

Piecewise-C¹ form of winding-number integrality. For a closed piecewise-C¹ curve that avoids w, the winding number about w is an integer. Piecewise-C¹ regularity supplies the continuity, differentiability and integrability hypotheses of exists_int_windingNumber_of_closed.