feat: define the Hecke operators T_n

[sqrt-of-2]

This PR defines the uniform Hecke operators heckeT_n and heckeT_n_cusp as the slash actions of the canonical double coset Γ₁(N) diag(1,n) Γ₁(N), and expose their underlying slash sums, the identity law T₁ = 1, the classical formula at every prime, and the bad-prime identification with the upper-triangular operator. This advances the ModularForms roadmap milestone “(b) The action on forms,” specifically its target def heckeT_n [NeZero N] (k : ℤ) (n : ℕ) [NeZero n], while fixing the normalization through the already-proved double-coset computation.

The small supporting lemmas prove that the unique upper-triangular representative and slash sum at index one are identities. The definition follows the architecture of AINTLIB’s LeanModularForms/HeckeRIngs/GL2/HeckeT_n.lean (Chris Birkbeck, Apache-2.0, commit 2baa76f742bdb4fb8ee323fabba41203bd390e08), but uses Tau Ceti’s existing canonical double-coset action directly; no proof code is transcribed.

After this PR, milestone (b) still needs preservation of general nebentypus spaces, the Hecke-ring homomorphism, coprime and prime-power multiplication laws, the general q-expansion recurrences, and the U_p notation milestone.

Roadmap: ModularForms

🤖 Prepared with Codex

[CBirkbeck]

✅ correctness — now passing on f09489e.

[CBirkbeck]

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 positive-index operators faithfully package the canonical double-coset actions; the identity, prime, and bad-prime laws agree with the underlying verified decompositions and normalization.
✅	reuse	approved	codex/gpt-5.6-sol	The indexed operators are a justified canonical API over the existing double-coset action. Searches of TauCeti and Mathlib found no declaration that directly replaces them and no avoidable duplicated proof or construction.
✅	scope	approved	codex/gpt-5.6-sol	The PR directly advances ModularForms milestone (b) by defining the roadmap’s uniform T_n action from the already-merged double-coset machinery. The index-one lemmas and prime/bad-prime identifications are coherent supporting material for that single topic.
✅	attribution	approved	codex/gpt-5.6-sol	The module credits the central AINTLIB formal source with file, author, license, and pinned commit, and cites the relevant informal references.
✅	api-design	approved	codex/gpt-5.6-sol	The linter-compliant heckeTNat naming matches the adjacent diamondOpNat API, and the definitions have sufficient characteristic, prime, bad-prime, and identity lemmas with appropriate simplification annotations.
✅	generality	approved	codex/gpt-5.6-sol	The operator definitions use the roadmap’s natural positive-index hypotheses, while the prime and level-divisor results now derive NeZero p internally from their explicit hypotheses.
✅	placement	approved	codex/gpt-5.6-sol	The new operators and supporting identity lemmas are in their canonical topic files, and the new module imports the directly relevant prime-level theory without an evidently unnecessary import.
✅	naming	approved	codex/gpt-5.6-sol	The introduced names follow adjacent Hecke and diamond-operator terminology, accurately describe their conclusions, and introduce no notation.
✅	documentation	approved	codex/gpt-5.6-sol	The new substantive module has a clear module docstring with scope, provenance, and references, and every added public declaration is documented accurately.
✅	proof-quality	approved	codex/gpt-5.6-sol	The added proofs are short and robust, using explicit defining lemmas, targeted rewriting, and straightforward extensionality without undocumented definitional-equality manipulation.

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

_{Reviewing this diff at head f09489e. rubrics @ f854a7e. Review spend: $3.81.}

[kbuzzard]

🟡 reuse — request_changes codex/gpt-5.6-sol

The public defining-equation lemmas are redundant reflexive restatements of the new definitions.

• TauCeti/NumberTheory/ModularForms/HeckeSlash/Operators.lean:87 — heckeTNat_def and heckeTCuspNat_def duplicate the immediately preceding definitions verbatim via rfl, adding unnecessary public API. Fix: Delete both lemmas; in coe_heckeTNat and coe_heckeTCuspNat, unfold the corresponding definition before applying the existing coe_heckeSlashGamma1*End 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.)

_{codex/gpt-5.6-sol · 16s · 41k in / 638 out tokens · reviewing this diff · rubric}

[kbuzzard]

🟡 generality — request_changes codex/gpt-5.6-sol

