feat: the Fourier-coefficient recurrence for T_p at every prime

[sqrt-of-2]

This PR proves Diamond–Shurman's Fourier-coefficient recurrence for the Hecke operator Tₚ, uniformly at every prime and at every level Γ₁(N): aₘ(Tₚ f) = a_{p m}(f) + p^{k−1} a_{m/p}(⟨p⟩ f), with the second term present exactly when p ∣ m. On a nebentypus space M_k(N, χ) with p ∤ N the diamond acts by the scalar χ(p), giving the classical aₘ(Tₚ f) = a_{p m}(f) + χ(p) p^{k−1} a_{m/p}(f); at p ∣ N the zero-extended ⟨p⟩ vanishes and the same statement degenerates to aₘ(Tₚ f) = a_{p m}(f), the operator modern papers write Uₚ. Following Miyake, Diamond–Shurman and Shimura no separate Uₚ is introduced — it is only this case of Tₚ. The Nat division m / p is guarded by an explicit if p ∣ m, so no index silently rounds down. Alongside the coefficient statements the same identity is recorded between power series, with the diamond term appearing as a PowerSeries.expand; and two immediate consequences are drawn: a₁(Tₚ f) = a_p(f), and the fact that the Hecke eigenvalue of a normalized eigenvector (a₁(f) = 1) is a_p(f) — the identity that turns an eigenvalue system into a system of Fourier coefficients.

The milestone served is Layer 2(b) of the ModularForms roadmap, "The action on forms": Tₙ, Tₚ as ℂ-linear endomorphisms of M_k(Γ₁(N)) together with "the explicit q-expansion recurrences", listed there as aₘ(Tₚ f) = a_{mp}(f) + χ(p) p^{k−1} a_{m/p}(f) (Diamond–Shurman §5.2–5.3), and the roadmap's own frontier item "Uniform Hecke operators … the full good- and bad-prime coefficient recurrences". #4042 supplied the slash-level identity Tₚ f = ∑_{b < p} f ∣[k] !![1, b; 0, p] + (⟨p⟩ f) ∣[k] !![p, 0; 0, 1]; UpperTri/QExpansion.lean and Diagonal/QExpansion.lean supplied the q-expansion of each of the two halves separately. This PR is the step that adds them, which is what makes the recurrence a statement about coefficients rather than about slashes. What remains on that milestone after this PR: the composite Tₙ for general n with Tₘ Tₙ = Tₘₙ for (m, n) = 1 and the prime-power recurrence, the Hecke-ring homomorphism onto each character space, and the theorem that Tₚ preserves the nebentypus at a good prime.

Files: TauCeti/NumberTheory/ModularForms/HeckeSlash/Recurrence.lean (new, 271 lines). One further change: one_mem_strictPeriods_Gamma1 in TauCeti/NumberTheory/ModularForms/HeckeSlash/UpperTri/ModularForm.lean stops being private, so the new file reuses it instead of restating it; it is now listed in that file's main results.

No Mathlib infrastructure is vendored, and no code is transcribed from AINTLIB. The hypotheses of the nebentypus statements — membership in modFormCharSpace k χ and Nat.Coprime p N — are the ones the roadmap asks to be kept verbatim from AINTLIB's HeckeRIngs/GL2/FourierHecke.lean (Apache-2.0), and the module docstring records that.

Roadmap: ModularForms

🤖 Prepared with Claude Code

[kbuzzard]

🟡 attribution — request_changes claude/claude-opus-5

Diamond–Shurman, Shimura, Miyake and the in-repo antecedents are properly credited, and the AINTLIB predecessor file is named; but the AINTLIB credit line drops the author/copyright holder (and the pinned commit) that every sibling module in this directory carries.

• TauCeti/NumberTheory/ModularForms/HeckeSlash/Recurrence.lean:59 — The Provenance credit for AINTLIB's HeckeRIngs/GL2/FourierHecke.lean gives only the repo URL and license, omitting the copyright holder (Chris Birkbeck) and a pinned commit, so the Apache-2.0 attribution is incomplete and the cited file is not verifiable at a revision. Fix: Extend the line to the neighbourhood's form, e.g. "(LeanModularForms/HeckeRIngs/GL2/FourierHecke.lean, https://github.com/CBirkbeck/AINTLIB, commit 2baa76f742bdb4fb8ee323fabba41203bd390e08, Apache-2.0, Chris Birkbeck)".

Reply in this thread to contest a finding; that re-runs only this rubric and posts an answer here. (To fix it, just push a commit — that re-reviews on its own. To contest again after an answer, post a NEW reply rather than editing an old one.)

_{claude/claude-opus-5 · 108s · 16 in / 7.1k out tokens · reviewing this diff · rubric}

[kbuzzard]

🟡 api-design — request_changes claude/claude-opus-5

