The winding number of the boundary contour at ρ + 1

The generalized winding number of the truncated-fundamental-domain boundary about the corner ρ + 1 is -1/6. Over the corner-excised parameter ranges the logarithmic integral of the shifted contour t ↦ fdBoundary H t - (ρ + 1) telescopes piece by piece through the boundary-tolerant logarithmic fundamental theorem, and the ε-excision of the principal value collapses to exactly those ranges with asymmetric half-widths — linear δ_L(ε) = ε/(H - √3/2) on the vertical side and chord-matched δ_R(ε) = 12/π·arcsin(ε/2) on the arc side. Both endpoint distances are then exactly ε, the log-norm parts cancel, and only the corner's interior angle π/3 survives the limit.

Main declarations

• TauCeti.ModularForm.hasCauchyPVAt_fdBoundary_rho_add_one (the principal value -πi/3).
• TauCeti.ModularForm.windingNumber_fdBoundary_rho_add_one (the winding number -1/6).

References

• AINTLIB LeanModularForms — the valence-formula development (ForMathlib/ValenceFormula/WindingWeights/RhoPlusOne.lean) this file ports onto the current Mathlib pin.
• N. Hungerbühler, M. Wasem, Non-integer valued winding numbers and a generalized Residue Theorem, arXiv:1808.00997.

theorem TauCeti.ModularForm.hasCauchyPVAt_fdBoundary_rho_add_one {H : ℝ} (hH : √3 / 2 < H) : Contour.HasCauchyPVAt (fdBoundary H) 0 5 (fun (z : ℂ) => (z - (↑UpperHalfPlane.ρ + 1))⁻¹) (↑UpperHalfPlane.ρ + 1) (-(↑Real.pi / 3) * Complex.I)

The principal value at ρ + 1: the Cauchy principal value of the index integrand of the boundary contour about the corner ρ + 1 is -πi/3 — the corner's interior angle π/3, taken clockwise.

@[simp]

theorem TauCeti.ModularForm.windingNumber_fdBoundary_rho_add_one {H : ℝ} (hH : √3 / 2 < H) : Contour.windingNumber (fdBoundary H) 0 5 (↑UpperHalfPlane.ρ + 1) = -(1 / 6)

The winding number of the boundary contour at ρ + 1 is -1/6: the corner ρ + 1 sits on the contour with interior angle π/3 — the gap between the one-sided argument limits π/2 and 5π/6 — and the clockwise traversal turns that into -1/6.