Winding of the boundary contour at the open unit arc

A point w of the open unit arc is fdBoundary H t₀ for a unique t₀ ∈ (1, 3); the arc is one smooth circle parameterization through t = 2, so no corner is in the way even at i, and the winding number at every open-arc point is -1/2. The adapted branch (Winding/NonCorner/Basic.lean) is c = w⁻¹, whose cut ray {r·w : r ≤ 1} runs from w through the open unit disc and leaves through the lower half-plane, missing the rest of the contour. The chord distance is 2·sin(|t - t₀|·π/12), uniform along the arc; the excised integral is -π·i - 2·arcsin(ε/2)·i, and the limit is -π·i.

The statements cover the whole open arc, including i: a consumer wanting the value there supplies the elliptic point's three elementary facts — ‖i‖ = 1, |re i| = 0 < 1/2, 0 < im i — directly to the theorems below.

The polar computations below restate angle and cast algebra as inline show _ by ring / show _ by push_cast; ring equations: each aims the expression at the exact spelling the next Real.cos/Complex.exp/Complex.log rewrite matches.

Main declarations

• TauCeti.ModularForm.hasCauchyPVAt_fdBoundary_arc, TauCeti.ModularForm.windingNumber_fdBoundary_arc: the principal value -πi and the winding number -1/2 at a point of the open unit arc.

The hypotheses are spelled the way the singular-set interface provides them (TauCeti.ModularForm.arcSingularSet): an arc point carries ‖w‖ = 1, |w.re| < 2⁻¹ and 0 < w.im. The theorems also assume 1 < H, which makes the contour the boundary of a genuine truncation: the ceiling then clears the arc point by H - 1 > 0.

References

• AINTLIB LeanModularForms (commit 2baa76f742bdb4fb8ee323fabba41203bd390e08, Apache-2.0, Chris Birkbeck) — the statement pair fills the arc role of that project's FDWindingDataFull.boundary_winding, whose arc input is the FTC-provider file ForMathlib/ArcGenericFTCProvider.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 arc

A point w of the open unit arc is fdBoundary H t₀ for a unique t₀ ∈ (1, 3); the arc is one smooth circle parameterization through t = 2, so no corner is in the way even at i. The adapted branch is c = w⁻¹, whose cut ray {r·w : r ≤ 1} runs from w through the open unit disc and leaves through the lower half-plane, missing the rest of the contour. The chord distance is 2·sin(|t - t₀|·π/12), uniform along the arc.

The polar computations below restate angle and cast algebra as inline show _ by ring / show _ by push_cast; ring equations: each aims the expression at the exact spelling the next Real.cos/Complex.exp/Complex.log rewrite matches.

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

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

@[simp]

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

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