The recurrence surface is complete and symmetric, with no compatibility artifacts, but the advertised bad-prime (Uₚ) lemmas carry a needless p.Prime hypothesis that makes them weaker than what the existing library already yields, and the newly de-privatised width lemma is exposed under a Hecke namespace it has nothing to do with.

• TauCeti/NumberTheory/ModularForms/HeckeSlash/Recurrence.lean:212 — qExpansion_coeff_heckeSlashGamma1ModularFormEnd_diagCosetGamma1_of_dvd (and its cusp counterpart, line 221) requires hp : p.Prime, but the identical statement holds for every p ∣ N; the primality hypothesis narrows the canonical Uₚ API for no reason. Fix: Drop hp and prove from the existing lemmas: rw [heckeSlashGamma1ModularFormEnd_diagCosetGamma1 k hpN, qExpansion_coeff_heckeSlashUpperTriModularFormEnd] (resp. the cusp-form versions).
• TauCeti/NumberTheory/ModularForms/HeckeSlash/UpperTri/ModularForm.lean:92 — one_mem_strictPeriods_Gamma1 becomes public in namespace HeckeRing.GL2, but it is a general statement about Gamma1 with no Hecke content, and the repo already spells the same fact inline elsewhere, leaving two spellings. Fix: Place the public lemma in the CongruenceSubgroup namespace beside the other Γ₁ cusp-width material and use it at the existing sites, or keep it private and discharge the new file's uses with by simp.

Reply in this thread to contest a finding; that re-runs only this rubric and posts an answer here. (To fix it, just push a commit — that re-reviews on its own. To contest again after an answer, post a NEW reply rather than editing an old one.)

_{claude/claude-opus-5 · 211s · 22 in / 15.2k out tokens · reviewing this diff · rubric}

[kbuzzard]

🟡 generality — request_changes claude/claude-opus-5

The two bad-prime statements assume p.Prime although the result holds for every divisor p ∣ N and already follows from two existing primality-free lemmas; everything else sits at the natural level.

• TauCeti/NumberTheory/ModularForms/HeckeSlash/Recurrence.lean:212 — qExpansion_coeff_heckeSlashGamma1ModularFormEnd_diagCosetGamma1_of_dvd assumes hp : p.Prime, but the statement holds for every p ∣ N (with [NeZero N]); primality is used only to route the proof through the prime recurrence. Fix: Drop hp and prove directly: rw [heckeSlashGamma1ModularFormEnd_diagCosetGamma1 k hpN]; exact qExpansion_coeff_heckeSlashUpperTriModularFormEnd k hpN f m, and adjust the docstring ("at a bad prime" → any divisor of the level).
• TauCeti/NumberTheory/ModularForms/HeckeSlash/Recurrence.lean:221 — Same over-strong hypothesis in the cusp-form counterpart qExpansion_coeff_heckeSlashGamma1CuspFormEnd_diagCosetGamma1_of_dvd. Fix: Drop hp and derive from heckeSlashGamma1CuspFormEnd_diagCosetGamma1 k hpN plus qExpansion_coeff_heckeSlashUpperTriCuspFormEnd k hpN f m.

Reply in this thread to contest a finding; that re-runs only this rubric and posts an answer here. (To fix it, just push a commit — that re-reviews on its own. To contest again after an answer, post a NEW reply rather than editing an old one.)

_{claude/claude-opus-5 · 172s · 19 in / 12.3k out tokens · reviewing this diff · rubric}

[kbuzzard]

🟡 placement — request_changes claude/claude-opus-5

The new file's location and imports are correct. But the lemma this PR promotes to public API, one_mem_strictPeriods_Gamma1, has no Hecke content and belongs in an earlier general file rather than in HeckeSlash/UpperTri/ModularForm.lean under HeckeRing.GL2.

• TauCeti/NumberTheory/ModularForms/HeckeSlash/UpperTri/ModularForm.lean:92 — one_mem_strictPeriods_Gamma1 becomes public API but is a generic statement about Γ₁(N) widths ((1:ℝ) ∈ ((Gamma1 N).map (mapGL ℝ)).strictPeriods) with no upper-triangular or Hecke content; it depends only on Mathlib's CongruenceSubgroup.strictPeriods_Gamma1 (mathlib/Mathlib/NumberTheory/ModularForms/Cusps.lean:442), yet lives in a Hecke file under namespace HeckeRing.GL2, where callers outside the Hecke tree will not find it. Fix: Move it to an earlier general file — TauCeti/NumberTheory/ModularForms/Cusps/Basic.lean is the repo's home for strictPeriods/cusp-width facts and is already upstream of the HeckeSlash tree — under a non-Hecke namespace, and use it at the sites that currently reprove it inline.

Reply in this thread to contest a finding; that re-runs only this rubric and posts an answer here. (To fix it, just push a commit — that re-reviews on its own. To contest again after an answer, post a NEW reply rather than editing an old one.)

