The boundary contour winds -1 above the corner row

For a point of the open strip |re| < 1/2 strictly between height 1 and the ceiling height H, the boundary contour winds exactly -1: the contour is traversed clockwise around its interior. The four piece values are principal logarithms whose arguments each lie in (-π, 0), so their sum lies in (-4π, 0); integrality of the winding number then pins the value to -1.

Points of the truncated fundamental domain below height 1 are reached from this strip by winding transport: the vertical lift of an interior point into the strip, together with the open strip box, is one preconnected region avoiding the contour, so the value transports.

Main declarations

• TauCeti.ModularForm.windingNumber_fdBoundary_eq_neg_one_of_interior.

References

The interior determination follows the fundamental-domain boundary development of AINTLIB's LeanModularForms (ForMathlib/FDBoundary.lean, FDBoundaryH.lean, FDBoundaryPath.lean), adapted to the raw-path winding machinery: the piece decomposition and logarithm values are summed and pinned by integrality rather than evaluated termwise.

theorem TauCeti.ModularForm.fdBoundary_ne_of_abs_re_lt_half_of_one_lt_norm_of_im_lt {H : ℝ} {w : ℂ} (hre : |w.re| < 1 / 2) (hnorm : 1 < ‖w‖) (him : w.im < H) (t : ℝ) : t ∈ Set.Icc 0 5 → fdBoundary H t ≠ w

Off-curve avoidance for interior points: each piece is separated from w in one coordinate, the arc by the norm.

theorem TauCeti.ModularForm.windingNumber_fdBoundary_eq_neg_one_of_interior {H : ℝ} (hH : 1 < H) {w : ℂ} (hnorm : 1 < ‖w‖) (hre : |w.re| < 1 / 2) (hpos : 0 < w.im) (him : w.im < H) : Contour.windingNumber (fdBoundary H) 0 5 w = -1

The boundary contour winds -1 about every point of the open truncated fundamental domain: the region 1 < ‖w‖, |re w| < 1/2, 0 < im w < H.