Winding of the boundary contour at the open vertical edges

A point w of an open vertical edge is crossed by exactly one straight segment of the boundary contour, and the winding number there is -1/2: half a clockwise turn. Along the crossing segment the shifted contour γ t - w is purely imaginary, so the chord distance is linear in the parameter and the matched half-width is δ(ε) = ε / (H - √3/2). The adapted branch (Winding/NonCorner/Basic.lean) negates on the right edge and is the principal one on the left; either way the excision endpoints are ±ε·i and the excised integral is the constant -π·i.

Two spellings recur below: linear bounds enter as inline show _ by linarith terms, stating each bound at the sign-adjusted operand its consuming abs estimate needs, and the log evaluations reshape real-cast products by show _ by push_cast; ring into the ((r : ℝ) : ℂ) * z operand that Complex.log_ofReal_mul splits.

Main declarations

• TauCeti.ModularForm.hasCauchyPVAt_fdBoundary_vertical, TauCeti.ModularForm.windingNumber_fdBoundary_vertical: the principal value -πi and the winding number -1/2 at a point of an open vertical edge.

The hypotheses are spelled the way the singular-set interface provides them (TauCeti.ModularForm.verticalSingularSet): a vertical point carries w.re = 2⁻¹ ∨ w.re = -(2⁻¹), 1 < ‖w‖, 0 < w.im and w.im < H; no lower height hypothesis is needed.

References

• AINTLIB LeanModularForms (commit 2baa76f742bdb4fb8ee323fabba41203bd390e08, Apache-2.0, Chris Birkbeck) — the statement pair fills the vertical-edge role of that project's FDWindingDataFull.boundary_winding, whose vertical inputs are the FTC-provider files ForMathlib/Seg1FTCProvider.lean and ForMathlib/Seg4FTCProvider.lean. The proof route is Tau Ceti's own rotated-branch telescope.
• N. Hungerbühler, M. Wasem, Non-integer valued winding numbers and a generalized Residue Theorem, arXiv:1808.00997.

The vertical edges

A point w of an open vertical edge is crossed by exactly one straight segment. Along it the shifted contour γ t - w is purely imaginary, so the chord distance is linear in the parameter and the matched half-width is δ(ε) = ε / (H - √3/2). The adapted branch negates on the right edge and is the principal one on the left; either way the excision endpoints are ±ε·i and the excised integral is the constant -π·i.

Two spellings recur below: linear bounds enter as inline show _ by linarith terms, stating each bound at the sign-adjusted operand its consuming abs estimate needs, and the log evaluations reshape real-cast products by show _ by push_cast; ring into the ((r : ℝ) : ℂ) * z operand that Complex.log_ofReal_mul splits.

theorem TauCeti.ModularForm.hasCauchyPVAt_fdBoundary_vertical {H : ℝ} {w : ℂ} (hre : w.re = 2⁻¹ ∨ w.re = -2⁻¹) (hnorm : 1 < ‖w‖) (him : 0 < w.im) (himH : w.im < H) : Contour.HasCauchyPVAt (fdBoundary H) 0 5 (fun (z : ℂ) => (z - w)⁻¹) w (-↑Real.pi * Complex.I)

The principal value at a vertical-edge point: the Cauchy principal value of the index integrand of the boundary contour about a point of an open vertical edge is -πi — half a clockwise turn, as the contour passes straight through w along the edge.

@[simp]

theorem TauCeti.ModularForm.windingNumber_fdBoundary_vertical {H : ℝ} {w : ℂ} (hre : w.re = 2⁻¹ ∨ w.re = -2⁻¹) (hnorm : 1 < ‖w‖) (him : 0 < w.im) (himH : w.im < H) : Contour.windingNumber (fdBoundary H) 0 5 w = -(1 / 2)

The winding number of the boundary contour at a vertical-edge point is -1/2: the point sits on an open vertical edge, and the principal-value normalization sees exactly half a clockwise turn.