The singular sets on the boundary contour

The two candidate exceptional sets the on-curve principal values excise, built from any finite set of upper half-plane points and closed under the identifications the contour pairings use: the arc singular set — the unit-norm points of a finite set S ⊆ ℍ together with their images under the inversion z ↦ -1/z and the corners ρ, ρ + 1 — and the vertical singular set — the re = ±1/2, norm-above-one points of S together with their translates onto the opposite vertical line. Their calculus: the corners belong to the arc set, the arc set consists of unit-norm points and is inversion-closed, the vertical set lies on the two vertical lines and is translation-paired, all points have positive imaginary part, and a single height bound dominates every vertical point.

Main declarations

• TauCeti.ModularForm.arcSingularSet and TauCeti.ModularForm.verticalSingularSet.
• TauCeti.ModularForm.neg_one_div_mem_arcSingularSet (inversion closure).
• TauCeti.ModularForm.sub_one_mem_verticalSingularSet and TauCeti.ModularForm.add_one_mem_verticalSingularSet (translation pairing).
• TauCeti.ModularForm.neg_conj_mem_arcSingularSet_union_verticalSingularSet (closure of the union under the vertical reflection z ↦ -conj z, through the two closures above).
• TauCeti.ModularForm.exists_height_bound (a height above √3/2 and 1 dominating S).

References

• AINTLIB LeanModularForms — the valence-formula development (ForMathlib/ValenceFormula/PVChain/Helpers.lean) this file ports onto the current Mathlib pin; the reflection and union closure lemmas adapt the per-part closure bookkeeping of ForMathlib/ValenceFormula/PVChain/Assembly.lean.

noncomputable def TauCeti.ModularForm.arcSingularSet (S : Finset UpperHalfPlane) : Finset ℂ

The arc singular set of a finite S ⊆ ℍ: its unit-norm members, their images under the inversion z ↦ -1/z, and the corners ρ and ρ + 1.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def TauCeti.ModularForm.verticalSingularSet (S : Finset UpperHalfPlane) : Finset ℂ

The vertical singular set of a finite S ⊆ ℍ: its re = ±1/2, norm-above-one members together with their translates onto the opposite vertical line.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.ModularForm.mem_arcSingularSet {S : Finset UpperHalfPlane} {s : ℂ} : s ∈ arcSingularSet S ↔ (∃ p ∈ S, ‖↑p‖ = 1 ∧ ↑p = s) ∨ (∃ p ∈ S, ‖↑p‖ = 1 ∧ -1 / ↑p = s) ∨ s = ↑UpperHalfPlane.ρ ∨ s = ↑UpperHalfPlane.ρ + 1

Membership in the arc singular set, by branch: an original unit-norm point, an inversion image, or one of the two corners.

@[simp]

theorem TauCeti.ModularForm.mem_verticalSingularSet {S : Finset UpperHalfPlane} {s : ℂ} : s ∈ verticalSingularSet S ↔ (∃ p ∈ S, ((↑p).re = 1 / 2 ∧ 1 < ‖↑p‖) ∧ ↑p = s) ∨ (∃ p ∈ S, ((↑p).re = 1 / 2 ∧ 1 < ‖↑p‖) ∧ ↑p - 1 = s) ∨ (∃ p ∈ S, ((↑p).re = -(1 / 2) ∧ 1 < ‖↑p‖) ∧ ↑p = s) ∨ ∃ p ∈ S, ((↑p).re = -(1 / 2) ∧ 1 < ‖↑p‖) ∧ ↑p + 1 = s

Membership in the vertical singular set, by branch: an original point on either line or a translate onto the opposite line.

theorem TauCeti.ModularForm.one_lt_norm_of_mem_verticalSingularSet {S : Finset UpperHalfPlane} {s : ℂ} (hs : s ∈ verticalSingularSet S) : 1 < ‖s‖

Every point of the vertical singular set has norm above 1: the translates keep the square norm because they only flip the sign of the real part.

theorem TauCeti.ModularForm.rho_mem_arcSingularSet (S : Finset UpperHalfPlane) : ↑UpperHalfPlane.ρ ∈ arcSingularSet S

The corner ρ belongs to the arc singular set.

theorem TauCeti.ModularForm.rho_add_one_mem_arcSingularSet (S : Finset UpperHalfPlane) : ↑UpperHalfPlane.ρ + 1 ∈ arcSingularSet S

The corner ρ + 1 belongs to the arc singular set.

theorem TauCeti.ModularForm.norm_eq_one_of_mem_arcSingularSet {S : Finset UpperHalfPlane} {s : ℂ} (hs : s ∈ arcSingularSet S) : ‖s‖ = 1

Every point of the arc singular set has norm 1.

