The winding decomposition of an immersed contour

This file completes Hungerbühler--Wasem Proposition 2.2. A closed piecewise-C¹ immersion meets a point s at finitely many parameter values. Provided the basepoint avoids s, we choose one common parameter radius around those crossings and then one common spatial exit radius. The corresponding first-exit windows are pairwise disjoint. Replacing each window by its circular cap produces a closed piecewise-C¹ curve avoiding s, and

n_s(γ) = n_s(excised γ) + ∑ₜ crossingAngle γ t / (2π).

The construction combines the finite-window accounting theorem in Crossing.Decomposition with the canonical equal-radius windows and their local principal-value calculation from Crossing.ExitWindow. The point-avoiding curve in the conclusion is the curve denoted \tilde{Λ} by Hungerbühler and Wasem.

Main results

• TauCeti.Contour.IsPwC1ImmersionOn.exists_crossingDecomposition -- HW Proposition 2.2, including an explicit closed, piecewise-C¹, point-avoiding excised curve.
• TauCeti.Contour.IsPwC1ImmersionOn.exists_avoiding_curve_windingNumber_eq -- curve existence form of Hungerbühler--Wasem Proposition 2.2.

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 from Tau Ceti's exit-window and finite-excision APIs. No external formalization is vendored. The ContourIntegration roadmap designates the AINTLIB LeanModularForms development (Apache-2.0) as the existing source for this area; its ForMathlib/HungerbuhlerWasem/Crossing.lean was consulted at revision 340875a for the mathematical decomposition statement.

theorem TauCeti.Contour.IsPwC1ImmersionOn.exists_crossingDecomposition {γ : ℝ → ℂ} {a b : ℝ} {s : ℂ} (h_imm : IsPwC1ImmersionOn γ a b) (hab : a < b) (hclosed : γ a = γ b) (hbase : γ a ≠ s) : ∃ (windows : List CircularCapWindow), List.Pairwise (fun (W V : CircularCapWindow) => W.upper < V.lower) windows ∧ IsPiecewiseC1On (exciseCrossings γ s windows) a b ∧ exciseCrossings γ s windows a = exciseCrossings γ s windows b ∧ (∀ t ∈ Set.Icc a b, exciseCrossings γ s windows t ≠ s) ∧ windingNumber γ a b s = windingNumber (exciseCrossings γ s windows) a b s + ↑(∑ t ∈ ⋯.toFinset, crossingAngle γ t) / (2 * ↑Real.pi)

Hungerbühler--Wasem Proposition 2.2 (winding decomposition). Let γ be a closed piecewise-C¹ immersion on [a, b], with a basepoint away from s. There is a finite ordered family of disjoint crossing windows whose circular-cap excision is again piecewise C¹, is closed, and avoids s. Its winding number accounts for the integer part of the original winding number; each crossing contributes its geometric angle divided by 2π.

The sum is indexed by the canonical finite crossing set supplied by IsPwC1ImmersionOn.finite_crossings.

theorem TauCeti.Contour.IsPwC1ImmersionOn.exists_avoiding_curve_windingNumber_eq {γ : ℝ → ℂ} {a b : ℝ} {s : ℂ} (h_imm : IsPwC1ImmersionOn γ a b) (hab : a < b) (hclosed : γ a = γ b) (hbase : γ a ≠ s) : ∃ (γ₀ : ℝ → ℂ), IsPiecewiseC1On γ₀ a b ∧ γ₀ a = γ₀ b ∧ (∀ t ∈ Set.Icc a b, γ₀ t ≠ s) ∧ windingNumber γ a b s = windingNumber γ₀ a b s + ↑(∑ t ∈ ⋯.toFinset, crossingAngle γ t) / (2 * ↑Real.pi)

Hungerbühler--Wasem Proposition 2.2 (winding decomposition, curve existence form). For a closed piecewise-C¹ immersion γ based away from s, there exists an avoiding closed piecewise-C¹ curve γ₀ whose winding number differs from γ's by the canonical finite sum of crossing angles divided by 2π.