funlean.
Step 48 / 64

Proof level

A room with no guest

One theorem proves that every cusp form in one weight-and-level space is zero.

Start with a concrete example

An allowed collection can contain just the zero function. Then it is not empty, but it contains no nonzero function. Compare the box {0} with an empty box: those are different.

A small check: try the idea

Think with the concrete example above. You can try again.

Is the collection {0} empty?

Read the answer and reasoning

No; it contains 0, but no nonzero element. Distinguish an empty box from a box containing a zero card. The vanishing argument excludes nonzero forms, not the zero form.

Build the idea in three steps

  1. This theorem concerns exactly one locked room: CuspForm (CongruenceSubgroup.Gamma0 2) 2, the cusp forms of weight two at level two.
  2. It states that every guest of that room is the zero function: for every f of this type, f = 0. The whole space collapses to its single zero element.
  3. Later chapters use this theorem to rule out a nonzero cusp form in that exact space. Zero itself remains: the absence is specifically the absence of nonzero forms.

A small example

The zero function itself is a cusp form, so the space is not nothing — it is the one-element set {0}. The argument only needs someone nonzero, and there is none.

Use in Lean · original excerpt

FLT · aa2d8b3 · Thm_ModularForm_S2_Gamma0_2_eq_zero.lean

theorem ModularForm.S2_Gamma0_2_eq_zero (f : CuspForm (CongruenceSubgroup.Gamma0 2) 2) : f = 0 := by p2m_exact_reverting @_root_.P2MW.S_ModularForm_S2_Gamma0_2_eq_zero.solution

How to read this Lean

The type fixes both the level and the weight in its name. The proof term delegates to a separately checked solution of the upstream project, so this page displays the statement; it does not re-run the larger argument.

Original source ↗ · L13–13Open the complete saved source

Where this idea is used

15. The concert of absolute silence16. The room with no room
I’m lost · Help

Mika’s help desk

A room with no guest

One thing at a time

Read the three explanation steps first. The Lean source is there for a closer look afterwards; you do not have to read it first.

In simpler words

One theorem proves that every cusp form in one weight-and-level space is zero.

Earlier ideas are listed under “Start with these ideas” on this page.

A small clue

The zero function itself is a cusp form, so the space is not nothing — it is the one-element set {0}. The argument only needs someone nonzero, and there is none.

Close this panel to return to the exact place you were reading. These are prepared hints for this page.

Start with the first small story →