Higher-weight Gamma1 cusp forms satisfy the dimension-formula lower bound

Proved

MTT.Cohomology.gammaOne_cuspForm_dimension_lower_bound

by cbirkbeck · Sep 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

dimensionmodular-formsmtt

Let $N\ge 5$ and $k\ge 3$ be natural numbers. Put $\mu=[\mathrm{SL}_2(\mathbb Z):\langle\Gamma_1(N),-I\rangle]$ and let $c$ be the cardinality of $\Gamma_1(N)\backslash\mathrm{SL}_2(\mathbb Z)/\langle T,-I\rangle$ , where $T$ is the translation matrix. Then the complex vector space of weight- $k$ cusp forms satisfies

(k-1)\mu\le 12\dim_{\mathbb C}S_k(\Gamma_1(N))+6c.

This is the lower-bound direction of the torsion-free, regular-cusp dimension formula. It is independent of the MTT period-map injectivity proof and supplies the analytic dimension input for the higher-level parabolic-cohomology upper-bound strategy. No cohomology bound or equality of dimensions is asserted.

Preamble

import Mathlib
open scoped MatrixGroups

Formal statement

theorem MTT.Cohomology.gammaOne_cuspForm_dimension_lower_bound {N k : ℕ} (hN : 5 ≤ N) (hk : 3 ≤ k) :
    (k - 1) * (CongruenceSubgroup.Gamma1 N ⊔ Subgroup.zpowers (-1 : SL(2, ℤ))).index ≤
      12 * Module.finrank ℂ (CuspForm (CongruenceSubgroup.Gamma1 N) (k : ℤ)) +
        6 * Nat.card (DoubleCoset.Quotient (CongruenceSubgroup.Gamma1 N : Set SL(2, ℤ))
          ((Subgroup.zpowers ModularGroup.T ⊔ Subgroup.zpowers (-1) : Subgroup SL(2, ℤ)) :
            Set SL(2, ℤ))) := by sorry

Source

William Stein, Modular Forms: A Computational Approach, Chapter 6, Proposition 6.6, N>=5 and k>=3 case, together with the genus formula immediately preceding that proposition: https://wstein.org/books/modform/modform/dimension_formulas.html#modular-forms-for-gamma-1-n. This is only the lower-bound direction after clearing denominators. The proof reuses the Prove2Me theorem ModularForm.exists_linearIndependent_gamma1_dimFormula_le_card (e52e7754-dd59-54dc-8282-e638ce354cfe), and a separately proved cusp-codimension bound.

View graph