Excising the corner of a model sector

TauCeti.Contour.exciseCrossing deletes a parameter window from a curve and caps it with a circular arc, and TauCeti.Contour.windingNumber_eq_exciseCrossing_add accounts exactly for the winding number that the surgery moves. This file runs that surgery on the one crossing whose geometry is completely known: the corner of the model sector TauCeti.Contour.modelSector of radius r and opening angle α, whose two rays leave the corner at the angles φ + α and φ.

Deleting the window [-ε, ε] about the corner and capping it with the arc of the circle of radius ε running from angle φ + α back to angle φ leaves a closed curve of winding number 0 (TauCeti.Contour.windingNumber_eq_zero_exciseCrossing_modelSector). Equivalently, the sector's entire index α / 2π is the local contribution of its crossing — the model case of the identification that Hungerbühler–Wasem Proposition 2.2 asserts for a general immersion, and hence an acceptance test for the surgery.

Main results

• TauCeti.Contour.windingNumber_eq_zero_exciseCrossing_modelSector — excising the corner of a model sector leaves winding number 0.

Provenance

No formalization is vendored; the statement is a direct application of TauCeti.Contour.windingNumber_eq_exciseCrossing_add to the model sector already in the tree.

References

• N. Hungerbühler, M. Wasem, Non-integer valued winding numbers and a generalized Residue Theorem, arXiv:1808.00997 — Proposition 2.2, and the model sector of their equation (2.4).

theorem TauCeti.Contour.windingNumber_eq_zero_exciseCrossing_modelSector {z₀ : ℂ} {r ε φ α : ℝ} (hε : 0 < ε) (hεr : ε < r) (hα : 0 ≤ α) : windingNumber (exciseCrossing (modelSector z₀ r φ α) z₀ ε (-ε) ε (φ + α) φ) (-r) (r + α) z₀ = 0

Excising the corner of a model sector leaves nothing. The model sector of radius r and opening angle α crosses its own corner along two straight radii; deleting the window [-ε, ε] and capping it with the arc from angle φ + α back to angle φ produces a closed curve of winding number 0.

Equivalently, the sector's entire index α / 2π is the local contribution of its crossing, which is the model case of the identification that HW Proposition 2.2 asserts for a general immersion.