Homotopy invariance of the winding number

Two piecewise-C¹ paths with the same endpoints, joined by an arbitrary continuous fixed-endpoint homotopy through ℂ \ {w}, have the same winding number about w. The proof regularizes finitely many horizontal slices of the homotopy by endpoint-preserving smooth approximations, then chains the resulting smooth paths with proximity invariance of the winding number.

Main results

• windingNumber_eq_two_pi_I_inv_mul_curveIntegral identifies Tau Ceti's raw-function winding number of a piecewise-C¹ path with Mathlib's curve integral of the Cauchy-kernel 1-form.
• windingNumber_eq_of_pathHomotopy proves the Layer 0 homotopy invariance result without any regularity hypothesis on the homotopy.
• curveIntegral_inv_sub_smul_id_eq_of_pathHomotopy is its curve-integral form: such a homotopy preserves the integral of the Cauchy-kernel 1-form.
• isNullHomologous_iff_of_pathHomotopy transfers null-homology across a homotopy in the ambient set.

Provenance

The regularization step is exists_contDiff_eq_endpoints_dist_lt, which reuses Mathlib's bernsteinApproximation_uniform. No formal source is vendored. Homotopy invariance of the classical winding number is standard complex analysis; see the references in the Contour Integration roadmap.

theorem TauCeti.Contour.windingNumber_eq_two_pi_I_inv_mul_curveIntegral {x y w : ℂ} {p : Path x y} (hp : IsPiecewiseC1On (⇑p.extend) 0 1) (havoid : ∀ (t : ↑(Set.Icc 0 1)), p t ≠ w) : windingNumber (⇑p.extend) 0 1 w = (2 * ↑Real.pi * Complex.I)⁻¹ * ∫ᶜ (z : ℂ) in p, (z - w)⁻¹ • ContinuousLinearMap.id ℂ ℂ

For a piecewise-C¹ path avoiding w, its winding number about w is the normalized curve integral of the closed 1-form z ↦ (z - w)⁻¹ dz. This is the bridge from Tau Ceti's raw-function winding number to Mathlib's path-based curve integral.

theorem TauCeti.Contour.windingNumber_eq_of_pathHomotopy {x y w : ℂ} {p q : Path x y} (φ : p.Homotopy q) (hp : IsPiecewiseC1On (⇑p.extend) 0 1) (hq : IsPiecewiseC1On (⇑q.extend) 0 1) (havoid : ∀ (st : ↑unitInterval × ↑unitInterval), φ st ≠ w) : windingNumber (⇑p.extend) 0 1 w = windingNumber (⇑q.extend) 0 1 w

Homotopy invariance of the winding number off the curve. Two piecewise-C¹ paths with the same endpoints, joined through ℂ \ {w} by an arbitrary continuous path homotopy, have the same winding number about w. No differentiability of the homotopy is required.

theorem TauCeti.Contour.curveIntegral_inv_sub_smul_id_eq_of_pathHomotopy {x y w : ℂ} {p q : Path x y} (φ : p.Homotopy q) (hp : IsPiecewiseC1On (⇑p.extend) 0 1) (hq : IsPiecewiseC1On (⇑q.extend) 0 1) (haway : ∀ z ∈ Set.range ⇑φ, z ≠ w) : ∫ᶜ (z : ℂ) in p, (z - w)⁻¹ • ContinuousLinearMap.id ℂ ℂ = ∫ᶜ (z : ℂ) in q, (z - w)⁻¹ • ContinuousLinearMap.id ℂ ℂ

A path homotopy avoiding w preserves the curve integral of the Cauchy kernel. Two piecewise-C¹ paths with the same endpoints, joined by an arbitrary continuous homotopy through ℂ \ {w}, have equal integrals of the 1-form z ↦ (z - w)⁻¹ dz. This is the curve-integral restatement of windingNumber_eq_of_pathHomotopy.

theorem TauCeti.Contour.isNullHomologous_iff_of_pathHomotopy {x y : ℂ} {p q : Path x y} {Ω : Set ℂ} (φ : p.Homotopy q) (hp : IsPiecewiseC1On (⇑p.extend) 0 1) (hq : IsPiecewiseC1On (⇑q.extend) 0 1) (hφΩ : ∀ (st : ↑unitInterval × ↑unitInterval), φ st ∈ Ω) : IsNullHomologous (⇑p.extend) 0 1 Ω ↔ IsNullHomologous (⇑q.extend) 0 1 Ω

Null-homology in Ω is invariant under an arbitrary continuous path homotopy whose image lies in Ω. The endpoint paths themselves are piecewise C¹; no regularity is assumed of the intermediate paths.