The boundary contour is a piecewise-C¹ immersion

Away from the three genuine corners every piece of the boundary contour has a nonvanishing tangent: the verticals and the horizontal move with constant nonzero chords (the height differing from the corner row keeps the verticals nondegenerate), and the unified arc moves at constant speed π/6. This is the regularity that feeds the principal-value existence of the winding decomposition and the residue sum along the contour.

Main declarations

• TauCeti.ModularForm.isPwC1ImmersionOn_fdBoundary.

References

The immersion condition is the regularity requirement of N. Hungerbühler and M. Wasem, Non-integer valued winding numbers and a generalized Residue Theorem, arXiv:1808.00997 (2018); the truncated-contour strategy follows the fundamental-domain boundary development of AINTLIB's LeanModularForms (ForMathlib/FDBoundary.lean, FDBoundaryH.lean, FDBoundaryPath.lean).

theorem TauCeti.ModularForm.isPwC1ImmersionOn_fdBoundary {H : ℝ} (hH : H ≠ √3 / 2) : Contour.IsPwC1ImmersionOn (fdBoundary H) 0 5

The boundary contour is a piecewise-C¹ immersion: every corner-free piece is C¹ with nonvanishing tangent.