Odd-weight cusp-form lower bound at level four

Proved

MTT.Cohomology.cuspForm_finrank_lower_bound_level_four_odd

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

modular-formsnumber-theory

For every odd integer $k\ge3$ , the space $S_k(\Gamma_1(4))$ of holomorphic cusp forms satisfies

k-3\le 2\dim_{\mathbf C}S_k(\Gamma_1(4)).

This is the lower-bound consequence of the level-four odd-weight dimension formula $\dim S_k=(k-3)/2$ . The irregular-cusp correction is essential at this level. Together with the two-generator cohomology estimate, this completes the level-four odd-weight dimension comparison needed by MTT.

Preamble

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

Formal statement

theorem MTT.Cohomology.cuspForm_finrank_lower_bound_level_four_odd {k : ℕ}
    (hk : 3 ≤ k) (hko : Odd k) :
    k - 3 ≤ 2 * Module.finrank ℂ (CuspForm (MTT.GammaOne 4) (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#modular-forms-for-gamma-1-n . Specialize to N=4, odd k>=3: g1=0, c1=3, and the additional 1/2 term gives (k-3)/2. Supporting analytic input for MTT frontier c2c1a34b-7bfe-4fff-8533-9266b78c666a.

View graph