Winding Number: Crossing Analysis

Technical analysis of curve crossings for generalized winding numbers. Contains the core monotonicity, cutoff boundary, and direction convergence lemmas.

Main Results

• piecewiseC1Immersion_norm_strictMono_near_crossing — local monotonicity at crossings
• exists_cutoff_boundary_times — existence of cutoff boundary times
• exp_cutoff_integral_eq_ratio — exponential of cutoff integral equals direction ratio
• crossing_ratio_tendsto — direction convergence as ε → 0
• tendsto_exp_cutoff_integral_crossing — exp(R(ε)) → exp(-iα)

theorem piecewiseC1Immersion_norm_strictMono_near_crossing (γ : PiecewiseC1Immersion) (z₀ : ℂ) (t₀ : ℝ) (ht₀ : t₀ ∈ Set.Ioo γ.a γ.b) (hcross : γ.toFun t₀ = z₀) : ∃ (l : ℝ) (r : ℝ), l < t₀ ∧ t₀ < r ∧ γ.a ≤ l ∧ r ≤ γ.b ∧ StrictAntiOn (fun (t : ℝ) => ‖γ.toFun t - z₀‖) (Set.Icc l t₀) ∧ StrictMonoOn (fun (t : ℝ) => ‖γ.toFun t - z₀‖) (Set.Icc t₀ r)

Helper: g = ‖γ(·) - z₀‖ is strictly decreasing on a left neighborhood of t₀ and strictly increasing on a right neighborhood, when γ is an immersion at t₀. This is the key "local monotonicity" fact that makes the cutoff boundary well-defined.

theorem exists_cutoff_boundary_times (γ : PiecewiseC1Immersion) (z₀ : ℂ) (t₀ : ℝ) (ht₀ : t₀ ∈ Set.Ioo γ.a γ.b) (hcross : γ.toFun t₀ = z₀) (honly : ∀ t ∈ Set.Icc γ.a γ.b, γ.toFun t = z₀ → t = t₀) : ∃ δ > 0, ∀ ε ∈ Set.Ioo 0 δ, ∃ (σ₁ : ℝ) (σ₂ : ℝ), γ.a ≤ σ₁ ∧ σ₁ < t₀ ∧ t₀ < σ₂ ∧ σ₂ ≤ γ.b ∧ ‖γ.toFun σ₁ - z₀‖ = ε ∧ ‖γ.toFun σ₂ - z₀‖ = ε ∧ (∀ t ∈ Set.Ico γ.a σ₁, ε < ‖γ.toFun t - z₀‖) ∧ (∀ t ∈ Set.Ioc σ₂ γ.b, ε < ‖γ.toFun t - z₀‖) ∧ ∀ t ∈ Set.Icc σ₁ σ₂, ‖γ.toFun t - z₀‖ ≤ ε

theorem exists_cutoff_boundary_times_with_mono (γ : PiecewiseC1Immersion) (z₀ : ℂ) (t₀ : ℝ) (ht₀ : t₀ ∈ Set.Ioo γ.a γ.b) (hcross : γ.toFun t₀ = z₀) (honly : ∀ t ∈ Set.Icc γ.a γ.b, γ.toFun t = z₀ → t = t₀) : ∃ δ > 0, ∃ (l : ℝ) (r : ℝ), l < t₀ ∧ t₀ < r ∧ γ.a ≤ l ∧ r ≤ γ.b ∧ StrictAntiOn (fun (t : ℝ) => ‖γ.toFun t - z₀‖) (Set.Icc l t₀) ∧ StrictMonoOn (fun (t : ℝ) => ‖γ.toFun t - z₀‖) (Set.Icc t₀ r) ∧ δ ≤ ‖γ.toFun l - z₀‖ ∧ δ ≤ ‖γ.toFun r - z₀‖ ∧ ∀ ε ∈ Set.Ioo 0 δ, ∃ (σ₁ : ℝ) (σ₂ : ℝ), γ.a ≤ σ₁ ∧ σ₁ < t₀ ∧ t₀ < σ₂ ∧ σ₂ ≤ γ.b ∧ ‖γ.toFun σ₁ - z₀‖ = ε ∧ ‖γ.toFun σ₂ - z₀‖ = ε ∧ (∀ t ∈ Set.Ico γ.a σ₁, ε < ‖γ.toFun t - z₀‖) ∧ (∀ t ∈ Set.Ioc σ₂ γ.b, ε < ‖γ.toFun t - z₀‖) ∧ ∀ t ∈ Set.Icc σ₁ σ₂, ‖γ.toFun t - z₀‖ ≤ ε

Extended version of exists_cutoff_boundary_times that also exposes the strict monotonicity interval and the bounds δ ≤ ‖γ(l) - z₀‖, δ ≤ ‖γ(r) - z₀‖.

