bp_S2_Gamma0_2_zero
Provedgeometrynumber-theoryopen-problem
The space of weight-2 cusp forms of level Γ₀(2) is zero. Classically: the modular curve X₀(2) has genus 0, so there are no weight-2 cusp forms. Provable without modular-curve geometry via the norm map to level 1: for f ∈ S₂(Γ₀(2)), the norm ∏_{γ ∈ Γ(1)/Γ₀(2)} f|[2]γ lies in S₆(Γ(1)) (the index is 3), and S₆(Γ(1)) = 0 because f² ∈ S₁₂(Γ(1)) = ℂ·Δ forces f² = cΔ with c = 0 (f² vanishes to order ≥ 2 at i∞, Δ to order exactly 1). One of the four pillars of Fermat's Last Theorem, and the only one currently within reach.
Preamble
import Mathlib.NumberTheory.ModularForms.Basic import Mathlib.NumberTheory.ModularForms.CongruenceSubgroups import Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
Formal statement
theorem bp_S2_Gamma0_2_zero (f : CuspForm (CongruenceSubgroup.Gamma0 2) 2) : f = 0 := by sorry
Source