The valence formula for level-one modular forms

The textbook valence formula, in orbit-sum form and with no hypothesis beyond f ≠ 0: for a nonzero weight-k modular form on SL₂(ℤ),

ord_∞ f + 1/2 · ord_i f + 1/3 · ord_ρ f + ∑ (non-elliptic orbits q) ord_q f = k / 12.

The proof assembles the two sides of the development. The contour side (FundamentalDomainBoundary/ValencePV.lean) proves the identity for the divisor points of any finite set capturing all zeros of the closed fundamental domain; instantiating it at the canonical divisor set fdZeros discharges both capture hypotheses using mem_fdZeros. The orbit side (Order/OrbitReduction.lean) rewrites the full non-elliptic orbit sum first as the sum over the canonical left representatives and then as the three point-sum families — strict interior, left vertical edge, left half-arc — which are literally the families of the contour identity.

The uniform form, and why it is the one general level needs

Singling out i and ρ is an artefact of level one, where those are the only two elliptic points. The intrinsic statement weights every orbit by the reciprocal 1 / e_P of its elliptic order — the order of its PSL(2, ℤ)-stabiliser, TauCeti.ModularGroup.ellipticOrder — and then reads

∑_{P ∈ SL₂(ℤ) \ ℍ} (1 / e_P) · ord_P f + ord_∞ f = k / 12,

with the 1/2 and the 1/3 produced by e_i = 2 and e_ρ = 3 and every other weight equal to 1. That is valence_formula_weighted below, stated over ℚ because the weights are rational and the two sides are; the level-one shape above is the special case obtained by splitting off the two orbits at which e_P ≠ 1.

The uniform shape is what the general-level formula of the Tau Ceti ModularForms roadmap's Layer 1 milestone "General level — by the coset norm" consumes: there the level-one formula is applied to the norm ∏_{γ ∈ Γ \ SL₂(ℤ)} f ∣[k] γ, and each level-one weight 1 / e_P is redistributed over the Γ-orbits inside the SL₂(ℤ)-orbit of P by a stabiliser count. Only in the uniform form is there a single weight per orbit to redistribute.

Main declarations

• valence_formula (in TauCeti.ModularForm): the valence formula.
• TauCeti.ModularForm.valence_formula_weighted: the uniform form.
• TauCeti.ModularForm.twelve_mul_orderOfVanishingOnOrbit_le_weight_mul_ellipticOrder: the resulting bound 12 · ord_P f ≤ k · e_P on a single orbit, and TauCeti.ModularForm.orderOfVanishingOnOrbit_eq_zero_of_weight_mul_ellipticOrder_lt_twelve, the vanishing-order-zero conclusion it forces when k · e_P < 12.

References

The statement shape follows AINTLIB's valence_formula_textbook_orbit_finsum (github.com/CBirkbeck/AINTLIB, commit 2baa76f742, Apache 2.0, projects/LeanModularForms/LeanModularForms/ForMathlib/ValenceFormula.lean), with its h_core hypothesis discharged by the contour development rather than assumed. The uniform form is the one displayed in the roadmap and follows the divisor-of-automorphic-forms development in Diamond–Shurman, A First Course in Modular Forms, §§3.5–3.6.

theorem TauCeti.ModularForm.valence_formula {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {k : ℤ} [ModularFormClass F (Matrix.SpecialLinearGroup.mapGL ℝ).range k] (f : F) (hf : ⇑f ≠ 0) : ↑(∑ᶠ (q : NonEllipticOrbit), orderOfVanishingOnOrbit f ↑q) + 1 / 2 * ↑(orderOfVanishingAt (⇑f) UpperHalfPlane.I) + 1 / 3 * ↑(orderOfVanishingAt (⇑f) UpperHalfPlane.ρ) + ↑(qExpansionOrderAtCusp 1 ⇑f) = ↑k / 12

The valence formula for weight-k modular forms on SL₂(ℤ): for f ≠ 0, the cusp order, the half-weighted order at i, the third-weighted order at ρ and the orders along the non-elliptic orbits sum to k / 12.

The uniform form, weighted by the elliptic orders

theorem TauCeti.ModularForm.valence_formula_weighted {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {k : ℤ} [ModularFormClass F (Matrix.SpecialLinearGroup.mapGL ℝ).range k] (f : F) (hf : ⇑f ≠ 0) : ∑ᶠ (q : MulAction.orbitRel.Quotient (Matrix.SpecialLinearGroup (Fin 2) ℤ) UpperHalfPlane), weightedOrderOfVanishingOnOrbit f q + ↑(qExpansionOrderAtCusp 1 ⇑f) = ↑k / 12

The valence formula, uniformly over the orbit space. For a nonzero weight-k modular form on SL₂(ℤ), weighting each orbit by the reciprocal of its elliptic order,

∑_{P ∈ SL₂(ℤ) \ ℍ} (1 / e_P) · ord_P f + ord_∞ f = k / 12.

This is valence_formula with the two exceptional orbits absorbed into the general weight: e_i = 2 and e_ρ = 3 restore the 1/2 and the 1/3, and e_P = 1 elsewhere makes every other orbit count once. It is the form the general-level formula redistributes along the norm map, where a single weight per orbit is what a stabiliser count can split.

Consequences for a single orbit

theorem TauCeti.ModularForm.twelve_mul_orderOfVanishingOnOrbit_le_weight_mul_ellipticOrder {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {k : ℤ} [ModularFormClass F (Matrix.SpecialLinearGroup.mapGL ℝ).range k] (f : F) (hf : ⇑f ≠ 0) (q : MulAction.orbitRel.Quotient (Matrix.SpecialLinearGroup (Fin 2) ℤ) UpperHalfPlane) : 12 * orderOfVanishingOnOrbit f q ≤ k * ↑(ModularGroup.ellipticOrder q)

The mass at one orbit is bounded by the total mass: every other term of the uniform valence formula is nonnegative, so 12 · ord_P f ≤ k · e_P for a nonzero form.

theorem TauCeti.ModularForm.orderOfVanishingOnOrbit_eq_zero_of_weight_mul_ellipticOrder_lt_twelve {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {k : ℤ} [ModularFormClass F (Matrix.SpecialLinearGroup.mapGL ℝ).range k] (f : F) {q : MulAction.orbitRel.Quotient (Matrix.SpecialLinearGroup (Fin 2) ℤ) UpperHalfPlane} (hk : k * ↑(ModularGroup.ellipticOrder q) < 12) : orderOfVanishingOnOrbit f q = 0

A small enough weighted degree forces vanishing order zero at an orbit. If f is nonzero, this says that f does not vanish there; the statement also covers the zero form under the convention that its vanishing order is zero.