Strong Multiplicity One — Lean blueprint

 Strong Multiplicity One — Lean blueprint🔗

Compiled2026-06-24T22:07:19ZProjecte84e276fSMO blueprint: add Hecke char-space, coeff/eigenvalue, old/new decomposition + proof sketchesLeanleanprover/lean4:v4.31.0-rc2VersoBlueprintv4.30.0@10305089592cMathlibd90090f647ca

This is the blueprint for the LeanModularForms formalisation of strong multiplicity one for cusp forms (Miyake, Modular Forms, Theorems 4.6.8 and 4.6.12): a newform is determined by all but finitely many of its Hecke eigenvalues. The development is built on an abstract \mathrm{GL}_2 Hecke-ring / newform theory (HeckeRing.GL2), and the headline \texttt{strongMultiplicityOne\_axiom\_clean} is sorry-free and axiom-clean.

Each node carries a (lean := …) reference to the actual declaration in the LeanModularForms library, so Verso reads its completion status directly from Lean, and its prose cites the corresponding numbered result in Miyake (Chapter 4 — Hecke operators in §4.5, newforms and strong multiplicity one in §4.6). The dependency graph at the foot of the page records the logical spine.

Contents

  1. 1. Hecke operators, diamond operators, and character spaces
  2. 2. Eigenforms and eigenvalue systems
  3. 3. The coefficient–eigenvalue relation
  4. 4. Degeneracy maps and the old/new decomposition
  5. 5. Multiplicity one (the Main Lemma)
  6. 6. Strong multiplicity one
  7. 7. Dependency graph
  8. Dependency Graph
  9. 8. Progress summary
  10. Blueprint Summary