Excising a crossing window and capping it with a circular arc

Hungerbühler–Wasem Proposition 2.2 decomposes a closed piecewise-C¹ immersion Λ that meets a point s finitely often as Λ = \tilde{\Lambda} + Γ₁ + ⋯ + Γₙ, where \tilde{\Lambda} avoids s and each Γ_ℓ is a local loop at a crossing, and concludes n_s(Λ) = n_s(\tilde{\Lambda}) + ∑_ℓ α_ℓ / 2π. The identity modulo an integer is TauCeti.Contour.IsPwC1ImmersionOn.exists_int_windingNumber_eq_add_sum_crossingAngle, whose integer is produced abstractly because the surgered curve \tilde{\Lambda} is never built. This file builds it.

The surgery is the obvious one. A parameter window [l, u] containing the crossing is chosen so that the curve sits on the circle |z - s| = |r| at both ends, γ l = circleMap s r θ and γ u = circleMap s r θ'. The window is then deleted and replaced by the arc of that circle running from angle θ to angle θ' (TauCeti.Contour.circleCap), giving exciseCrossing γ s r l u θ θ', a curve that agrees with γ outside the window. Each further property it has comes with its own hypotheses:

• it is again piecewise C¹ on [a, b] (IsPiecewiseC1On.exciseCrossing) provided γ is and the window sits strictly inside with a < l < u < b, the two endpoint conditions being what glues the cap to γ;
• it is again closed (exciseCrossing_closed) provided γ a = γ b and the window misses the two endpoints, a < l and u < b;
• and — this is the point — it avoids s (exciseCrossing_ne_center) provided the signed radial scale is nonzero, r ≠ 0, and γ itself meets s only strictly inside the window.

Under all of these together its winding number about s is an integer.

Crossing.Decomposition builds on this surgery to prove the exact finite-window winding-number accounting identity and its one-window specialization.

What remains of HW Proposition 2.2 is the identification of the local contribution with the crossing angle α_ℓ / 2π for a general immersion. It is congruent to α_ℓ / 2π modulo 1 — that is exactly the content of the modulo-an-integer theorem cited above — and the outstanding step is the estimate that pins the representative, namely that the local loop over a small enough window winds less than once.

Main definitions

• TauCeti.Contour.circleCap — for a nondegenerate window l ≠ u, the arc with signed radial scale r about s sweeping from angle θ to angle θ', parametrised affinely over [l, u]; when l = u the affine change of parameter degenerates and the arc is constantly circleMap s r θ.
• TauCeti.Contour.exciseCrossing — the curve γ with the window [l, u] replaced by that cap.

Main results

