Orbit-reduction machinery for the valence formula

The valence formula will be proved as an identity over an arbitrary complete divisor set: for every finite S ⊆ 𝒟 catching all nonzero-order points, three sums — over the strict interior, the left vertical edge, and the left half-arc minus ρ — together with the weighted elliptic and cusp terms equal k/12. This file provides the orbit-reduction machinery a future proof of that theorem will need: a canonical set of representatives for the non-elliptic orbits of nonzero order, and the rewriting of a ∑ᶠ over those orbits as the sum over the three representative families.

The reduction picks one representative per non-elliptic orbit of nonzero order inside the canonical set canonicalReps: interior points represent themselves; a right-vertical-edge point is moved to the left edge by z ↦ z - 1; a right-half-arc point is moved to the left half-arc by z ↦ -1/z (TauCeti.ModularGroup.exists_smul_mem_fd_left). Faithfulness is the injectivity of the orbit map on the left part of 𝒟 (TauCeti.ModularGroup.orbit_mk_injOn_fd_left), and the elliptic orbits are excluded by their closed-domain descriptions (orbit_mk_eq_I_iff, orbit_mk_eq_ρ_iff).

Main declarations

• TauCeti.ModularForm.fdZeros: the canonical complete divisor set — the nonzero-order points of the closed fundamental domain of a level-one form, empty for the zero form.
• TauCeti.ModularForm.canonicalReps: one representative per non-elliptic orbit of nonzero order — the strict-interior, left-vertical and left-half-arc points of fdZeros.
• TauCeti.ModularForm.exists_mem_canonicalReps_orbit_mk_eq: every non-elliptic orbit of nonzero order has a representative in canonicalReps.
• TauCeti.ModularForm.finsum_orderOfVanishingOnOrbit_eq_sum_canonicalReps: the ∑ᶠ over the non-elliptic orbit space equals the canonicalReps sum.
• TauCeti.ModularForm.sum_canonicalReps_split: the canonicalReps sum splits into the three family sums of the core identity.

References

• AINTLIB LeanModularForms — the valence-formula development (ForMathlib/Orbits.lean, ForMathlib/CanonicalReps.lean and ForMathlib/ValenceFormula.lean), ported onto the current Mathlib pin. The denominator analysis behind AINTLIB's representative selection is replaced here by Mathlib's classification ModularGroup.cases_of_mem_fd_smul_mem_fd, through the orbit lemmas of TauCeti.NumberTheory.Modular.Orbits.

noncomputable def TauCeti.ModularForm.fdZeros {k : ℤ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] [ModularFormClass F (Matrix.SpecialLinearGroup.mapGL ℝ).range k] (f : F) : Finset UpperHalfPlane

The canonical complete divisor set of a level-one form: the finitely many points of the closed fundamental domain 𝒟 carrying nonzero vanishing order, as a Finset.

No nonvanishing hypothesis — the zero form has order 0 everywhere, so this is empty for it.

Equations

• TauCeti.ModularForm.fdZeros f = ⋯.toFinset

@[simp]

theorem TauCeti.ModularForm.mem_fdZeros {k : ℤ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] [ModularFormClass F (Matrix.SpecialLinearGroup.mapGL ℝ).range k] {f : F} {p : UpperHalfPlane} : p ∈ fdZeros f ↔ p ∈ ModularGroup.fd ∧ orderOfVanishingAt (⇑f) p ≠ 0

Membership in the canonical divisor set: a point of 𝒟 of nonzero order.

noncomputable def TauCeti.ModularForm.canonicalReps {k : ℤ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] [ModularFormClass F (Matrix.SpecialLinearGroup.mapGL ℝ).range k] (f : F) : Finset UpperHalfPlane

One representative per non-elliptic orbit of nonzero order: the points of fdZeros in the strict interior, on the left vertical edge, or on the left half-arc minus ρ. The right vertical edge and right half-arc are omitted — z ↦ z - 1 and z ↦ -1/z move them onto the left representatives — and the elliptic points are excluded by all three filters.

Equations

• TauCeti.ModularForm.canonicalReps f = {p ∈ TauCeti.ModularForm.fdZeros f | 1 < ‖↑p‖ ∧ |(↑p).re| < 1 / 2 ∨ (↑p).re = -(1 / 2) ∧ 1 < ‖↑p‖ ∨ ↑p ≠ ↑UpperHalfPlane.ρ ∧ ‖↑p‖ = 1 ∧ (↑p).re < 0}

