Orientation reversal for contour winding numbers

This file records the basic orientation-reversal API for the generalized winding number. Reversing the interval orientation negates the single-point Cauchy principal value defining Contour.windingNumber, so the winding number itself changes sign.

These lemmas are bookkeeping for the roadmap's curve and cycle layer. Cycles are oriented formal combinations of curves, and finite decompositions of curves into avoiding pieces and model sectors need both concatenation and orientation reversal.

Main results

• Contour.windingNumber_symm — the generalized winding number changes sign when the interval is reversed.
• Contour.IsNullHomologous.symm, Contour.IsNullHomologous.symm_of_avoidance — null-homology is preserved by reversing orientation, under the same honest principal-value existence hypotheses used elsewhere in the winding-number API.

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_symm {γ : ℝ → ℂ} {a b : ℝ} {z₀ : ℂ} (h : CauchyPVExistsAt γ a b (fun (w : ℂ) => (w - z₀)⁻¹) z₀) : windingNumber γ b a z₀ = -windingNumber γ a b z₀

The generalized winding number changes sign when the interval orientation is reversed, provided the principal value defining the original winding number exists.

theorem TauCeti.Contour.windingNumber_eq_zero_symm {γ : ℝ → ℂ} {a b : ℝ} {z₀ : ℂ} (hzero : windingNumber γ a b z₀ = 0) (hpv : CauchyPVExistsAt γ a b (fun (w : ℂ) => (w - z₀)⁻¹) z₀) : windingNumber γ b a z₀ = 0

Pointwise vanishing of a winding number is preserved by reversing the interval orientation, under the principal-value existence hypothesis that makes the two winding-number values honest.

theorem TauCeti.Contour.IsNullHomologous.symm {γ : ℝ → ℂ} {a b : ℝ} {Ω : Set ℂ} (h : IsNullHomologous γ a b Ω) (hpv : ∀ z ∉ Ω, CauchyPVExistsAt γ a b (fun (w : ℂ) => (w - z)⁻¹) z) : IsNullHomologous γ b a Ω

Null-homology is preserved by reversing orientation, provided the pointwise principal values defining the exterior winding numbers exist.

theorem TauCeti.Contour.IsNullHomologous.symm_of_avoidance {γ : ℝ → ℂ} {a b : ℝ} {Ω : Set ℂ} (h : IsNullHomologous γ a b Ω) (hγ : ∀ t ∈ Set.uIcc a b, γ t ∈ Ω) (hcont : ContinuousOn γ (Set.uIcc a b)) (hint : ∀ z ∉ Ω, IntervalIntegrable (fun (t : ℝ) => (γ t - z)⁻¹ * deriv γ t) MeasureTheory.volume a b) : IsNullHomologous γ b a Ω

Null-homology is preserved by reversing orientation in the ordinary avoided-pole case. If the curve lies in Ω, every exterior point is avoided, so the required principal values are ordinary integrals.