Pairing the boundary divisor points of the fundamental domain

The boundary of the fundamental domain is identified with itself in pairs: z ↦ z + 1 carries the left vertical edge onto the right one, and z ↦ -1/z swaps the two halves of the unit arc, fixing i and exchanging the two ρ-corners. A slash-invariant form has the same vanishing order at paired points, so — over a divisor set that is complete for the closed fundamental domain 𝒟 — each right-half order sum equals its left-half partner, and the full non-elliptic boundary sum is twice the sum over left representatives.

These are the bookkeeping identities that turn the winding-weighted boundary count of the valence formula (each non-elliptic boundary point carries weight -1/2) into a sum with one full-weight representative per pair.

Main results

• TauCeti.ModularForm.sum_orderOfVanishingAt_rightVertical_eq_leftVertical: the vertical pairing.
• TauCeti.ModularForm.sum_orderOfVanishingAt_rightArc_eq_leftArc: the arc pairing.
• TauCeti.ModularForm.sum_orderOfVanishingAt_rightArc_ne_ρ_add_one_eq_leftArc_ne_ρ: the arc pairing with the two ρ-corners removed.
• sum_orderOfVanishingAt_nonEllipticBoundary_eq_verticals_add_arcs (in TauCeti.ModularForm): the order sum over the non-elliptic boundary points splits into the four half-edge sums.
• TauCeti.ModularForm.sum_orderOfVanishingAt_nonEllipticBoundary_eq_two_mul: the non-elliptic boundary sum is twice the left-representative sum.

References

• AINTLIB LeanModularForms — the valence-formula development (ForMathlib/OrbitPairing.lean and the partition lemmas of ForMathlib/CoreIdentityProof.lean), ported onto the current Mathlib pin.