@[simp]

theorem TauCeti.ModularForm.mem_canonicalReps {k : ℤ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] [ModularFormClass F (Matrix.SpecialLinearGroup.mapGL ℝ).range k] {f : F} {p : UpperHalfPlane} : p ∈ canonicalReps f ↔ p ∈ fdZeros f ∧ (1 < ‖↑p‖ ∧ |(↑p).re| < 1 / 2 ∨ (↑p).re = -(1 / 2) ∧ 1 < ‖↑p‖ ∨ ↑p ≠ ↑UpperHalfPlane.ρ ∧ ‖↑p‖ = 1 ∧ (↑p).re < 0)

Membership in the canonical representatives: a point of fdZeros in the strict interior, on the left vertical edge, or on the left half-arc minus ρ.

theorem TauCeti.ModularForm.orbit_mk_ne_I_and_ne_ρ_of_mem_canonicalReps {k : ℤ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] [ModularFormClass F (Matrix.SpecialLinearGroup.mapGL ℝ).range k] {f : F} {p : UpperHalfPlane} (hp : p ∈ canonicalReps f) : Quotient.mk'' p ≠ Quotient.mk'' UpperHalfPlane.I ∧ Quotient.mk'' p ≠ Quotient.mk'' UpperHalfPlane.ρ

The canonical representatives lie in the non-elliptic orbits.

theorem TauCeti.ModularForm.orbit_mk_injOn_canonicalReps {k : ℤ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] [ModularFormClass F (Matrix.SpecialLinearGroup.mapGL ℝ).range k] (f : F) : Set.InjOn (fun (p : UpperHalfPlane) => Quotient.mk'' p) ↑(canonicalReps f)

The orbit map is injective on the canonical representatives, which lie left of the boundary identifications of 𝒟.

theorem TauCeti.ModularForm.exists_mem_canonicalReps_orbit_mk_eq {k : ℤ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] [ModularFormClass F (Matrix.SpecialLinearGroup.mapGL ℝ).range k] {f : F} {q : MulAction.orbitRel.Quotient (Matrix.SpecialLinearGroup (Fin 2) ℤ) UpperHalfPlane} (hqI : q ≠ Quotient.mk'' UpperHalfPlane.I) (hqρ : q ≠ Quotient.mk'' UpperHalfPlane.ρ) (hq : orderOfVanishingOnOrbit f q ≠ 0) : ∃ p ∈ canonicalReps f, Quotient.mk'' p = q

Every non-elliptic orbit of nonzero order has a representative among the canonical ones.

theorem TauCeti.ModularForm.finsum_orderOfVanishingOnOrbit_eq_sum_canonicalReps {k : ℤ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] [ModularFormClass F (Matrix.SpecialLinearGroup.mapGL ℝ).range k] (f : F) : ∑ᶠ (q : NonEllipticOrbit), orderOfVanishingOnOrbit f ↑q = ∑ p ∈ canonicalReps f, orderOfVanishingAt (⇑f) p

The ∑ᶠ over the non-elliptic orbit space equals the sum over the canonical representatives: the orbit map matches canonicalReps bijectively with the non-elliptic orbits of nonzero order, and the order is orbit-constant.

theorem TauCeti.ModularForm.sum_canonicalReps_split {k : ℤ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] [ModularFormClass F (Matrix.SpecialLinearGroup.mapGL ℝ).range k] (f : F) : ∑ p ∈ canonicalReps f, orderOfVanishingAt (⇑f) p = ∑ p ∈ fdZeros f with 1 < ‖↑p‖ ∧ |(↑p).re| < 1 / 2, orderOfVanishingAt (⇑f) p + ∑ p ∈ fdZeros f with (↑p).re = -(1 / 2) ∧ 1 < ‖↑p‖, orderOfVanishingAt (⇑f) p + ∑ p ∈ fdZeros f with ↑p ≠ ↑UpperHalfPlane.ρ ∧ ‖↑p‖ = 1 ∧ (↑p).re < 0, orderOfVanishingAt (⇑f) p

The canonical-representative sum splits into the three family sums of the core identity: strict interior, left vertical edge, and left half-arc minus ρ.