theorem exp_cutoff_integral_eq_ratio (γ : PiecewiseC1Immersion) (hclosed : γ.IsClosed) (z₀ : ℂ) (σ₁ σ₂ ε : ℝ) (hσ₁ : γ.a ≤ σ₁) (hσ₁₂ : σ₁ < σ₂) (hσ₂ : σ₂ ≤ γ.b) (hε : 0 < ε) (hσ₁_val : ‖γ.toFun σ₁ - z₀‖ = ε) (hσ₂_val : ‖γ.toFun σ₂ - z₀‖ = ε) (h_left : ∀ t ∈ Set.Ico γ.a σ₁, ε < ‖γ.toFun t - z₀‖) (h_right : ∀ t ∈ Set.Ioc σ₂ γ.b, ε < ‖γ.toFun t - z₀‖) (h_middle : ∀ t ∈ Set.Icc σ₁ σ₂, ‖γ.toFun t - z₀‖ ≤ ε) : Complex.exp (∫ (t : ℝ) in γ.a..γ.b, if ‖γ.toFun t - z₀‖ > ε then (γ.toFun t - z₀)⁻¹ * deriv γ.toFun t else 0) = (γ.toFun σ₁ - z₀) / (γ.toFun σ₂ - z₀)

For a closed piecewise C¹ immersion, when the cutoff integral is split at boundary times where ‖γ-z₀‖ = ε with strict inequality outside, the exponential equals the ratio (γ(σ₁)-z₀)/(γ(σ₂)-z₀) by FTC + closedness.

theorem crossing_ratio_tendsto (γ : PiecewiseC1Immersion) (z₀ : ℂ) (t₀ : ℝ) (ht₀ : t₀ ∈ Set.Ioo γ.a γ.b) (hcross : γ.toFun t₀ = z₀) (honly : ∀ t ∈ Set.Icc γ.a γ.b, γ.toFun t = z₀ → t = t₀) (σ₁ σ₂ : ℝ → ℝ) (hσ₁_lt : ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), σ₁ ε < t₀) (hσ₂_gt : ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), t₀ < σ₂ ε) (hσ₁_val : ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), ‖γ.toFun (σ₁ ε) - z₀‖ = ε) (hσ₂_val : ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), ‖γ.toFun (σ₂ ε) - z₀‖ = ε) (hσ₁_in : ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), γ.a ≤ σ₁ ε) (hσ₂_in : ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), σ₂ ε ≤ γ.b) : Filter.Tendsto (fun (ε : ℝ) => (γ.toFun (σ₁ ε) - z₀) / (γ.toFun (σ₂ ε) - z₀)) (nhdsWithin 0 (Set.Ioi 0)) (nhds (Complex.exp (-(Complex.I * ↑(angleAtCrossing γ t₀ ht₀)))))

Direction convergence: as ε → 0, the ratio (γ(σ₁(ε))-z₀)/(γ(σ₂(ε))-z₀) (where σ₁(ε), σ₂(ε) are the boundary times from exists_cutoff_boundary_times) converges to exp(-i·angleAtCrossing). This follows from the immersion property: γ(σ₁)-z₀ ≈ L_left·(σ₁-t₀) with σ₁-t₀ < 0, so direction → -L_left/|L_left|, and γ(σ₂)-z₀ ≈ L_right·(σ₂-t₀) with σ₂-t₀ > 0, so direction → L_right/|L_right|. The ratio of directions is exp(-i·α) where α = arg(L_right) - arg(-L_left).

theorem tendsto_exp_cutoff_integral_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₀) : Filter.Tendsto (fun (ε : ℝ) => Complex.exp (∫ (t : ℝ) in γ.a..γ.b, if ‖γ.toFun t - z₀‖ > ε then (γ.toFun t - z₀)⁻¹ * deriv γ.toFun t else 0)) (nhdsWithin 0 (Set.Ioi 0)) (nhds (Complex.exp (-(Complex.I * ↑(angleAtCrossing γ t₀ ht₀)))))

Core analysis: exp(R(ε)) → exp(-iα) as ε → 0, where R(ε) is the cutoff integral ∫ 1_{‖γ-z₀‖>ε} (γ-z₀)⁻¹ γ' and α is the crossing angle.

Proof strategy (H-W Proposition 2.2):

1. For each small ε, the set {t : ‖γ(t)-z₀‖ ≤ ε} is a single interval (σ₁(ε), σ₂(ε)) containing t₀ (by continuity + isolated crossing).
2. By piecewise FTC on segments where ‖γ-z₀‖ > ε (using the G-function technique from exp_integral_eq_endpoint_ratio_piecewise): exp(R(ε)) = (γ(σ₁)-z₀)/(γ(a)-z₀) · (γ(b)-z₀)/(γ(σ₂)-z₀).
3. By closedness γ(a) = γ(b): exp(R(ε)) = (γ(σ₁)-z₀)/(γ(σ₂)-z₀).
4. Since ‖γ(σ₁)-z₀‖ = ε = ‖γ(σ₂)-z₀‖, this ratio has modulus 1.
5. By the immersion property: as ε → 0, σ₁ → t₀⁻ and σ₂ → t₀⁺, and arg(γ(σ₁)-z₀) → arg(-L_left), arg(γ(σ₂)-z₀) → arg(L_right).
6. Therefore exp(R(ε)) → exp(i(arg(-L_left) - arg(L_right))) = exp(-iα).