Winding-number accounting for finitely many crossing excisions

Hungerbühler--Wasem Proposition 2.2 replaces finitely many crossing windows of a closed piecewise-C¹ immersion by circular caps. Crossing.FiniteExcision constructs a simultaneously excised curve from a supplied list of windows. This file proves the finite accounting identity

n_s(γ) = n_s(exciseCrossings γ s windows) + ∑ localContribution.

The proof partitions the curve at the window endpoints and compares the original and excised curves piece by piece. The windows must be listed in strictly increasing order: every earlier window satisfies W.upper < V.lower for every later window. Pairwise disjointness alone does not suffice for the recursive left-to-right accounting. The ordering ensures that an earlier replacement does not change a later window, so every local term is computed on the original curve.

This file does not construct windows from the actual crossings or identify their local contributions with crossing angles; those geometric steps remain downstream inputs to the full proposition.

Main results

• TauCeti.Contour.windingNumber_eq_exciseCrossings_add_sum: exact winding accounting for a finite list of cap replacements.
• TauCeti.Contour.windingNumber_eq_exciseCrossing_add: the one-window specialization.

References

• N. Hungerbühler, M. Wasem, Non-integer valued winding numbers and a generalized Residue Theorem, arXiv:1808.00997 (2018), Proposition 2.2.

Provenance

Independently reconstructed; no formalization is vendored. The ContourIntegration roadmap designates the AINTLIB LeanModularForms development (github.com/CBirkbeck/AINTLIB, Apache-2.0) as the existing source for this area. Its ForMathlib/HungerbuhlerWasem/Crossing.lean and ForMathlib/HungerbuhlerWasem/MultiCrossingCPV.lean were consulted at revision 340875a. The former supplies sector geometry and the latter a multi-crossing principal-value engine; neither contains this excise-and-cap winding-number accounting identity. The proof below instead composes Tau Ceti's finite-excision, concatenation, cap, and winding-number APIs.

theorem TauCeti.Contour.windingNumber_eq_exciseCrossings_add_sum {γ : ℝ → ℂ} {s : ℂ} {a b : ℝ} {windows : List CircularCapWindow} (hγ : IsPiecewiseC1On γ a b) (hordered : List.Pairwise (fun (W V : CircularCapWindow) => W.upper < V.lower) windows) (hinside : ∀ W ∈ windows, a < W.lower ∧ W.lower < W.upper ∧ W.upper < b) (hr : ∀ W ∈ windows, W.radius ≠ 0) (havoid : ∀ t ∈ Set.Icc a b, (∀ W ∈ windows, t ∉ Set.Ioo W.lower W.upper) → γ t ≠ s) (hpv : ∀ W ∈ windows, CauchyPVExistsAt γ W.lower W.upper (fun (z : ℂ) => (z - s)⁻¹) s) : windingNumber γ a b s = windingNumber (exciseCrossings γ s windows) a b s + (List.map (fun (W : CircularCapWindow) => W.localContribution γ s) windows).sum

Finite crossing excision decomposes the winding number. Replacing disjoint windows, listed from left to right, of a piecewise-C¹ curve by nonzero-radius circular caps changes its winding number by the sum of the local window-minus-cap contributions.

The original curve need not be closed and the windows need not contain crossings. The hypotheses state exactly what makes the surgery and the principal values well-defined: the windows lie strictly inside [a, b], the curve avoids s off their open interiors, and the Cauchy-kernel principal value exists on each window. Endpoint values do not affect this winding identity; matching endpoints are instead needed when applying the regularity results for the excised curve.

theorem TauCeti.Contour.windingNumber_eq_exciseCrossing_add {γ : ℝ → ℂ} {s : ℂ} {a b l u r θ θ' : ℝ} (hγ : IsPiecewiseC1On γ a b) (hal : a < l) (hlu : l < u) (hub : u < b) (hr : r ≠ 0) (havoid : ∀ t ∈ Set.Icc a b, t ∉ Set.Ioo l u → γ t ≠ s) (hpv : CauchyPVExistsAt γ l u (fun (z : ℂ) => (z - s)⁻¹) s) : windingNumber γ a b s = windingNumber (exciseCrossing γ s r l u θ θ') a b s + (windingNumber γ l u s - ↑(θ' - θ) / (2 * ↑Real.pi))

Excising one crossing decomposes the winding number. This is the singleton-window specialization of windingNumber_eq_exciseCrossings_add_sum. The curve need not be closed and no endpoint conditions relating it to the cap are needed, because winding numbers are insensitive to endpoint values.

theorem TauCeti.Contour.exists_int_windingNumber_eq_add_windingNumber_sub_angle_div_two_pi {γ : ℝ → ℂ} {s : ℂ} {a b l u r θ θ' : ℝ} (hγ : IsPiecewiseC1On γ a b) (hal : a < l) (hlu : l < u) (hub : u < b) (hr : r ≠ 0) (hclosed : γ a = γ b) (hθ : γ l = circleMap s r θ) (hθ' : γ u = circleMap s r θ') (havoid : ∀ t ∈ Set.Icc a b, t ∉ Set.Ioo l u → γ t ≠ s) (hpv : CauchyPVExistsAt γ l u (fun (z : ℂ) => (z - s)⁻¹) s) : ∃ (k : ℤ), windingNumber γ a b s = ↑k + (windingNumber γ l u s - ↑(θ' - θ) / (2 * ↑Real.pi))

One-window integrality consequence of crossing excision. Under the hypotheses of windingNumber_eq_exciseCrossing_add on a closed curve, its winding number is an integer plus the window's local contribution. This is not yet Hungerbühler--Wasem Proposition 2.2: that proposition also requires identifying the local contribution with the crossing angle. The witness here is the winding number of the closed, point-avoiding excised curve.