Winding of the fundamental-domain boundary: the exterior

Every point off the closed truncated fundamental domain lies in one of five regions — below the corner height, right or left of the fundamental strip, above the ceiling, or in the open unit disc under the arc — and each region sits in the unbounded connected component of the contour's complement, where the winding number vanishes. Together the five determinations package as null-homology of the boundary contour in the truncated fundamental domain, the exterior input to the valence-formula residue count.

The file also carries the arc-excision geometry shared by the corner winding computations at i, at ρ and at ρ + 1. Each excises a parameter window around its corner and needs that window's chord to be exactly the excision radius ε. The half-width realising this for a radius below the corner chord 2·sin(π/12) is stated once here rather than three times.

Main declarations

• TauCeti.ModularForm.windingNumber_fdBoundary_eq_zero_of_im_lt: points below the corner height wind zero, with the analogous determinations on the other sides (_of_half_lt_re, _of_re_lt_neg_half, _of_lt_im) and in the unit disc (_of_norm_lt_one).
• TauCeti.ModularForm.isNullHomologous_fdBoundary: the packaged null-homology.
• TauCeti.ModularForm.fdBoundaryArcExcisionHalfWidth: the parameter half-width whose chord along the arc is a prescribed ε below the corner chord, characterised under that bound by TauCeti.ModularForm.fdBoundaryArcExcisionHalfWidth_pos_and_lt_one_and_two_mul_sin_eq.

References

The truncated-contour strategy follows the fundamental-domain boundary development of AINTLIB's LeanModularForms (ForMathlib/FDBoundary.lean, FDBoundaryH.lean, FDBoundaryPath.lean); the winding transport is Tau Ceti's Hungerbühler–Wasem machinery.

The arc-excision geometry is not from those files: it is extracted from the same project's winding-value development (ForMathlib/ValenceFormula/WindingWeights/I.lean, Rho.lean and RhoPlusOne.lean), where each corner computation built its own chord-matched half-width. It is stated once here so the three share it.

@[simp]

theorem TauCeti.ModularForm.windingNumber_fdBoundary_eq_zero_of_im_lt {H : ℝ} (hH : √3 / 2 ≤ H) {w : ℂ} (hw : w.im < √3 / 2) : Contour.windingNumber (fdBoundary H) 0 5 w = 0

Every point strictly below the contour's height winds zero.

@[simp]

theorem TauCeti.ModularForm.windingNumber_fdBoundary_eq_zero_of_half_lt_re {H : ℝ} {w : ℂ} (hw : 2⁻¹ < w.re) : Contour.windingNumber (fdBoundary H) 0 5 w = 0

Every point strictly right of the fundamental strip winds zero. The bound is stated in simp-normal form so the lemma can participate in simplification.

@[simp]

theorem TauCeti.ModularForm.windingNumber_fdBoundary_eq_zero_of_re_lt_neg_half {H : ℝ} {w : ℂ} (hw : w.re < -2⁻¹) : Contour.windingNumber (fdBoundary H) 0 5 w = 0

Every point strictly left of the fundamental strip winds zero.

@[simp]

theorem TauCeti.ModularForm.windingNumber_fdBoundary_eq_zero_of_lt_im {H : ℝ} (hH : 1 ≤ H) {w : ℂ} (hw : H < w.im) : Contour.windingNumber (fdBoundary H) 0 5 w = 0

Every point strictly above the contour's height winds zero.

@[simp]

theorem TauCeti.ModularForm.windingNumber_fdBoundary_eq_zero_of_norm_lt_one {H : ℝ} (hH : 1 ≤ H) {w : ℂ} (hw : ‖w‖ < 1) : Contour.windingNumber (fdBoundary H) 0 5 w = 0

Every point of the open unit disc winds zero: the disc sits under the arc, inside the contour's complement, and connects through the origin to the region below the corner height. Together with the four half-plane determinations this covers every point off the closed truncated fundamental domain.

theorem TauCeti.ModularForm.isNullHomologous_fdBoundary {H : ℝ} (hH : 1 ≤ H) : Contour.IsNullHomologous (fdBoundary H) 0 5 (UpperHalfPlane.coe '' ModularGroup.truncatedFundamentalDomain H)

The boundary contour is null-homologous in the truncated fundamental domain: every point off the closed truncated domain lies in one of the five exterior regions, where the winding number vanishes.

noncomputable def TauCeti.ModularForm.fdBoundaryArcExcisionHalfWidth (ε : ℝ) : ℝ

The chord-matched excision half-width. The parameter half-width whose chord along the unit-circle arc is the excision radius ε.

The chord identity 2·sin(δ·π/12) = ε holds throughout |ε| ≤ 2, the range on which Real.arcsin inverts the sine, and fails beyond it because Real.arcsin saturates. fdBoundaryArcExcisionHalfWidth_pos_and_lt_one_and_two_mul_sin_eq nonetheless assumes the narrower 0 < ε < 2·sin(π/12): that is the range the excision arguments need, because it also places the half-width strictly between 0 and 1, inside the corner's own arc window.

Equations

• TauCeti.ModularForm.fdBoundaryArcExcisionHalfWidth ε = 12 / Real.pi * Real.arcsin (ε / 2)

@[simp]

theorem TauCeti.ModularForm.fdBoundaryArcExcisionHalfWidth_def (ε : ℝ) : fdBoundaryArcExcisionHalfWidth ε = 12 / Real.pi * Real.arcsin (ε / 2)

The chord-matched excision half-width, unfolded.

theorem TauCeti.ModularForm.fdBoundaryArcExcisionHalfWidth_mul_pi_div_twelve (ε : ℝ) : fdBoundaryArcExcisionHalfWidth ε * (Real.pi / 12) = Real.arcsin (ε / 2)

The half-width is exactly the angle arcsin (ε / 2) once scaled by the corner's angular unit π / 12. This is the shape in which the half-width enters the sine identity below, the excised arc away from the corners, and the excised integrals at ρ and ρ + 1.

AINTLIB gives the same fact its own name at the corner i, where the angular unit is 5π / 12: half_angle_arcsinDelta in LeanModularForms/ForMathlib/CrossingAtI.lean (github.com/CBirkbeck/AINTLIB, Apache-2.0).

theorem TauCeti.ModularForm.fdBoundaryArcExcisionHalfWidth_pos_and_lt_one_and_two_mul_sin_eq {ε : ℝ} (hε : 0 < ε) (hε₃ : ε < 2 * Real.sin (Real.pi / 12)) : 0 < fdBoundaryArcExcisionHalfWidth ε ∧ fdBoundaryArcExcisionHalfWidth ε < 1 ∧ 2 * Real.sin (fdBoundaryArcExcisionHalfWidth ε * (Real.pi / 12)) = ε

The chord-matched excision half-width does what it is for. For an excision radius ε below the corner chord 2·sin(π/12), the half-width lies strictly between 0 and 1 and reproduces ε as its own chord: 2·sin(δ·π/12) = ε.

This is the trigonometric content shared by the excision constructions at i, at ρ and at ρ + 1; it needs no upper bound on ε beyond the chord bound.