Translation invariance for contour winding numbers

This file records the basic translation-invariance API for the generalized winding number. Translating both the curve and the distinguished point by the same complex number leaves the index principal value unchanged, so the winding number and null-homology are invariant.

These lemmas are bookkeeping for the roadmap's curve and cycle layer. The geometry of the generalized winding number is local at a crossing or sector, and finite-decomposition arguments frequently translate the crossing point to the origin before applying the model computation.

Main results

• Contour.windingNumber_translate — translating the curve and base point together preserves the generalized winding number.
• Contour.IsNullHomologous.translate — null-homology is preserved by translating both the curve and the ambient set.

Provenance

This is routine API around the Hungerbühler--Wasem generalized winding number from the contour integration roadmap; no formal source is vendored.

theorem TauCeti.Contour.windingNumber_translate {γ : ℝ → ℂ} {a b : ℝ} {z₀ : ℂ} (c : ℂ) : windingNumber (fun (t : ℝ) => γ t + c) a b (z₀ + c) = windingNumber γ a b z₀

The generalized winding number is invariant under simultaneous translation of the curve and the base point.

theorem TauCeti.Contour.IsNullHomologous.translate {γ : ℝ → ℂ} {a b : ℝ} {Ω : Set ℂ} (h : IsNullHomologous γ a b Ω) (c : ℂ) : IsNullHomologous (fun (t : ℝ) => γ t + c) a b ((fun (z : ℂ) => z + c) '' Ω)

Null-homology is preserved by translating the curve and the ambient set together.