Winding Number: H-W Decomposition Theorems

The main decomposition results for generalized winding numbers, showing how the winding number splits into an external integer winding contribution and crossing angle contributions.

Main Results

• exp_pv_eq_exp_neg_crossing_angle — FTC + direction limit for CPV
• externalWindingContribution_isInt — external winding is an integer
• generalizedWindingNumber_eq_external_sub_angle — H-W Prop 2.2 decomposition
• generalizedWindingNumber_eq_neg_angleContribution_single — N=0 specialization
• generalizedWindingNumber_eq_neg_half_smooth_crossing — smooth crossing gives -1/2
• windingNumberWithAngles_union — additivity over disjoint crossings

theorem exp_pv_eq_exp_neg_crossing_angle (γ : PiecewiseC1Immersion) (hclosed : γ.IsClosed) (z₀ : ℂ) (t₀ : ℝ) (ht₀ : t₀ ∈ Set.Ioo γ.a γ.b) (hcross : γ.toFun t₀ = z₀) (honly : ∀ t ∈ Set.Icc γ.a γ.b, γ.toFun t = z₀ → t = t₀) (hγ_meas : Measurable γ.toFun) (hC2 : ContDiffAt ℝ 2 γ.toFun t₀) (h_cont_deriv : ∃ (a' : ℝ) (b' : ℝ), t₀ ∈ Set.Ioo a' b' ∧ Set.Icc a' b' ⊆ Set.Icc γ.a γ.b ∧ ContinuousOn (deriv γ.toFun) (Set.Icc a' b')) : Complex.exp (cauchyPrincipalValue' (fun (x : ℂ) => x⁻¹) (fun (t : ℝ) => γ.toFun t - z₀) γ.a γ.b 0) = Complex.exp (-(Complex.I * ↑(angleAtCrossing γ t₀ ht₀)))

FTC + direction limit: For a closed piecewise C¹ immersion with unique crossing at t₀ through z₀, the exponential of the Cauchy PV integral equals exp(-i · α) where α is the crossing angle.

Proved by combining:

• PV existence (cpv_exists_inv_sub)
• Continuity of exp composed with the PV limit
• The core analysis (tendsto_exp_cutoff_integral_crossing)
• Uniqueness of limits in a T₂ space

theorem externalWindingContribution_isInt (γ : PiecewiseC1Immersion) (hclosed : γ.IsClosed) (z₀ : ℂ) (t₀ : ℝ) (ht₀ : t₀ ∈ Set.Ioo γ.a γ.b) (hcross : γ.toFun t₀ = z₀) (honly : ∀ t ∈ Set.Icc γ.a γ.b, γ.toFun t = z₀ → t = t₀) (hγ_meas : Measurable γ.toFun) (hC2 : ContDiffAt ℝ 2 γ.toFun t₀) (h_cont_deriv : ∃ (a' : ℝ) (b' : ℝ), t₀ ∈ Set.Ioo a' b' ∧ Set.Icc a' b' ⊆ Set.Icc γ.a γ.b ∧ ContinuousOn (deriv γ.toFun) (Set.Icc a' b')) : ∃ (N : ℤ), externalWindingContribution γ z₀ t₀ ht₀ = ↑N

The external winding contribution is always an integer. This is the key structural result from H-W Proposition 2.2: the generalized winding number decomposes as N - α/(2π) where α is the crossing angle and N ∈ ℤ is the classical winding of the modified curve.

The regularity hypotheses (hγ_meas, hC2, h_cont_deriv) ensure that the Cauchy PV integral of 1/(z-z₀) converges, so the generalized winding number is well-defined (not the default value 0).

theorem generalizedWindingNumber_eq_external_sub_angle (γ : PiecewiseC1Immersion) (z₀ : ℂ) (t₀ : ℝ) (ht₀ : t₀ ∈ Set.Ioo γ.a γ.b) : generalizedWindingNumber' γ.toFun γ.a γ.b z₀ = externalWindingContribution γ z₀ t₀ ht₀ - ↑(angleAtCrossing γ t₀ ht₀) / (2 * ↑Real.pi)

H-W Proposition 2.2: The generalized winding number decomposes as the external winding integer minus the crossing angle contribution. n_{z₀}(γ) = N - α/(2π) where N is the external winding.

theorem generalizedWindingNumber_eq_neg_angleContribution_single (γ : PiecewiseC1Immersion) (_hclosed : γ.IsClosed) (z₀ : ℂ) (t₀ : ℝ) (ht₀ : t₀ ∈ Set.Ioo γ.a γ.b) (_hcross : γ.toFun t₀ = z₀) (_honly : ∀ t ∈ Set.Icc γ.a γ.b, γ.toFun t = z₀ → t = t₀) (h_external : externalWindingContribution γ z₀ t₀ ht₀ = 0) : generalizedWindingNumber' γ.toFun γ.a γ.b z₀ = -(↑(angleAtCrossing γ t₀ ht₀) / (2 * ↑Real.pi))

H-W Proposition 2.3 (specialized): For a closed piecewise C¹ immersion passing through z₀ exactly once at t₀, with zero external winding, the generalized winding number equals minus the crossing angle divided by 2π.

theorem generalizedWindingNumber_eq_neg_half_smooth_crossing (γ : PiecewiseC1Immersion) (hclosed : γ.IsClosed) (z₀ : ℂ) (t₀ : ℝ) (ht₀ : t₀ ∈ Set.Ioo γ.a γ.b) (hcross : γ.toFun t₀ = z₀) (honly : ∀ t ∈ Set.Icc γ.a γ.b, γ.toFun t = z₀ → t = t₀) (hsmooth : t₀ ∉ γ.partition) (h_external : externalWindingContribution γ z₀ t₀ ht₀ = 0) : generalizedWindingNumber' γ.toFun γ.a γ.b z₀ = -(1 / 2)

At a smooth crossing with zero external winding, contribution is -1/2.

theorem generalizedWindingNumber_eq_neg_corner_contribution (γ : PiecewiseC1Immersion) (hclosed : γ.IsClosed) (z₀ : ℂ) (t₀ α : ℝ) (ht₀ : t₀ ∈ Set.Ioo γ.a γ.b) (hcross : γ.toFun t₀ = z₀) (honly : ∀ t ∈ Set.Icc γ.a γ.b, γ.toFun t = z₀ → t = t₀) (hangle : angleAtCrossing γ t₀ ht₀ = α) (h_external : externalWindingContribution γ z₀ t₀ ht₀ = 0) : generalizedWindingNumber' γ.toFun γ.a γ.b z₀ = -(↑α / (2 * ↑Real.pi))

At a corner crossing with angle α and zero external winding, contribution is -α/(2π).

theorem externalWindingContribution_zero_of_windingNumber_eq (γ : PiecewiseC1Immersion) (z₀ : ℂ) (t₀ : ℝ) (ht₀ : t₀ ∈ Set.Ioo γ.a γ.b) (h_eq : generalizedWindingNumber' γ.toFun γ.a γ.b z₀ = -(↑(angleAtCrossing γ t₀ ht₀) / (2 * ↑Real.pi))) : externalWindingContribution γ z₀ t₀ ht₀ = 0

The external winding contribution vanishes when a curve with the same winding number has zero external winding. This lets you prove the external winding is zero by exhibiting a homotopy to a "model" curve (e.g., a sector curve) whose winding number equals -α/(2π).

theorem externalWindingContribution_translate (γ : PiecewiseC1Immersion) (c : ℂ) (t₀ : ℝ) (ht₀ : t₀ ∈ Set.Ioo γ.a γ.b) (z₀ : ℂ) : externalWindingContribution (γ.translate c) (z₀ + c) t₀ ht₀ = externalWindingContribution γ z₀ t₀ ht₀

The external winding contribution is translation-invariant.

theorem windingNumberWithAngles_union (γ : PiecewiseC1Immersion) (z₀ : ℂ) (S T : Finset ℝ) (hST : Disjoint S T) (hS_in : ∀ t ∈ S, t ∈ Set.Ioo γ.a γ.b) (hT_in : ∀ t ∈ T, t ∈ Set.Ioo γ.a γ.b) (hS_at : ∀ t ∈ S, γ.toFun t = z₀) (hT_at : ∀ t ∈ T, γ.toFun t = z₀) : windingNumberWithAngles' γ z₀ (S ∪ T) ⋯ ⋯ = windingNumberWithAngles' γ z₀ S hS_in hS_at + windingNumberWithAngles' γ z₀ T hT_in hT_at

Winding number with angles is additive over disjoint crossing sets.