feat(HeckeRing): the twisting character of the χ-twisted Γ₀(N) Hecke ring

[CBirkbeck]

Roadmap: ModularForms

The coefficient the χ-twisted double-coset operator attaches to a monoid element:

noncomputable def delta0NebentypusChar (χ : (ZMod N)ˣ →* ℂˣ) : Delta0 N →* ℂˣ :=
  χ.comp (Delta0UpperUnit N)

@[simp] lemma delta0NebentypusChar_mapGL (χ : (ZMod N)ˣ →* ℂˣ) (γ : Gamma0 N) :
    delta0NebentypusChar N χ ⟨_, mapGL_mem_Delta0 N γ⟩ = (χ ((Gamma0Map N).toHomUnits γ))⁻¹

The definition is thin on purpose; the lemma is the content

Delta0UpperUnit is already a MonoidHom, so the character is a composition and needs no
multiplicativity argument. That is the whole point of having bundled it: AINTLIB's
delta0NebentypusDeltaChar builds the same character as a bare MonoidHom and discharges
map_one' and map_mul' by hand against its Classical.choose witness API.

The lemma is what makes the definition worth naming, and it ships in the same PR rather than
being deferred. It says the character restricts on Γ₀(N) to the inverse of χ ∘ Gamma0Map
— the character modFormCharSpace is defined by. That inverse is the convention, not a slip:
the twisted operator divides by the character, each representative contributing
χ(·)⁻¹ • (f ∣[k] ·), so the value attached to a monoid element is the reciprocal of the one
attached to a group element acting on forms. Reading this as an extension of the nebentypus and
dropping the inverse would negate every twist downstream. It is inherited directly from
Delta0UpperUnit_mapGL, where the inverse first appears, so the proof is three rewrites.

Two measured design decisions

delta0NebentypusChar_apply uses (rfl), not rfl. Bare rfl fails:

Not a definitional equality: the left-hand side (delta0NebentypusChar N χ) g is not
definitionally equal to the right-hand side χ ((Delta0UpperUnit N) g)
Note: This theorem is exported from the current module. This requires that all definitions
that need to be unfolded to prove this theorem must be exposed.

The definition sits in a public section without @[expose], so its body is sealed and a bare
rfl would opt the theorem into exporting that definitional equality. The parenthesised form
elaborates against the sealed body instead.

Only one of the pair is @[simp]. _apply and _mapGL share a left-hand side; tagging
both would let _apply fire first and leave _mapGL unable to apply — the simpNF failure
mode. _mapGL is the normal form worth rewriting towards, so it carries the attribute and
_apply records in its docstring why it does not.

Absence

delta0NebentypusChar and Delta0NebentypusChar match zero files on main. Checked with
git grep -w, not git grep -E "\bfoo\b" — \b is unsupported in git grep's POSIX ERE and
matches nothing silently. Controls: Delta0UpperUnit matches 2 files, a nonsense name matches 0.

delta0NebentypusDeltaChar — the source's name — matches one file, but with zero declaration
lines: it is provenance prose in Gamma0/UpperUnit.lean:59, not a declaration. A raw name
grep counts docstring mentions.

Placement

A new file Gamma0/NebentypusChar.lean, importing Gamma0/UpperUnit.lean for
Delta0UpperUnit_mapGL and Mathlib.Data.Complex.Basic for ℂˣ. It is deliberately not added
to UpperUnit.lean: that file is about the (ZMod N)ˣ-valued unit and is concurrently modified
by #4319, and the character is a different object with a different codomain.

Provenance: github.com/CBirkbeck/AINTLIB @ 2baa76f742bdb4fb8ee323fabba41203bd390e08,
Apache-2.0, projects/LeanModularForms/LeanModularForms/HeckeRIngs/GL2/Unified/TwistedHeckeRing.lean
line 120, declaration delta0NebentypusDeltaChar. Restated as a composition, since the
multiplicativity obligations the source discharges by hand are already carried by
Delta0UpperUnit. The same citation is in the file's References section.

Roadmap target

TauCetiRoadmap/ModularForms/README.md:1461-1462 names the ring-hom layer
HeckeRIngs/GL2/Unified/{Gamma0RingDn,NebentypusHeckeRingHom,RingTransport,TwistedHeckeRing}.lean
with heckeRingDn and heckeRingHomCharSpace as its objects; TwistedHeckeRing.lean is exactly
where this character lives in the source. heckeRingHomCharSpace is README:407 (the operator
Φ_χ), which EigenformAwayFromLevel is stated against (README:515), which README:609-617 needs
for strongMultiplicityOne / StrongMultiplicityOne/ConstantMultiple.lean. So this is
CLAUDE.md's "supplies a prerequisite that a specific target needs" — the twisting character is
what the χ-twisted Hecke ring is built from, two rungs below the Layer-5 headline.

