The arc keeps its distance from the vertical excision centres

The principal-value assembly of the valence formula excises the union arcSingularSet S ∪ verticalSingularSet S. Along the closed arc [1, 3] of the boundary contour only the arc part can fire once ε is small: a vertical centre outside the arc set never lies on the closed arc — the open arc has |re| < 1/2 strictly, and the endpoints are the corners ρ + 1 and ρ, which the arc set contains unconditionally — so compactness gives a positive distance from the arc to each such centre, uniform over the finitely many of them. Below that distance the union excision test agrees with its arc part at every arc parameter, which is what lets the arc pairing machinery, built for unit-norm inversion-closed excision sets, apply to the union.

Main declarations

• TauCeti.ModularForm.exists_pos_forall_le_norm_fdBoundary_sub_of_mem_verticalSingularSet: a positive δ under the distance from every arc point to every vertical centre outside the arc set.
• TauCeti.ModularForm.exists_norm_fdBoundary_sub_le_union_iff: for ε under that distance the union excision test along the arc reads the same as the arc-only test.
• TauCeti.ModularForm.eventually_forall_lt_norm_fdBoundary_sub_of_mem_verticalSingularSet: the separation holds for every sufficiently small ε > 0.

References

• AINTLIB LeanModularForms — the valence-formula development (ForMathlib/ValenceFormula/PVChain/ArcContribution.lean: the strict real-part bounds, the corner capture, the compactness minimum, and the ∀ᶠ reduction of the union test to the arc test) this file ports onto the current Mathlib pin.

theorem TauCeti.ModularForm.exists_pos_forall_le_norm_fdBoundary_sub_of_mem_verticalSingularSet (H : ℝ) (S : Finset UpperHalfPlane) : ∃ δ > 0, ∀ s ∈ verticalSingularSet S, s ∉ arcSingularSet S → ∀ t ∈ Set.Icc 1 3, δ ≤ ‖fdBoundary H t - s‖

The arc keeps a positive distance from the non-arc vertical centres. The closed arc is compact and misses every vertical centre outside the arc set, so each such centre sits at a positive infimum distance from it, and a single δ under all the finitely many of them works uniformly.

theorem TauCeti.ModularForm.exists_norm_fdBoundary_sub_le_union_iff {H ε : ℝ} {S : Finset UpperHalfPlane} (hfar : ∀ s ∈ verticalSingularSet S, s ∉ arcSingularSet S → ∀ t ∈ Set.Icc 1 3, ε < ‖fdBoundary H t - s‖) {t : ℝ} (ht : t ∈ Set.Icc 1 3) : (∃ s ∈ arcSingularSet S ∪ verticalSingularSet S, ‖fdBoundary H t - s‖ ≤ ε) ↔ ∃ s ∈ arcSingularSet S, ‖fdBoundary H t - s‖ ≤ ε

Under the separation the union excision test degenerates to its arc part on the arc. The vertical centres already in the arc set are absorbed by it, and the remaining ones are farther than ε from every arc point by hfar, so along the arc only the arc part of the union can fire.

theorem TauCeti.ModularForm.eventually_forall_lt_norm_fdBoundary_sub_of_mem_verticalSingularSet (H : ℝ) (S : Finset UpperHalfPlane) : ∀ᶠ (ε : ℝ) in nhdsWithin 0 (Set.Ioi 0), ∀ s ∈ verticalSingularSet S, s ∉ arcSingularSet S → ∀ t ∈ Set.Icc 1 3, ε < ‖fdBoundary H t - s‖

The separation of the arc from the non-arc vertical centres holds for every sufficiently small ε > 0: the positive distance of exists_pos_forall_le_norm_fdBoundary_sub_of_mem_verticalSingularSet dominates.