Add roadmap: Modular forms — Hecke theory, newforms, and L-functions

[CBirkbeck]

Adds a roadmap under TauCetiRoadmap/ModularForms/ (README + Suggested.lean): the classical
arithmetic theory of modular forms on top of Mathlib's analytic foundation. It supersedes the
closed #36, rewritten to be self-contained and grounded all the way down.

What it covers (Layers 0–11). Diamond operators and modular forms with character (nebentypus)
→ the valence formula at general level → the Hecke algebra → the Petersson inner product →
newforms and strong multiplicity one → Atkin–Lehner/Fricke → L-functions (Euler product,
functional equation) → the coefficient field is a number field → the LMFDB invariants → the
modular curve as the analytic quotient Γ\ℍ and the dimension formulas by the
valence/counting route → the level-one Eichler–Selberg trace formula. The modular curve is the compactified analytic quotient — no functor, no
representability, no moduli problem — and the cusp/elliptic-point counts and genus of Γ\ℍ are
built analytically within the roadmap.

Notes

• Character spaces (Layer 0) are defined exactly as in AINTLIB: the simultaneous
  χ-eigenspace of the slash-defined diamond operators inside M_k(Γ₁(N)) (modFormCharSpace,
  a Submodule), with the classical transformation law as a bridge theorem
  (modFormCharSpace_iff_nebentypus) and the proved internal DirectSum.IsInternal nebentypus
  decomposition migrated as-is — not re-founded via a character-twisted slash action.