theorem TauCeti.ModularForm.sum_orderOfVanishingAt_rightVertical_eq_leftVertical {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {S : Finset UpperHalfPlane} (f : F) (hper : Function.Periodic (⇑f ∘ ↑UpperHalfPlane.ofComplex) 1) (hS : ∀ p ∈ S, orderOfVanishingAt (⇑f) p ≠ 0 → p ∈ ModularGroup.fd) (hcomp : ∀ p ∈ ModularGroup.fd, orderOfVanishingAt (⇑f) p ≠ 0 → p ∈ S) : ∑ p ∈ S with (↑p).re = 1 / 2 ∧ 1 < ‖↑p‖, orderOfVanishingAt (⇑f) p = ∑ p ∈ S with (↑p).re = -(1 / 2) ∧ 1 < ‖↑p‖, orderOfVanishingAt (⇑f) p

The vertical pairing. Over a divisor set complete for the closed fundamental domain, the order sum along the right vertical edge equals the order sum along the left one.

theorem TauCeti.ModularForm.sum_orderOfVanishingAt_rightArc_eq_leftArc {k : ℤ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} {S : Finset UpperHalfPlane} [SlashInvariantFormClass F (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k] (f : F) (hSmem : ModularGroup.S ∈ Γ) (hS : ∀ p ∈ S, orderOfVanishingAt (⇑f) p ≠ 0 → p ∈ ModularGroup.fd) (hcomp : ∀ p ∈ ModularGroup.fd, orderOfVanishingAt (⇑f) p ≠ 0 → p ∈ S) : ∑ p ∈ S with ‖↑p‖ = 1 ∧ 0 < (↑p).re, orderOfVanishingAt (⇑f) p = ∑ p ∈ S with ‖↑p‖ = 1 ∧ (↑p).re < 0, orderOfVanishingAt (⇑f) p

The arc pairing. Over a divisor set complete for the closed fundamental domain, the order sum along the right half of the unit arc equals the order sum along the left half: z ↦ -1/z matches the two halves point by point — carrying ρ + 1 to ρ — and slash-invariance carries the order across.

theorem TauCeti.ModularForm.sum_orderOfVanishingAt_rightArc_ne_ρ_add_one_eq_leftArc_ne_ρ {k : ℤ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} {S : Finset UpperHalfPlane} [SlashInvariantFormClass F (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k] (f : F) (hper : Function.Periodic (⇑f ∘ ↑UpperHalfPlane.ofComplex) 1) (hSmem : ModularGroup.S ∈ Γ) (hS : ∀ p ∈ S, orderOfVanishingAt (⇑f) p ≠ 0 → p ∈ ModularGroup.fd) (hcomp : ∀ p ∈ ModularGroup.fd, orderOfVanishingAt (⇑f) p ≠ 0 → p ∈ S) : ∑ p ∈ S with ↑p ≠ ↑UpperHalfPlane.ρ + 1 ∧ ‖↑p‖ = 1 ∧ 0 < (↑p).re, orderOfVanishingAt (⇑f) p = ∑ p ∈ S with ↑p ≠ ↑UpperHalfPlane.ρ ∧ ‖↑p‖ = 1 ∧ (↑p).re < 0, orderOfVanishingAt (⇑f) p

The arc pairing with the two ρ-corners removed: the pairing map matches them with each other, so deleting one from each half preserves the identity. This is the shape the valence formula consumes, whose arc family excludes the corner it weights separately.

theorem TauCeti.ModularForm.mem_boundary_iff {p : UpperHalfPlane} (hp : p ∈ ModularGroup.fd) : ↑p ∉ {Complex.I, ↑UpperHalfPlane.ρ, ↑UpperHalfPlane.ρ + 1} ∧ ¬(1 < ‖↑p‖ ∧ |(↑p).re| < 1 / 2) ↔ (↑p).re = 1 / 2 ∧ 1 < ‖↑p‖ ∨ (↑p).re = -(1 / 2) ∧ 1 < ‖↑p‖ ∨ ↑p ≠ ↑UpperHalfPlane.ρ + 1 ∧ ‖↑p‖ = 1 ∧ 0 < (↑p).re ∨ ↑p ≠ ↑UpperHalfPlane.ρ ∧ ‖↑p‖ = 1 ∧ (↑p).re < 0

The pointwise boundary classification. A point of 𝒟 avoids the three elliptic points and the open fundamental domain exactly when it lies on one of the four half-edges.

theorem TauCeti.ModularForm.sum_orderOfVanishingAt_nonEllipticBoundary_eq_verticals_add_arcs {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {S : Finset UpperHalfPlane} (f : F) (hS : ∀ p ∈ S, orderOfVanishingAt (⇑f) p ≠ 0 → p ∈ ModularGroup.fd) : ∑ p ∈ S with ↑p ∉ {Complex.I, ↑UpperHalfPlane.ρ, ↑UpperHalfPlane.ρ + 1} ∧ ¬(1 < ‖↑p‖ ∧ |(↑p).re| < 1 / 2), orderOfVanishingAt (⇑f) p = ∑ p ∈ S with (↑p).re = 1 / 2 ∧ 1 < ‖↑p‖, orderOfVanishingAt (⇑f) p + ∑ p ∈ S with (↑p).re = -(1 / 2) ∧ 1 < ‖↑p‖, orderOfVanishingAt (⇑f) p + ∑ p ∈ S with ↑p ≠ ↑UpperHalfPlane.ρ + 1 ∧ ‖↑p‖ = 1 ∧ 0 < (↑p).re, orderOfVanishingAt (⇑f) p + ∑ p ∈ S with ↑p ≠ ↑UpperHalfPlane.ρ ∧ ‖↑p‖ = 1 ∧ (↑p).re < 0, orderOfVanishingAt (⇑f) p

The boundary partition. A non-elliptic point of the closed fundamental domain that is not strictly interior lies on exactly one of the four half-edges — the two verticals and the two open arc halves — so the order sum over the non-elliptic boundary splits into the four half-edge sums.

theorem TauCeti.ModularForm.sum_orderOfVanishingAt_nonEllipticBoundary_eq_two_mul {k : ℤ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} {S : Finset UpperHalfPlane} [SlashInvariantFormClass F (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k] (f : F) (hper : Function.Periodic (⇑f ∘ ↑UpperHalfPlane.ofComplex) 1) (hSmem : ModularGroup.S ∈ Γ) (hS : ∀ p ∈ S, orderOfVanishingAt (⇑f) p ≠ 0 → p ∈ ModularGroup.fd) (hcomp : ∀ p ∈ ModularGroup.fd, orderOfVanishingAt (⇑f) p ≠ 0 → p ∈ S) : ∑ p ∈ S with ↑p ∉ {Complex.I, ↑UpperHalfPlane.ρ, ↑UpperHalfPlane.ρ + 1} ∧ ¬(1 < ‖↑p‖ ∧ |(↑p).re| < 1 / 2), orderOfVanishingAt (⇑f) p = 2 * (∑ p ∈ S with (↑p).re = -(1 / 2) ∧ 1 < ‖↑p‖, orderOfVanishingAt (⇑f) p + ∑ p ∈ S with ↑p ≠ ↑UpperHalfPlane.ρ ∧ ‖↑p‖ = 1 ∧ (↑p).re < 0, orderOfVanishingAt (⇑f) p)

The boundary sum collapses to left representatives. Over a divisor set complete for the closed fundamental domain, the order sum across all non-elliptic boundary points is twice the sum over one representative per pair — the left vertical and the left arc half without its corner. Each boundary point carries winding weight -1/2 in the valence count, so this is the step that gives each pair a single full-weight representative.