The winding number of the boundary contour at ρ

The generalized winding number of the truncated-fundamental-domain boundary about the corner ρ is -1/6. Over the corner-excised parameter ranges the logarithmic integral of the shifted contour t ↦ fdBoundary H t - ρ 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 — chord-matched δ_L(ε) = 12/π·arcsin(ε/2) on the arc side and linear δ_R(ε) = ε/(H - √3/2) on the vertical side. Both endpoint distances are then exactly ε, the log-norm parts cancel, and only the corner angle defect π/3 survives to the limit.

Main declarations

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

References

• AINTLIB LeanModularForms — the valence-formula development (ForMathlib/ValenceFormula/WindingWeights/Rho.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 {H : ℝ} (hH : √3 / 2 < H) : Contour.HasCauchyPVAt (fdBoundary H) 0 5 (fun (z : ℂ) => (z - ↑UpperHalfPlane.ρ)⁻¹) (↑UpperHalfPlane.ρ) (-(↑Real.pi / 3) * Complex.I)

The principal value at ρ: the Cauchy principal value of the index integrand of the boundary contour about the corner ρ is -πi/3 — the corner's angle defect.

@[simp]

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

The winding number of the boundary contour at ρ is -1/6: the corner ρ sits on the contour with interior angle π/3, and the principal-value normalization sees exactly that angle as a clockwise turn, giving -(π/3) / (2π) = -1/6.