The level-three cusp-form dimension lower bound

Proved

MTT.Cohomology.cuspForm_finrank_lower_bound_level_three

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

modular-formsnumber-theory

For every integer $k\ge3$ , the cusp-form space of $\Gamma_1(3)$ satisfies

\left\lfloor\frac{k}{3}\right\rfloor-1\le\dim_{\mathbf C}S_k(\Gamma_1(3)).

This is the lower-bound consequence of the level-three dimension formula, valid in both parities. In odd weight it combines with the numeric parabolic cohomology estimate to supply the remaining level-three MTT dimension comparison.

Preamble

import Definitions.Def_MTT_ParabolicCohomology
import Mathlib.LinearAlgebra.FiniteDimensional.Defs

Formal statement

theorem MTT.Cohomology.cuspForm_finrank_lower_bound_level_three {k : ℕ}
    (hk : 3 ≤ k) :
    k / 3 - 1 ≤ Module.finrank ℂ (CuspForm (MTT.GammaOne 3) (k : ℤ)) := by sorry

Source

William Stein, Modular Forms: A Computational Approach, Chapter 6, Proposition 6.6, https://wstein.org/books/modform/modform/dimension_formulas.html . Specialize to N=3: g1=0, c1=2, a=-1, and the elliptic term is floor(k/3), giving dim S_k=floor(k/3)-1 for k>=3. Supporting input for MTT frontier 03513b57-2878-4a4a-8605-3db4bbbcae31.

View graph