Four public theorems retain a logically redundant NeZero p assumption already derivable from their explicit hypotheses.

• TauCeti/NumberTheory/ModularForms/HeckeSlash/Operators.lean:106 — coe_heckeTNat_prime, coe_heckeTCuspNat_prime, heckeTNat_eq_upperTri, and heckeTCuspNat_eq_upperTri expose [NeZero p], although p.Prime or p ∣ N with [NeZero N] proves p ≠ 0. Fix: Remove [NeZero p] from these signatures and construct the required NeZero p instance internally from hp.ne_zero or from hpN and NeZero.out N.

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 · 26s · 40.1k in / 1.2k out tokens · reviewing this diff · rubric}

[kbuzzard]

AI review — changes requested

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	stale (re-run pending)	codex/gpt-5.6-sol	The definitions and stated computation laws are semantically consistent with the canonical double-coset action, including the identity and bad-prime cases. No correctness or faithfulness defect is evident.
🟡	reuse	changes requested	codex/gpt-5.6-sol	The public defining-equation lemmas are redundant reflexive restatements of the new definitions.
♻️	scope	stale (re-run pending)	codex/gpt-5.6-sol	The PR directly implements the cited ModularForms hecke-t-n target, and its index-one supporting lemmas are tightly coupled prerequisites for the identity law. The changes form one coherent topic.
♻️	attribution	stale (re-run pending)	codex/gpt-5.6-sol	The new module credits its central formal inspiration with project, file, author, license, and commit, and cites the relevant informal textbook sources in code.
✅	api-design	approved	codex/gpt-5.6-sol	The linter-compliant canonical names heckeTNat and heckeTCuspNat appropriately realize the roadmap target, and the public API provides defining, coercion, identity, prime-formula, and bad-prime characterization lemmas with suitable simplification annotations.
🟡	generality	changes requested	codex/gpt-5.6-sol	Four public theorems retain a logically redundant NeZero p assumption already derivable from their explicit hypotheses.
♻️	placement	stale (re-run pending)	codex/gpt-5.6-sol	The new operators are naturally placed in the existing ModularForms/HeckeSlash hierarchy, while the supporting identity lemmas remain beside the representative and slash-sum definitions they elaborate. The import of HeckeSlash.Prime is directly justified by the prime computation rules and supplies the surrounding operator API.
♻️	naming	stale (re-run pending)	codex/gpt-5.6-sol	The introduced names accurately describe their conclusions, follow adjacent API terminology, and add no gratuitous notation.
♻️	documentation	stale (re-run pending)	codex/gpt-5.6-sol	The new module and all added public declarations have accurate, useful documentation, including scope, normalization, and provenance.
♻️	proof-quality	stale (re-run pending)	codex/gpt-5.6-sol	The added proofs are short, readable, and use stable simplification or direct defining equations without undocumented definitional-equality manipulation or substantial duplicated reasoning.

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

_{Reviewing this diff at head 323e7b6. rubrics @ f854a7e. Review spend: $1.46.}

[CBirkbeck]

✅ api-design — now passing on f09489e.

[sqrt-of-2]

I contest this finding because the requested spelling is rejected by the enforced Mathlib linter, and repo rules forbid silencing it. Commit 25c286b already tried heckeT_n and heckeT_n_cusp. Its sandboxed-build failed (https://github.com/TauCetiProject/TauCeti/actions/runs/32666593428/job/97260825452) with defsWithUnderscore violations for both declarations and LINT-ENV: FAIL — 2 new violation(s); the log explicitly requires lowerCamelCase or UpperCamelCase. Commit 323e7b6 then renamed them to heckeTNat and heckeTCuspNat and restored green CI. This also agrees with the round-2 naming approval, which says the current names follow adjacent Hecke and diamond-operator terminology. Restoring heckeT_n therefore necessarily regresses enforced lint/naming quality; adding nolint or a compatibility alias is forbidden. Please accept the linter-compliant canonical Lean API.

[CBirkbeck]

Re: your reply on api-design — re-reviewed on f09489e; this clears the finding ✅ — approved on f09489e.

_{codex/gpt-5.6-sol · addresses your replies through comment 3839765733.}

[CBirkbeck]

✅ generality — now passing on f09489e.