$S_k(\mathrm{SL}_2(\mathbb{Z}))=0$ for $k<12$

Vanishing of level-one cusp forms of weight below 12.

Write $\Gamma(1)=\mathrm{SL}_2(\mathbb Z)$ for the full modular group acting on the upper half plane $\mathbb H$, and for $k\in\mathbb Z$ let $S_k(\Gamma(1))$ be the space of weight-$k$ cusp forms of level one: holomorphic functions $f:\mathbb H\to\mathbb C$ satisfying

and vanishing at the cusp, i.e. $f(\tau)\to 0$ as $\operatorname{Im}\tau\to\infty$. The claim is that this space is trivial in every weight below 12:

The bound is sharp: $S_{12}(\Gamma(1))$ is one-dimensional, spanned by the discriminant form $\Delta$.

Why it is true. For $k<0$ there are no nonzero holomorphic modular forms at all, and for odd $k$ evaluating the transformation law at $-I$ forces $f=-f$. The remaining cases $k\in\{0,2,4,6,8,10\}$ are the substance, and the standard argument is the valence formula: a nonzero $f\in M_k(\Gamma(1))$ satisfies

the sum running over the remaining points of $\Gamma(1)\backslash\mathbb H$. A cusp form has $\operatorname{ord}_\infty f\ge 1$, so a nonzero element of $S_k(\Gamma(1))$ would force $k\ge 12$. Equivalently, multiplication by $\Delta$ identifies $S_k(\Gamma(1))$ with $M_{k-12}(\Gamma(1))$, which vanishes for $k-12<0$.

Formalization notes. Here the level-one group is the image of $\mathrm{SL}_2(\mathbb Z)$ in $\mathrm{GL}_2(\mathbb R)$, written 𝒮ℒ, which is what Mathlib's CuspForm API takes as its group argument. The statement is phrased as "every element of the space is zero" rather than as a rank computation, so that it applies directly to a given form. The corresponding result upstream in Mathlib is CuspForm.rank_eq_zero_of_weight_lt_twelve, proved there from the discriminant isomorphism CuspForm.discriminantEquiv : CuspForm 𝒮ℒ k ≃ₗ[ℂ] ModularForm 𝒮ℒ (k - 12) together with ModularForm.levelOne_neg_weight_rank_zero. That machinery — the discriminant form and the order of its $q$-expansion — is not present in this environment's Mathlib, so it has to be built or ported.