The excised logarithmic telescope for a branch adapted to a crossing point

The engine shared by the non-corner winding computations (Winding/NonCorner/Vertical.lean and Winding/NonCorner/Arc.lean): running the excised logarithmic telescope on the branch log ((γ t - w) · c) for a unit c that rotates the branch cut into a ray from w missing the rest of the contour. With the cut so aimed, the whole excised contour is slit-plane-valued for the one branch, the telescope needs no interior crossing corrections, and both pieces evaluate by the comparison-free logarithmic FTC; closedness of the contour cancels the shared basepoint, leaving the endpoint-log difference across the excision window.

Main declarations

• TauCeti.ModularForm.truncated_integral_spec_of_slit_branch: over a two-piece excision of the parameter range, the truncated winding integrand is interval integrable and its integral is the branch-log difference at the excision endpoints.

theorem TauCeti.ModularForm.truncated_integral_spec_of_slit_branch {H t₀ δ ε : ℝ} {w c : ℂ} (hc : c ≠ 0) (h0 : 0 ≤ t₀ - δ) (hδ : 0 < δ) (h5 : t₀ + δ ≤ 5) (hslit : ∀ t ∈ Set.Icc 0 5, t ∉ Set.Ioo (t₀ - δ) (t₀ + δ) → (fdBoundary H t - w) * c ∈ Complex.slitPlane) (hfar_left : ∀ s ∈ Set.Ioo 0 (t₀ - δ), ε < ‖fdBoundary H s - w‖) (hfar_right : ∀ s ∈ Set.Ioo (t₀ + δ) 5, ε < ‖fdBoundary H s - w‖) (hnear : ∀ s ∈ Set.Icc (t₀ - δ) (t₀ + δ), ‖fdBoundary H s - w‖ ≤ ε) : IntervalIntegrable (fun (t : ℝ) => if ε < ‖fdBoundary H t - w‖ then (fdBoundary H t - w)⁻¹ * deriv (fdBoundary H) t else 0) MeasureTheory.volume 0 5 ∧ (∫ (t : ℝ) in 0..5, if ε < ‖fdBoundary H t - w‖ then (fdBoundary H t - w)⁻¹ * deriv (fdBoundary H) t else 0) = Complex.log ((fdBoundary H (t₀ - δ) - w) * c) - Complex.log ((fdBoundary H (t₀ + δ) - w) * c)

The excision collapse for an adapted branch. If beyond the excised parameter window the contour keeps distance more than ε from w while the rotated branch stays in the slit plane, and within the window it stays within ε, then the ε-truncated index integrand is interval integrable over the whole contour and its integral is the window-endpoint log difference of the rotated branch.