[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 definition faithfully composes the verified upper-left-unit homomorphism with χ, and the restriction lemma correctly transports the inverse relation through χ. No semantic defect, vacuity, or misplaced assumption was found.
✅	reuse	approved	codex/gpt-5.6-sol	No duplication found. The character is a new semantic composition, its evaluation lemma is required by module sealing, and the named mapGL specialization is justified as the consumer-facing restriction formula.
✅	scope	approved	codex/gpt-5.6-sol	The character and its restriction lemma form one coherent prerequisite for the roadmap’s Layer 2 twisted nebentypus Hecke-ring action; the required Γ₀/Δ₀ infrastructure is already present.
✅	attribution	approved	codex/gpt-5.6-sol	The file credits both the central informal reference and the adapted AINTLIB formalization, including author, repository, exact source path, commit, declaration, and adaptation details.
✅	api-design	approved	codex/gpt-5.6-sol	The canonical definition has a minimal, complete interface: its sealed body is characterized by a correctly annotated application lemma, and the Γ₀(N) specialization reduces through that normal form without redundant automation.
✅	generality	approved	codex/gpt-5.6-sol	The declarations have the natural generality for the roadmap’s complex-valued nebentypus: no assumptions are unused or unnecessarily strong, and no duplicated special-case proof is introduced.
✅	placement	approved	codex/gpt-5.6-sol	The character and its Γ₀ specialization are naturally placed beside UpperUnit in the existing Gamma0 topic directory. UpperUnit supplies the defining map and specialization lemma, while Complex.Basic supplies the ℂ-valued codomain; neither import is evidently wrong.
✅	naming	approved	codex/gpt-5.6-sol	The introduced names accurately describe their declarations and follow the adjacent Delta0UpperUnit_apply_val and Delta0UpperUnit_mapGL conventions. No notation is introduced.
✅	documentation	approved	codex/gpt-5.6-sol	The new module and all public declarations have accurate, useful documentation describing their mathematical purpose and results.
✅	proof-quality	approved	codex/gpt-5.6-sol	The defining equation documents why definitional unfolding is necessary, and the specialization is a short, robust rewrite through stable named lemmas.

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

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

[kbuzzard]

🟡 documentation — request_changes codex/gpt-5.6-sol

The module documentation incorrectly claims downstream simp cannot recover the defining equation, although the equation is explicitly tagged @[simp].

• TauCeti/NumberTheory/HeckeRing/GL2/Gamma0/NebentypusChar.lean:39 — The main-results documentation says simp cannot recover the defining equation downstream, contradicting @[simp] lemma delta0NebentypusChar_apply at line 77. Fix: Clarify that unfolding or simp [delta0NebentypusChar] fails downstream, while ordinary simp succeeds via delta0NebentypusChar_apply.

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 · 31s · 38.7k in / 888 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	approved	codex/gpt-5.6-sol	The definition is a faithful composition with Delta0UpperUnit, and the specialization to Gamma0 correctly transports the existing inverse through the monoid homomorphism. No semantic correctness issue is evident.
✅	reuse	approved	codex/gpt-5.6-sol	The new character is a meaningful composition of the existing Delta0UpperUnit with χ, and the specialization records the nontrivial inverse convention without duplicating a located TauCeti or Mathlib declaration.
✅	scope	approved	codex/gpt-5.6-sol	The new character and its restriction lemma form one coherent prerequisite for the ModularForms roadmap’s χ-twisted Hecke-ring construction.
✅	attribution	approved	codex/gpt-5.6-sol	The file credits both the informal mathematical source and the adapted AINTLIB formalization, including author, repository path, commit, declaration, license, and the nature of the adaptation.
✅	api-design	approved	codex/gpt-5.6-sol	The new monoid hom has a minimal public surface, a sealed body with a characteristic application lemma, and a named Γ₀ specialization. The simp annotation selects the general defining equation while allowing the specialization to normalize through existing simp lemmas without introducing a redundant rule.
✅	generality	approved	codex/gpt-5.6-sol	The definition and its specialization are stated at the natural level for the roadmap’s complex-valued twisting character, with no unused or unnecessarily strong assumptions.
✅	placement	approved	codex/gpt-5.6-sol	The character and its Gamma0 specialization are naturally placed beside UpperUnit in the existing Gamma0 topic directory, and the two imports directly supply the construction and complex-unit codomain.
✅	naming	approved	codex/gpt-5.6-sol	The introduced names follow adjacent Delta0UpperUnit_mapGL terminology, and the _apply and _mapGL suffixes accurately describe their conclusions. No notation is introduced.
🟡	documentation	changes requested	codex/gpt-5.6-sol	The module documentation incorrectly claims downstream simp cannot recover the defining equation, although the equation is explicitly tagged @[simp].
✅	proof-quality	approved	codex/gpt-5.6-sol	The proofs are short and robust; the definitional-equality proof is explicitly documented, and the specialization uses a clear three-step rewrite.

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

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