Orbit Pairing Lemmas for the Valence Formula

Pure-algebra lemmas about orbit pairings under the modular group actions T (z ↦ z + 1) and S (z ↦ -1/z). These collapse the explicit coefficient expansion of the valence formula, pairing left/right vertical and arc contributions.

Main results

• sum_ord_rightVert_eq_sum_ord_leftVert: Orders on right vertical edge equal orders on left.
• sum_ord_rightArc_eq_sum_ord_leftArc: Orders on right arc equal orders on left arc.

theorem vAdd_one_coe (p : UpperHalfPlane) : ↑(1 +ᵥ p) = ↑p + 1

Coercion identity for T-translation: ((1 : ℝ) +ᵥ p : ℂ) = (p : ℂ) + 1.

theorem vAdd_one_re (p : UpperHalfPlane) : (1 +ᵥ p).re = p.re + 1

T-translation shifts real part by 1.

theorem vAdd_one_im_eq (p : UpperHalfPlane) : (1 +ᵥ p).im = p.im

T-translation preserves imaginary part.

theorem vAdd_neg_one_coe (p : UpperHalfPlane) : ↑(-1 +ᵥ p) = ↑p - 1

T⁻¹-translation coercion: ((-1 : ℝ) +ᵥ p : ℂ) = (p : ℂ) - 1.

theorem vAdd_neg_one_re (p : UpperHalfPlane) : (-1 +ᵥ p).re = p.re - 1

T⁻¹-translation shifts real part by -1.

theorem vAdd_neg_one_im_eq (p : UpperHalfPlane) : (-1 +ᵥ p).im = p.im

T⁻¹-translation preserves imaginary part.

theorem norm_add_one_eq_of_re_neg_half (z : ℂ) (hre : z.re = -1 / 2) : ‖z + 1‖ = ‖z‖

T-translation preserves norm for left-vertical points (re = -1/2).

theorem norm_sub_one_eq_of_re_half (z : ℂ) (hre : z.re = 1 / 2) : ‖z - 1‖ = ‖z‖

T⁻¹-translation preserves norm for right-vertical points (re = 1/2).

theorem vAdd_one_norm_eq_of_re_neg_half (p : UpperHalfPlane) (hre : (↑p).re = -1 / 2) : ‖↑(1 +ᵥ p)‖ = ‖↑p‖

T-translation preserves norm for UpperHalfPlane points with re = -1/2.

theorem vAdd_neg_one_norm_eq_of_re_half (p : UpperHalfPlane) (hre : (↑p).re = 1 / 2) : ‖↑(-1 +ᵥ p)‖ = ‖↑p‖

T⁻¹-translation preserves norm for UpperHalfPlane points with re = 1/2.

theorem vAdd_one_mem_fd_of_left_vert (p : UpperHalfPlane) (hp_fd : p ∈ ModularGroup.fd) (hre : (↑p).re = -1 / 2) : 1 +ᵥ p ∈ ModularGroup.fd

T-translation sends left-vertical FD points to 𝒟.

theorem vAdd_neg_one_mem_fd_of_right_vert (p : UpperHalfPlane) (hp_fd : p ∈ ModularGroup.fd) (hre : (↑p).re = 1 / 2) : -1 +ᵥ p ∈ ModularGroup.fd

T⁻¹-translation sends right-vertical FD points to 𝒟.

theorem vAdd_one_rho_eq_rho_plus_one : 1 +ᵥ ellipticPointRho' = ellipticPointRhoPlusOne'

(1 : ℝ) +ᵥ ρ' = ρ'+1 as UpperHalfPlane elements.

theorem vAdd_neg_one_rho_plus_one_eq_rho : -1 +ᵥ ellipticPointRhoPlusOne' = ellipticPointRho'

