The winding number of each boundary piece is a principal logarithm

Each smooth piece of the boundary contour of the truncated fundamental domain is confined to an axis-aligned half-plane: the verticals have constant real part ±1/2, the arc stays below height 1, and the truncation ceiling has constant height H. About a point w on the far side of the corresponding line, the chord ratios of the piece therefore lie in the slit plane, so its index integral is a principal logarithm of the endpoint ratio and the winding number of the piece is (2πi)⁻¹ times that logarithm.

Summing the four values over the piece decomposition and pinning with integrality is how the interior winding number -1 of the contour is computed.

Main declarations

• TauCeti.ModularForm.windingNumber_fdBoundarySegment1_eq_log, TauCeti.ModularForm.windingNumber_fdBoundary_arc_eq_log, TauCeti.ModularForm.windingNumber_fdBoundarySegment4_eq_log and TauCeti.ModularForm.windingNumber_fdBoundarySegment5_eq_log — the four logarithm values.

References

The piece-logarithm evaluation follows the fundamental-domain boundary development of AINTLIB's LeanModularForms (ForMathlib/FDBoundary.lean, FDBoundaryH.lean, FDBoundaryPath.lean); the logarithm FTC and the slit-plane criteria are Tau Ceti's.

theorem TauCeti.ModularForm.windingNumber_fdBoundarySegment1_eq_log {H : ℝ} {w : ℂ} (hw : w.re < 1 / 2) : Contour.windingNumber (fdBoundary H) 0 1 w = (2 * ↑Real.pi * Complex.I)⁻¹ * Complex.log ((↑UpperHalfPlane.ρ + 1 - w) / (1 / 2 + ↑H * Complex.I - w))

The winding number of the right vertical about a point strictly to its left is the principal logarithm of the endpoint ratio.

theorem TauCeti.ModularForm.windingNumber_fdBoundary_arc_eq_log {H : ℝ} {w : ℂ} (hw : 1 < w.im) : Contour.windingNumber (fdBoundary H) 1 3 w = (2 * ↑Real.pi * Complex.I)⁻¹ * Complex.log ((↑UpperHalfPlane.ρ - w) / (↑UpperHalfPlane.ρ + 1 - w))

The winding number of the arc about a point strictly above height 1 is the principal logarithm of the endpoint ratio.

theorem TauCeti.ModularForm.windingNumber_fdBoundarySegment4_eq_log {H : ℝ} {w : ℂ} (hw : -(1 / 2) < w.re) : Contour.windingNumber (fdBoundary H) 3 4 w = (2 * ↑Real.pi * Complex.I)⁻¹ * Complex.log ((-1 / 2 + ↑H * Complex.I - w) / (↑UpperHalfPlane.ρ - w))

The winding number of the left vertical about a point strictly to its right is the principal logarithm of the endpoint ratio.

theorem TauCeti.ModularForm.windingNumber_fdBoundarySegment5_eq_log {H : ℝ} {w : ℂ} (hw : w.im < H) : Contour.windingNumber (fdBoundary H) 4 5 w = (2 * ↑Real.pi * Complex.I)⁻¹ * Complex.log ((1 / 2 + ↑H * Complex.I - w) / (-1 / 2 + ↑H * Complex.I - w))

The winding number of the truncation ceiling about a point strictly below height H is the principal logarithm of the endpoint ratio.