The excision leaves the arc's full length in the limit

The valence formula integrates over the fundamental-domain boundary with the integrand excised within ε of the elliptic points. On the arc the excised integral turns out to be a constant multiple of the length of the surviving parameter set, so its ε → 0 limit is governed by that length alone.

This file supplies both halves. The arc runs once around a π/3 sector of the unit circle, so it meets each excision centre at most once (injOn_fdBoundary_arc), and TauCeti.Contour.tendsto_intervalIntegral_excisionIndicator applies with the whole length 2. The constant is the contour's own logarithmic derivative, which on the arc is (π/6)·I (logDeriv_fdBoundary_arc), so the excised integral tends to (π/3)·I.

References

• AINTLIB LeanModularForms — the valence-formula development; this file adapts the arc-specific half of ForMathlib/ValenceFormula/PVChain/ArcContribution.lean (arc_preimage_subsingleton and the specialisation of arc_non_excluded_measure_tendsto) onto the current Mathlib pin.

Main results

• TauCeti.ModularForm.tendsto_intervalIntegral_excisionIndicator_fdBoundary_arc: the surviving length of [1, 3] tends to 2 as ε → 0⁺.
• TauCeti.ModularForm.intervalIntegral_excised_logDeriv_fdBoundary_arc: at a fixed ε, the excised arc integral of logDeriv (fdBoundary H) is (π/6)·I times the surviving length.
• TauCeti.ModularForm.tendsto_intervalIntegral_excised_logDeriv_fdBoundary_arc: hence it tends to (π/3)·I.

theorem TauCeti.ModularForm.tendsto_intervalIntegral_excisionIndicator_fdBoundary_arc (H : ℝ) (S : Finset ℂ) : Filter.Tendsto (fun (ε : ℝ) => ∫ (t : ℝ) in 1..3, if ∃ s ∈ S, ‖fdBoundary H t - s‖ ≤ ε then 0 else 1) (nhdsWithin 0 (Set.Ioi 0)) (nhds 2)

The excision leaves the arc's full length in the limit. Deleting from [1, 3] the times at which the boundary comes within ε of one of finitely many centres costs no length as ε → 0⁺: the surviving length tends to 2.

theorem TauCeti.ModularForm.intervalIntegral_excised_logDeriv_fdBoundary_arc (H : ℝ) (S : Finset ℂ) (ε : ℝ) : (∫ (t : ℝ) in 1..3, if ∃ s ∈ S, ‖fdBoundary H t - s‖ ≤ ε then 0 else logDeriv (fdBoundary H) t) = ↑(Real.pi / 6) * Complex.I * ↑(∫ (t : ℝ) in 1..3, if ∃ s ∈ S, ‖fdBoundary H t - s‖ ≤ ε then 0 else 1)

The excised arc integral of the contour's own logarithmic derivative. On the arc logDeriv (fdBoundary H) is the constant (π/6)·I (logDeriv_fdBoundary_arc), so the excised integral is that constant times the surviving length.

theorem TauCeti.ModularForm.tendsto_intervalIntegral_excised_logDeriv_fdBoundary_arc (H : ℝ) (S : Finset ℂ) : Filter.Tendsto (fun (ε : ℝ) => ∫ (t : ℝ) in 1..3, if ∃ s ∈ S, ‖fdBoundary H t - s‖ ≤ ε then 0 else logDeriv (fdBoundary H) t) (nhdsWithin 0 (Set.Ioi 0)) (nhds (↑(Real.pi / 3) * Complex.I))

The arc's excised logarithmic-derivative integral tends to (π/3)·I. Combining the constant value on the arc with the surviving length's limit 2.