(-1 : ℝ) +ᵥ (ρ'+1) = ρ' as UpperHalfPlane elements.

theorem ellipticPointRhoPlusOne_mem_fd : ellipticPointRhoPlusOne' ∈ ModularGroup.fd

ρ+1 is in the standard fundamental domain 𝒟.

theorem ord_rho_plus_one_eq_ord_rho_via_vAdd {k : ℤ} (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) : orderOfVanishingAt' (⇑f) ellipticPointRhoPlusOne' = orderOfVanishingAt' (⇑f) ellipticPointRho'

ord(f, ρ+1) = ord(f, ρ) via the T-translation identity.

theorem S_smul_coe (p : UpperHalfPlane) : ↑(ModularGroup.S • p) = (-↑p)⁻¹

S-action coe: (S·z : ℂ) = (-z)⁻¹.

theorem S_smul_norm_of_unit (p : UpperHalfPlane) (hp : ‖↑p‖ = 1) : ‖↑(ModularGroup.S • p)‖ = 1

S-action preserves norm on the unit circle.

theorem S_smul_re_neg_of_unit (p : UpperHalfPlane) (hp : ‖↑p‖ = 1) : (ModularGroup.S • p).re = -p.re

S-action negates real part on the unit circle.

theorem S_smul_mem_fd_of_unit (p : UpperHalfPlane) (hp_fd : p ∈ ModularGroup.fd) (hp_norm : ‖↑p‖ = 1) : ModularGroup.S • p ∈ ModularGroup.fd

S-action preserves 𝒟 for unit-circle points.

noncomputable def sLeftVert (S : Finset UpperHalfPlane) : Finset UpperHalfPlane

The left-vertical filter of S: points with re = -1/2 and ‖p‖ > 1.

Equations

• sLeftVert S = {p ∈ S | (↑p).re = -1 / 2 ∧ ‖↑p‖ > 1}

noncomputable def sRightVert (S : Finset UpperHalfPlane) : Finset UpperHalfPlane

The right-vertical filter of S: points with re = 1/2 and ‖p‖ > 1.

Equations

• sRightVert S = {p ∈ S | (↑p).re = 1 / 2 ∧ ‖↑p‖ > 1}

theorem vAdd_one_leftVert_subset_rightVert {k : ℤ} (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) (S : Finset UpperHalfPlane) (hS_complete : ∀ p ∈ ModularGroup.fd, orderOfVanishingAt' (⇑f) p ≠ 0 → p ∈ S) (p : UpperHalfPlane) : p ∈ sLeftVert S → orderOfVanishingAt' (⇑f) p ≠ 0 → 1 +ᵥ p ∈ sRightVert S

T-translation maps sLeftVert S into sRightVert S.

theorem sum_ord_leftVert_eq_sum_T_image {k : ℤ} (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) (S : Finset UpperHalfPlane) : ∑ p ∈ sLeftVert S, ↑(orderOfVanishingAt' (⇑f) p) = ∑ p ∈ sLeftVert S, ↑(orderOfVanishingAt' (⇑f) (1 +ᵥ p))

Left-vertical sum equals sum of T-translated orders.

theorem ord_vAdd_neg_one_eq {k : ℤ} (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) (p : UpperHalfPlane) : orderOfVanishingAt' (⇑f) (-1 +ᵥ p) = orderOfVanishingAt' (⇑f) p

T⁻¹-invariance of vanishing order: ord(f, (-1)+ᵥp) = ord(f, p).

noncomputable def sLeftArc (S : Finset UpperHalfPlane) : Finset UpperHalfPlane

The left-arc filter: points on the unit circle with negative real part.

Equations

• sLeftArc S = {p ∈ S | ‖↑p‖ = 1 ∧ (↑p).re < 0}

noncomputable def sRightArc (S : Finset UpperHalfPlane) : Finset UpperHalfPlane

The right-arc filter: points on the unit circle with positive real part.

Equations

• sRightArc S = {p ∈ S | ‖↑p‖ = 1 ∧ (↑p).re > 0}

theorem S_smul_S_smul (p : UpperHalfPlane) : ModularGroup.S • ModularGroup.S • p = p

S² acts as the identity on ℍ.

theorem S_smul_injective : Function.Injective fun (x : UpperHalfPlane) => ModularGroup.S • x

The S-action is injective on ℍ.

theorem sum_ord_rightVert_eq_sum_ord_leftVert {k : ℤ} (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) (S : Finset UpperHalfPlane) (hS : ∀ p ∈ S, p ∈ ModularGroup.fd) (hS_complete : ∀ p ∈ ModularGroup.fd, orderOfVanishingAt' (⇑f) p ≠ 0 → p ∈ S) : ∑ p ∈ sRightVert S, ↑(orderOfVanishingAt' (⇑f) p) = ∑ p ∈ sLeftVert S, ↑(orderOfVanishingAt' (⇑f) p)

Orders on right vertical edge equal orders on left vertical edge.

theorem sum_ord_rightArc_eq_sum_ord_leftArc {k : ℤ} (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) (S : Finset UpperHalfPlane) (hS : ∀ p ∈ S, p ∈ ModularGroup.fd) (hS_complete : ∀ p ∈ ModularGroup.fd, orderOfVanishingAt' (⇑f) p ≠ 0 → p ∈ S) : ∑ p ∈ sRightArc S, ↑(orderOfVanishingAt' (⇑f) p) = ∑ p ∈ sLeftArc S, ↑(orderOfVanishingAt' (⇑f) p)

Orders on right arc equal orders on left arc (via S-action).