• Hecke algebra (Layer 2) consumes Mathlib's new abstract Hecke ring
  (NumberTheory/HeckeRing/Defs.lean, [Merged by Bors] - feat(NumberTheory): the abstract Hecke ring of a Hecke pair leanprover-community/mathlib4#41251; the convolution /
  ring-structure stack feat(NumberTheory): the double coset API for abstract Hecke rings leanprover-community/mathlib4#41253–#41328, upstreamed from AINTLIB's
  AbstractHeckeRing/*) and adds the GL₂ realization (Γ₀(N)/Γ₁(N) Hecke pairs),
  commutativity via the transpose anti-involution, and the classical Tₙ, Tₚ, ⟨d⟩ action on
  M_k(N,χ) (heckeRingHomCharSpace). The adelic reformulation is out of scope, left to a
  future roadmap.
• Finite-dimensionality vs. dimension formulas (Layer 10). General-level
  finite-dimensionality is consumed from the in-flight Mathlib Sturm bound work (level one
  merged, [Merged by Bors] - feat(NumberTheory/ModularForms): Sturm bound for level-1 modular forms leanprover-community/mathlib4#38993; the finite-index sturm_bound_finiteIndex with a
  Module.Finite ℂ (ModularForm 𝒢 k) instance in review,
  feat(NumberTheory/ModularForms): Sturm bound for finite-index subgroups leanprover-community/mathlib4#39000 with #39083/#39086/#39087/#39088). The summit stays the
  exact ε₂, ε₃, ε∞, g dimension formulas by the valence route.
• Trace formula (Layer 11, new ground). The level-one Eichler–Selberg formula
  tr(Tₙ | S_k(SL₂(ℤ))) via Hurwitz class numbers defined combinatorially by reduced binary
  quadratic forms (no class field theory; absent from Mathlib and AINTLIB, no Lean prior art) —
  either the Petersson-kernel route on the Layer-3 apparatus or the Popa–Zagier
  period-polynomial route on the modular-symbol subtree. tr T(1) re-derives Mathlib's
  level-one dimension formula and tr T(2)∣S₁₂ = −24 meets the Δ worked example. The
  general-level formula (Miyake Thm 6.8.4: optimal embeddings, Eichler symbols, class numbers of
  orders) is an explicit scope wall left to a future roadmap.
• Suggested.lean seeds five concrete dimension instances — four at Γ₀
  (dim S₂(Γ₀(11))=1, …(23)=2, …(2)=0, dim M₂(Γ₀(11))=2) and one non-Γ₀
  (dim S₂(Γ₁(13))=2). The general even-weight formula is stated, grounded, in the README; the
  two false free-parameter schemas are not seeded.
• Provenance. Migrated and cleaned from the AINTLIB LeanModularForms project, with every
  named statement checked against the live dev/leanmodularforms (2026-07-17) so the roadmap
  drops no hypotheses (strong multiplicity one keeps the shared nebentypus and finite
  exceptional set; the conductor result is the proved descend-or-vanish dichotomy; the
  functional equation keeps k > 0, width one, and the Fricke-companion form). The Main Lemma
  is now fully proved there; the three flagged open sorrys are exists_HeckeStableLattice_one
  (weight-1 lattice, Deligne–Serre), interior_edges_cancel_sum (the Eichler–Shimura Stokes
  step), and the bad-prime adjoint peterssonInner_aggregate_eq_zero_of_new_old (DS Prop
  5.6.2).

Review comments from the closed #36, addressed. Per @kim-em's request, the still-applicable
comments are linked here with how each is resolved; the roadmap itself is kept clean of the review
trail.

#36 comment	Resolution
@kbuzzard r3480434748 — "representable moduli problems… a fantasy"; analytic quotient "looks fine"	Layer 10: X(Γ) = Γ\ℍ* analytic; moduli not used
@kbuzzard r3480503537 / r3480509434 / r3480511489 — Katz–Mazur / RR "100–300 pages into a textbook"	cut
@kim-em r3472487631 / @kbuzzard r3480548139 — algebraic↔analytic bridge needs GAGA, ungrounded	cut; modular curve is analytic only
@kbuzzard r3480559583 — Ramanujan bound needs Weil + Deligne	dropped as a target; the bound only frames the Satake definition
@kbuzzard r3480582493 — weight-60 non-solvable form	added as the coefficient-field summit (worked examples)
@kbuzzard r3480472531 — "what does the abstract Hecke ring buy you? do it adelically"	the abstract double-coset ring is now Mathlib's (mathlib4#41251 + #41253–#41328, upstreamed from AINTLIB) and the roadmap consumes it; the adelic reformulation is deferred to a future roadmap
@kbuzzard r3480483984 — K_f should be CoefficientField	renamed throughout
@kbuzzard r3480450508 / r3480608247 — ⊕χ is external, pin the statement	Layer 0: stated as an internal DirectSum.IsInternal (proved in AINTLIB, ModularForm_Gamma1_charSpace_directSum)
@kbuzzard r3480498491 — eta quotients are an example, not general theory	moved to worked examples
@kbuzzard r3480593857 — free-parameter dimension schema "almost vacuous"	removed from Suggested.lean; general formula pinned in README prose
@kbuzzard r3473453151 / r3480375701, @kim-em r3485250105 — ModularFormClass / cuspFunction are Mathlib-isms	linked to Mathlib docs on first use

Engine. Consumes the sibling Contour Integration roadmap (#35) for the valence formula
(the README's ../ContourIntegration/ link resolves once #35 also lands on main).

Status. build is green — Suggested.lean (four Γ₀ instances + one Γ₁(13) instance, the
two schemas removed) elaborates against the pinned Mathlib.

🤖 Generated with Claude Code

[mrdouglasny]

A 3-agent review pass (Claude Opus 4.8 + Codex/GPT-5.x + Gemini 3.1 Pro, with lean-lsp), offered as possibly-useful comments. Overall: strong, faithful, well-grounded — approve-with-minor. Every checkable number/formula is correct; the items below are wording/sequencing/scope. (We did not independently re-verify the deep Hecke/L-function proofs.)

Confirmed correct (all three): the five Targets.lean dimension instances; the even-weight dimension formula = Diamond–Shurman 3.5.1 incl. the S₂=g exception; the valence formula (incl. the general-level Σ_{P∈Γ\ℍ*}(1/e_P)·ord_P = k·[index]/12); Hecke/eigenform recurrences (Prop 5.8.5); L-function convergence/Euler product/completed Λ + s↦k−s; coefficient-field-via-integral-Hecke-algebra; the adelic Hecke constructions; Satake; the Buzzard weight-60 example. Not seeding the free-parameter dimension formula is the right call.

Near-blocking

• Layer 2(c): "the level-K corner is exactly the abstract double-coset Hecke ring" overclaims (flagged independently by two agents). That adelic↔classical identification is a comparison theorem (strong approximation), not a definition — name it as a milestone and weaken "is exactly". Relatedly, the full smooth adelic algebra is a large sub-project not actually consumed by the classical Layers 3–10 (its "natural home for Layers 3–5" is aspirational); worth confirming it's in-scope here vs. a separate roadmap.

Important

• sorry-count inconsistency: Targets.lean says {Atkin–Lehner Main Lemma, heckeAlgℤ_finite}; README Layer 4 says {AL Main Lemma, "nonzero prime eigenvalue"}; provenance L408 says "the two sorries." Reconcile (AL@L4, heckeAlgℤ_finite@L8, and name/justify the third).
• Layer 0 sequencing: the nebentypus decomposition is stated via diamond operators, which only exist in Layer 2 — keep L0 intrinsic, move the diamond-eigenspace theorem to L2.
• "each Tₙ-eigenspace is one-dimensional" is too strong — should be "each simultaneous Hecke eigenspace."

Minor: ε₂,ε₃ are for the PSL₂(ℤ) image (state it); pin χ(p)=0 for p∣N so one recurrence also covers Uₚ; the illustrative Eigenform prototype drops χ (CuspForm (Gamma1 N) k); the weight-60 example needs an explicit Galois-group certification milestone in Layer 9.

Cross-roadmap note: #47 correctly depends on ContourIntegration (its valence formula uses the on-cycle generalized winding numbers for the ½,⅓ weights) and not on ConformalMapping. We've separately corrected a stale claim in the merged ConformalMapping roadmap that wrongly listed #47 as consuming its L4/L5 (TauCetiRoadmap#48).

[CBirkbeck]

@kim-em @kbuzzard — this is the smaller, grounded successor to the closed #36.

• The geometric summit is cut: the modular curve is the analytic quotient Γ\ℍ, and the dimension formulas come by the valence/counting route — no moduli, no representability, no GAGA bridge.
• The classical arithmetic Layers 0–9 are kept; Layer 2 plans the full smooth adelic Hecke algebra C_c^∞(GL₂(𝔸_f)), with Shimura's abstract double-coset ring identified as its level-K corner e_K·ℋ·e_K (the general reductive case is cited to the Reductive groups roadmap).
• The Add roadmap: Modular Forms — Hecke theory, newforms, L-functions, and modular curves #36 review comments that still apply are linked, with resolutions, in the PR description.

Rebased onto current main; build is green and the PR is mergeable. Ready for review.

[CBirkbeck]

Thanks @mrdouglasny — the 3-agent pass was genuinely useful. Addressed in 331ad63, which also resyncs the roadmap to the latest AINTLIB dev (projects/LeanModularForms on dev/leanmodularforms, 2026-07-03). Point by point:

Near-blocking (adelic / "is exactly"). Resolved by removing the adelic layer outright: Layer 2(c) — the full smooth adelic Hecke algebra and the Shimura level-corner identification — is cut to a one-line "out of scope, deferred to a future roadmap" marker, and the Edixhoven / Getz–Hahn adelic references are dropped. The "is exactly … double-coset Hecke ring" overclaim goes with it; #47 now keeps only the classical double-coset ring.

Important — sorry-count. Reconciled — and it had drifted further than the wording. Against the latest dev: the conductor theorem and the per-character Main Lemma (mainLemma_charSpace_routeB) are proved (the bare global mainLemma is an unused skeleton sorry); the "nonzero prime eigenvalue" obligation doesn't exist; and L8 has advanced a lot — Newform.coeffField + coeffField_numberField_of_two_le give the number-field property for k ≥ 2 via the integral modular-symbol period route, with heckeAlgℤ_finite_of_lattice for k < 2. The residual is the weight-1 Hecke-stable lattice + a Stokes/boundary step, not "the single heckeAlgℤ_finite sorry." Provenance is repointed to the monorepo tree and flagged indicative (it's actively restructuring — Chapters/ merged away, SMOObligations/→StrongMultiplicityOne/, new HeckeRIngs/GL2/ModularSymbols/).

Important — eigenspace. Fixed: "each simultaneous Hecke eigenspace is one-dimensional (multiplicity one)."

Important — Layer 0 sequencing. Kept intrinsic: M_k(N,χ) is defined by the transformation law and the diamond-eigenspace description is recovered in Layer 2 — as before.

Minors. All in: ε₂, ε₃ stated as counts in the PSL₂(ℤ)-image; χ(p) = 0 for p ∣ N pinned so the single recurrence also covers Uₚ; the illustrative Eigenform prototype now carries χ, modFormCharSpace membership, and [NeZero N]; and a Galois-group certification milestone added in Layer 9 for the weight-60 summit.

One addition prompted by the sibling Contour port: a standing convention making explicit that every target rides Mathlib's bundled ModularForm/CuspForm types and must copy AINTLIB's visible hypotheses verbatim (the T_p recurrence's modFormCharSpace membership + Coprime p N; a₁ = 1 as a Newform field, not Eigenform) — so this roadmap doesn't repeat the "raw restatement drops an invariant" failure we hit in the contour work.

Thanks also for the cross-roadmap #48 correction.

[kim-em]

🤖 Codex says:

Thanks. There is one blocking mathematical correction, followed by several concrete roadmap-specification corrections.

Conductor theorem. The sentence saying every normalized eigenform is “the level-raise of a newform” is false for the Eigenform structure defined here, because it records eigen-ness only for T_n with (n,N)=1. If g is the level-11 weight-two newform and the ambient level is 22, every

g(z) + c·g(2z)

is normalized and has the same good-Hecke eigenvalues, but for c ≠ 0 it is not a single degeneracy image. Adding U_p data produces the different p-stabilizations, which are themselves linear combinations rather than single level-raises.

The correct target is:

Every normalized good-Hecke eigenform at level N shares its eigenvalues away from N with a unique newform g of a unique minimal level M ∣ N, its conductor, and lies in the associated oldspace
span { g(dz) | d ∣ N/M }.

The uniqueness is of (M,g), equivalently the good-Hecke eigensystem—not of the original eigenform. Please replace the current claim accordingly. Opus independently checked this point and reached the same conclusion.

Further corrections:

1. Add the standard “This file is not the roadmap and is not exhaustive” header to Suggested.lean.
2. Remove the “cheap upgrade target, not an obligation” formulation for the improved L-series bound. Either make it a real milestone or move it explicitly out of scope.
3. Likewise, assign the weight-two trace-formula correction to a concrete later milestone or declare it out of scope; do not leave it as an unspecified “later refinement.”
4. Pin the analytic-conductor normalization. N·(…Γ-factor…) is not a usable specification.
5. Replace the numeric range #41253–#41328 with the actual Hecke-ring stack: #41253–#41256, #41277, #41279, and #41328. The intervening PR numbers include unrelated work.
6. For Layer 11, select a primary proof route, or state an explicit decision gate and the dependencies of each outcome. “Choose one” leaves a major architectural decision to the implementer and makes the dependency order ambiguous.