A nonzero weight-five cusp form on Gamma1(4)

Proved

MTT.Cohomology.exists_nonzero_cuspForm_weight_five_level_four

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

modular-formsnumber-theory

The weight-five cusp-form space of $\Gamma_1(4)$ is nonzero:

S_5(\Gamma_1(4))\ne0.

A witness is $D(z)=\eta(z)^4\eta(2z)^2\eta(4z)^4$ . This supplies the cuspidal seed for the odd-weight level-four MTT dimension estimate. The assertion is on $\Gamma_1(4)$ and does not claim an odd-weight form with trivial character on $\Gamma_0(4)$ .

Preamble

import Definitions.Def_MTT_Arithmetic

Formal statement

theorem MTT.Cohomology.exists_nonzero_cuspForm_weight_five_level_four :
    ∃ D : CuspForm (MTT.GammaOne 4) 5, D ≠ 0 := by sorry

Source

Explicit eta-product construction for MTT seed theorem 9af94959-aa50-47b9-85f6-e2ab387a3d8e. Transformation identities adapted with attribution from accepted proof 9f9d7099-dd4e-5af0-8131-7c3e5d2d1482 (anthropics/fermats-last-theorem, commit aa2d8b34692b16c70f699536de0d8e75b9a3e9ef). Cuspidality of the square uses Proved CuspForm.exists_gamma0_four_apply_eq_eta_pow_mul, theorem 90051634-9f66-535b-b6be-e9977b9d4dee, at exponents (8,4,8). The Gamma1(4) generator argument and square-root transfer are proved in the submitted file.

View graph