theorem TauCeti.ModularForm.neg_one_div_mem_arcSingularSet {S : Finset UpperHalfPlane} {s : ℂ} (hs : s ∈ arcSingularSet S) : -1 / s ∈ arcSingularSet S

The arc singular set is closed under the inversion z ↦ -1/z.

theorem TauCeti.ModularForm.re_eq_of_mem_verticalSingularSet {S : Finset UpperHalfPlane} {s : ℂ} (hs : s ∈ verticalSingularSet S) : s.re = 1 / 2 ∨ s.re = -(1 / 2)

Every point of the vertical singular set lies on one of the two vertical lines.

theorem TauCeti.ModularForm.sub_one_mem_verticalSingularSet {S : Finset UpperHalfPlane} {s : ℂ} (hs : s ∈ verticalSingularSet S) (hre : s.re = 1 / 2) : s - 1 ∈ verticalSingularSet S

A right-line point of the vertical singular set has its left translate in the set.

theorem TauCeti.ModularForm.add_one_mem_verticalSingularSet {S : Finset UpperHalfPlane} {s : ℂ} (hs : s ∈ verticalSingularSet S) (hre : s.re = -(1 / 2)) : s + 1 ∈ verticalSingularSet S

A left-line point of the vertical singular set has its right translate in the set.

theorem TauCeti.ModularForm.neg_conj_mem_arcSingularSet {S : Finset UpperHalfPlane} {s : ℂ} (hs : s ∈ arcSingularSet S) : -(starRingEnd ℂ) s ∈ arcSingularSet S

The arc singular set is closed under the reflection z ↦ -conj z that exchanges the two verticals of the boundary contour: on unit-norm points the reflection coincides with the inversion z ↦ -1/z, and the set is inversion-closed.

theorem TauCeti.ModularForm.neg_conj_mem_verticalSingularSet {S : Finset UpperHalfPlane} {s : ℂ} (hs : s ∈ verticalSingularSet S) : -(starRingEnd ℂ) s ∈ verticalSingularSet S

The vertical singular set is closed under the reflection z ↦ -conj z that exchanges the two verticals of the boundary contour: on the lines re = ±1/2 the reflection coincides with the translation onto the opposite line, and the set is translation-paired.

theorem TauCeti.ModularForm.neg_conj_mem_arcSingularSet_union_verticalSingularSet {S : Finset UpperHalfPlane} {s : ℂ} (hs : s ∈ arcSingularSet S ∪ verticalSingularSet S) : -(starRingEnd ℂ) s ∈ arcSingularSet S ∪ verticalSingularSet S

The union of the two singular sets is closed under the reflection z ↦ -conj z — the reflection invariance the excised vertical cancellation (intervalIntegral_excised_fdBoundarySegment4_eq_neg_segment1) asks of its excision set.

theorem TauCeti.ModularForm.exists_height_bound (S : Finset UpperHalfPlane) : ∃ (H : ℝ), √3 / 2 < H ∧ 1 < H ∧ ∀ p ∈ S, (↑p).im < H

Some height above √3/2 and 1 dominates the imaginary parts of a finite S ⊆ ℍ.

theorem TauCeti.ModularForm.im_lt_of_mem_verticalSingularSet {S : Finset UpperHalfPlane} {s : ℂ} {H : ℝ} (hs : s ∈ verticalSingularSet S) (h_bound : ∀ p ∈ S, (↑p).im < H) : s.im < H

A height bound on S bounds the vertical singular set.

theorem TauCeti.ModularForm.im_pos_of_mem_arcSingularSet {S : Finset UpperHalfPlane} {s : ℂ} (hs : s ∈ arcSingularSet S) : 0 < s.im

Every point of the arc singular set lies in the open upper half-plane.

theorem TauCeti.ModularForm.im_pos_of_mem_verticalSingularSet {S : Finset UpperHalfPlane} {s : ℂ} (hs : s ∈ verticalSingularSet S) : 0 < s.im

Every point of the vertical singular set lies in the open upper half-plane.

theorem TauCeti.ModularForm.im_lt_of_mem_arcSingularSet {S : Finset UpperHalfPlane} {s : ℂ} {H : ℝ} (hs : s ∈ arcSingularSet S) (hH : 1 < H) : s.im < H

Every arc excision centre sits below the ceiling: it has unit norm, and the imaginary part is bounded by the norm.

theorem TauCeti.ModularForm.im_lt_of_mem_arcSingularSet_union_verticalSingularSet {S : Finset UpperHalfPlane} {s : ℂ} {H : ℝ} (hH : 1 < H) (hHgt : ∀ p ∈ S, (↑p).im < H) (hs : s ∈ arcSingularSet S ∪ verticalSingularSet S) : s.im < H

Every union excision centre sits below the ceiling: arc points by their unit norm, vertical points by the height bound on their source set.