Single-Crossing Winding Number Framework

Unified framework for computing generalizedWindingNumber' γ a b s when the curve γ crosses the point s at exactly one parameter value t₀ ∈ (a, b).

Overview

The three edge/arc winding proofs (RightEdge, LeftEdge, UnitArc) share a common 5-step structure:

1. Identify the unique crossing parameter t₀
2. Define a cutoff function δ(ε) that maps the norm threshold ε to a parameter-space interval radius around t₀
3. Prove far/near bounds: curve is ε-far from s outside [t₀-δ, t₀+δ], and ε-close inside
4. Prove the FTC telescope: the far-segment integrals sum to some E(ε)
5. Prove E(ε) → L as ε → 0⁺, giving gWN = L / (2πi)

This file provides:

• SingleCrossingData: a structure bundling all geometric ingredients
• gWN_of_singleCrossing: the master theorem that assembles these ingredients into a generalizedWindingNumber' computation
• gWN_eq_neg_half_of_singleCrossing: specialized version for gWN = -1/2

Design

The key abstraction is that pv_tendsto_of_crossing_limit already handles steps 3-5 at the level of the PV integral. This framework adds the final conversion from PV Tendsto to generalizedWindingNumber', handling the deriv (fun t => γ t - s) = deriv γ rewrite that every caller must perform.

The SingleCrossingData structure bundles the 8 obligations of pv_tendsto_of_crossing_limit together with a target limit value, making it easy to instantiate for each geometric case.

structure SingleCrossingData (γ : ℝ → ℂ) (a b : ℝ) (s : ℂ) : Type

Data for a single-crossing winding number computation.

Bundles all the geometric ingredients needed by pv_tendsto_of_crossing_limit:

• A curve γ : ℝ → ℂ on [a, b] with a unique crossing at t₀
• A cutoff function δ : ℝ → ℝ mapping norm thresholds to parameter radii
• A threshold below which all bounds hold
• The far/near bounds, FTC telescope, integrability, and limit target

• L : ℂ

  Target limit value for the PV integral.

• t₀ : ℝ

  Unique crossing parameter in (a, b).

• ht₀ : self.t₀ ∈ Set.Ioo a b

  Proof that t₀ ∈ (a, b).

• δ : ℝ → ℝ

  Cutoff function: maps norm threshold ε to parameter-space radius.

• threshold : ℝ

  Threshold below which all bounds hold.

• hthresh : 0 < self.threshold

  Threshold is positive.

• hδ_pos (ε : ℝ) : 0 < ε → ε < self.threshold → 0 < self.δ ε

  δ(ε) is positive for valid ε.

• hδ_small (ε : ℝ) : 0 < ε → ε < self.threshold → self.δ ε < min (self.t₀ - a) (b - self.t₀)

  δ(ε) is small enough: stays within (a, b) around t₀.

• h_far (ε : ℝ) : 0 < ε → ε < self.threshold → ∀ t ∈ Set.Icc a b, self.δ ε < |t - self.t₀| → ε < ‖γ t - s‖

  Far bound: curve is ε-far from s outside the δ-neighborhood of t₀.

• h_near (ε : ℝ) : 0 < ε → ε < self.threshold → ∀ (t : ℝ), |t - self.t₀| ≤ self.δ ε → ‖γ t - s‖ ≤ ε

  Near bound: curve is within ε of s inside the δ-neighborhood.

• E : ℝ → ℂ

  Expression that the far-segment integrals sum to.

• h_ftc (ε : ℝ) : 0 < ε → ε < self.threshold → (∫ (t : ℝ) in a..self.t₀ - self.δ ε, (γ t - s)⁻¹ * deriv γ t) + ∫ (t : ℝ) in self.t₀ + self.δ ε..b, (γ t - s)⁻¹ * deriv γ t = self.E ε

  FTC telescope: far-segment integrals equal E(ε).

• hint_left (ε : ℝ) : 0 < ε → ε < self.threshold → IntervalIntegrable (fun (t : ℝ) => (γ t - s)⁻¹ * deriv γ t) MeasureTheory.volume a (self.t₀ - self.δ ε)

  Integrability on the left segment.

• hint_right (ε : ℝ) : 0 < ε → ε < self.threshold → IntervalIntegrable (fun (t : ℝ) => (γ t - s)⁻¹ * deriv γ t) MeasureTheory.volume (self.t₀ + self.δ ε) b

  Integrability on the right segment.

• h_limit : Filter.Tendsto self.E (nhdsWithin 0 (Set.Ioi 0)) (nhds self.L)

  Limit: E(ε) → L as ε → 0⁺.

theorem SingleCrossingData.pvTendsto {γ : ℝ → ℂ} {a b : ℝ} {s : ℂ} (D : SingleCrossingData γ a b s) : Filter.Tendsto (fun (ε : ℝ) => ∫ (t : ℝ) in a..b, if ‖γ t - s‖ > ε then (γ t - s)⁻¹ * deriv γ t else 0) (nhdsWithin 0 (Set.Ioi 0)) (nhds D.L)

The PV integral of (γ - s)⁻¹ · γ' tends to L. This is the core intermediate result, obtained directly from pv_tendsto_of_crossing_limit.

theorem gWN_of_singleCrossing {γ : ℝ → ℂ} {a b : ℝ} {s : ℂ} (D : SingleCrossingData γ a b s) : generalizedWindingNumber' γ a b s = D.L / (2 * ↑Real.pi * Complex.I)

Master theorem: compute generalizedWindingNumber' from single-crossing data.

Given SingleCrossingData for curve γ, the generalized winding number at s equals L / (2πi).

This handles the conversion from (γ t - s)⁻¹ * deriv γ t (used in the PV integral) to the form (γ t - s)⁻¹ * deriv (fun t => γ t - s) t expected by generalizedWindingNumber'.

theorem gWN_eq_neg_half_of_singleCrossing {γ : ℝ → ℂ} {a b : ℝ} {s : ℂ} (D : SingleCrossingData γ a b s) (hL : D.L = -(↑Real.pi * Complex.I)) : generalizedWindingNumber' γ a b s = -1 / 2

Specialized version: if L = -(π * I), then gWN = -1/2.

This is the most common case, used by RightEdge, LeftEdge, and UnitArc.

theorem gWN_eq_neg_sixth_of_singleCrossing {γ : ℝ → ℂ} {a b : ℝ} {s : ℂ} (D : SingleCrossingData γ a b s) (hL : D.L = -(↑Real.pi / 3 * Complex.I)) : generalizedWindingNumber' γ a b s = -1 / 6

Specialized version: if L = -(π / 3 * I), then gWN = -1/6.

Used for elliptic point winding number computations.