_{claude/claude-opus-5 · 166s · 33 in / 12.6k out tokens · reviewing this diff · rubric}

[kbuzzard]

🟡 naming — request_changes claude/claude-opus-5

Names track the adjacent Prime.lean/UpperTri precedent and no notation is introduced, but the newly public one_mem_strictPeriods_Gamma1 sits in the wrong namespace and the _of_dvd suffix is ambiguous between p ∣ N and the p ∣ m guard that every other lemma in the file carries.

• TauCeti/NumberTheory/ModularForms/HeckeSlash/UpperTri/ModularForm.lean:92 — one_mem_strictPeriods_Gamma1 becomes public inside namespace HeckeRing.GL2 (line 78), but it states (1 : ℝ) ∈ ((Gamma1 N).map (mapGL ℝ)).strictPeriods — a fact about Γ₁(N) and cusp widths, unrelated to Hecke rings. As public API the name is misplaced in that namespace and undiscoverable next to its siblings. Fix: Put it in the root namespace (matching Mathlib's one_mem_strictPeriods_SL) or in CongruenceSubgroup (matching strictPeriods_Gamma1), and adjust the three call sites in UpperTri/ModularForm.lean and Recurrence.lean.
• TauCeti/NumberTheory/ModularForms/HeckeSlash/Recurrence.lean:212 — qExpansion_coeff_heckeSlashGamma1ModularFormEnd_diagCosetGamma1_of_dvd names the hypothesis p ∣ N as bare _of_dvd, but in this file the salient divisibility is p ∣ m (the if p ∣ m guard in every recurrence statement). The name reads as the p ∣ m case of the recurrence rather than the bad-prime case. Fix: Rename to …_of_dvd_level (repo precedent: twistedDivisorSum_apply_prime_pow_of_dvd_left_level, TauCeti/NumberTheory/ArithmeticFunction/TwistedDivisorSum.lean:115), and update the Main results bullet at line 49 and the module-doc mention at line 35.
• TauCeti/NumberTheory/ModularForms/HeckeSlash/Recurrence.lean:221 — Same ambiguous _of_dvd suffix on the cusp-form counterpart qExpansion_coeff_heckeSlashGamma1CuspFormEnd_diagCosetGamma1_of_dvd (hypothesis p ∣ N). Fix: Rename in step with the modular-form version, e.g. …_of_dvd_level.

Reply in this thread to contest a finding; that re-runs only this rubric and posts an answer here. (To fix it, just push a commit — that re-reviews on its own. To contest again after an answer, post a NEW reply rather than editing an old one.)

_{claude/claude-opus-5 · 183s · 27 in / 14.2k out tokens · reviewing this diff · rubric}

[kbuzzard]

🟡 proof-quality — request_changes claude/claude-opus-5

Proofs are short and mostly explicit, but the file re-derives two analyticity facts that already exist (one private) in the files it imports, and the cusp-form recurrence closes by unfolding the ModularFormClass.modularForm wrapper rather than by an explicit coercion step.

• TauCeti/NumberTheory/ModularForms/HeckeSlash/Recurrence.lean:106 — The hU block re-derives, from the form class, the exact statement of analyticAt_cuspFunction_heckeSlashUpperTri (private, UpperTri/QExpansion.lean:190) — same four arguments, plus a re-instantiation of the Fact (IsCusp .infty Γ) instance that qExpansion_coeff_heckeSlashUpperTri' also builds. Fix: Drop private from analyticAt_cuspFunction_heckeSlashUpperTri, or add a class-level analyticAt_cuspFunction_heckeSlashUpperTri' beside qExpansion_coeff_heckeSlashUpperTri' (which already derives hfper and the Fact instance from hΓ), and call it here — the same de-privatization this PR already performs for one_mem_strictPeriods_Gamma1.
• TauCeti/NumberTheory/ModularForms/HeckeSlash/Recurrence.lean:86 — analyticAt_cuspFunction_slash_scaleRep is a private, Γ₁(N)-specific repeat of the reasoning in Diagonal/QExpansion.lean (rewrite the diagonal slash as d^(k-1) • levelRaise, then use analyticity of the level raise). Analyticity of the cusp function of f ∣[k] diag(d,1) is the reusable fact needed whenever the two halves are added — it will be needed again for the composite Tₙ the PR description defers. Fix: State it in Diagonal/QExpansion.lean next to ModularForm.qExpansion_slash_natDiagGL_d_one, in the general {𝒢 𝒢'} (h𝒢') (hle) (f) form, and use it both there (its proof currently inlines the same ModularFormClass.analyticAt_cuspFunction_zero (levelRaise …) step) and here.
• TauCeti/NumberTheory/ModularForms/HeckeSlash/Recurrence.lean:148 — The exact typechecks only because ⇑(ModularFormClass.modularForm (diamondOpCuspNat k p f)) unfolds to ⇑(diamondOpCuspNat k p f): the private lemma's conclusion mentions the wrapper, the goal does not. Undocumented defeq across a coercion wrapper, and nothing in the proof shows the reader where the two spellings meet. Fix: Make the identification explicit — e.g. simpa only [<the @[simps]-generated coercion lemma for ModularFormClass.modularForm>] using … — or restate qExpansion_coeff_add_slash_scaleRep so the second argument is passed as a ModularFormClass type and the wrapping happens inside the lemma.

Reply in this thread to contest a finding; that re-runs only this rubric and posts an answer here. (To fix it, just push a commit — that re-reviews on its own. To contest again after an answer, post a NEW reply rather than editing an old one.)

_{claude/claude-opus-5 · 276s · 31 in / 22.4k out tokens · reviewing this diff · rubric}

[kbuzzard]

AI review — approved

Each rubric is judged independently by multiple review agents; the PR merges only once every rubric is green — any rubric that is not green (changes requested, blocked, errored, stale, or not yet run) blocks the merge. See the rubrics.

	rubric	state	judge	summary
✅	correctness	approved	codex/gpt-5.6-sol	The coefficient and power-series identities faithfully encode the slash decomposition, including divisibility guarding, nebentypus specialization, bad-prime degeneration, and the normalized-eigenvector consequence.
✅	reuse	approved	codex/gpt-5.6-sol	The prior thin-wrapper issue is absent from the current diff; the recurrence composes existing upper-triangular and diagonal q-expansion APIs without duplicating a located declaration.
✅	scope	approved	codex/gpt-5.6-sol	The PR advances the single cited ModularForms Layer 2(b) target by deriving the explicit prime Hecke q-expansion recurrence. Its minor supporting change and coefficient/eigenvalue corollaries are tightly coupled to that topic.
✅	attribution	approved	codex/gpt-5.6-sol	The module credits its central informal sources with specific locations and documents the related AINTLIB formalization, including repository, commit, license, author, file, and precise scope of influence.
✅	api-design	approved	codex/gpt-5.6-sol	The canonical public surface provides the roadmap-required coefficient recurrence, reusable power-series and normalized-eigenvector consequences, and parallel cusp-form results without compatibility shims, exposed proof helpers, or inappropriate automation annotations.
✅	generality	approved	codex/gpt-5.6-sol	The statements sit at the natural level: each prime, coprimality, character-space, divisibility, and normalization hypothesis is used for its corresponding conclusion, while the bad-level recurrence is appropriately generalized beyond primes.
✅	placement	approved	codex/gpt-5.6-sol	The recurrence and its consequences are naturally placed under HeckeSlash/Recurrence, and both public imports provide declarations substantively used by the new proofs.
✅	naming	approved	codex/gpt-5.6-sol	The introduced names accurately describe their conclusions, distinguish modular-form and cusp-form variants consistently, and use standard suffixes such as _of_prime, _of_dvd_level, and _eq_smul. No new notation is introduced.
✅	documentation	approved	codex/gpt-5.6-sol	The new substantive module has an accurate module docstring, and every added public theorem is documented in terms of its statement and purpose without overclaiming.
✅	proof-quality	approved	codex/gpt-5.6-sol	The proofs are concise, factor shared analytic and coefficient reasoning into a helper, and rely on explicit rewriting plus stable automation. No undocumented definitional-equality manipulation, brittle proof chain, or substantial unfactored argument is present.

♻️ = approved on an earlier commit, re-run before merge.

_{Reviewing this diff at head 6ef1dab. rubrics @ f854a7e. Review spend: $2.31.}

[CBirkbeck]

✅ reuse — now passing on 471c5a7.

[CBirkbeck]

✅ generality — now passing on 471c5a7.

[CBirkbeck]

🟡 proof-quality — request_changes codex/gpt-5.6-sol

The shared recurrence helper still closes the diagonal branch through undocumented definitional equality across the generic ModularFormClass wrapper.

• TauCeti/NumberTheory/ModularForms/HeckeSlash/Recurrence.lean:118 — The exact applies a theorem about ModularFormClass.modularForm g to a goal stated using generic g; both modular- and cusp-form callers therefore rely on wrapper/coercion definitional equality. Fix: State the helper’s diagonal input as a ModularForm, or add and use an explicit lemma relating a ModularFormClass value’s q-expansion and slash to its bundled modular form.

Reply in this thread to contest a finding; that re-runs only this rubric and posts an answer here. (To fix it, just push a commit — that re-reviews on its own. To contest again after an answer, post a NEW reply rather than editing an old one.)

_{codex/gpt-5.6-sol · 30s · 108.3k in / 1.2k out tokens · reviewing this diff · rubric}