• TauCeti.Contour.windingNumber_circleCap — the cap has winding number (θ' - θ) / 2π about s.
• TauCeti.Contour.IsPiecewiseC1On.exciseCrossing — the excised curve is piecewise C¹, TauCeti.Contour.exciseCrossing_closed — it is closed if γ is, and TauCeti.Contour.exciseCrossing_ne_center — it avoids s.

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, and assigns LeanModularForms/ForMathlib/HungerbuhlerWasem/Crossing.lean to "Prop 2.2 / sector geometry". That file was consulted and carries no excise-and-cap construction: at revision 340875a it is the per-pole principal-value composition (HasCauchyPV.add, HasCauchyPV.finset_sum, cpv_polarPart_at_pole_under_conditions) together with the crossing angle-compatibility lemmas, and the surgered curve \tilde{Λ} is never built there either. The one place AINTLIB names this excision, ForMathlib/ExitTime.lean, constructs only the exit-time parameters bounding the window (firstExitTimeLeft, firstExitTimeRight), not the spliced curve. So the definitions and proofs below are new, assembled from Tau Ceti's existing winding-number API for reparametrisation and circles.

References

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

The circular cap

noncomputable def TauCeti.Contour.circleCap (s : ℂ) (r l u θ θ' : ℝ) : ℝ → ℂ

The circular cap with signed radial scale r about s: the arc of the circle |z - s| = |r| parametrised affinely over the window [l, u], running from angle θ at l (circleCap_left) to angle θ' at u (circleCap_right) whenever the window is nondegenerate, l ≠ u. For l = u the affine change of parameter divides by zero, so the cap is constantly circleMap s r θ and does not reach angle θ'; every result below that needs the far endpoint assumes l < u or l ≠ u.

It is written as circleMap s r precomposed with an affine change of parameter, which is the shape the reparametrisation and principal-value lemmas for circular arcs consume.

Equations

• TauCeti.Contour.circleCap s r l u θ θ' = circleMap s r ∘ fun (t : ℝ) => (θ' - θ) / (u - l) * t + (θ - (θ' - θ) / (u - l) * l)

theorem TauCeti.Contour.circleCap_apply (s : ℂ) (r l u θ θ' t : ℝ) : circleCap s r l u θ θ' t = circleMap s r (θ + (θ' - θ) / (u - l) * (t - l))

Characteristic value lemma for the circular cap: at parameter t it is the point of the circle at angle θ advanced by the fraction (t - l) / (u - l) of the sweep θ' - θ.

Deliberately not @[simp]: it rewrites the left-hand sides of the endpoint lemmas circleCap_left and circleCap_right, which are the simp-normal forms this file's consumers actually meet.

@[simp]

theorem TauCeti.Contour.circleCap_left (s : ℂ) (r l u θ θ' : ℝ) : circleCap s r l u θ θ' l = circleMap s r θ

The cap starts at the point of angle θ.

@[simp]

theorem TauCeti.Contour.circleCap_right {l u : ℝ} (s : ℂ) (r : ℝ) (hlu : l ≠ u) (θ θ' : ℝ) : circleCap s r l u θ θ' u = circleMap s r θ'

The cap ends at the point of angle θ', the window being nondegenerate.

theorem TauCeti.Contour.contDiff_circleCap (s : ℂ) (r l u θ θ' : ℝ) : ContDiff ℝ 1 (circleCap s r l u θ θ')

The cap is C¹ (indeed smooth): the circle map is, and the change of parameter is affine.

theorem TauCeti.Contour.circleCap_ne_center {s : ℂ} {l u r θ θ' t : ℝ} (hr : r ≠ 0) : circleCap s r l u θ θ' t ≠ s

The cap misses the centre when its signed radial scale is nonzero.

theorem TauCeti.Contour.cauchyPVExistsAt_circleCap (s : ℂ) (r l u θ θ' a b : ℝ) : CauchyPVExistsAt (circleCap s r l u θ θ') a b (fun (z : ℂ) => (z - s)⁻¹) s

The index principal value along the cap exists, the cap being an affinely reparametrised circular arc.

theorem TauCeti.Contour.windingNumber_circleCap {s : ℂ} {l u r : ℝ} (hr : r ≠ 0) (hlu : l ≠ u) (θ θ' : ℝ) : windingNumber (circleCap s r l u θ θ') l u s = ↑(θ' - θ) / (2 * ↑Real.pi)

The winding number of the cap is its angular extent over 2π. The arc misses s, so the principal value collapses to the ordinary index integral, and the affine change of parameter carries [l, u] onto [θ, θ'].

The excised curve

noncomputable def TauCeti.Contour.exciseCrossing (γ : ℝ → ℂ) (s : ℂ) (r l u θ θ' : ℝ) : ℝ → ℂ

The excised curve: γ with the parameter window [l, u] deleted and replaced by the circular cap with signed radial scale r about s running from angle θ to angle θ'. This is the curve HW Proposition 2.2 calls \tilde{\Lambda}.

The definition itself assumes nothing; the properties that make it a surgery each need hypotheses. If γ is continuous (indeed piecewise C¹) on [a, b], the window is nondegenerate and strictly inside, a < l < u < b, and the two endpoint conditions γ l = circleMap s r θ and γ u = circleMap s r θ' hold, then the replacement glues continuously and the result is again piecewise C¹ (IsPiecewiseC1On.exciseCrossing). If moreover γ a = γ b it is again closed (exciseCrossing_closed). And if the signed radial scale is nonzero, r ≠ 0, and γ meets s only inside the open window, then the excised curve misses s altogether (exciseCrossing_ne_center).

Equations

• TauCeti.Contour.exciseCrossing γ s r l u θ θ' t = if l ≤ t ∧ t ≤ u then TauCeti.Contour.circleCap s r l u θ θ' t else γ t

@[simp]

theorem TauCeti.Contour.exciseCrossing_of_mem {γ : ℝ → ℂ} {s : ℂ} {l u r θ θ' t : ℝ} (ht : t ∈ Set.Icc l u) : exciseCrossing γ s r l u θ θ' t = circleCap s r l u θ θ' t

Characteristic value lemma inside the window: there the excised curve is the cap.

@[simp]

theorem TauCeti.Contour.exciseCrossing_of_notMem {γ : ℝ → ℂ} {s : ℂ} {l u r θ θ' t : ℝ} (ht : t ∉ Set.Icc l u) : exciseCrossing γ s r l u θ θ' t = γ t

Characteristic value lemma outside the window: there the excised curve is γ.

theorem TauCeti.Contour.exciseCrossing_eqOn_Iic {γ : ℝ → ℂ} {s : ℂ} {l u r θ : ℝ} (hlu : l ≤ u) (hθ : γ l = circleMap s r θ) (θ' : ℝ) : Set.EqOn (exciseCrossing γ s r l u θ θ') γ (Set.Iic l)

Left of the window the excised curve is γ, including at the left endpoint, where the cap starts at γ l.

theorem TauCeti.Contour.exciseCrossing_eqOn_Ici {γ : ℝ → ℂ} {s : ℂ} {l u r θ' : ℝ} (hlu : l < u) (θ : ℝ) (hθ' : γ u = circleMap s r θ') : Set.EqOn (exciseCrossing γ s r l u θ θ') γ (Set.Ici u)

Right of the window the excised curve is γ, including at the right endpoint, where the cap ends at γ u.

theorem TauCeti.Contour.exciseCrossing_eqOn_Icc (γ : ℝ → ℂ) (s : ℂ) (r l u θ θ' : ℝ) : Set.EqOn (exciseCrossing γ s r l u θ θ') (circleCap s r l u θ θ') (Set.Icc l u)

Inside the window the excised curve is the cap.

theorem TauCeti.Contour.exciseCrossing_closed {γ : ℝ → ℂ} {s : ℂ} {a b l u r : ℝ} (hal : a < l) (hub : u < b) (hclosed : γ a = γ b) (θ θ' : ℝ) : exciseCrossing γ s r l u θ θ' a = exciseCrossing γ s r l u θ θ' b

The excised curve is closed whenever γ is: the window [l, u] lies strictly inside [a, b], so both endpoints of [a, b] fall outside it and the excised curve takes the values of γ there.

theorem TauCeti.Contour.exciseCrossing_ne_center {γ : ℝ → ℂ} {s : ℂ} {a b l u r : ℝ} (hr : r ≠ 0) (θ θ' : ℝ) (havoid : ∀ t ∈ Set.Icc a b, t ∉ Set.Ioo l u → γ t ≠ s) (t : ℝ) : t ∈ Set.Icc a b → exciseCrossing γ s r l u θ θ' t ≠ s

The excised curve avoids s. Inside the window it runs along a circle with nonzero signed radial scale about s, and outside it agrees with γ, which by hypothesis meets s only strictly inside the window.

theorem TauCeti.Contour.IsPiecewiseC1On.exciseCrossing {γ : ℝ → ℂ} {s : ℂ} {a b l u r θ θ' : ℝ} (hγ : IsPiecewiseC1On γ a b) (hal : a < l) (hlu : l < u) (hub : u < b) (hθ : γ l = circleMap s r θ) (hθ' : γ u = circleMap s r θ') : IsPiecewiseC1On (Contour.exciseCrossing γ s r l u θ θ') a b

The excised curve is piecewise C¹. The two window endpoints join a piecewise-C¹ curve to a smooth arc, so they are the only new breakpoints.