# ROADMAP: from the conditional Theorem 1.1 to an unconditional one

Goal: remove the four assumed inputs of `MM.moonshine_conjecture` (listed in `README.md`,
section "Assumed") one at a time, in an order that keeps every intermediate state a *compiling* Lean
package.  Per-batch `sorry`s are allowed for the parts that are not yet proved (see the policy
bullet in "Working agreement"): `sorry`-freeness is the **completion criterion** of the whole
project, not an invariant of an intermediate state.

**How to read this file.**  It is the **plan**: goals, one task entry per task (S/T/M/A numbering)
with its status, and the campaign's compressed status tables at the end.  The dated dispatcher
blocks inside old task entries are **evidence, not instruction** — several are explicitly superseded,
and each says so in place; a route that was tried and failed is worth more than one never tried.
**Per-batch records do not live here**: they are in `NOTES.md` (Appendix A for the dispatcher
narratives, `§` entries for the analysis and lessons).  Anything you need in order to act is in the
section **"The FLM campaign (batches 151--229): status, compressed"** below and `HANDOVER.md` §6; for
what is proved, see `README.md`.

Working agreement
-----------------
* One task (S/T/M/A numbering below) is dispatched at a time, to one subagent.  Parallel
  work is restricted to genuinely disjoint files; the dispatcher verifies before moving on.
* Every task must end with: `tools/build.sh <its files>` (the Linux port of `tools/build.ps1`,
  same `LEAN_PATH`; the discipline is `AGENTS.md`, "Build and verification") exiting 0, no `axiom`,
  no `native_decide`.  A task that does not compile is rejected.
* **Per-batch `sorry` policy (owner's standing instruction, 2026-09-22).**  A batch **may** land
  `sorry`s marking the parts that are not yet proved --- this is the sanctioned way to deliver a
  statement whose proof is still open.  Each such `sorry` must (a) be registered in the `sorry` map
  of `README.md`, and (b) be tied to the open task/residual it belongs to here or in `HANDOVER.md`;
  the declaration that consumes it must carry a `#guard_msgs in #print axioms` guard printing
  `[propext, sorryAx, Classical.choice, Quot.sound]`, so the hole is visible in the build.
  **"No `sorry` anywhere" is the criterion for the completion of the whole project** (the
  formalization of monstrous moonshine), not for a batch.
* **Build cost: take `AGENTS.md`'s figures.**  An earlier revision of this file said "~3 m 50 s for
  one module"; that is superseded (see the protocol section at the end, which also records the
  memory cap and the "do not build a file its author is still editing" rule).
* New source goes in a new file (e.g. `Definitions/MMCoxeter.lean`); existing files are
  edited only by the dispatcher.  Subagents never run `git` write commands.
* Files that a task creates should be added to the list in `FinalCheck.lean` (dispatcher).

Status legend: `[ ]` todo, `[~]` dispatched, `[x]` verified accepted, `[!]` blocked,
`[paused]` stopped by an owner decision with the reason recorded in place.

---

## Stream S — the monster group (removes assumed input 1)

The monster is **defined** here by a presentation: the `Y₄₄₃` Coxeter group modulo the spider
relation and then modulo the centre.  The Lean 3 project `formalabstracts` does the same.
Mathlib has the needed pieces: `GroupTheory/Coxeter/{Basic,Matrix,Length,Inversion}.lean`,
`Combinatorics/SimpleGraph/*`, `GroupTheory/PresentedGroup.lean`.

### Foundation: is that presentation the monster?  **Yes — it is a theorem** (settled 2026)

This was the largest risk in the project and it is now closed.  Full evidence in
`refs/README.md`; the short version:

* **Ivanov, *Y-groups via transitive extension*, J. Algebra 218 (1999) 412--435**, abstract:
  Conway conjectured (c. 1980) that the Coxeter diagram `Y555` plus the single spider relation
  `(ab₁c₁ab₂c₂ab₃c₃)¹⁰ = 1` presents the wreath product `M ≀ C₂`; **"This conjecture was proved
  by S. P. Norton and the author in 1990."**  Second treatment: Ivanov, *The Monster Group and
  Majorana Involutions*, CUP 2009.
* **Borcherds, *Problems in moonshine* (2001), Problem 5** confirms it independently and calls it
  the "Y presentation" of the monster from the ATLAS, "conjectured by Conway and Norton and
  finally proved by Ivanov ... roughly the presentation of a Coxeter group with one extra
  relation".  (Borcherds lists the *connection between the presentation and moonshine* as an open
  problem — the presentation is not in doubt, the conceptual link was.)
* **Bray's 1997 tables** record the 12-generator `Y₄₄₃` form we use (arms 4, 4, 3; 79 relators;
  same spider relation), with the remark that `Y₅₅₃` and `Y₅₄₃` present the same group.

Consequences: (a) defining the monster this way is legitimate, and the `formalabstracts`
attribution to a MathOverflow comment should not be propagated as the justification; (b) **`Y_pqr`
notation is ambiguous** — Bray: "There is more than one definition of `Y_pqr` in existence" — so
we fix our convention explicitly (arm lengths are the components of `[4,4,3]`, every bond is
labelled `3`); (c) **S3 is de-risked**: what remains is "does the presented group have order
`|M|`", no longer "is the presentation correct".

### [x] S1 — first attempt: **REJECTED**, superseded by S1b

`Definitions/MMCoxeter.lean` (321 lines, 0 `sorry`, clean build) is a correct formalization of
the **wrong diagram**: it is not the reference `Y443`.  Kept only until S1b replaces it.  Both
defects were verified against the primary source (`formalabstracts/formalabstracts`,
`src/group_theory/presentation.lean` and `src/group_theory/monster.lean`):

1. **Node count.**  `coxeter_vertices {n} (xs : dvector N+ n)` has constructors `torso` and
   `arm : ∀ x : dfin n, dfin (xs.nth'' x) → coxeter_vertices`, so the arm lengths *are* the
   components of `[4,4,3]`: `1 + 4 + 4 + 3 = 12` nodes.  `monster.lean`'s own comment agrees
   ("12 relators of the form x^2=1, one for each node").  The file has 9 nodes, arms `2,2,3`.
2. **Edge labels.**  `matrix_of_graph E x y := if x = y then 1 else if E x y then 3 else 2`
   **discards all annotations**, and `monster.lean` never calls `matrix_of_annotated_graph`.
   Hence every edge of the reference `Y443` has Coxeter number `3`; the file's
   `M 0 1 = M 0 3 = 4`, `M 0 5 = 3` is not what the reference produces.

**Correct reference data**, recomputed by the dispatcher from the source: 12 nodes; edges are
`{torso -- arm i 0}` and `{arm i v -- arm i (v+1)}` for `i < 3` and `v + 1 < (4,4,3) i`, i.e.
`3 + 3 + 3 + 2 = 11` unordered edges; the matrix has `1` on the diagonal, `3` on adjacent pairs
and `2` otherwise.  Counts: `12` ones, `22` ordered edge entries with `3`, and
`144 - 12 - 22 = 110` ordered non-adjacent pairs, i.e. `55` unordered, so
`12 + 11 + 55 = 78` Coxeter relators, exactly as the reference comment states.  (The S1-V
report's "131 ordered non-adjacent pairs" is an arithmetic slip; 78 is right.)

**API facts worth keeping from this attempt** (verified, corrected during S1b):
(1) `tauto` **times out** on a disjunctive relation at the default 200000 heartbeats — use
`rcases h with h|...|h <;> aesop`.  (2) `Matrix.of f i j` is **not** definitionally `f i j`
(`Matrix.of` is `Equiv.refl`), so `decide` cannot see through it; add a `Matrix.of_apply` bridge.
(3) `Matrix.IsSymm` is `∀ i j, A j i = A i j`, the **opposite** orientation to `A i j = A j i`;
discharge the field with `Matrix.IsSymm.ext fun i j => (entry_symm i j).symm`.
(4) **`decide` works on `Finset`/`Multiset` counts -- but only if the `Decidable` instance actually
computes.**  A `DecidableRel` written with `if h : ...` inside a dependent pattern match gets
**stuck**, and can produce an `isFalse` whose proof term does not match, so `decide` reports
*"proved that the proposition is false"* for a **true** goal; this was misdiagnosed twice (first as
a `Finset`-reduction limitation, then as a `Fin`-proof-component problem).  The fix: prove
`Edge x y ↔ (EdgeBool x y = true)` for a `Bool` function comparing `Nat`s (`v.val`, `w.val`)
rather than `Fin`s, then `DecidableRel Edge := fun x y => decidable_of_iff (EdgeBool x y = true) _`.
After that `Fintype.card = 12`, the `Finset` counts and the full `144`-entry multiset go through
with no timeout.  Remaining limitation: `Decidable (∀ i j : Fin n, ...)` has no instance, so write
`forall`-shaped facts as a filtered `Finset` count, e.g.
`(sq.filter (fun p => p.1 != p.2 && M p.1 p.2 < 2)).card = 0`.
(5) `cases h` on `h : EdgeD x x` with `x` a variable does **not** close (unification needs `x` to
be a constructor application); `cases x with | torso => ... | arm i v => ...` first.  Likewise
`rw [h, h]` on `X = X` fails after `subst`; use `(h.trans h.symm)`.

**Anti-pattern to avoid:** a "verification" theorem that does not mention the object it claims to
verify.  S1's `Y443Matrix_off_diagonal_multiset` was `9 + 4 + 14 + 54 = 81` conjoined with
`Multiset.add_assoc` -- true of every matrix, and its arithmetic was false of its own.  Any
theorem whose job is to certify a definition must have that definition's term in its statement.

### [x] S1-V — independent verification: verdict **WRONG**
* Ran as an adversarial check and reported honestly; it found both defects above and refuted
  the claimed `decide` obstruction.  Its evidence was re-verified by the dispatcher against the
  primary source before acting on it.
* Its one error: the "131 ordered non-adjacent pairs" count (should be 110, see above).

### [x] S1b — the actual `Y4 4 3` Coxeter matrix (12 nodes, every edge labelled 3) — **ACCEPTED**
* Deliverable: `Definitions/MMCoxeter.lean`, rewritten from scratch (348 lines, Mathlib only,
  0 `sorry`/`axiom`/`native_decide`).
  * `MM.Y443Arms : Fin 3 -> Nat` with `4, 4, 3`; `MM.Y443Vertex` inductive (`torso` and
    `arm i v` for `v : Fin (Y443Arms i)`) with `DecidableEq`, `Fintype`, and
    `Y443Vertex_card : Fintype.card = 12`.
  * `MM.Y443EdgeD` (the two directed `coxeter_edges_directed` constructors) and
    `MM.Y443Edge` (its symmetric closure), with `Y443Edge_symm`, `Y443Edge_irrefl`,
    `Y443EdgeD_card = 11`, `Y443Edge_card = 22`.
  * `MM.Y443Matrix : CoxeterMatrix Y443Vertex`, `1` on the diagonal, `3` on the `11` bonds, `2`
    otherwise, built with `Matrix.of` plus the `Y443Matrix_apply` bridge.
  * `MM.Y443Matrix_multiset`: the `144` entries are exactly
    `replicate 12 1 + replicate 22 3 + replicate 110 2`, **stated about `Y443Matrix.M` itself**,
    so it is non-vacuous.
  * `MM.Y443 := Y443Matrix.Group`, `Group` instance, `y443CoxeterSystem`, `y443Simple` with
    `y443Simple_mul_self`, `y443Simple_mul_simple_pow`, `y443_closure_range_simple`,
    `y443Simple_surjective`.
  * Spider generators `MM.y443A`, `MM.y443B i`, `MM.y443C i` (`i : Fin 3`) and
    `MM.y443Spider` with `y443Spider_def : y443Spider = (A * B 0 * C 0 * A * B 1 * C 1 * A * B 2 * C 2)^10`.
* Acceptance: **passed** — clean full-package build, no `sorry`/`axiom`, axioms exactly the
  three standard ones; dispatcher re-read the primary source and checked the multiset theorem's
  statement verbatim before merging.
* Verified against the reference a second time by S1b itself, independently of the brief.
* Weaker than the brief: `Y443Edge_card_half` is stated as `22 / 2 = 11`, not as a genuine
  unordered-pair cardinality (no convenient `Sym2` API was found); and the file is 348 lines
  against the ~300 guidance (one coherent unit: diagram -> matrix -> group -> generators).
* Recorded in `README.md`'s module table; merged to `main` on branch `task/s1b`.

### [x] S2 — the spider relation and `Monster` — **ACCEPTED**

* Deliverable: `Definitions/MMMonster.lean` (249 lines, 0 `sorry`/`axiom`/`native_decide`),
  wired into `FinalCheck.lean` with four guarded `#print axioms` checks.
  * `MM.y443NormalClosure := Subgroup.normalClosure ({y443Spider} : Set Y443)`, with the `Normal`
    instance — the Lean 3 `group_modulo_relations` applied to the singleton;
  * `MM.Y443Quotient := Y443 ⧸ y443NormalClosure` with `Group`, and `MM.y443Projection`;
  * `MM.monsterCenter := Subgroup.center Y443Quotient`; `MM.Monster := Y443Quotient ⧸ monsterCenter`
    with `Group`, and `MM.monsterProjection`;
  * **`MM.Monster_eq : MM.Monster = (MM.Y443Quotient ⧸ Subgroup.center MM.Y443Quotient)` is `rfl`**
    — i.e. the definition *is* the reference's, definitionally, which is exactly the kind of
    evidence wanted here;
  * `MM.monsterMk : Y443 →* Monster`, `monsterMk_apply`, `monsterMk_one`,
    `monsterMk_eq_one_iff`, `monsterMk_ker` (the kernel is
    `y443NormalClosure ⊔ monsterCenter.comap y443Projection`, via `MonoidHom.comap_ker`),
    `monsterMk_surjective`, `monsterMk_range_eq_top`, and `monsterMk_y443Spider` (the spider
    relator really is imposed);
  * a genuinely non-obvious lemma: `MM.y443Spider_mem_center` — the *image* of the spider lies in
    the centre of `Y443Quotient`, so the second quotient contributes nothing on the spider.  The
    proof is that the normal closure contains `spider⁻¹ * a⁻¹ * (spider * a)` for every `a`.
* Acceptance: **passed** — clean full-package build; no `sorry`/`axiom`; axioms exactly the three
  standard ones; dispatcher read the definitions and confirmed `Monster_eq` is `rfl`.
* **Non-triviality was attempted and correctly abandoned.**  The abelianisation argument cannot
  work, and the agent computed *why* rather than asserting it: the spider has word length
  `9 * 10 = 90` with each factor of order 2, so its image in the abelianisation
  `∏ᵥ ZMod 2` is `1 ^ 90 = 0`, i.e. the spider lies in the kernel of the abelianisation, which
  therefore does not descend to `Y443 ⧸ ⟪spider⟫`.  More fundamentally, the monster is perfect,
  so **every** abelian quotient is trivial and no abelian argument can ever detect
  non-triviality.  This is recorded in the file's `Nontriviality` section.  Consequence: `S3`
  is the only route to non-triviality, finiteness, and the order.
* Honest status of "does the reference definition give the monster": the definition matches the
  reference *definitionally*; the theorem that the reference presents `M × C₂` is
  **Norton–Ivanov 1990** (`refs/README.md`) and is **not** formalized here.  So the remaining
  gap is a named, cited theorem, not an unexamined assumption.

**Independent verification (S2-V): verdict `CONFIRMED`.**  A separate agent checked every link
against the Lean 3 source and by compiling its own probes: `y443NormalClosure` is the normal
closure of the *singleton* (proved minimal, contains all conjugates, so it agrees with Lean 3's
`closure (conjugates s)` — though no Mathlib lemma identifies the two definitions, the agreement
is semantic); `monsterCenter` is `Subgroup.center` of *that* quotient; `Monster_eq` is `rfl`.
Two findings were acted on, see the commit:

* **`monsterMk_ker` was true but uninformative.**  The join `⟪spider⟫ ⊔ center.comap mk` is the
  *whole group*, because the projection is surjective so the second summand is already `⊤`.  The
  theorem is now stated in the informative form `monsterMk.ker = center.comap mk`, matching what
  the proof derives internally.
* **The non-triviality paragraph was duplicated and gave a weak reason.**  Rewritten: the
  obstruction is structural (every relation `(sᵢsⱼ)^m = 1` is a word of length `2m`, hence `1` in
  any abelian quotient; the abelianisation of `Y443` is `ZMod 2`, not a product of twelve copies,
  because `m = 3` is odd forces all generators to the same image; the spider has length `9·10`.
  The two arithmetic lemmas are now labelled as bookkeeping, and building the actual map
  `Y443 →* Multiplicative (ZMod 2)` via `Abelianization.lift` is recorded as a refinement.

**Correction to the S2-V report itself:** it claimed the parity argument was wrong and that the
abelianisation is `∏ᵥ ZMod 2`.  Both are incorrect — in an abelian quotient `(sᵢsⱼ)^m = 1` with
`m ≥ 2` forces `sᵢsⱼ = sⱼsᵢ`, and with `m` odd it forces `sᵢ = sⱼ`.  The verifier's alternative
("the spider lies in the commutator subgroup, every abelian quotient kills it") is also true and
is now recorded alongside; it is the same phenomenon.

**Mathlib API facts found here — worth not rediscovering** (all verified):

| need | exact name |
| --- | --- |
| normal closure | `Subgroup.normalClosure : Set G → Subgroup G`; instance `Subgroup.normalClosure_normal` |
| quotient type / map | `G ⧸ N`; `QuotientGroup.mk' N : G →* G ⧸ N`, `QuotientGroup.mk'_apply` |
| centre | `Subgroup.center G`; normality is **`Subgroup.instNormalCenter`** (there is no `center_normal`); membership `Subgroup.mem_center_iff` |
| kernel | `MonoidHom.ker`, `MonoidHom.mem_ker` (use `.mp`; do **not** write `(MonoidHom.mem_ker f).mp`) |
| kernel of a composite | **there is no `MonoidHom.ker_comp`**; use `MonoidHom.comap_ker g f : (g.comp f).ker = g.ker.comap f` |
| kernel of a quotient map | `QuotientGroup.ker_mk' N : (QuotientGroup.mk' N).ker = N` |
| equality in a quotient | `QuotientGroup.eq_one_iff`, `QuotientGroup.eq`, or `Quotient.sound ∘ QuotientGroup.leftRel_apply.mpr`; prefer the last, because `rw [QuotientGroup.eq]` fails when the goal prints as `↑a * ↑s = ↑s * ↑a` rather than `↑(a*s) = ↑(s*a)` |
| conjugation-closed | **`Subgroup.Normal.conj_mem' n hn g : g⁻¹ * n * g ∈ N`** — counter-intuitive argument order (third argument is the conjugated element, fourth the conjugator) and it produces `g⁻¹ * n * g`, not `g * n * g⁻¹` |
| comap of top | `Subgroup.comap_top f : (⊤ : Subgroup N).comap f = ⊤` (not `comap_id`) |
| induction on a quotient | `QuotientGroup.induction_on`, branch syntax `| _ a => ...` |

### [ ] S3 — `Monster` is finite, of the known order
* Deliverable: `Finite MM.Monster` and/or `Nat.card MM.Monster = 808017424794512875886459904961710757005754368000000000`.
* Acceptance: builds, no `sorry`.
* Risk: **very high**.  Lean 3 did not prove this.  The realistic route is a permutation
  representation (the monster acts on 196884 points of the Griess algebra) or the
  `2²⁴·Co₁` route; either is a project of its own.  If this task proves intractable, the
  fallback is to keep `Finite` as a *hypothesis* in `MoonshineModule` and record it here.

> **S3-RECON LANDED (task agent, dispatcher-reviewed 2026-09): NONE of the three "real" routes is
> dispatchable, and the reason is structural rather than a matter of effort.**  `Finite MM.Monster` is
> not a statement about a concrete group but about a **presentation**: `MM.Monster` is
> `Y443 ⧸ ⟪spider⟫ ⧸ center` (`Definitions/MMMonster.lean`).  Every Mathlib mechanism for `Finite X`
> with `X` presented is a `MulEquiv` with a known finite type, an injection into one, or a surjection
> out of one — there is **no Todd--Coxeter, no coset enumeration, no rewriting engine, and no
> finiteness theorem about any presented group except the trivial "finite ⟹ finitely presented"**
> (`FinitelyPresentedGroup.lean:176`) — and any upper bound for `Nat.card MM.Y443Quotient` is verbatim
> a normal-form certificate for the 12-generator presentation of `M × C₂`, with `2·|M| ≈ 1.6 × 10^54`
> entries.  **So S3's *first* half is already the hard half.**  Route (c) ("finiteness and the order
> from the presentation via Seysen") does not exist: neither Seysen paper proves anything from a
> presentation — they implement a *given* representation.  Route (b) is a strict sub-part of (a), and
> (a) — the only route that has ever worked mathematically — would still not prove `Finite
> MM.Monster`, for the reason above.
>
> **Correction of record: the 51-digit order literal that circulated in the dispatching brief is
> wrong; the 54-digit literal in this entry's own Deliverable line above is right** — verified here by
> recomputing the product (`2^46·3^20·5^9·7^6·11^2·13^3·17·19·23·29·31·41·47·59·71`), whose value
> equals the Deliverable literal and is `1000 ×` the brief's.  No file in the repository carries the
> wrong literal (checked by search over `ROADMAP.md`, `README.md`, `Challenge.lean`,
> `Definitions/MMMonsterMoonshine.lean`, `FinalCheck.lean`).  A Lean statement with the brief's numeral
> would be a false statement about `MM.Monster`.
>
> **Recommendation, and the dispatchable first increment (S3-D).**  Take the recorded fallback (d),
> but *sharpened*: make the missing input a named, non-vacuous declaration with proved conditional
> consequences, and attempt none of (a)/(b)/(c) as a route to finiteness or the order.  The brief is
> new file `Definitions/MMMonsterOrder.lean` (≈150--250 lines, one agent-run, low risk): (1)
> `Finite MM.Y443Quotient → Finite MM.Monster` (the quotient map is surjective); (2) under that
> hypothesis, `Nat.card MM.Monster = MM.monsterCenter.index`; (3) a named
> `MM.NortonIvanovPresentation : Prop` — `Nonempty (MM.Y443Quotient ≃* (MM.Monster × Multiplicative
> (ZMod 2)))` — whose docstring says that this is Norton--Ivanov 1990, that it is **not** proved here,
> that its only known proof is a coset enumeration, and that it is the only missing input for
> finiteness; (4) its conditional consequences, including explicitly that it does **not** give the
> order; (5) a scope section saying that no finiteness, order or non-triviality of `MM.Monster` is
> proved and that the order is a third, independent input.  The full report, with the per-route
> pricing, the verified Mathlib inventory (`path:line`) and the literature (Seysen ×2, Aschbacher, the
> ATLAS) is `Probe/S3_RECON.md` (gitignored — this block is its committed substance).
>
> **S3-D LANDED, dispatcher-verified (2026-09): the fallback is now declarations, not prose.**
> `Definitions/MMMonsterOrder.lean` (244 lines, 20 declarations, guarded in `FinalCheck.lean`)
> proves the **free** direction — `MM.finite_monster_of_finite_y443Quotient : Finite MM.Y443Quotient →
> Finite MM.Monster` — the index formula for the centre (`MM.card_monster_eq_monsterCenter_index`,
> `MM.card_monster_mul_card_monsterCenter`) and, **with** the identification, that the centre *is*
> the `C₂` (`MM.card_monsterCenter_eq_two_of_nortonIvanov`).  It names the two inputs as `Prop`s
> (`MM.Y443QuotientFinite`, `MM.NortonIvanovPresentation`, quoted from Ivanov's abstract as
> `refs/README.md` has it) and a third for the order (`MM.MonsterOrder`), and it settles the order's
> arithmetic in Lean: the **54-digit** numeral `MM.monsterOrder`, its prime-power factorization, its
> digit count, and `MM.monsterOrder_ne_wrongLiteral` — **the 51-digit literal that circulated in this
> dispatcher's brief is now refuted by a theorem.**  **The task caught a real error in its own
> brief:** `NortonIvanovPresentation → Finite MM.Monster` is *not provable* (an isomorphism with
> `M × C₂` bounds neither side), so the finiteness engine is `Y443QuotientFinite` and the delivered
> theorem carries it explicitly — nothing was weakened.  Dispatcher-verified from source: `--- OK ---`
> for `MMCoxeter`, `MMMonster`, `MMMonsterOrder` and an independent axiom probe,
> `forbidden_tokens` 0/0/0/0, every guarded declaration on `[propext, Classical.choice, Quot.sound]`
> (two arithmetic ones on `[propext]` alone), and `FinalCheck.lean` green with the new guards.
> **What is missing is unchanged and is the hard part:** the finiteness of the presented quotient,
> and then its order.

### [x] S4 — retarget `MoonshineModule` to `MM.Monster` — **ACCEPTED (S4 + S4b, this session)**
* Deliverable: `MoonshineModule.G` instantiated at `MM.Monster`, so that
  `MM.moonshine_conjecture` becomes a statement about the Fischer--Griess monster.
* Depends on S2 (S3 optional).
* **PROGRESS (this session).**  `Definitions/MMMonsterMoonshine.lean` (207 lines) supplies
  `MM.MoonshineModule.IsMonsterModule M := Nonempty (M.G ≃* MM.Monster)`,
  `MM.MoonshineModule.MoonshineConjectureStatementMonster` (the headline with that conjunct),
  proved reductions to `MoonshineConjectureStatementGenus` and to the pre-D0-g statement, and — as
  real content rather than plumbing — **`MM.MoonshineModule.reindex`**, which transports a whole
  `MoonshineModule` along a group isomorphism (graded pieces, actions, traces, `replication` via
  `map_pow`), so that `isMonsterModule_reindex` makes the monster property a property of the
  **isomorphism class** and the statement is not an artefact of a presentation.
  **What is NOT bought, and is recorded in the file:** no finiteness, order or non-triviality of
  `MM.Monster` (that is **S3**), no formalized identification with Griess's construction (the cited
  Norton--Ivanov theorem), and no inhabitant — `IsMonsterModule` is not known satisfiable because no
  `MoonshineModule` is known at all.
  **THE RE-POINT IS DONE (task S4b).**  `IsMonsterModule` and `MoonshineConjectureStatementMonster`
  moved into `MMMoonshine.lean` (which now imports `Definitions.MMMonster`, verified acyclic), so the
  standing goal is
  `MM.MoonshineModule.moonshine_conjecture : MoonshineConjectureStatementMonster := by sorry`
  — the repository's one open-problem `sorry` now names `MM.Monster`.  `Challenge.lean` follows, and
  `MMGenusZeroStatement.lean` / `MMLevelOneGenusZero.lean` had docstrings that had just become false
  and were corrected.  The proved chain is monster ⟹ genus ⟹ pre-repair, and each level has a
  non-vacuity theorem.  **Still not bought:** finiteness/order (S3) and the cited Norton--Ivanov
  identification.

---

## Stream T — the monster Lie algebra and (8.3) (removes assumed input 3)

### [x] T1 — formal power series infrastructure for (8.3) — **PARTIAL, merged**

The scope of T1 turned out to be three things, not one: the infrastructure (done), a Mathlib gap
(found and named), and the Möbius inversion (deferred to T2).  Recorded accordingly.

* Deliverable: `Definitions/MMPowerSeries.lean` (170 lines, 19 declarations, 0 `sorry`/`axiom`).
  **Design decision, now settled:** the paper's two-variable series live in
  `PowerSeries (HahnSeries ℤ ℚ)` — power series in `p` whose coefficients are formal Laurent
  series in `q`.  `MvPowerSeries.exp` does not exist in Mathlib, whereas `PowerSeries.exp`/`log`
  need only `[CommRing A] [Algebra ℚ A]`, which this ring has; and the convergence structure is
  right (each `p`-degree is affected by only finitely many factors).
  * `MM.EulerSeries` and `MM.adamsLog`: verbatim the paper's `E = Σ_{m>0,n∈ℤ} c(g,mn) pᵐ qⁿ` and
    `L = Σ_{i>0} Σ_{m>0,n∈ℤ} c(g^i,mn) p^{mi} q^{ni}/i`, the `i`-th term of `L` being the Adams
    operation `ψⁱ`.
  * `MM.monomial`, `coeff_monomial`, `MM.qCoeffOfBounded` with `qCoeffOfBounded_mono`
    (independence of the truncation bound).  The bound is an explicit parameter rather than
    extracted by `Classical.choice` from the finiteness hypothesis — cleaner, and it means every
    downstream statement carries a bound until a bound-extraction lemma is available.
  * `MM.seriesIdentity_of_adamsLogIsLog`: the paper's exponential form `exp L = 1 + E`, derived
    from the two named hypotheses below.
  * Non-vacuity: `eulerSeries_zero`, `adamsLog_zero`, `adamsLogIsLog_zero`.
* **Not proved, stated as named `Prop`s rather than asserted** (this is the honest record):
  * `MM.ExpLogOf (f) : expOp (logOf f) = f` — **a genuine Mathlib gap.**  In this revision
    `PowerSeries/Exp.lean` and `Log.lean` provide `exp_unique_of_derivative_eq_self`,
    `derivative_exp`, `deriv_log`, `logOf_eq`, `logOf_one_add_X`, `HasSubst.log`,
    `HasSubst.exp_sub_one`, `derivative_subst` — but **nothing composes `exp` with `logOf`**.
    The missing ingredient is a chain rule for `PowerSeries.subst` at `log` (or at `exp - 1`),
    i.e. `derivative (subst g f) = subst g (derivative f) * derivative g`, usable at `g = log`;
    `derivative_subst` exists precisely for that purpose and is not yet applied to `log`.
    Dispatcher note: the route is `exp_unique_of_derivative_eq_self` on `expOp (logOf f)`, whose
    derivative is `expOp (logOf f) * (derivative f / f)`; the first factor is the inductive
    hypothesis and the second is `f' / f`, so the identity follows once the chain rule is in
    place.  The `f` must have `constantCoeff f = 1`, and the target is to state it in
    `PowerSeries A` for `A` a `ℚ`-algebra (our use is `A = HahnSeries ℤ ℚ`).
  * `MM.AdamsLogIsLog (c) (g) (bound) : adamsLog c g bound = logOf (1 + EulerSeries c g bound)`
    — **this is the Möbius inversion (10.3) ⇒ (10.4)**, i.e. T2's target.
  * The root-multiplicity formula (10.4) with `ArithmeticFunction.moebius`, and the recursion
    (9.1): **not attempted** (reported as such rather than half-done).
* Acceptance: build exits 0 for all modules; no `sorry`/`axiom`/`native_decide`; axioms exactly
  the three standard ones.
* Note for the next agent: `PowerSeries.exp` is an **element**, not a function, in this Mathlib
  revision; `MM.expOp` wraps it.
* **Next task becomes `T1b` (below), not T2**: the cheap half of T2 is the Mathlib gap.

### [x] T1b — the composition law `exp ∘ logOf f = f` — **ACCEPTED**

> **CLOSED.**  `Definitions/MMExpLog.lean` now proves the theorem the task asked for:
> `MM.expOp_logOf_eq (f) (hf : PowerSeries.constantCoeff f = 1) : expOp (PowerSeries.logOf f) = f`,
> with the uniqueness step it rests on, `MM.eq_zero_of_derivative_eq_mul (hd : derivative h = h * L')
> (hc : constantCoeff h = 0) : h = 0`, and the two consequences that wire it into
> `Definitions/MMPowerSeries.lean`: `MM.expOp_logOf_holds` and
> `MM.seriesIdentity_of_adamsLogIsLog`.  Build exits 0; all four new declarations are guarded in
> `FinalCheck.lean` and print exactly `[propext, Classical.choice, Quot.sound]`.
>
> **Two corrections to the plan recorded below, both verified by compiling.**
> 1. **The uniqueness lemma needs NO hypothesis on `L'`.**  The plan's `constantCoeff L' = 1` is not
>    merely unused, it is **false** at the intended instantiation `L' = (logOf f)'`:
>    `constantCoeff ((logOf f)') = coeff 1 f`, which is `2` for `f = 1 + 2X`.  A lemma stated with
>    that binder could never have been applied.  The induction needs only that `n + 1` is not a zero
>    divisor (`MM.instIsAddTorsionFreeHahnSeries`); even `L' = 0` is allowed.  The task's own
>    justification ("valid because `L'` is a unit with constant coefficient `1`") was wrong about
>    *why*.
> 2. **The last step is one subtraction, not the `f⁻¹` route.**  The plan's steps 4--7 (product rule,
>    `PowerSeries.derivative_inv'`, `(S * f⁻¹)' = 0`) are unnecessary: `h := S - f` already has
>    `h' = h * L'` and `constantCoeff h = 0`, so `S = f` directly.  No inverse, no unit argument.
>
> **API fact worth keeping** (it cost a probe round): in this Mathlib pin `Finset.antidiagonal` is
> the `Set.IsPWO` version, so `Finset.mem_antidiagonal` has the wrong type for the ℕ-antidiagonal
> that `PowerSeries.coeff_mul` produces.  The right names are
> **`Finset.HasAntidiagonal.antidiagonal`** and **`Finset.HasAntidiagonal.mem_antidiagonal`**, and
> `omega` then reads the membership directly (`p.1 ≤ n`).  Likewise `Nat.cast_succ` +
> `nsmul_right_inj (Nat.succ_ne_zero n)` is the working idiom for cancelling `(n + 1)` over
> `HahnSeries` -- there is **no** synthesizable `CharZero (HahnSeries ℤ ℚ)`.
>
> **New finding, and it changes how T2 is wired (flagged for T2, not resolved here).**
> `MM.constantCoeff (1 + EulerSeries c g bound) ≠ 1` whenever `c g 0 ≠ 0` -- the `p^0` coefficient of
> `EulerSeries` is `Σ_{1 ≤ m ≤ bound} c(g,0) q^m`, non-zero for the monster, where `c(g,0) = 1`.  So
> `expOp_logOf_eq` **cannot** be applied to `1 + EulerSeries c g bound` without a constant-term
> hypothesis, and `MM.seriesIdentity_of_adamsLogIsLog` now carries that hypothesis explicitly.  The
> paper's series carries the `p⁻¹` prefactor of (8.3), which is what removes the term.  Verified by
> compiling, not merely asserted.

**Delivered and guarded** (T1b's own scaffold; the file has since grown to carry the closure above):

| declaration | statement |
| --- | --- |
| `MM.deriv_log_eq_inv` | `(log A)' = (1 + X)⁻¹` over `A = HahnSeries ℤ ℚ`, from `MMGeomSeries` |
| `MM.subst_inv_one_add_X` | `subst (f - 1) ((1+X)⁻¹) = f⁻¹` |
| `MM.derivative_logOf_mul` | **`(logOf f)' * f = f'`** — the identity that drives the route |
| `MM.constantCoeff_expOp_logOf` | `constantCoeff (subst (logOf f) (exp A)) = 1` |
| `MM.derivative_eq_mul_derivative_logOf` | `f' = f * (logOf f)'` |

plus the previously landed `HasSubst` facts and `MM.instIsAddTorsionFreeHahnSeries`, and
`Definitions/MMGeomSeries.lean` (committed as `c728014`) with the geometric series.

#### Earlier history of this entry (kept: each revision was wrong in an instructive way)

This entry has been rewritten twice, and the previous two readings were **both wrong**.  **Read all of
it before dispatching; the two failure modes recorded here cost two full rounds.**

**Attempt 1 (agent, no file modified)** corrected the map but left the task believed to be "a few
hours, bookkeeping".  Its one durable contribution was closing the instance gap (Correction 2 below).
Its failure mode was "probe for a guessed lemma name instead of reading the file".

**Attempt 2 (agent) killed the substitution route outright.**  The results, re-verified by the
dispatcher:

1. **`Probe/Probe.lean` does not compile** — `tools/build.ps1 Probe/Probe.lean` exits 1 with
   three errors (`24:6` a failed `rw` pattern, `28:79` where `MvPowerSeries.C 1 = PowerSeries.C 1`
   is not `rfl`, `40:4` where `subst_comp_subst_apply` wants `HasSubst (exp A)` and is handed
   `HasSubst (exp A - 1)`); its `h1` step `subst (exp A - 1) f = f - 1` is **false** (at
   `f = 1 + X`: left `exp A`, right `X`).  Attempt 1 had recorded this probe as a "compiling
   witness"; it had never been compiled.  **A scratch file that "must compile" is not evidence until
   it has been compiled.**
2. **The substitution route is circular, not bookkeeping.**  `subst_comp_subst_apply`
   (`Substitution.lean:391`) is functoriality of `subst a : p ↦ p(a)`; it rewrites one composite
   substitution into another and can never identify a composite with a given series (at `p = X` it
   degenerates to `subst a b = subst a b`).  The three identities the route needs —
   `subst (log A) (exp A - 1) = X`, `subst (exp A - 1) (log A) = X`, `subst (log A) (exp A) = 1 + X`
   — are each **equivalent to `exp (log (1+X)) = 1+X`**, i.e. to the statement being proved.

**Correction 2 stands, and is delivered.**  `IsAddTorsionFree (HahnSeries ℤ ℚ)` is not synthesizable,
and `PowerSeries.exp_unique_of_derivative_eq_self` demands it; the instance is now
`MM.instIsAddTorsionFreeHahnSeries` in `Definitions/MMExpLog.lean`, with the `HasSubst` facts
(`MM.hasSubst_logOf`, `MM.hasSubst_sub_one`), `MM.expOp_eq_subst_comp` and
`MM.hasSubst_logOf_one_add_X`.

**Not delivered at that round:** `MM.expOp_logOf` / `MM.ExpLogOf` as theorems — they were the
`Prop`-valued definitions of `MMPowerSeries.lean:193,218`, and **exactly one step was missing**: with
`h := subst (logOf f) (exp A) - f` and `L := logOf f`, the product rules give `h' = h * L'` and
`constantCoeff h = 0`, and what was needed was `h' = h * L' → constantCoeff h = 0 → h = 0` —
uniqueness for a first-order linear equation over `A`, by induction on the coefficient using
`coeff n (h * L') = coeff (n+1) h * (n+1)`.  `PowerSeries.derivative.ext` does **not** give this
(it needs `h * L' = 0`, which is the conclusion); **short-circuiting it produces a self-referential
proof that Lean rejects** (`fail to show termination`) — that is how the gap was found.

**Three dead ends, recorded so they are not re-entered:** (1) the substitution route is circular
(above); (2) `subst (logOf f) (exp A) = exp A` is **false** — `subst` is composition, so it says
`exp ∘ logOf f = exp`, and `logOf f ≠ X`; (3) the constant coefficient does **not** come from
`PowerSeries.constantCoeff_subst`, whose `finsum` collides with the `MvPowerSeries`/`PowerSeries`
namespace split — `MM.constantCoeff_expOp_logOf` splits `exp A = 1 + (exp A - 1)` instead.

**The live route that closed it: derivative.**  With `S := subst (logOf f) (exp A)`,
`hf : constantCoeff f = 1`, and `A = HahnSeries ℤ ℚ`:

1. `(f - 1)' = f'`.
2. `(logOf f)' = ((log A)').subst (f - 1) * (f - 1)'` by `PowerSeries.derivative_subst`
   (`Derivative.lean:140`) at `g = f - 1`, using `HasSubst (f - 1)` from `hasSubst_sub_one`.
3. **The one substantive identity: `f' = f * (logOf f)'`.**  `PowerSeries.deriv_log`
   (`Log.lean:67`) gives `(log A)' = mk fun n ↦ algebraMap ℚ A ((-1)^n)`, so this needs the
   geometric-series identity `mk (fun n ↦ ((-1 : ℚ) ^ n : A)) * (1 + X) = 1`, i.e.
   `(log A)' = (1+X)⁻¹`, and then that `subst` carries inverses:
   `((1+X)⁻¹).subst (f - 1) = ((1+X).subst (f - 1))⁻¹ = f⁻¹`, the last step by
   `(1+X).subst (f - 1) = 1 + (f - 1) = f`.  **The geometric-series identity comes first: it is
   independent, it is real work, and everything else depends on it.**
4. `S' = S * (logOf f)'` by `derivative_subst` at `g = logOf f`.
5. Hence `(S * f⁻¹)' = 0` (product rule plus `PowerSeries.derivative_inv`, `Derivative.lean:117`;
   `f` is a unit since `HahnSeries ℤ ℚ` is a field and `constantCoeff f = 1`).
6. `S * f⁻¹ = 1` from step 5, `constantCoeff (S * f⁻¹) = 1`, and `PowerSeries.derivative.ext`
   (`Derivative.lean:112`, needs `[IsAddTorsionFree R]`) — or by `PowerSeries.coeff_derivative`
   (`Derivative.lean:60`), which gives `coeff (n+1) = 0` for all `n` directly.
7. `S = S * f⁻¹ * f = f`.

**Four "obstructions" recorded by attempt 2 are mostly false** (attempt 3 measured each):
(a) `Finset.sum_eq_single` *does* match the `antidiagonal` binder notation — Mathlib itself writes
`rw [coeff_mul, Finset.sum_eq_single (d, n), ...]` at `RingTheory/PowerSeries/Basic.lean:347`; the
real trap is that `rw [sum_eq_single a]` emits its subgoals in the order "`a ∉ s` first, main
equality second", the opposite of `apply`; (b) pair projections do **not** need `show` —
`norm_num`/`ring` handle them; (c) `set_option maxHeartbeats 800000` is **not** needed, the default
200000 suffices.  Only the fourth (using `eq_inv_iff_mul_eq_one`, `Inverse.lean:178`, not the
reversed `inv_eq_iff_mul_eq_one`) survived.  **A reported blocker is a hypothesis too.**

**The winning tactic is a change of ring, not new mathematics.**  Working directly over
`A = HahnSeries ℤ ℚ` puts an `algebraMap ℚ A` in every coefficient and `ring` cannot close the
arithmetic; working over `ℚ` makes the coefficients plain rationals and `ring`/`norm_num` finish,
after which `PowerSeries.map` pushes the result to `A`.

> **CORRECTION (attempt 4, verified by the dispatcher).**  Attempt 3 reported that
> `Probe/Geom4.lean` "compiled" `altQ`, `coeff_one_add_X`, `mem_one`, `mem_zero`,
> `sum_eq_two_terms` and `third_pair_zero`.  **It did not compile at all.**  The dispatcher
> reproduced it: `lean` on `Geom4.lean` exits non-zero at line 44 (`rw` cannot find its pattern in
> `F (1, n) = F (1, n) + F (0, n+1)`), and `build/lib/lean/Probe/` contained no `.olean` for it.
> **The dispatcher then repeated the mistake by putting "Geom4 already compiles" into the attempt-4
> brief without verifying it — the third occurrence of this failure mode in this task, and the one
> that cost a whole round.**  Do not treat any `Probe/` file as a starting point unless you have
> just compiled it yourself.
>
> What attempt 4 *did* establish, by its own `#eval`: `coeff j (1+X)` is `[1, 1, 0, 0, 0]` for
> `j < 5`, and the two-term sum `(-1)^m·[X^m](1+X) + (-1)^(m+1)·[X^(m+1)](1+X)` vanishes for every
> `m` — identically zero, not merely for `m ≥ 2`.  It compiled `coeff_altQ`, `coeff_altQ_zero`,
> `coeff_altQ_one`, `coeff_one_add_X_zero/one/of_two_le`, `summand_eq_zero_of_two_le`, both
> elimination branches of `sum_eq_two`, and both `m`-branch arithmetics.  **Not obtained:**
> `altQ * (1 + X) = 1`.
>
> Two residuals, both `Finset` bookkeeping rather than mathematics: `Finset.sum_eq_single` leaves a
> **membership side goal** that `rw [Finset.mem_antidiagonal]` cannot discharge (the goal mentions
> `Finset.HasAntidiagonal.antidiagonal`), and `PowerSeries.coeff_one` produces its condition in
> **`m.succ` form**, so `if_neg` on an `m + 1`-shaped hypothesis does not fire.  Also measured: `rw`
> with an elaboration-bearing argument (`rw [lemma (by tac)]`) produces spurious `⊢ False` goals
> inside a longer chain — use `have h := lemma (by omega)` then `rw [h]`; and `Prod.ext` takes `fst`
> first.  **Attempt 5's route avoids `antidiagonal` altogether**: split `altQ * (1+X) = altQ + altQ * X`
> and use `PowerSeries.coeff_mul_X_pow` (`Basic.lean:345`), which sends `coeff (m+1) (altQ * X)` to
> `coeff m altQ`, leaving the pure arithmetic `(-1)^(m+1) + (-1)^m = 0`.
>
> **Meta-lesson, now in `AGENTS.md`:** an uncompiled file is not evidence, and neither is a
> dispatcher's summary of one.

**Attempt 3's own error, located:** in `altQ_mul_one_add_X` it negated the coefficients of
`[X^m](1+X)` and `[X^(m+1)](1+X)`.  The correct values are `m = 0 → 1`, `m = 1 → 1`, `m ≥ 2 → 0`
for the first, and `m = 0 → 1`, `m ≥ 1 → 0` for the second; hence the `m = 1` leaf goal is
`(-1)*1 + 1*0 = 0`, which is true, where attempt 3 wrote `(-1)*1 + 1*1 = 0`, which is false.  That
false leaf — not the tactics — is why its `norm_num`/`ring` finishes kept failing.  The fix is to
discharge the three `if`s (`m = 0`, `m + 1 = 0`, `m + 1 = 1`) with `if_neg` separately before `ring`.

**On the `IsAddTorsionFree` instance — attempt 3's closing recommendation is wrong and must not be
acted on.**  It reported that `MM.instIsAddTorsionFreeHahnSeries` is not needed because
`derivative.ext` needs `[IsAddTorsionFree R]` and `ℚ` is not torsion-free.  The premise is right
(`IsAddTorsionFree` is `to_additive` of `IsMulTorsionFree`, `Algebra/Group/Defs.lean:787`; indeed
`2 • (1/2) = 1 = 2 • 0` in `ℚ`), but the conclusion is backwards: our series live in
`PowerSeries (HahnSeries ℤ ℚ)`, so the `R` in `derivative.ext` **is** `HahnSeries ℤ ℚ`.  It is
**required**, not decorative, and cannot be synthesised.  The alternative it offered (induct on `n`
via `PowerSeries.coeff_derivative`) is a legitimate fallback but is *additional* work.

**Kept from the previous revision, for the record only — this is NOT the route:**
`subst_comp_subst_apply` was claimed to be "the composition law the proof needs" and the two lemmas
below were claimed to suffice via substitution.  Point 2 above refutes that.  The lemmas themselves
are still true statements and are *consequences* of the derivative route, not inputs to it:

```lean
theorem derivative_logOf {f : A⟦X⟧} (hf : constantCoeff f = 1) :
    (d⁄dX A) (PowerSeries.logOf f) * f = (d⁄dX A) f

theorem expOp_logOf (f : A⟦X⟧) (hf : constantCoeff f = 1) :
    expOp (PowerSeries.logOf f) = f
```

* Acceptance: build exits 0; no `sorry`/`axiom`/`native_decide`; axioms the three standard ones;
  and `MM.expOp_logOf`'s theorem statement must agree verbatim with the `Prop` it replaces.
* Risk: **medium-high, not low-medium.**  This is genuine proof work (a geometric series identity,
  substitution of inverses, and a derivative-zero argument), not bookkeeping.  The map above is
  verified at the level of lemma names and signatures; the remaining risk was in steps 3 and 5.

### [~] T2 — the denominator identity (8.3): sections 6--8 (unproved), plus its self-contained §10 half (T2a, `Prop` unproved) — **the apparent (8.3)-vs-(10.1) conflict was a verifier artefact and is closed**

> **T2a CLOSED — the alarm was a VERIFIER ARTEFACT.  The paper's (8.3) and (10.1) AGREE, and the
> repository's `MM.DenominatorIdentity` is a faithful transcription of (8.3).**
>
> Task T2-VERIFY's self-checking exact-arithmetic program (`Probe/t2_verify_result.py`; the fuller
> `Probe/t2_verify.py` carries more self-checks) compares the divisor arithmetic of the two
> printed identities — `[p^a q^b] log PROD = −Σ_{k|gcd(a,b)} mult(a/k,b/k)/k` against
> `[p^a q^b](−L) = −Σ_{i|gcd(a,b)} c(ab/i²)/i` — with no series normalisation anywhere, and reports
> **agreement on all 36 coefficients with `1 ≤ a,b ≤ 6`**: `[p¹q¹] = −196884`,
> `[p²q¹] = −21493760`, `[p²q²] = −20245954698`, `[p³q³] = −65628`.
>
> **A dispatcher error, found by that task and re-verified independently.**  Both the dispatching
> brief and an earlier revision of this entry expected `mult(2,1) = c(2) + c(1)/2 = 21592202`.  That
> is **wrong**: `gcd(2,1) = 1`, so (2.3) has the single term `(d,s) = (1,1)` and
> `mult(2,1) = c(2) = 21493760`.  The value `21592202` mis-sums `ds | m` instead of `ds | gcd(m,n)`,
> the substitution the paper defines in the sentence after (2.3).  Checked by direct implementation:
> `mult(1,1) = c(1)`, `mult(2,1) = c(2)`, `mult(2,2) = c(4)`, `mult(1,−1) = 1` (`V_{−1} = 1`).
> **A wrong expectation in a brief is how a correct formula comes to look broken.**
>
> **Why there were seven unstable runs, in one sentence:** both sides equal
> `P := p·(T_g(p) − T_g(q))` (the `p` matters: (2.1)/(2.2) carry `p⁻¹` on the left), and `P`'s `p⁰`
> block is `−q⁻¹ + Σ c(n)qⁿ`, a **unit** in the `q`-Laurent ring, so comparing `p`-blocks of `log P`
> requires dividing by that `p`-free factor first.  Every shortcut tried — `log(1+(P−1))` (invalid:
> `P` is not `1 + O(p)`), multiplying all blocks by `−q`, forgetting to drop the `p`-free remainder —
> produced a spurious mismatch of exactly `c(1)²`.  The verifier was the problem, not the paper.
>
> **What was actually open in stream T, unchanged and ordinary:** `MM.DenominatorIdentity` is a
> faithful transcription of (8.3) that is **unproved** (task T2 proper, the paper's §6--8), and
> T2a's `(10.4)` was then an unproved `Prop` in the untracked `Definitions/MMRootMultiplicity.lean`.
>
> **One finding that stands, and it is a design question rather than a defect:**
> `MM.EulerSeries`'s `q`-side is one-sided (positive powers) while the paper's sum runs over `n ∈ ℤ`;
> `MM.adamsLog` is faithful — its `q ↦ q^i` substitution is the third argument of `MM.qCoeffOf`, and
> a later agent's report that the `ψ^i` substitution was missing is **false**, settled by the code at
> `MMPowerSeries.lean:112` and `:160`.  Whether to re-express either definition over the two-sided
> ring is the owner's call; the `p`-multiplied `MM.DenominatorIdentity` works around the one-sidedness.
>
> **Two dispatcher errors are on record, both caught by verification rather than by reading:** the
> false `c(1)²` alarm, and the false `mult(2,1)` expectation.  The corollary this entry adds to
> `AGENTS.md`'s *a reported blocker is a hypothesis* is that **the dispatcher's own brief and its own
> arithmetic are hypotheses too**.

> **T2a IS PROVED AND ACCEPTED (2026-09-13).**  `Definitions/MMRootMultiplicity.lean` (261 lines) +
> `Definitions/MMRootMultiplicityArith.lean` (201 lines), both in `FinalCheck.lean` with six
> `#print axioms` guards: **`MM.moebiusSum_adamsSum : 0 < k → moebiusSum (adamsSum B) k = B k`** is
> the Möbius inversion of the `p`-grading — `adamsSum B k = Σ_{i|k} B(k/i)/i` is the `p^k`-block of
> (10.3) — proved coefficientwise in any `CommRing R` that is a `ℚ`-algebra, with **no hypothesis on
> `B`**; the old proof target `MM.moebiusSum_adamsSum_holds` keeps its name and is now a theorem of
> the same statement, so that file carries **no unproved `Prop`** any more.  The paper's (10.4) ⇒
> (10.5) sentence is a theorem too (`MM.moebiusBlock_eq_zero_of_not_dvd`, `MM.multSum_restrict`),
> resting on `MM.sum_moebius_divisors`, `MM.divisors_gcd_eq_filter` and
> `MM.sum_divisors_filter_dvd_moebius`.  **No series occurs in either file**, so none of this touches
> `MM.adamsLog`, `MM.EulerSeries` or `MM.DenominatorIdentity`.  Dispatcher-verified by a from-scratch
> rebuild (`MMRootMultiplicityArith` → `MMRootMultiplicity` → `FinalCheck`, all `--- OK ---`, exit 0)
> and by an independent exact check of the inversion identity itself (50 random families, `k ≤ 60`).
> The remaining content of T2 is therefore **only** the denominator formula of §6--8.

> **SPLIT AND DISPATCHED (dispatcher, 2026-09-13).**  T2 as originally written is "prove
> `MM.DenominatorIdentity` for the moonshine family", i.e. the paper's §6--8 (monster Lie algebra,
> no-ghost theorem, twisted denominator formula) — no Lean machinery for any of it, and the largest
> gap in the project.  Its **§10 half is separable and is T2a**: the Möbius inversion (10.3) ⇒ (10.4),
> pure divisor arithmetic over the coefficient family.
>
> **The source is the author's own TeX** (`../Monstrous moonshine and monstrous Lie
> superalgebras.tex`; see `AGENTS.md`), which settles by quotation what the extracted text left open:
> * **(10.3)** is obtained "if we compare the logarithms of (10.1) and (10.2)"; the `pᵐ`-block form is
>   `Σ_{i | m} C_{m/i}(q^i)/i`, whose inversion is
>   `a_m(q) = Σ_{d | m} (μ(d)/d)·mult_{m/d}(q^d)` — coefficientwise (10.4).
> * **The summation subscript is DEFINED, not guessed.**  Immediately after (2.3) the paper says
>   *"(The symbol `(m,n)` under the summation sign means the greatest common divisor of `m` and `n`,
>   rather than the ordered pair.)"*  So `ds | (m,n)` means `ds | gcd(m,n)`.  **This question was
>   raised to the owner as an ambiguity and is closed by the source**: (2.3) and (10.4) are the same
>   formula with `(d,s)` renamed.
> * **(10.5)** is the paper's own simplification of (10.4): since `Tr(g^d|V_n)` depends only on
>   `(d, N)` with `N = ord g`, the sum `Σ_{ds=k} μ(s)Tr(g^d|·)` vanishes unless `k | N`, so the
>   subscript may be restricted to `(m,n,N)`.
> * The paper then uses this for the seven ATLAS classes (§9--10, (10.6)--(10.8)) and **states
>   explicitly that (9.1) itself is never used** — only that the coefficients for `n = 1,2,3,5`
>   determine all of them.  That is the sentence T3 should have been built on.

> **T2's UNSETTLED box, now SETTLED (after task T2-pre landed `Definitions/MMLogCoeff.lean`).**  The
> UNSETTLED box that stood here recorded two open questions and named the decisive step: derive the
> coefficient formula for `PowerSeries.logOf`.  That is done (`MM.coeff_logOf`), and with it both
> questions are answered — **one of them against the route this entry was built on.**  The material
> below is superseded where the two disagree.
>
> 1. **`MM.AdamsLogIsLog` is FALSE as a general identity** — `MM.not_adamsLogIsLog`, at the
>    coefficient of `p²`, by an explicit counterexample (trivial group, `c(1) = 1`, `bound = 1`)
>    that satisfies `MM.FiniteSupportCoeff`.  So it is not "the Möbius inversion" and cannot be
>    T2's target.  The reduction to a per-degree equality is `MM.adamsLogIsLog_iff`; the coefficient
>    of `adamsLog` is `MM.coeff_adamsLog` (a divisor sum, as the paper's `L` requires).
>    **Scope, and it matters:** the counterexample is **not** `MM.IsReplicable` (it violates the
>    recursion at `k = 2`, `mn = 1`: `c(4) + 2c(1) = 2 ≠ 0 = 2c(4)`), so **whether replicability
>    implies the `Prop` is not settled** by it, and no claim either way is made here.
> 2. **The real obstruction is the object, not a hypothesis on `c`.**  From the primary source
>    (the paper's text is in this workspace as `../mm_text.txt`, section 8 — read it, do not
>    reconstruct it), (8.3) is
>
>    `p⁻¹ · exp(− Σ_{i>0} Σ_{m>0, n∈ℤ} Tr(g^i|V_mn) p^{mi} q^{ni} / i) = Σ_{m∈ℤ} Tr(g|V_m) p^m − Σ_{n∈ℤ} Tr(g|V_n) q^n`,
>
>    i.e. `exp(−L) = p·(T_g(p) − T_g(q))`, and the right-hand side is **two-sided in `q`** — it
>    contains `−p·q⁻¹`, because `T_g = q⁻¹ + Σ_{n≥0} c(g,n)q^n` with `c(g,-1) = 1` (`V_{-1} = 1`
>    acts trivially, `V_0 = 0`).  `MM.EulerSeries`'s `q`-side is `qCoeffOf … bound 1`: **positive
>    `q`-powers only**, plus an extra `m = 0` term (`MM.constantCoeff_one_add_eulerSeries_ne_one`).
>    So `1 + EulerSeries` is *not* `p·(T_g(p) − T_g(q))`, and the earlier derivation's step
>    "`L` is the logarithm of `1 + E`" is not available.
>    **The shape is not refuted**: with the correct two-sided `E`, `−L = logOf (1 + E)` is just the
>    definition of the logarithm (T1b, `MM.expOp_logOf_eq`).  What is missing is the **two-sided
>    `q`-expansion object** — the same defect task **D0** already records and
>    `Definitions/MMQExpansionGap.lean` proves the limits of.  **That is T2's first requirement.**
> 3. **What T2 therefore is, restated.**  (i) Build the two-sided `q`-object and state (8.3) with it
>    (`E := p·(T_g(p) − T_g(q)) − 1`) — **(i) IS NOW DONE**: `MM.HasLaurentQExpansion` in
>    `Definitions/MMQExpansionTwoSided.lean` is that object, the series determined by `f` and the
>    level-one instance proved (`MM.levelOneJ_sub_hasLaurentQExpansion`); what remains of (i) is
>    **integrality** (`ℂ`-valued coefficients) and the restatement of (8.3) with it;
>    (ii) then the Möbius inversion proper — the equivalence
>    between `MM.IsReplicable` and the product form (10.1)/(10.4), for which `MM.coeff_adamsLog`
>    now supplies the Adams side in the right shape.  **Do not start from `logOf (1 + EulerSeries)`.**
>
> 4. **AND THE RESTATEMENT IS NOW DONE, WITH THE TARGET RE-SCOPED (task T2-ii, this session).**
>    `Definitions/MMDenominatorIdentity.lean` states (8.3) faithfully as `MM.DenominatorIdentity`,
>    after recording the two forced reformulations: multiply through by `p` (`PowerSeries` has no
>    negative `p`-exponents), and note that the paper's `q`-side is **two-sided and sits at `p¹`
>    alone** — so the right-hand side is `[p⁰] = c(g,-1)`, `[p¹] = c(g,0) − T_g`, `[p^k] = c(g,k−1)`
>    for `k ≥ 2`, *not* `c(g,k−1) − T_g` at every degree.
>    Proved: `MM.DenominatorIdentity.iff_coeff` (the honest per-degree reduction),
>    `MM.DenominatorIdentity.coeff_zero` — **the normalization `c(g,-1) = 1` is *derived* from the
>    identity**, not assumed — and `MM.DenominatorIdentity.coeff_one` (`c(g,0) = 0`, the FLM fact
>    `V_0 = 0`).
>    **Consequences for this entry, taken from the paper's own section 9:** the `p¹` comparison
>    carries no recursion; the `p²`/`p⁴` comparisons *are* the paper's recursion (9.1) and are task
>    **T3**; and **the Möbius inversion (10.4) is not a coefficient of (8.3) at all** — section 10
>    *defines* `mult(m,n)` by (10.4), inverting the recursion.  So what remains of T2 is exactly one
>    thing: **prove `MM.DenominatorIdentity` for the moonshine coefficient family**, i.e. the paper's
>    sections 6--8 (monster Lie algebra, no-ghost theorem, twisted denominator formula).  The
>    "Möbius inversion" is a definition plus a divisor-arithmetic lemma, not a series identity, and
>    the old T2a/T2b split below is superseded where it disagrees with this.
>
> **Also verified and worth not rediscovering:**
> `Finset.sum_Icc_eq_sum_range` does not exist; `ArithmeticFunction.sum_divisors_moebius` does not
> exist; the Möbius-inversion lemma that *does* exist is
> `ArithmeticFunction.sum_eq_iff_sum_mul_moebius_eq` (`Moebius.lean:238`), of the form
> `(∀ n > 0, Σ_{i|n} f i = g n) ↔ ∀ n > 0, Σ_{x ∈ n.divisorsAntidiagonal} μ x.fst * g x.snd = f n`.
> T2a does **not** depend on T1b (no `exp` appears on either side).

The paper's section 10 passes from the denominator formula

  `p⁻¹ ∏_{m>0, n∈ℤ} (1 − pᵐqⁿ)^{mult(m,n)} = T_g(p) − T_g(q)`   (10.1)

to the root multiplicities via Möbius inversion.  The *direction* determines what there is to prove:

* `mult` is **defined** by (10.4), `mult(m,n) = Σ_{d·s | (m,n)} μ(s)/(ds) · c(g^d, mn/(d²s²))`.  So
  (10.1)'s product is *not* something to prove — it is the definition of that product.
* What is to be proved is the **recursion** obtained by comparing (10.1)--(10.3) with the definition:
  for every `k > 0` and all `m, n` with `mn ≠ 0`,

    `Σ_{i | k} i · c(g^i, mn·(k/i)²) = k · c(g, mn·k²)`,

  which is exactly `MM.IsReplicable` as stated in `Definitions/MMMoonshine.lean`.  (The originally
  recorded four-step spine — step 3 was `MM.AdamsLogIsLog` — is superseded by the SETTLED box above,
  where `MM.AdamsLogIsLog` is refuted as a general identity; `MM.seriesIdentity_of_adamsLogIsLog` is
  the surviving shape.)  **Dependencies:** T1b (`ExpLogOf`) for the exponent comparison; T1's
  `EulerSeries`/`adamsLog` for the setup.

* Acceptance: build exits 0; no `sorry`/`axiom`; axioms the three standard ones; and the recursion
  stated for the true divisor sum (a statement that is true only up to a bound, or only for `k = 1`,
  must be labelled as such rather than presented as the theorem).

> **T3-RECON (2026-09-13): the determination statement was priced, and candidate (A) is FALSE.**
> A reconnaissance task (read-only; report `Probe/T3_DETERMINATION_RECON.md`) asked whether the
> paper's sentence — *"the coefficients for n = 1, 2, 3 and 5 determine all the coefficients"* — can be
> formalized **without** the four formulas (9.1), since only formulas 1 and 3 are theorems here.
>
> **Candidate (A) — determination from `MM.IsReplicable` alone plus agreement on the first few
> coefficients — is refuted, and not vacuously.**  The replicability relation for level `k` and index
> `p` exists only when `k² ∣ p`, so it never constrains a **squarefree** level.  Explicit
> counterexample: the perturbation `δ = 1` at `(g², 7)`, `2` at `(g, 28)`, `0` elsewhere satisfies every
> relation (the only one meeting its support is `(k,p) = (2,28)`: `2·1 − 2 = 0`) and vanishes on all
> inputs `n ∈ {1,2,3,5}` for every power.  Checked to `p = 200`; the pinned perturbation space has exact
> kernel dimension 3 at `B = 40` and 8 at `B = 60`.  So `IsReplicable` plus five coefficients does **not**
> determine the family, and the paper's claim is not a consequence of replicability alone.
>
> **What the claim actually needs, measured by rule-subset closure.**  Descent is by index: the formula
> for `n` names only smaller indices **except** at `n ∈ {1,2,3,5}`, where the recursion degenerates
> (F2 at `k = 1` gives `c(5) = c(5)` — the paper says so explicitly).  Exhaustive checks to `n = 4000`
> show: `F1 + F3` alone reaches only 9 of the first 400 indices; `F1+F3+F2` reaches 72;
> **`F1+F3+F2+F4` reaches all of them.**  So determination needs **all four** formulas — and the pair
> `{RecursionFormulaTwo, RecursionFormulaFour}` is the single decisive missing input, exactly where this
> stream stalled before (they are unproved `Prop`s in `MMReplicationFormulaTargets.lean` because the
> route that was supposed to produce them was refuted by T3e).
>
> **Two further findings worth keeping.**  (i) The published second formula fails against exact `j` at
> every `k` unless the sign correction already recorded in `MMReplicationFormulasOdd.lean` is applied;
> with it, all four formulas check at `k = 1..5`.  (ii) Norton's 12-coefficient theorem is *not* the
> route the paper's section 9 uses, and is not formalizable from the coefficient relations alone: it
> needs a strictly stronger notion than `IsReplicable`.  **Do not dispatch a determination task whose
> statement does not name `{F2, F4}` as an input** — it would be a slightly more elaborate version of
> the two refutations this stream already has on record.
>
> Verified API facts from the probes (`Probe/T3ReconProbe.lean`, `…Shine.lean`, both `--- OK ---`):
> `MMReplicationFormulaTargets` does **not** import `MMMoonshine`, so there is no import edge between
> the (9.1) machinery and `IsReplicable`; `IsReplicable` appears in no other `Definitions/` file; and
> `Nat.divisors_pos_of_pos` does not exist in this pin.

### [~] T3 — the recursion (9.1) from (8.3) — **first step landed (this session)**
* Deliverable: extraction of the paper's recursion (9.1) for `c_g(4k), c_g(4k+1),
  c_g(4k+2), c_g(4k+3)` from `MM.IsReplicable`, i.e. a theorem
  `MM.IsReplicable.recursion`.
* Acceptance: builds, no `sorry`.
* Risk: medium.  Purely combinatorial once T1 exists.
* **PROGRESS (this session).**
* **T3d + T3e (this session): the `p³` comparison landed, and then the ROUTE TO FORMULAS 2 AND 4 WAS
  REFUTED — the stream is stopped here on purpose.**  `Definitions/MMReplicationPThree.lean` (175 lines)
  lands `MM.DenominatorIdentity.pThree` / `…pThree_apply` — the first comparison in which
  `c(g,4k+1)` and `c(g,4k+3)` occur at all (it also settled the paper's `p⁻¹` shift: the paper's
  "compare `p²` and `p⁴`" is this repository's `p²`, `p³`, `p⁴`).  `Definitions/MMReplicationFormulaTargets.lean`
  (124 lines) records formulas 2 and 4 as **`Prop`-valued targets** — not theorems — because T3e
  established, by exact polynomial computation in the symbols `c(g^i,n)`, that they lie in **no linear
  combination** of (8.3)'s coefficient relations (residual 7--8 terms for `p`-degree `≤ 6`,
  `q ∈ [−8,26]`), nor of the reciprocal presentation `exp(L)·p(T(p)−T(q)) = 1`, nor after adjoining
  products of relations.  **The dispatcher independently reproduced the span test** (validated by the
  self-check that formulas 1 and 3 *are* single relations) **and tested the two natural repairs, both
  of which failed**: adjoining (8.3) for `g, g², g³, g⁴` (60 → 240 relations) leaves the residuals stuck
  at 19 and 9 terms, and the **replicability** relations (the divisor recursion, `k ≤ 6`, `|P| ≤ 12`) do
  not span them either.  The formulas are nevertheless **true** (checked at `k = 1…5` against `j`
  recomputed from `E₄ = 1 + 240Σσ₃(n)qⁿ` and `Δ = q∏(1−qⁿ)²⁴`).  **Conclusion: the paper's "elementary
  algebra" sentence is not reproduced by any route tried; the extra input that would yield formulas 2
  and 4 is unidentified, and no further elimination round should be scheduled until it is found.**
  Two docstrings on `main` that asserted the refuted route (`MMReplicationPThree.lean`'s title/§1/§3 and
  `MMDenominatorIdentity.lean`'s §4 bullet) were corrected; the file headers and the README carry the
  evidence.
* **Formulas 1 and 3 ARE landed (task T3b), and they are conditional on `MM.DenominatorIdentity`.**
  `Definitions/MMReplicationRecursion.lean` (145 lines) derives the **`p²` comparison** of (8.3) from
  `MM.DenominatorIdentity`: `MM.coeff_expOp_two` (the general `p²` coefficient of the exponential) and
  `MM.DenominatorIdentity.pTwo` / `.pTwo_apply`.  `Definitions/MMReplicationFormulas.lean` (498 lines)
  contains `MM.DenominatorIdentity.cg_four_mul` and `…cg_four_mul_add_two` **verbatim at the paper's
  ranges and its `k ≥ 1`**, with every implicit hypothesis explicit — the FLM grading `c(g,n) = 0` for
  `n < −1` (not derivable from `FiniteSupportCoeff`; it confines the convolution to finite ranges),
  `c(g,0) = 0`, and the truncation bound — while `c(g,-1) = 1` is *derived* from (8.3).  Both readings
  are verified numerically against the true `j`-coefficients (first formula at `k = 1, 2`, third at
  `k = 1`).  The extraction chain (convolution normal form, the two collapses, the pairing lemmas via
  `j ↦ 2k−j`, the evaluated square coefficients, `[p²]L = E₂ + ½ψ²(E₁)`) is reusable.
* **T3c: the `p⁴` comparison landed, and TWO FINDINGS that changed the next step.**
  `Definitions/MMReplicationFormulasOdd.lean` (303 lines) has `MM.coeff_expOp_four` and
  `MM.DenominatorIdentity.pFour` (+ its coefficientwise form), all conditional on `MM.DenominatorIdentity`.
  **Finding 1 — the paper's second formula is WRONG AS EXTRACTED.**  The paper says the recursion
  degenerates at `n = 5`; the extracted sign gives `c_g(5) + c_g(2)²` there instead of `c_g(5)`.  With
  `(cg2(2k) − cg(2k)²)/2` in place of the first square term it degenerates exactly and holds at
  `k = 2, 3`.  Both the file's author and the **dispatcher, independently**, checked this numerically
  (extracted: `462314921578200` against `c(5) = 333202640600`; corrected: exactly `c(5)`, then
  `c(9) = 3176440229784420`).  The correction is **recorded and not applied**: no theorem states
  formulas 2 or 4, precisely so that a false statement cannot enter.
  **Finding 2 — the route to formulas 2 and 4 is NOT the coefficient comparison.**  `c(g,4k+1)` can only
  enter `pFour` through an `L₁` factor, whose surviving contributions carry `c(g,0) = 0` or
  `c(g,-1) = 1` — yet formula 2 contains the ALTERNATING sum `Σ_{1≤j≤2k}(−1)^j cg(j)cg(4k−j)`.  No
  coefficient comparison of `exp(−L) = p(T(p) − T(q))` produces alternating signs; they come from a
  reciprocal/product (`(1+X)^{-1}`-type) expansion, or from combining the `p²` and `p⁴` comparisons to
  eliminate a term — **which one is not established**.  The `p²` comparison at `q^{2k+1}` is *minus*
  formula 3 (no new information at odd degrees), `c(g,4k+1)`/`c(g,4k+3)` do **not** occur in the `p²`
  comparison at `q^{4k+1}`/`q^{4k+3}` at all, and no single comparison *is* the formula: the `p³`
  comparison at `q⁹` has 26 monomials against the formula's 11.  The route actually taken is the (8.3)
  comparison, not `MM.IsReplicable` as the deliverable line above says; the relationship between the two
  is *not* assumed and is recorded as open in the file header.

### [ ] T4 — generalized Kac--Moody algebras (the long game)
* Deliverable: not attempted here.  Recorded for completeness: the paper's sections 4--8 need
  the definition of a generalized Kac--Moody algebra, its denominator formula, Lie algebra
  homology `H(E)` and its identification with the sum over the Weyl group, and the no-ghost
  theorem.  None of this exists in Lean.  This is the single largest gap in the whole
  project and should be scoped as a multi-month effort.

---

## THE LONG CAMPAIGN — discharging the four assumed inputs outright

The four assumed inputs are listed in `README.md`; this section is the plan for removing them, as
opposed to the task-by-task list below.  It exists because the goal of the project is Theorem 1.1
**unconditional**, and the honest scoping of that differs enormously between the four.

### Measured state of the foundations (COMPILED inventory, this revision)

| what is needed | what exists | verdict |
| --- | --- | --- |
| vertex algebras (for FLM) | Mathlib `Algebra/Vertex/`: `VertexOperator.lean` (98 lines) + `HVertexOperator.lean` (161 lines) = **259 lines**, with `Locality`, `HasseDerivative` and `Residue products` still in their `## TODO` | **not a foundation**; vertex algebras, modules, and the state--field correspondence would all be from scratch |
| the Leech lattice Λ (for `V_Λ`) | nothing in Mathlib, nothing in MM | from scratch; an even unimodular rank-24 lattice with no roots |
| Γ₀(N) | `MM` has **no definition at all** — `Γ₀(11)` appears only in documentation; Mathlib's `CongruenceSubgroup.Gamma N` is the *principal* congruence subgroup `Γ(N)`, not `Γ₀(N)` | must be built, or imported from FLT |
| genus of `X₀(N)` | FLT proves `genusFormula` **unconditionally in characteristic 0**; its `Definitions` layer is importable in ~5 s | **the one piece that is genuinely available** |
| `Γ₀(N)⁺` (the normalizer, which the table actually needs) | nothing in Mathlib or FLT | from scratch |
| the monster group | `MM.Monster`, by the Norton--Ivanov presentation, as a *definition* (`Definitions/MMMonster.lean`) | defined; finiteness and order are task S3 |
| the monster's character table | nothing anywhere | from scratch, and needed for the section 9 case check |
| no-ghost theorem | nothing | the single hardest item |

### M1's COST WAS MIS-STATED: the arithmetic half is 140 lines and needs no FLT (measured)

> **The claim that `decide`/`norm_num` cannot recompute the genus-zero list, and that the 2297-line
> FLT file is therefore necessary, is REFUTED for the arithmetic half.**
>
> Measured: `Probe/ProbeArithFull.lean` — **Mathlib only, 0 FLT imports, 140 lines, compiles**,
> `#print axioms` exactly the three standard axioms, containing
> `genusZero_level (N) (hN : N ∈ genusZeroLevels) : genusFormula N = 0` for the 15 Conway--Norton
> levels and `genusFormula_eleven : genusFormula 11 = 1`.  The `genusFormula` there is `rfl`-equal to
> FLT's, so nothing is lost by not importing it.
>
> **The two real blockers, each removed by one rewrite** (measured on `N = 2` and `N = 11`):
> * `Nat.card` does not kernel-reduce, so bare `decide` fails on `nuTwo`/`nuThree`; the fix is
>   `rw [Nat.card_eq_fintype_card]`, which needs `[NeZero N]` and so is applied at a numeral.
> * **`Squarefree` does not kernel-reduce** — `Nat.instDecidablePredSquarefree` goes through
>   `Nat.minSqFac`, a well-founded recursion; `decide` cannot prove even `Squarefree 2`, and the
>   `norm_num` squarefree prover is **commented out in this Mathlib pin**
>   (`Mathlib/Data/Nat/Squarefree.lean`, "Porting note: comment out NormNum tactic").  A 25-line
>   bridge (`squarefree_iff_of_le_twentyfive`, via `Nat.squarefree_iff_prime_squarefree` +
>   `interval_cases`) replaces it with divisor arithmetic for `n ≤ 25`, which is all the levels need.
> Everything else (`Nat.divisors`, `Nat.totient`, `Nat.gcd`, `Nat.div`, `Fintype.card` over `ZMod`
> at literals) reduces fine.  The final `ℚ` equality is easier as the integer relation
> `12 + ψ = 3ν₂ + 4ν₃ + 6·cusps`.
>
> **What the 1115 figure actually belongs to.**  It is real, and it was reproduced exactly — but it
> is the *geometry*: `Thm_ModularCurve_genus_modularFunctionFieldBar_eq_genusFormula` (510 Theorems +
> 511 P2M + 94 Definitions).  And that theorem is **conditional** on
> `HasCanonicalDivisor (AlgebraicClosure ℚ)`; FLT supplies that instance only for `K := ℂ`.  The
> cheapest **unconditional** genus identity is the **1656**-module
> `genusFF_modularFunctionFieldFullC_eq_genusFormula_algebraicClosure` (≈16 h floor, and with 4.2 GB
> peak RSS per `lean` process it is effectively serial).  The **arithmetic** closure is **6
> modules**, measured at **165.7 s**.  So: a number costs minutes, the *identification* costs
> overnight-plus.
>
> **`Def_CohCarrier_Level` (broken in FLT) is in none of the closures we need** — 0 hits in the 6-,
> 1115-, 1297- and 1656-module closures.  It blocks `Def_ModularCurve_XH`, which is not needed.
>
> **`Γ₀(N)` and the bridge.**  MM mentions `Gamma0`, `CongruenceSubgroup` and Atkin--Lehner
> **nowhere** in its own sources; the missing one-liner is
> `Gamma0GL N := Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma0 N)`
> (compiles).  `Γ₀(N)⁺` has nothing at all — no Atkin--Lehner, no Fricke, no normalizer in Mathlib,
> and FLT has only the *operator* `AtkinLehnerDatum`/`alSlash` on forms.
>
> **The honest limit of the arithmetic file.**  `genusFormula N = 0` is arithmetic about a
> definition.  It establishes **nothing** about `Γ₀(N)`, `X₀(N)`, `ℍ/Γ` or Hauptmoduls; the
> identification "this formula = the genus of `X₀(N)`" is the whole geometric content and is
> untouched.  The next honest step is the **η-quotient** route (Mathlib has
> `NumberTheory/ModularForms/DedekindEta.lean` with `eta`, `eta_ne_zero`, `logDeriv_eta_eq_E2` —
> but **no** S-transformation law `η(-1/z) = √(-iz) η(z)` and no multiplier system), and even that
> yields only "here is the explicit `f` with the right `q`-expansion and modularity", **not**
> `IsHauptmodul`: orbit separation is the degree-1/argument-principle condition on `X(Γ)` and stays
> open (the `f = j²` counterexample in `README.md` is why).
>
> **Restated in one line, since this box and the `M1` entry below both carry it:** the *genus number*
> is available from FLT (arithmetic closure 6 modules / 165.7 s; geometry conditional, 1656 modules
> unconditional), and what is missing is the **bridge** from FLT's algebraic function field to MM's
> analytic `ℍ/Γ`.

### A THIRD EXTERNAL DEVELOPMENT — AND IT IS THE VERTEX-ALGEBRA FOUNDATION ITSELF

> **`dbrueg/lean-geometric-vertex-algebras` (GeomVA).**  Downloaded, inspected and **fully compiled
> by the dispatcher**: **18/18 modules, 0 errors, ~4 minutes total**, against **our exact pin** —
> Lean `v4.33.1` / Mathlib `v4.33.1`.  **No port is needed.**  **16,077 lines** in 18 files,
> formalizing Daniel Bruegmann, *Geometric Vertex Algebras*, arXiv:2012.09717 (Graduate J. Math. 10
> (2025) 1--20), with the paper's LaTeX source in the repository.  By module:
> * `Formal/Dist.lean` (476 lines) — **the formal-calculus layer that was missing**: `FormalDist M`
>   = `M[[x^{±1}]]` with mode indexing, `FormalDist₂`, `mulX`, `deriv`, `IsCreation`, `idDist`,
>   `mulXSubY`, `mulXSubYPow` (closed binomial formula), `commutator`, `prodApply`, `NoNegY`,
>   `setYZero` — the bookkeeping of the vertex axioms (Def 3.1 of the paper);
> * `Analytic/` (5 files, ~3,900 lines) — holomorphic functions on domains in `ℂⁿ` (Def 1.1), normal
>   convergence and sums in a vector space *without* topology (Def 1.4), circle-integral lemmas
>   **missing from Mathlib** including analyticity in a parameter, Laurent expansions on annuli
>   (Def 2.8), `ℂⁿ ∖ Δ`, the domains `D_m`, `U_ij`, `U_{r,R}`;
> * `Graded/Basic.lean` — `ℤ`-graded spaces, the `ℂ^×`-action, homogeneous maps (Def 2.5);
> * `VA/Defs.lean`, `GVA/Defs.lean`, `GVA/Modes.lean` — **`GeomVA.VertexAlgebra`** and
>   **`GeomVA.GeometricVertexAlgebra`**;
> * `GVAtoVA.lean` (2,229 lines) and `VAtoGVA.lean` (4,265 lines) — **both directions of the
>   equivalence**, proved; `Equivalence.lean`, `Category.lean` — the main theorem.
>
> **Verified main results** (the dispatcher re-checked every `#print axioms`):
> `GeomVA.VertexAlgebra.Phi_Psi`, `GeomVA.GeometricVertexAlgebra.Psi_Phi`,
> `GeomVA.GradedHom.isGVAHom_iff_isVAHom`, and
> **`GeomVA.PhiCatIso : Cat.of GVACat ≅ Cat.of VACat`** — an isomorphism of categories between
> geometric vertex algebras and `ℤ`-graded vertex algebras.  All four print exactly
> `[propext, Classical.choice, Quot.sound]`.  The `sorry` tokens in the tree are **six docstring
> occurrences of the phrase "no `sorry`"**; there are none live.
>
> **What this changes.**  The `vertexAlg` axiom layer (vendored earlier) and Mathlib's 259 lines are
> no longer the state of the art here: **this is a complete, compiled, paper-backed formalization of
> vertex algebras** — and, through the geometric side, the contour-integral construction route rather
> than the abstract Borcherds-identity route.  **What it still does NOT contain** (grepped): nothing
> about lattices, the Leech lattice, the monster, moonshine, generalized Kac--Moody algebras, the
> no-ghost theorem, or lattice vertex operators `e^λ`.  So the *concrete* objects remain to be built;
> what is available is a **working, complete vertex-algebra theory to build them in**, on our pin.

### EXTERNAL FOUNDATION, FOUND — TWO developments, both measured, neither ported

> **`ScottCarnahan/vertexAlg`** — downloaded and measured directly (not from its README):
> **35 files, 10,772 lines, 0 active `sorry`/`admit`/`axiom`** after comment-stripping.
> `VertexBasic/Defs.lean` defines `stateField`, `order`, `associativity`, `commutatorFormula`,
> `IsLocal`, `T`, `skewSymmetry`, `translationCovariance` and **`class VertexAlgebra`**;
> `VertexBasic/Borcherds.lean` defines the Borcherds sums and **`class VertexAlgebra1`** axiomatized
> by the Borcherds identity, and **proves** `borcherdsId_at_zero_iff_associativity`,
> `borcherdsId_at_zero_iff_commutatorFormula`, `locality_left_eq_borcherdsSum2`,
> `locality_right_eq_borcherdsSum3` and the `Borcherds_sums_2_3_eq_if_locality` pair, plus a
> hom/subalgebra/equivalence API and a Lie layer (`Lie/Loop.lean`, `Cocycle.lean`,
> `CentralExtension.lean`, `ChevalleyEilenberg.lean`, `PBW.lean`).  **But not one concrete vertex
> algebra is instantiated**: `VertexBasic/Lattice.lean` is a 34-line stub with no definitions,
> `VertexBasic/Affine.lean` has its `positiveEnergy`/`smooth` classes commented out, and its own TODO
> names Golay-24, Mathieu₂₄, the Leech lattice, lattice VOAs, the `-1`-twisted module, the `-1`
> orbifold, generalized Kac--Moody algebras, the **no-ghost theorem** and Hauptmoduls.
>
> **So the foundation question is now sharp:** the *axiom layer* exists (twice over, with
> `VirasoroProject` covering the Virasoro/Heisenberg/Fock/Sugawara side at `c = 1`), and **every
> concrete object is missing**.  **Two measured corrections that change the phasing.**
>
> 1. **The no-ghost theorem does NOT need a rank-24 lattice.**  Theorem 5.1's hypotheses are a
>    nonsingular form, a Virasoro action with `L_i† = L_{-i}` and central element `24`, `L_0`
>    diagonalizable over `ℕ` with finite-dimensional eigenspaces, and a group `G` preserving the
>    structure.  Only `II^{1,1}` (rank **2**) appears.  The paper says so itself after Theorem 6.1:
>    the construction works for any vertex algebra with a conformal vector, "but it is only when this
>    vector has dimension 24 that we can apply the no-ghost theorem".  So `E8³` or `D24⁺` suffice.
> 2. **The Leech lattice is forced by the moonshine module, by arithmetic.**  For `V_Λ` with `Λ` even
>    unimodular of rank 24, the `L_0 = 1` space has dimension `24 + #{λ : λ² = 2}`, while
>    `j - 744 = q⁻¹ + 0 + 196884q + ⋯` has vanishing `c(0)`; so `c(0) = 0` forces the lattice to have
>    **no roots**, and the Leech lattice is the unique such lattice.  (Computed: Leech `0` roots,
>    `E8³` `24 + 720 = 744`, `D24⁺` `24 + 1104 = 1128`.)  `V_Λ` itself still has a 24-dimensional
>    weight-1 space — **the orbifold is what removes it**, so "`V_Λ` already has the right character"
>    is false.
>
> **What the paper actually consumes, and a load-bearing simplification.**  The paper's conditions
> (1) vertex algebra over `ℝ` with a conformal vector of dimension 24 and a positive definite form,
> and (2) `V = ⊕ V_i` with `V_i` the `L_0 = i+1` eigenspace and `∑ dim V_i q^i = j - 744`, **alone
> imply that for any automorphism `g` preserving the structure, `∑ Tr(g|V_i) q^i` is completely
> replicable, i.e. (8.3) holds.**  The monster is needed only for condition (3) (the action) and for
> section 9.  So the replication identity — one of the four assumed inputs — follows from (1)+(2).
>
> **Indexing trap, frozen before any statement is written:** the paper's `V_i` is the `L_0 = i+1`
> eigenspace, but Theorem 5.1's `V^i` is the `L_0 = i` eigenspace, and `V^i = V_{i-1}`; `dim V_0 = 0`
> gives `V^1 = 0`, hence `dim M_{0,0} = 2 = ℝ²` (the Cartan), consistently.
>
> **Measured negatives, so nobody re-searches them.**  No formalization of moonshine, `V^♮`, the
> Griess algebra, a generalized Kac--Moody/Borcherds algebra, a lattice VOA, or the no-ghost theorem
> exists in **any** proof assistant (Isabelle/AFP entry URLs scanned, Coq/Rocq, Agda, Metamath,
> Mizar, HOL Light).  The only machine-checked Monster artifact anywhere is a 44-line Lean 3
> *definition* in the frozen 2019 `formalabstracts` repo — which is what `MM.Monster` already is, so
> **stream S is at the state of the art and S3 (finiteness and order) has no precedent anywhere.**
> `JustinMcClung/formal-distribution` (formal calculus, ~3850 lines, reported `sorry`-free) is now
> **404** — do not plan around it.
>
> **Revised dependency note.**  The construction graph is **not a chain**: the no-ghost sub-theorems
> need neither the Leech lattice nor the monster action, and the rank-2 Lorentzian Virasoro module
> can be built directly without constructing a vertex algebra at all.  The pivot object for
> everything downstream is **`V_{II^{1,1}}` — the first concrete vertex algebra** — because it is
> what the no-ghost *statement* names and what the tower is built from.
### EXTERNAL FOUNDATION, FOUND — and why it changes Phases 3/4 (measured, port UNVERIFIED)

> **An external Lean 4 development already contains the Virasoro / Heisenberg / Fock / Sugawara
> layer that this repository has nothing of.**
>
> * Kalle Kytölä, `VirasoroProject` — <https://github.com/kkytola/VirasoroProject>, docs
>   <https://kkytola.github.io/VirasoroProject/>, paper arXiv:2510.21741, *Virasoro algebra and
>   Sugawara constructions formally in Lean* (Oct 2025).
> * ~3058 lines over ~11 core files; reported `sorry`/`admit`/`axiom`-free (the reconnaissance
>   grepped the downloaded sources rather than trusting the README).
> * Contents: the Witt algebra and its 2-cocycle; the Virasoro algebra as the corresponding central
>   extension; `H²(Witt)` one-dimensional; the Heisenberg algebra; a Fock space and
>   `ChargedFockSpace`; the bosonic **Sugawara construction** (`VirasoroProject.sugawaraRepresentation`,
>   a Virasoro representation of central charge `1` from any locally-truncated Heisenberg
>   representation); Verma modules with a triangular decomposition; and a
>   Lie-algebra-representation-from-basis layer.
> * It does **not** contain lattice vertex algebras, vertex operators `e^λ`, the rank-2 Lorentzian
>   `II^{1,1}` VOA, the no-ghost theorem, or anything moonshine — verified by the reconnaissance,
>   not assumed.
>
> **THE PORT IS UNVERIFIED AND MUST NOT BE ASSUMED.** `VirasoroProject` pins
> `leanprover/lean4:v4.27.0-rc1`; this repository pins **Lean 4.33.1 / Mathlib `db584cd6`**. Nobody
> has compiled it against our pin. The few Mathlib names it is known to use are present in our pin
> (`LieModule.Cohomology.twoCochain`/`twoCocycle`, `LieAlgebra.loopAlgebra`,
> `UniversalEnvelopingAlgebra`, `TensorProduct.LieModule.lieRingModule`/`lieModule`), but that is a
> handful of `#check`s, **not** a compile. A dedicated port-feasibility task is measuring the real
> drift (file-by-file, error-by-error, classified as rename vs signature change vs elaboration
> change) before anything in this repository depends on it. **Do not cite this box as evidence that
> the layer is available.**
>
> **What it changes if the port is cheap.**  Phase 3 becomes "state the no-ghost theorem, having
> ported the Virasoro/Heisenberg/Fock/Sugawara layer" rather than "build that layer and then state
> it".  Phase 4's bottleneck moves *up* the stack: from "there is no vertex algebra foundation at
> all" to "there is no **lattice** VOA, no vertex operators, and no tensor product of Virasoro
> modules" — the last matters immediately because the paper's §5 no-ghost argument runs on
> `V ⊗ V_{II^{1,1}}`.  **Correction to the phasing paragraph below:** Phase 3's no-ghost *proof* is
> independent (lemmas 5.1--5.5 are abstract linear algebra), but its *statement* is not, because it
> names `V_{II^{1,1}}` and a tensor product that exist nowhere.

### THREE CORRECTIONS THAT SHARPEN THE PLAN (one removes a library from the critical path)

> **1. `Λ(E) = H(E)` is NOT a consequence of the no-ghost theorem, and Lie-algebra homology is NOT
> on the critical path to (8.3).**  The paper's §2 (`mm_text.txt:900-905`) derives it from the
> standard Chevalley--Eilenberg sequence `… → Λ²(E) → Λ¹(E) → Λ⁰(E) → 0`: it is the
> Euler-characteristic identity — the alternating sum of a complex equals the alternating sum of its
> homology.  It holds for every generalized Kac--Moody algebra, independently of no-ghost, and is
> reused as (8.1) in §8 and again in §13.  An earlier reconnaissance wrongly made no-ghost necessary
> for it.  **The task is split:** `T3a` is `Λ(E) = H(E)` (free Euler characteristic; Mathlib already
> has `⋀[R]^n M`), `T3b` is the replication identity (8.3) via §7's simple roots and the explicit
> `H_i(E)`.
>
> **What no-ghost actually supplies** is: (i) `M := (P¹/DP⁰)/radical` is a well-defined
> `II^{1,1}`-graded Lie algebra; (ii) `M_{(m,n)} ≅ V_{mn}` — the root multiplicities; (iii) positive
> definiteness in every non-zero degree, which is what makes `M` a GKM algebra.  So plan on deriving
> **"`M` is a GKM algebra with root multiplicities `V_{mn}`"** from no-ghost, not `Λ(E) = H(E)`.
>
> **2. The corrected chain, with its four independent gaps.**
> no-ghost ⇒ (`M` is GKM with root multiplicities `V_{mn}`) ⇒ plus §7's determination of the
> **simple** roots (from the product formula (7.1) for `j`, i.e. from modularity and Hecke operators —
> *not* from no-ghost; no-ghost gives root *multiplicities*, and (7.1) then determines the *simple*
> roots) ⇒ plus §4's free homological algebra ⇒ (8.2) ⇒ Adams operations and traces ⇒ (8.3) ⇒ §9 and
> Koike ⇒ Theorem 1.1.  The gap between no-ghost and (8.3) is therefore four independent items: the
> VOA/Lie-algebra construction; the GKM axioms; the simple roots (§7); and virtual-module-to-trace
> identities (Adams operations `ψⁱ`, the splitting principle, pointed-cone finiteness).
>
> **3. §5 of the paper is explicitly a sketch.**  `mm_text.txt:949-951`: "For convenience we give a
> quick sketch of their proof", with the full proofs referred to Goddard--Thorn and to I. Frenkel
> (1985).  A formal proof must fill in the zigzag `H ⊃ P ⊃ S, N, T, K` via Lemmas 5.1--5.5; it cannot
> transcribe §5.
>
> ### The smallest case is pinned, and the target for Phase 3 is now sharp
>
> Hypothesis (3) pins `c = 24` exactly, and the only freedom is to replace `II^{1,1}` by an even
> unimodular Lorentzian lattice of rank `26 - c`, which exists only when `26 - c ≡ 2 (mod 8)`, i.e.
> **`c ∈ {24, 16, 8, 0}`**.  There is **no `c = 1` case and no vacuous instance**, so the search space
> for a "smallest case" is genuinely tight.
>
> **Target: `V` = the rank-24 Heisenberg VOA (24 free bosons) tensored with `V_{II^{1,1}}`, with
> conclusion `dim (P¹_r / null) = p₂₄(1 - r²/2)`.**  This is the classical Goddard--Thorn theorem in
> its cleanest form, it is finitely decidable, and the partition numbers `p₂₄` appear verbatim in both
> the monster and the fake-monster formulas.  The literature agrees on the order: (1) rank-24
> Heisenberg × `II_{1,1}`; (2) the Leech case `V_Λ` = the fake monster — the first case giving a real
> `Λ(E) = H(E)` with an explicit denominator formula, avoiding FLM's construction of `V^♮`; (3)
> `V^♮` and the monster.
>
> ### Bibliography corrections — three names that must not be cited
>
> * The no-ghost paper is **P. Goddard, C. B. Thorn, *Phys. Lett. B* **40** (1972) 235--238**,
>   "Compatibility of the dual Pomeron with unitarity and the absence of ghosts in the dual resonance
>   model", doi:10.1016/0370-2693(72)90420-0.
> * There is **no** Goddard--Thorn paper titled "Unitary representations of the Virasoro algebra and
>   a no-ghost theorem" (INSPIRE: 40 no-ghost titles, none this one; Goddard--Thorn have exactly
>   three joint records).
> * **"Frenkel--Goddard--Olive" appears not to exist** — INSPIRE has 0 records for the three authors,
>   zbMATH 0 for Frenkel&Goddard and 0 for Frenkel&Olive.  It looks like a conflation of
>   Frenkel--Lepowsky--Meurman with Goddard--Olive, *Algebras, lattices and strings*, MSRI Publ. 3
>   (1985).  The genuine `c = 24` generalization is **I. B. Frenkel, *Lect. Appl. Math.* **21**, AMS
>   (1985) 325--353**.
> * Kac's *Vertex Algebras for Beginners* and the FLM book **do not contain** the no-ghost theorem
>   (checked against tables of contents).
> * Rigour caveat to carry: Borcherds states that Goddard--Thorn's proof *is* rigorous;
>   S. Parrott, *Results in Math.* **21** (1992) 379--395 argues the contrary.  The disagreement is
>   unresolved in the literature, so a formalization is not merely a transcription in either case.
>
> ### Indexing: fix it in ONE place before any statement is frozen
>
> Two independent opportunities to get the indexing wrong, both now measured:
> * the paper's `V_i` is the `L_0 = i+1` eigenspace while Theorem 5.1's `V^i` is the `L_0 = i`
>   eigenspace, with `V^i = V_{i-1}`;
> * the distributed `monster.tex` §6 reads "degree `1 - (m,n)²/2 = 1 - mn`", but with the stated Gram
>   matrix `((0,-1),(-1,0))` one has `(m,n)² = -2mn`, so the consistent reading is `1 + mn`, matching
>   Theorem 6.1(3) `M_{(m,n)} ≅ V_{mn}` and §12's norm `λ² - 2mn`.  **The TeX appears to carry a sign
>   slip; take Theorem 6.1(3) as authoritative.**
>
> **RESOLVED IN CODE, and the resolution reverses this entry's sign.**  `Definitions/MMLatticeDoubleCover.lean`
> **freezes `II^{1,1}`'s Gram matrix as `((0,1),(1,0))`** — positive off-diagonal — so that for
> `λ = m·e + n·f` one has `(λ,λ) = 2mn` and `λ²/2 = mn`.  That makes Theorem 6.1(3)'s degree
> `1 - mn` (equivalently `1 - λ²/2`) the *consistent* reading, matching `M_{(m,n)} ≅ V_{mn}`, and the
> `1 + mn` above belongs to the *other* sign convention `((0,-1),(-1,0))`.  The two conventions differ
> by the isometry `n ↦ -n`; **mixing them is a sign error**, so the convention used is recorded in the
> module docstring and every downstream statement must name it.  What is still *not* frozen anywhere is
> the `L_0`-grading convention (`V_i` with `L_0 = i+1` versus `V^i` with `L_0 = i`) — nothing written
> so far is graded, so that trap must be frozen in the file that first states the no-ghost theorem.
>
### LEECH LATTICE: CONSTRUCTION FOUND AND NUMERICALLY VERIFIED — and why two attempts failed

> **The construction.**  `Λ = 2^{-3/2} · A`, where
>
> ```
> A := { a ∈ ℤ²⁴ :  a₁+⋯+a₂₄ ≡ 4a₁ ≡ ⋯ ≡ 4a₂₄  (mod 8)
>                  and for each residue class mod 4, the 24-bit word whose 1s mark the
>                  coordinates i with a_i in that class is a codeword of the binary Golay code }
> ```
>
> with the form `(x,y) = (Σ xᵢyᵢ)/8` on `A`.  This is the Conway--Sloane SPLAG Ch. 4 §4.9
> "even coordinate system" description.
>
> **Why two earlier attempts produced zero norm-4 vectors — the diagnosis is worth keeping.**
> **No construction of the shape "`Λ ⊆ ℤ²⁴` with the standard dot product" can possibly work.**  A
> finite-index sublattice of the unimodular `ℤ²⁴` has determinant equal to the square of its index,
> so determinant `1` forces index `1`, i.e. the whole of `ℤ²⁴`, which has roots.  **The `1/√8`
> scaling is essential**, and `A` genuinely has index `2³⁶` in `ℤ²⁴`: `det(A, (·,·)/8) = 2⁷²/8²⁴ = 1`.
> A future attempt that drops the scaling is wrong before it starts.
>
> **Numerically verified** (script `Probe/leech_verify.py`, run end to end, "ALL CHECKS PASSED"):
> * the Golay code from the cyclic quadratic-residue code of length 23 plus a parity bit: `|C| = 4096`,
>   weights `{0, 8, 12, 16, 24}`, weight enumerator `1 + 759q⁸ + 2576q¹² + 759q¹⁶ + q²⁴`, linear and
>   self-orthogonal, hence self-dual;
> * all 48 explicit generators lie in `A`; the index `[ℤ²⁴ : span(gens)] = 2³⁶` by integer HNF, equal
>   to the independently counted `|A/8ℤ²⁴| = 2³⁵ + 2³⁵`, so the generators span `A`;
> * `(A, (·,·)/8)` is integral, even, of determinant `1`, and positive definite (Sylvester minors);
> * the minimum of `a·a` over non-zero `a ∈ A` is exactly **32**, so `Λ` has **no vectors of norm 2,
>   4 or 6** — minimum norm **4**;
> * a complete enumeration gives exactly **196560** vectors of norm `32`, in the three shapes, with
>   the count factorisations read out of the source:
>   `1104 = 4·C(24,2)` of multiset shape `(4,4)` (support 2);
>   `97152 = 759·2⁷` of shape `(2,2,2,2,2,2,2,2)` (support 8, i.e. `2⁸` on a Golay octad);
>   `98304 = 4096·24` of shape `(3,1,1,…,1)` (support 24);
>   equivalently `196560 = 4·C(24,2) + 759·2⁷ + 4096·24` — matching the source exactly.
>   (An earlier note in this entry wrote the third shape as `(3,1²³)` and did not explain the factor
>   `24`; the correct factorisation of `98304` is `4096·24`, and `1²³` is the component multiset, not
>   the count.)
>
> **Consequence for the plan: this is elementary.**  Integer congruences plus a finite check over a
> 4096-word code.  No SPLAG Ch. 10 machinery, no Niemeier or "holy construction" theory, no uniqueness
> theorem.  Every one of the five bullets above is a **finite computation** on a finite set, so a Lean
> formalization can be entirely concrete: state `A` as a subtype of `Fin 24 → ℤ` with the congruences
> and the Golay condition, and prove the norm facts and the count over that finite set.  (The count of
> norm-32 vectors is the expensive one and should be budgeted the way section 11's `thetaCoeff` was.)
> The crystallographic point that must not be lost: `Λ` lives in `ℝ²⁴`, not in `ℤ²⁴`, and norms are
> `Σ aᵢ²/8` on the integer representatives.
### LEECH: MILESTONES, MEASURED TRAPS, AND A SOURCING WEAKNESS THAT MUST BE STATED

> **Sourcing weakness, stated plainly.**  There is **no copy of SPLAG in this workspace.**  The
> construction above was read from **two independent online expositions** — the HandWiki mirror of the
> Wikipedia article (§"Using the binary Golay code", HTTP 200) and PlanetMath's `leechlattice`
> (HTTP 200) — which agree with each other, and it was then **verified from scratch by computation**
> (independently re-run by the dispatcher: `ALL CHECKS PASSED`).  So the *construction* is not in doubt,
> but its *primary citation* is not in this workspace.  Anyone writing it into a docstring must cite
> SPLAG Ch. 4 §4.9 and note that it was checked against two secondary sources rather than the book.
> The local `_external/borcherds/03_leech.tex:419--490` is the **holy-construction/Niemeier existence
> proof**, which in its own words "says nothing about the Leech lattice apart from the fact that it
> exists" — vastly more expensive in Lean and not the route taken.
>
> **A previous reconnaissance's shape list was wrong in all three entries.**  It had
> `48 + 97152 + 4096 = 101296`; the correct counts are `1104 = 4·C(24,2)`, `97152 = 759·2⁷` and
> `98304 = 4096·24`, summing to `196560`.  `(±4, 0²³)` has norm `16` and is not minimal, the octad
> vectors carry `2⁷` sign choices not `2⁸`, and the third family is `(∓3, ±1²³)` not `(±1²⁴)`.
>
> **`vertexAlg`'s Golay file is scaffolding, not a contribution.**  `VertexAlg/GroupTheory/Golay.lean`
> (256 lines, 203 code) compiles at our pin in 4.5 s with no live `sorry`, but it contains only
> projective-line preliminaries, `Golay24.Q` and a bijection `Fin 24 ≃ ℙ(F₂₃²)` — **no submodule of
> `(ℤ/2)²⁴`, no weight function, no weight enumerator, no double-evenness, no self-duality**; its own
> docstring lists those as TODO.  It removes essentially none of the work.
>
> **Milestones** (D = definition, F = finite kernel computation, T = theorem; difficulty 1–5):
>
> | id | content | kind | diff |
> | --- | --- | --- | --- |
> | ~~M0~~ | ~~Golay code from the systematic generator matrix `[I₁₂ \| B]`~~ — **DONE** | D | 1 |
> | ~~M1a–d~~ | ~~`card = 4096`; doubly even; minimum weight `8`; weight enumerator `759, 2576, 759, 1`~~ — **DONE** | F | 1 |
> | ~~M1e~~ | ~~self-duality via `G·Gᵀ = 0` and `rank 12`~~ — **DONE** | F | 1 |
> | ~~M2~~ | ~~carrier `A` with `Decidable`, `0 ∈ A`, `8eᵢ ∈ A`~~ — **DONE** | D/F | 1 |
> | ~~M3~~ | ~~structure theorem `IsLeechVec a ↔ IsEvenForm a ∨ IsOddForm a`~~ — **DONE, in a corrected form** | T | 3 |
> | ~~M3b~~ | ~~the index `\|A/8ℤ²⁴\| = 2³⁶`, as `MM.leech_index : [ℤ²⁴ : A] = 2³⁶`~~ — **DONE** | T | 3 |
> | ~~M4a,b~~ | ~~integrality `8 ∣ a·b`; evenness `8 ∣ a·a` and exactness of `normSq`~~ — **DONE** | T | 2 |
> | ~~M5~~ | ~~unimodularity `Λ* = Λ` by the determinant-free congruence argument~~ — **DONE** | T | 3 |
> | ~~M6~~ | ~~**minimum `32` / no roots**~~ — **DONE** | T | **4–5 (the crux)** |
> | ~~M7~~ | ~~kissing number `196560` with the three shapes~~ | T | 3 |
> | ~~M8~~ | ~~packaging, and `dim V_Λ(1) = 24 + #{λ : λ² = 2} = 24`~~ | D/T | 2 | — **DONE**
>
> **M2 + M3 + M3b are LANDED**, split into `Definitions/MMLeech.lean` (1018 lines: carrier and
> structure theorem) and `Definitions/MMLeechIndex.lean` (457 lines: the index), 0
> `sorry`/`axiom`/`native_decide`, ~3 s to build because it deliberately contains **no
> `decide +kernel`**, unlike `MMGolay`.  `MM.isLeechVec_iff : IsLeechVec a ↔ IsEvenForm a ∨ IsOddForm a`,
> with `IsEvenForm a := ∃ d t, Golay d ∧ Even (Σt) ∧ a = 2·lift d + 4t` and the odd form with
> `Odd (Σt)` and the `1 +`; plus closure under addition and negation and `8ℤ²⁴ ⊆ A`.  Guarded in
> `FinalCheck.lean`.
>
> **M3's recorded shape was WRONG and the work corrected it.**  The reconnaissance said
> "`a = x₀ + 2(d + 2t)` with `t ∈ D₂₄`", i.e. no parity condition on `t`.  Condition (ii)
> `Σa ≡ 4a₀ (mod 8)` forces **`Σt` even in the even branch and odd in the odd branch**, and the
> report's literal `x₀ + 2(d + 2t)` with `Σt` even has `Σa = 0` while `4a₀ = 4` in `ZMod 8`, so it is
> **never** in `A`.  The coset statement survives; the literal form does not.  (Equivalently the odd
> coset is `(x₀ − 4e₀) + 2C + 4D₂₄` with `Σt` even — recorded in the docstring as prose, not as a
> theorem.)
>
> **M3b, the index, is LANDED**: `MM.leech_index : [ℤ²⁴ : A] = 2³⁶`, with `MM.relIndex_sm8_AHat`
> (`|A / 8ℤ²⁴| = 2³⁶`), `MM.card_quotient_AHat` (the order of `ℤ²⁴/A`) and `MM.card_image_leech` (the
> count itself) as equivalent forms.  A residue class of `A` mod `8ℤ²⁴` is exactly
> `key d τ = Στ + 2·lift d + 4τ` with `d ∈ C` and `τ : Idx → ZMod 2` — the `Στ` term is the parity
> correction the mod-8 congruence forces, by M3 — so `key` injective gives `4096 · 2²⁴ = 2³⁶` classes
> (`MM.key_injective_pair`), and `relIndex_mul_index` applied to `8ℤ²⁴ ≤ A` against
> `index (8ℤ²⁴) = 8²⁴` (`MM.index_sm8`, from `AddSubgroup.index_range_nsmul`) gives
> `2³⁶ · [ℤ²⁴ : A] = 2⁷²`.  `Probe/leech_verify.py` had already computed the same number from the
> definition, independently of Lean.
>
> **The previously recorded obstruction was WRONG, and the correction is worth keeping.**  The record
> said "`key_injective` times out deterministically at `whnf` … because `omega` is asked to split
> `e + 2x + 4u = e' + 2x' + 4u'` over `ZMod 2`-derived integers", and that the only fix was to redo the
> count over `Nat` masks.  In fact the attempt in `Probe/LeechIndex.lean` had **ten errors**, of which
> the `whnf` timeout was one: `eq_of_lift_eq` (lines 110/116) was broken from the start, so
> `key_injective` only *elaborated* on top of an error-recovered `sorryAx` dependency — the evidence file
> `Probe/LpAx1.lean` reproduces it: run `tools/build.sh Probe/LpAx1.lean` and its last
> line is `'MM.Attempt2.key_injective' depends on axioms: [propext, sorryAx, Classical.choice,
> Quot.sound]`.  `MM.key_injective` itself is fine and was never the problem; the timeout
> comes from *applying* a `Function.Injective` statement whose implicit pair-argument is stuck behind
> `Prod.fst`/`Prod.snd` — the unifier then reduces `key`, `keyInt` and the `ZMod 8` casts.  The fix is
> `MM.key_injective_pair`, with the four arguments as explicit binders.  Two smaller traps: the
> `rw [zmod_int_eq_iff_dvd_sub …]` pattern does not match the goal of `key_of_even`/`key_of_odd` (the
> sides come out swapped; use `exact <Iff>.mpr <witness>`), and `key_mem`'s final goals need `key`
> unfolded, not just `keyInt`.  Nothing needed `Nat` masks.
>
> **THE REPORTED OBSTRUCTION FOR M3b WAS WRONG IN THREE WAYS, and this is the fifth time in this
> project that a recorded blocker, once checked, was not what it claimed.**  Keeping the corrections
> is the point — the rule "a reported blocker is a hypothesis" keeps earning its place:
> 1. **The file had ten errors**, the first at lines 110/116, not the single `whnf` timeout at line
>    241 that was reported.  Because that earlier proof was error-recovered, **`key_injective` only
>    ever *elaborated* on a `sorryAx` dependency** — `Probe/LpAx1.lean` still reproduces
>    `'…key_injective' depends on axioms: [propext, sorryAx, Classical.choice, Quot.sound]`.  So the
>    claim that it "now compiles" was an artefact of error recovery, and **the only thing that
>    detects this is `#print axioms`**: a file can compile, and a theorem can exist, while depending
>    on an axiom nobody declared.  This is the sharpest argument in the repository for why that check
>    is not optional.
> 2. **`key_of_even` had no timeout at all.**  It was a plain `rw` pattern-match failure:
>    `zmod_int_eq_iff_dvd_sub 8 A B` instantiates with its two sides swapped against a goal of the
>    form `↑A = ↑B`.  Fixed by `exact (…).mpr ⟨k, by omega⟩`, with no `rw`.
> 3. **The `whnf` timeout was neither `ZMod 2` instance search nor `omega` — that was the
>    dispatcher's own diagnosis, and it was wrong**, as was the fix recorded from it ("redo the count
>    over `Nat` masks").  It fires when the `Function.Injective` statement `key_injective` is
>    *applied* to a hypothesis not syntactically of the form `key d τ = key d' τ'`: instantiating its
>    implicit pair argument makes the unifier compare `key (Prod.fst ?a) (Prod.snd ?a)` with
>    `key d τ`, reducing `key`, `keyInt` and the `ZMod 8` casts.  Fixed by `MM.key_injective_pair`
>    (explicit binders) plus a bijection whose codomain is the plain function type.  **No `Nat` masks
>    were needed.**
>
> **M6's arithmetic is now verified and recorded, because it is easy to get wrong.**  Writing the
> M3 shapes with `b := d + 2t` (so the vector is `2b` in the even case and `1 + 2b` in the odd case,
> `|d|` the codeword weight in `{0,8,12,16,24}`):
>
> * **Even case:** `a·a = 4·(b·b)` and `b·b = |d| + 4S + 4Q` with `S := Σ_{j ∈ supp d} t_j`,
>   `Q := Σ_j t_j² ≥ 0`.  So `b·b ≤ 7` forces `|d| ≤ 7`, hence **`|d| = 0`**; then `b = 2t` gives
>   `b·b = 4Q ≤ 7`, so `Q ≤ 1`, and `Σt` even rules out `Q = 1`.  Hence **`a = 0`** — the even case
>   needs no case analysis at all.
> * **Odd case:** `a·a = 24 + 4·(Σ_j b_j) + 4·(b·b)`, so `a·a ≥ 32 ⟺ Σ ≤ …` where
>   `Σ := Σ_j b_j + b·b` must be `≥ 2`.  If `|t_j| ≥ 2` then `b_j² ≥ 9` (inside `supp d`) or `≥ 16`
>   (outside), so `b·b > 6`; hence under `b·b ≤ 6` we have `t_j ∈ {-1,0,1}`, and then `Q = 0` forces
>   `t = 0`, contradicting `Σt` odd.  **Exhaustive check over `|d| ∈ {0,8,12,16,24}` and `Σt` odd:
>   the minimum of `Σ` is exactly `2`, attained only at `|d| = 0` with `t = -e_j`** (one coordinate
>   `-1`), giving `a = 1 - 4e_j`, `a·a = 32`.  For `|d| = 8, 12, 16, 24` the minima are
>   `64, 96, 128, 192`, a large margin — only `|d| = 0` needs care.
>
> **Two corrections were needed to get here:** the reconnaissance's recorded case split for M6 said "`b·b ≤ 8 ⟹ |d| ≤ 8 ⟹ |d| ∈ {0,8}`, both cases
> elementary", which is loose (the true forcing is `|d| = 0` in the even case); and the dispatcher's
> own first bound for the odd case, `Q ≤ 3`, was **wrong** and had to be replaced by the `Q ∈ {0,1,≥2}`
> split above.  This is the sixth correction of a recorded route, split or bound on the Leech
> milestones alone.
>
> **M4 and M6 are LANDED.**
>
> * **M4** — `Definitions/MMLeechForm.lean` (301 lines): `MM.leech_sum_mul_dvd : 8 ∣ ∑ aⱼbⱼ`,
>   `MM.leech_sq_dvd : 8 ∣ ∑ aⱼ²`, and the exact division `MM.normSq_spec : 8 * normSq a = ∑ aⱼ²` —
>   so `(x,y) = (Σxᵢyᵢ)/8` is integral on `A`.
>   **The input M4a actually needs is "Golay is doubly even AND closed under addition"** — `4 ∣ wt`
>   applied to `d`, `e` **and** `d + e` (the last through `MM.two_dvd_wt_mul`, which supplies
>   "`|c ∩ c'|` even"); `2 ∣ wt` alone would not suffice.  **And M3's parity correction is equally
>   load-bearing**: the terms `4·ca·S` and `4·cb·T` are each `4 mod 8` in the odd branch and cancel
>   only via `S ≡ cb`, `T ≡ ca (mod 2)`.  So integrality is an **independent confirmation that the
>   corrected M3 shape is right** — the reconnaissance's `x₀ + 2(d+2t)` with `Σt` even gives `4 mod 8`.
>   Recorded precision: the "`4ℤ²⁴` direction" of `A` is generated by `4·lift d` and `8·eᵢ`, **not** by
>   `4·eᵢ` — indeed `4eᵢ ∉ A` (coordinate sum `4` but `4a₀ = 16 ≡ 0 mod 8`).
> * **M6** — `Definitions/MMLeechMinNorm.lean` (455 lines):
>   `MM.leech_min_norm : IsLeechVec a → a ≠ 0 → 32 ≤ ∑ aⱼ²`, with `MM.leech_min_norm_attained`
>   exhibiting the minimiser.  So `Λ` is **rootless** with minimum norm `4`, which is the arithmetic
>   that forces the moonshine module to use a rootless lattice.
>   **The odd branch is proved by a 2-line argument that supersedes both the reconnaissance's split and
>   the dispatcher's replacement for it.**  With `b := d + 2t` and `Z := Σⱼ (tⱼ + dⱼ)(1 + 2tⱼ)`:
>   `Σⱼ bⱼ + b·b = 2Z` **exactly** (so `a·a = 24 + 8Z` and the goal is `Z ≥ 1`); `Z ≥ 0` **pointwise
>   for every integer `tⱼ`** (the two factors always share a sign — so no bound on `|tⱼ|`, no support
>   bound, no `b·b ≤ 6` hypothesis is needed); and `Z` is **odd** because `Z ≡ Σt + wt d (mod 2)` with
>   `Σt` odd and `4 ∣ wt d`.  Hence `Z ≥ 1` and `a·a ≥ 32`.  The odd branch's only Golay input is
>   `4 ∣ wt d`; the weight set `{0,8,12,16,24}` is needed only in the even branch, where
>   `2 ∣ Σtⱼ² − Σtⱼ` makes `Q` have the parity of `Σt` and so rules out `Q = 1` without support counting.
>   **Minimiser:** `a = x₀ − 4eⱼ` (one coordinate `−3`, the rest `+1`, `a·a = 32`); `t = +eⱼ` gives
>   `a·a = 48`, so the **sign matters** — the substance of the dispatcher's correction, which was
>   right, though its case analysis was not needed.
>
> **M5 is LANDED** — `Definitions/MMLeechUnimodular.lean` (546 lines, 0 `sorry`/`axiom`/`native_decide`,
> 2.8 s to build, no enumeration): `MM.isLeechVec_iff_eight_dvd : (∀ a ∈ A, 8 ∣ ∑ aⱼyⱼ) ↔ y ∈ A`;
> `MM.leech_unimodular` and `MM.leech_dual_eq_eighth`, stating the dual of `A` as `A* = (1/8)A` — with
> `x = y/√8`, `λ = a/√8` one has `⟨x,λ⟩ = ⟨y,a⟩/8`, so this is **literally `Λ* = Λ`**.
>
> **The unimodularity statement I proposed in the task brief was FALSE, and the proof corrected it.**
> I suggested "`x` integral against every `a ∈ A` ⟹ `x` has integral coordinates and lies in `A`".  The
> counterexample is `x = x₀/4 = (1/4,…,1/4)`: it pairs integrally against every `a ∈ A` because
> `Σⱼ aⱼ ∈ 4ℤ` (it is `0` or `4` mod `8`), yet `x ∉ A`.  The correct unscaled statement is `8A* = A`,
> i.e. `A* = (1/8)A` — the scaling is load-bearing, exactly as it was for the definition of `A` itself
> (where `1/√8` was essential and two memory-based attempts failed for want of it).  **This is the
> seventh recorded route or statement on these milestones that the work corrected.**
>
> The four steps of the recorded route all survived, with one normalization correction and one
> statement correction: `4(eᵢ − e_j) ∈ A` gives `4(xᵢ − x_j) ∈ ℤ` (**not** `xᵢ ≡ x_j (2)` for the
> rational `x` — that was the recorded route's imprecision); `2c ∈ A` gives `4 ∣ Σ_{i∈c} yᵢ`; the class
> words land in `C^⊥ = C` via `MM.golay_self_dual`; and the odd generator is **`x₀ − 4e₀`**, not `x₀`
> (the brief's tentative `x₀ = 1` is **not** in `A`, since `24 ≢ 4 mod 8`).  An independent numeric
> cross-check (`Probe/m5_dual_check.py`) confirms the four generator families really generate `A`
> (`[ℤ²⁴ : span] = 2³⁶`) and tests `x₀/4`, `x₀ ∉ A`, `2x₀ ∈ A`.
>
> **Evenness is LANDED too** — `Definitions/MMLeechEven.lean` (215 lines, 1.6 s):
> `MM.leech_sq_dvd_sixteen : IsLeechVec a → 16 ∣ ∑ aⱼ²` and `MM.two_dvd_normSq`, so every norm is an
> **even** integer and `Λ` is an even lattice.  **M4b's recorded input list was incomplete:** its
> docstring said the sharpening follows from the same expansion with `(lift d j)² = lift d j` and
> `4 ∣ wt d`, which is complete for the **even** branch, but the **odd** branch also consumes
> `Odd (∑t)`.  With `∑t` even one gets `24 + 8·wt d ≡ 8 (mod 16)`, so `2 ∤ normSq` — witness
> `a = x₀`, where `∑aⱼ² = 24` and `normSq = 3`.  **So evenness follows from M3's parity correction,
> not from the Golay code alone** — the same conclusion M4a's integrality and M6's minimum each forced
> independently, making this the third such confirmation.  The stale docstring is corrected in place
> (including a `30000` that should have been `20000`, the count the checked-in script actually uses).
>
> **M7's parametrisation is found and verified, and the three families are now precise.**  The
> reconnaissance's three *numbers* are all correct; its *prose* was imprecise in one place.  Writing
> `W := wt d`, and using the M3 shapes:
>
> | family | count | parametrisation | why |
> | --- | --- | --- | --- |
> | `(4,4)` | `1104 = 4·C(24,2)` | even branch, `W = 0`: `a = 4t` with `Σtⱼ² = 2`, so `t = ±eᵢ ± eⱼ`, `i ≠ j` | unordered pair `{i,j}` plus a sign per element |
> | `(2⁸)` | `97152 = 759·2⁷` | even branch, `W = 8`: `S + Q = 0` pointwise forces `t_k ∈ {0,−1}` on `supp d` and `0` off it, so `a = 2·1_d − 4·1_u` with `u ⊆ d` | **M3's parity condition `Even (Σt)` is exactly `\|u\|` even**, and an 8-set has `2⁷` even subsets |
> | `(∓3, ±1²³)` | `98304 = 4096·24` | odd branch: `a·a = 24 + 8Z` with `Z = Σ_k (t_k + d_k)(1 + 2t_k) ≥ 0` pointwise, so `a·a = 32 ⟺ Z = 1`, i.e. exactly one summand is `1` | data is `(codeword, coordinate)`; the two ways a summand can be `1` give `−3` and `+3`, and `Σt = −wt d + 2d_{j₀} − 1` is **automatically odd**, so the odd parity hypothesis is free here |
>
> `1104 + 97152 + 98304 = 196560`.  **The dispatcher re-derived all three independently and checked
> family 2 exhaustively**: over a fixed octad, exactly the `128 = 2⁷` even subsets `u` are admissible
> and every one of them gives `a·a = 32`.  The bijection `u ↦ u Δ {k₀}` (even ↔ odd subsets) is what
> makes `2⁷` rather than `2⁸`, so the count is **a consequence of M3's parity correction** — the
> **fourth** place that correction is load-bearing, after M4a's integrality, M6's minimum and
> `MMLeechEven`'s evenness (where, without it, `a = x₀` gives `normSq = 3`).
>
> **A `Fintype`/`DecidablePred` trap measured on this file**: instance search does **not** unfold the
> `Golay` `abbrev` under `DecidablePred`, so `Fintype {d // Golay d}` and `Fintype {d // Golay d ∧
> wt d = 8}` are not synthesizable; they need an explicit `DecidablePred` instance for the octads and
> an `inferInstanceAs`-transported `Fintype` for the codewords — the sharper form of the milder note
> already recorded under M0/M1.
>
> **M7 is LANDED** — `Definitions/MMLeechKissing.lean` (1373 lines, 0 `sorry`/`axiom`/`native_decide`,
> 2.5 s to build, no enumeration): **88 declarations, every axiom footprint a subset of the three
> standard axioms** (77 exactly, 9 without choice, 2 with none at all), and
> * `MM.leech_kissing_number : {a | IsLeechVec a ∧ ∑aⱼ² = 32}.ncard = 196560` — the classical Leech
>   kissing number;
> * `MM.leech_min_iff_shape`, the classification of the minimal vectors;
> * `MM.leech_shape44_ncard = 1104`, `MM.leech_shape28_ncard = 97152`, `MM.leech_shape3_ncard = 98304`.
>
> The three families' **intrinsic** shape predicates are worth recording, since they are what the
> classification actually says: `IsShape44` (two coordinates `±4`, the rest `0`), `IsShape28`
> (coordinates in `{0,±2}`, the `+2`-support a Golay octad, and an **even** number of `−2`s), and
> `IsShape3` (coordinates in `{±1,±3}` with a **unique** coordinate of absolute value `3`).  Each
> parametrisation is proved injective, in the carrier, and of squared length `32`, and the three are
> pairwise disjoint.
>
> **M8 is LANDED, and the Leech sequence M0--M8 is CLOSED.**
> `Definitions/MMLeechLattice.lean` (661 lines, 0 `sorry`/`axiom`/`native_decide`, 1.8 s):
> `structure MM.LeechLattice` with fields `ASub`, `ASub_eq`, `rank_eq`, `index_eq`, `integral`, `even`,
> `selfDual`, `posDef`, `noRoots` — **all five properties filled, none assumed** — inhabited by
> `MM.leech_lattice_isLeech`.  Plus `MM.leech_rank : Module.finrank ℚ QSpan = 24` (the earlier files
> had only the index), the pruned enumerator `MM.leechBox` with its pruning-correctness lemma,
> `MM.leechThetaCoeff` with `MM.leechThetaCoeff_zero`, and the moonshine consequence.
>
> **Two deliberate honesties.**  (i) The `selfDual` field is `A* = (1/8)A`, the true form — the
> docstring states that the unscaled `A* = A` is false, and **no `24 × 24` Gram determinant is
> computed**: `det = 1` is the field `index_eq : [ℤ²⁴ : A] = 2³⁶`, since `[ℤ²⁴ : A]² = 8²⁴`.
> (ii) **`V_Λ` is not constructed anywhere in this repository**, so the moonshine consequence is
> stated as the arithmetic the future construction consumes — `MM.leechWeightOneDim := 24 +
> MM.leechCount 2` with `MM.leech_weight_one_dim : MM.leechWeightOneDim = 24` and
> `MM.leechCount_two : leechCount 2 = 0` from M6 — and **not** as a `finrank` of an object that does
> not exist.
>
> **A name collision the dispatcher had to fix at merge time**: the file had mirrored `MM.E8`'s
> vocabulary too faithfully and used `MM.Candidate`, which `Definitions/MMLevelTwo.lean` already
> declares, so `FinalCheck.lean` failed with `environment already contains 'MM.Candidate.mk.injEq'`.
> Renamed to `MM.LeechCandidate` / `MM.IsLeechLattice`; the E8 names are untouched.  **Mirroring a
> sibling module's vocabulary is fine for the shape and dangerous for the names.**
>
> **What the closed sequence says**: `Λ = 2^{-3/2}·A` is an **even integral unimodular rank-24 lattice
> with no roots and kissing number `196560`** — the Leech lattice — with every one of those words a
> named, guarded theorem.  **What it does not say**: nothing about `V_Λ`, which is not built.  The
> remaining multi-year items are unchanged: the `c = 1 → c = 24` tensor layer (which exists nowhere)
> and the no-ghost theorem.
>
> **Only M1a–M1e are finite kernel computations.**  M3–M7 are elementary but are congruence and
> sum-of-squares **case analyses, not enumerations**: `A/8ℤ²⁴` has `2³⁶` elements, and this
> repository's own rank-8 experience is the warning (`thetaCoeff 1 = 240` and even `thetaCoeff 0 = 1`
> did **not** finish in ~18 min when task D-d re-measured them; the earlier "11 s / 497 s" figures did
> not reproduce, and neither did the suggested `countP`/`Bool`-predicate rewrite — the pruned
> enumeration `boxAux` is what does not scale, not the predicate).  Brute-force lattice enumeration is
> out; the M6 case split actually used is the one recorded above, and the numeric script enumerates
> exactly those cases, so a subagent can check its split against machine-verified lists.
>
> **M0 + M1a--M1e are LANDED** in `Definitions/MMGolay.lean` (746 lines, 58 theorems, 0 `sorry`,
> 0 `axiom`, 0 `native_decide`; every declaration's `#print axioms` is the three standard axioms
> except `msgOf_xor`, which is the strict subset `[propext, Quot.sound]` because it never uses
> choice).  Guarded in `FinalCheck.lean`.  Measured: the file takes **3 m 25 s** to build and
> `FinalCheck.lean` **25 s** with it imported.
>
> **Two claims in the brief for that task were refuted by the work, and both are recorded rather
> than smoothed over.**
> * **"doubly even (indeed by 8)" is FALSE.**  The extended Golay code has **2576 words of weight
>   `12`**, so `8 ∣ wt` fails.  The sharp true statement is `4 ∣ wt` (`golay_doubly_even`), with the
>   exact weight set `{0, 8, 12, 16, 24}` (`golay_weights`).
> * **The twelve generator masks' provenance is NOT formalized.**  They are literals produced by
>   `Probe/leech_verify.py` from the length-23 quadratic-residue code plus a parity bit; what is
>   re-proved here is that these twelve words generate a `[24,12,8]` doubly-even self-dual code,
>   agree with the parity-block enumeration on all `4096` messages (`codeWord_eq_encLin`), and
>   contain the all-ones word.  Formalizing the QR-code provenance is not part of M0/M1.
>
> **Two NEW traps, both measured, both of which M2 onward must avoid.**
> * **`ZMod 2` division-ring instance paths HANG the elaborator.**  `LinearMap.finrank_range_add_finrank_ker`
>   and `Submodule.eq_of_le_of_finrank_le` are stated for `[DivisionRing K]`; at `K = ZMod 2` the
>   elaborator cannot reconcile `CommRing.toCommSemiring.toSemiring` with
>   `DivisionRing.toDivisionSemiring.toSemiring` and does not terminate — deterministic whnf timeout
>   at 200k heartbeats, and **over 300 s wall clock even with `maxHeartbeats 8000000`**.  Rank and
>   dimension arguments over `ZMod 2` must go through `finrank_span_eq_card`,
>   `Submodule.card_eq_card_quotient_mul_card` and `LinearMap.quotKerEquivRange` instead.
>   `Set.eq_of_subset_of_ncard_le` is also dangerous there (its `toFinite_tac` default plus
>   `Nat.card_coe_set_eq` rewrites hung the elaborator).
> * **One big `decide +kernel` can OOM the machine.**  The `4096 × 12` bridge check peaks above
>   `7 GB` RSS and was **OOM-killed** (`journalctl -k`: `anon-rss:7255024kB`); split into `8` blocks
>   of `512` it peaks at `~5.7 GB`.  With `~7 GB` free the build is comfortable, so **do not run
>   these checks concurrently with another heavy build.**
> * A third, milder one: instance search does **not** find `Fintype {w // Golay w}` (application
>   form) even with a `Decidable (Golay w)` instance; `Fintype {w // inGolay w = true}` and
>   `{w // w ∈ Golay}` do work, so all counting statements use the explicit form.
>
> **Measured kernel costs** so M2 onward can budget: `golay_low_bits` (4096×12 bits) ≈ 21 s,
> `golay_weights` ≈ 25 s, `golay_weight_counts` ≈ 24 s, the `bridgeHigh_0..7` blocks ≈ 17 s each
> (~136 s total).  Also noted: `inGolay` costs a `4096`-candidate search per kernel evaluation, which
> M2a's carrier will pay per class word — the Leech design already accepts this, but a cheaper
> decision procedure (extract the low 12 bits, `codeMask n % 4096 = n`) is available and not done.
>
> **Measured traps a subagent must not re-discover** (from `Probe/LeechRecon.lean`, which compiles
> in 1 m 27 s with seven proved declarations, all printing the three standard axioms):
> * enumerating a **function type** such as `Fin 12 → ZMod 2` blows up in `piFinset` `Nodup`
>   bookkeeping — enumerate `Nat` masks over `Finset.range 4096` instead;
> * plain `decide` exceeds the heartbeat limit; **`decide +kernel`** (the device already used at
>   `Definitions/MMLevelTwo.lean:102`) is what works;
> * instance search neither unfolds a plain `def` nor sees through `w ∈ Golay`: make the code an
>   `abbrev` with a `Bool` membership test and state the carrier condition as
>   `inGolay (cls a r) = true`; index the four class words by `Fin 4`;
> * **no `native_decide` is needed** — the 4096-word checks are affordable in the kernel (75 s).
>
> **A discipline note, kept for the record:** M8's guarded moonshine statement depends on `noRoots`,
> so **M6 had to be discharged before any guarded declaration could cite it**; the "no roots"
> hypothesis stayed explicit until then, exactly as the paper's `c(0) = 0 ⟹ no roots` argument carries
> it.  (Discharged: see M6 above.)

### PHASE 0 DECIDED, AND PHASE 1's FIRST INCREMENT LANDED (both measured)

> **Phase 0: vendor the `vertexAlg` axiom core.**  Both port measurements are in.
>
> * `vertexAlg` (commit `bd8adbb`, tag `v4.33.1`): **35/35 modules compile against our pin, 0 errors,
>   0 warnings.**  The reason is decisive and measured rather than assumed: its Mathlib pin is
>   `0df444a3`, ours is `db584cd`, and **`db584cd` is its direct parent** — distance **1 commit**,
>   touching only `lean-toolchain` (`v4.33.0` → `v4.33.1`).  The Mathlib source is identical, so the
>   error-classification table is empty *by construction*, not by luck.
> * **Vendored**: the minimal compiling core, **9 files / 5507 lines**, byte-identical to upstream.
>   `tools/build.sh` gained a `--vendor` mode, because `lean` resolves `VertexAlg.*` on the **module**
>   path while the compile loop derives outputs from the **source** path — listing them as ordinary
>   files writes oleans where no `VertexAlg.*` import can find them.  Verified: 9/9 OK and
>   `import VertexAlg.VertexBasic.Borcherds` works from an MM module.
> * **Two corrections to the earlier reconnaissance, both by compiling.**  (i) The **locality half of
>   the axiom equivalence is NOT proved**: `locality_if_Borcherds_sums_2_3_eq`,
>   `Borcherds_sums_2_3_eq_if_locality`, `borcherdsId_at_large_t_iff_locality`,
>   `skew_symmetry_iff_Borcherds_at_zero` are inside comment blocks with `sorry` bodies, and
>   `def IsLocal` is commented out.  (ii) **There are no models at all**: 6,414 of 10,772 lines are
>   live and there are 714 live declarations, but **no instance of `VertexAlgebra` or
>   `VertexAlgebra1` exists anywhere upstream**, and `Affine.lean`, `Lattice.lean`,
>   `ChevalleyEilenberg.lean`, `Lie/Basic.lean` are 100 % doc-comment.  So what is formalized is the
>   **interface**, not vertex algebras; `V_L`, `V_{II^{1,1}}` and `V^♮` are all still to be built.
>   See `vendor/vertexAlg/README.md`.  Upstream tracks **no LICENSE file** despite Apache-2.0
>   headers — recorded, not worked around.
>
> **`VirasoroProject` is the real port, and it is small — but it does not contain the moonshine
> layer.**  At our pin `main` (`555a9096`) gives **47 independent errors in 6 files**, blocking 15 of
> 32 modules; but upstream branch **`bump-202606`** (`e3e08a3b`, same mathematics, no `sorry`) already
> did most of the work and leaves only **21 errors in 4 files**.  Porting those 4 files (~50 changed
> lines, two of them one-liners) reaches **25 of 32 modules green**, measured.  Realistic total:
> **5 files, ~60--100 lines, 2--4 hours, no mathematical statement changed**.  The drift is
> mechanical: `LieRing.ofAssociativeRing` demoted to file-local, the Lean core split of
> `nsmul`/`zsmul` into `NSMul`/`ZSMul` parents, `Set`/`DecidablePred` reducibility, and
> `UniversalEnvelopingAlgebra` re-based from `RingQuot` to `RingCon`.  Bottleneck file
> `LieCohomologySmallDegree.lean`.  **And it contains no `TensorProduct` of modules, no coalgebra,
> no lattice/VOA/vertex machinery — zero hits in both trees** — so `V ⊗ V_{II^{1,1}}` is new
> mathematics at any pin, not a port.
>
> **Phase 1's first increment landed: `Definitions/MMGenusZeroArith.lean`** (224 lines,
> Mathlib-only, no FLT import, 0 `sorry`/`axiom`/`native_decide`) — the packaged form of the
> `genusZero_level` / `genusFormula_eleven` result measured in "M1's COST WAS MIS-STATED" above, both
> guarded in `FinalCheck.lean`.  **It is arithmetic about a definition and asserts nothing about
> `Γ₀(N)`**; the identification "this formula = the genus of `X₀(N)`" remains the open geometric
> content.  Two measured semantic traps are recorded there: `ψ` must be
> `∑ d ∈ N.divisors with Squarefree d, N / d` (the tempting `if Squarefree d then d else 0` is *not*
> Dedekind psi — at `N = 4` it gives `3` instead of `6`, so the formula returns `-1/4`), and the
> completeness half (that no other `N` has genus zero) is checked only numerically, for `N ≤ 300`,
> and is **not** formalized.

### Phasing (each phase ends in a compiling, `sorry`-free increment)

**Phase 1 — the modular half of the Conway--Norton table (tractable; no vertex algebras).**
Deliver: `Γ₀(N)` as a subgroup of `GL(2, ℝ)`, the genus-zero list as a *proved* statement for the 15
Conway--Norton levels, and the bridge to `MM.IsAnalyticNormalizedHauptmodul`.  The genus numbers come
from FLT; the bridge is the open question (see the `M1` entry).  Discharges the *modular* part of
assumed input 4.

**Phase 2 — the monster group as a real object.**  Finiteness and order `|M| = 2^46·3^20·5^9·7^6·
11^2·13^3·17·19·23·29·31·41·47·59·71` from the presentation (task S3), then retargeting
`MoonshineModule` to `MM.Monster` (S4), then the character table for section 9's case check (M1').

**Phase 3 — the no-ghost theorem.**  Self-contained and independent of the module construction
(Frenkel--Goddard--Olive / Goddard--Thorn).  This is the item to attack *before* Phase 4, because it
is a finite, well-stated theorem rather than an open-ended construction.

**Phase 4 — the moonshine module itself.**  Lattice vertex algebras `V_Λ` for Λ even unimodular,
the tower construction of `V^♮` (`V_Λ⁺`, the orbifold, the `σ`-twisted module), the monster action,
and the graded character `j - 744`.  **This is the multi-year item** and it is the only one where the
plan cannot be given as a finite task list today; it needs its own reconnaissance before it can be
phased, which is dispatched as part of Phase 1's work.

### Reporting rule for this campaign

Each phase's increment must compile (`tools/build.sh`, exit 0), add no `sorry`/`axiom`/`native_decide`,
and land with the README/ROADMAP updated.  A phase that turns out to be mis-scoped is recorded as
such rather than quietly dropped — the third defect of the `IsHauptmodul` family is the reason that
rule exists.

## Stream M — the Conway--Norton table (removes assumed input 4)

> **M1-L1h IS DONE (2026-09-13): the level-one integrality input `hq` is PROVED.**  Two files,
> `Definitions/MMLevelOneJCoeffs.lean` (582 lines) and `Definitions/MMLevelOneHq.lean` (507 lines), both
> in `FinalCheck.lean` with ten `#print axioms` guards, each exactly
> `[propext, Classical.choice, Quot.sound]`: `MM.levelOneA : HahnSeries ℤ ℤ` satisfies
> `MM.levelOneA_isNormalized` and **`MM.levelOneA_hasQExpansion : HasQExpansion ((levelOneJ - 744) - qInv)
> levelOneA`**, and `MM.levelOne_hauptmodul_of_orbitSeparation_discharged` /
> `…isAnalyticNormalizedHauptmodul_of_orbitSeparation_discharged` restate the two conditional theorems of
> `Definitions/MMLevelOneCusp.lean` with that hypothesis discharged — **still taking
> `MM.LevelOneOrbitSeparation` explicitly**.  `MMLevelOneCusp.lean` itself is deliberately unmodified, so
> its own theorems still carry `hq`; the proved versions live in the new file.
>
> **Why it took five attempts, recorded because the lesson is general: the first four were chasing an
> IMPOSSIBLE intermediate.**  `qExpansion 1 MM.qInv = 0` is **not provable**, and not for want of effort:
> `cuspFunction h f = update (f ∘ invQParam h) 0 (limUnder (𝓝[≠] 0) (f ∘ invQParam h))`
> (`Mathlib/Analysis/Complex/Periodic.lean:119`) and `q ↦ q⁻¹` is unbounded near `0`, so its `limUnder` is
> `Classical.epsilon (fun _ : ℂ => False)` — a canonical *arbitrary* element of ℂ — and `qExpansion`'s 0-th
> coefficient **is** that value (`qExpansion_coeff`, `m = 0`).  So the statement is false, not hard, and the
> dispatcher's own briefs asked for it three times.  **The working route never touches it:** expand the
> *analytic* function `(j − 744) − q⁻¹` as a whole (`MM.levelOneCuspBounded`), use
> `qExpansion 1 Δ = X·map P_Z`, do the **division in `ℤ⟦q⟧` before mapping** (`invOfUnit`; `P_Z` has constant
> term 1) and cancel `X`.  Coefficients verified: `coeff 0 = 0`, `coeff 1 = 196884`, `coeff 2 = 21493760` —
> `c(g,0) = 0` being the FLM fact `V_0 = 0` (`MM.DenominatorIdentity.coeff_one`) and `196884 = dim V_1`.
>
> **What this changes, and what it does not.**  Level one's *analytic* story is now complete except for
> orbit separation: invariance, surjectivity, the cusp expansion, the integrality of the coefficients and the
> two-sided `q`-expansion are all theorems.  The **only** remaining input for `MM.IsAnalyticNormalizedHauptmodul`
> at level one is still `MM.LevelOneOrbitSeparation`, which is the valence formula — and the owner has paused
> that.  So this increment does not reopen stream M; it finishes the half that never depended on the pause.
>
> **Dispatcher verification (not the task's report):** oleans deleted, then
> `tools/build.sh Definitions/MMLevelOneJCoeffs.lean Definitions/MMLevelOneHq.lean FinalCheck.lean` →
> three `--- OK ---` lines, exit 0; `forbidden_tokens.py` clean on all three, exit 0; `FinalCheck.lean`
> prints only its pre-existing unguarded `MoonshineConjectureStatement.genusZero_exists` line.
> **Three dispatcher errors from this sub-stream are on record in the files themselves** (the `qExpansion qInv`
> route asked for three times; a wrong "induct instead of using Mathlib's `iter_deriv_inv'`" instruction; and a
> false claim that `invOfUnit_mul` needs a `Field`), plus one library figure the retry found wrong in a
> repository header (`[q²]P_Z` is `252`, not `553176`).

### [paused] M1 — genus zero for the groups in the table — **PAUSED BY THE OWNER 2026-09-13**

> **Owner decision (2026-09-13): stream M1 is paused.**  Asked to choose between funding the
> level-one valence formula (1,500--3,000 lines, no partial credit — see the M1-L1g reconnaissance
> block below, which is the measured case for it), landing only the cheap restatements, taking FLT's
> 606-module algebraic route, or pausing M1 for another stream, the owner chose **pause and move
> elsewhere**.  What that decision means in practice, stated so it is not misread:
> * **No further M1 task is dispatched**; the M1-L1g reconnaissance result stands as evidence, and
>   the valence-formula project is *not* cancelled — it is unstarted and priced.
> * **The level-one integrality half is not M1-blocked and was allowed to finish** (task M1-L1f,
>   accepted 2026-09-13: `MM.qExpansion_levelOneDiscTprod_eq_formal`), because it needs no valence
>   formula.  A follow-on packaging task (level-one `hq`) may complete independently.
> * **The consequence the owner should weigh:** the headline's conclusion still contains
>   `IsHauptmodul` (inside `IsAnalyticNormalizedHauptmodul`), whose orbit-separation conjunct is what
>   the valence formula supplies.  So at the pause, "genus zero" and orbit separation were
>   **load-bearing hypotheses** of `MoonshineConjectureStatement*`, not proved properties — for `𝒮ℒ`
>   as much as for `Γ₀(N)⁺`.  `MM.IsGenusZeroGroup` alone does not carry orbit separation;
>   `MM.IsGenusZeroGroup.exists_isHauptmodul_of_orbitSeparation` takes it as an explicit hypothesis.
>   (**Superseded for level one**: batches 7--9 proved `MM.LevelOneOrbitSeparation` and the level-one
>   Hauptmodul unconditionally — see the HANDOVER blocks.  The pause stands for every other level.)

> **FLT ASSETS SURVEYED (see `refs/FLT-ASSETS.md`, 604 lines).**  A read-only
> reconnaissance of the sibling `fermats-last-theorem` development answered "can it accelerate MM?"
> with evidence, and it **corrected this repository's earlier pessimism**: FLT **does** have a valence
> result, in divisor form — `AlgebraicCurve.Divisor.isPrincipal_of_genus_eq_zero` ("on a genus-0 curve
> every degree-0 divisor is principal", closure **50** modules) — together with genuine order-of-
> vanishing identities at general level (`…sum_ord_jBar_sub_eq_finrank`, `…_eq_dedekindPsi`) and a
> `ComplexPlaceDictionary` whose `pt_eq_pt_iff` turns "inequivalent points" into "distinct places".
> **BUT A VERIFICATION PASS (`refs/FLT-L1-VERIFY.md`, 415 lines) THEN CORRECTED THAT ROUTE, and this is the
> state to work from.**  (a) The survey's flagged caveat was misdirected: `modularFunctionFieldBar N`
> *is by definition* `laurentBaseChange ℚ̄ (modularFunctionFieldFull N)`
> (`Def_ModularCurve_ArithmeticGalois.lean:111`), and FLT itself bridges the two constructions
> (`…laurentBaseChange_…_eq_…FullC`, `genusFF_…FullC_eq_…Bar`); the genuinely open link is
> `genus` vs `genusFF` and the ℚ̄ → ℂ transfer at the `genus` level.  (b) **The route's step 5 is
> invalid as written**: `WLight.levelOne_holFn_eq_polynomial_j` requires `hol : MDiff h` (holomorphic
> on all of `ℍ`), while step 4 concludes that `realize 1 X` has an interior pole at `τ` — the two
> contradict each other, and step 6 evaluates `X` where step 4 says it has a pole.  A repair is sketched
> (`X·(j − j τ)`) and marked unverified.  (c) Costs, measured by walking FLT's import graph with no
> compile: stating the step-2 objects needs **4 modules (1 to compile, ≈5 s)**;
> `Nonempty (ComplexPlaceDictionary 1)` needs **43 (37 to compile)**; making the dictionary usable
> (`pt_eq_pt_iff`) needs **345 (330 to compile)**; the whole route steps 1--3 is **606 modules, 585 to
> compile — realistically 4--15 hours serial**.  (d) Missing pieces not previously listed:
> `Gamma0 1 = ⊤` (Mathlib has `Gamma_one_top` but **no `Gamma0_one`**), the
> `realize 1 (jqModC) = E₄³/Δ` identification, and the `orbitMk` orientation.
> The survey's §4.3 gives a **six-step route to `MM.LevelOneOrbitSeparation`** with every gap named,
> and its honest caveat is that **two objects may differ**: the dictionary targets
> `laurentBaseChange ℂ (modularFunctionFieldFull N)` while the genus theorem is about
> `modularFunctionFieldBar N` — "whether the level-one instances agree is not verified and is the
> first thing to check".  **Where the band is narrow, measured:** FLT has **no `Γ₀(N)⁺`**, and the
> dictionary is typed over `Subgroup SL(2,ℤ)`/`Gamma0 N`, so it cannot be instantiated at `Γ₀(N)⁺` —
> where most of the Conway--Norton table lives.  Cost, measured: FLT's own build directory holds **8
> oleans** while MM's holds 205 (36 of them FLT imports); the decisive closures are 50 modules (the
> divisor theorem) and 345 (the dictionary), a one-off multi-hour compile.  Also recorded there: the
> five theorems with "hauptmodul" in the name are **classical modular relations among `j`-values**, not
> genus-zero/Hauptmodul-function statements, and `Thm_ModularCurve_evalAtJGen_injective` is about the
> *polynomial-ring* map, not about `j` being injective on `ℍ` — two names that would otherwise be
> misread into a brief.

> **Increments landed, level one (`Γ = 𝒮ℒ`) — the only level the sibling repository covers.**
>
> * **M1-L1a** — `Definitions/MMLevelOneHauptmodul.lean` (455 lines): `MM.levelOneJ := E₄³/Δ` on
>   `MM.levelOneGamma := 𝒮ℒ`.  Two of `MM.IsHauptmodul`'s three conjuncts are proved — invariance
>   (`MM.levelOneJ_invariant`) and surjectivity (`MM.levelOneJ_surjective`, from the sibling
>   repository) — and the third, **orbit separation**, is isolated as the named hypothesis
>   `MM.LevelOneOrbitSeparation`.  The route to separation through the sibling's *polynomiality*
>   theorem was proposed, then **refuted as a dead end** with three theorems
>   (`MM.levelOne_polynomial_in_j_constant_on_fibre` and friends, commit `310553a`): every function
>   that theorem certifies is constant on `j`-fibres, so it can never witness a collision.
> * **M1-L1b (this session)** — `Definitions/MMLevelOneDiscUnit.lean` (229 lines) and
>   `Definitions/MMLevelOneCusp.lean` (285 lines): **the cusp expansion is now a theorem**,
>   `MM.levelOneJ_cusp_expansion : IsZeroAtImInfty ((j − 744) − q⁻¹)`, i.e. the classical
>   `j = q⁻¹ + 744 + 196884q + ⋯`.  It rests on the missing coefficient
>   `MM.levelOneDiscUnit_coeff_one : levelOneDiscUnit.coeff 1 = −24`, equivalently
>   `MM.qExpansion_discriminant_coeff_two : (qExpansion 1 Δ).coeff 2 = −24` (from
>   `discriminant_eq_E₄_cube_sub_E₆_sq` plus `E_qExpansion_coeff`), and on the Jacobi product
>   `Δ = 𝕢·∏' n, (1 − eta_q n)^24` with `MM.qExpansion_levelOneDiscTprod : qExpansion 1 P =
>   levelOneDiscUnit`.  A by-product worth reusing: **`MM.isBoundedAtImInfty_div_qParam_pow`** —
>   the first `n` `q`-coefficients of `f` vanishing implies `f/𝕢ⁿ` is bounded at `i∞`.
>   Consequence: `MM.levelOne_hauptmodul_of_orbitSeparation_and_qExpansion` and
>   `MM.levelOne_isAnalyticNormalizedHauptmodul_of_orbitSeparation_and_qExpansion` restate the
>   level-one results with **only two** inputs left — `MM.LevelOneOrbitSeparation` and the
>   integrality input `HasQExpansion ((j−744) − qInv) a`.
> * **Still NOT obtained, with the obstruction named.**  `HasQExpansion` *is* the integrality of the
>   Fourier coefficients of `j − 744 − q⁻¹` (`196884, 21493760, …`), packaged as `HahnSeries ℤ ℤ`.
>   The one missing Lean step is the **analytic-to-formal product comparison**
>   `qExpansion 1 P = PowerSeries.map (Int.castRingHom ℂ) (∏' n, ((1 : ℤ⟦X⟧) − X^(n+1))^24)`:
>   Mathlib has both sides separately but no lemma identifying Taylor coefficients of an infinite
>   product of analytic functions with the formal product's coefficients.  The route around it
>   (`P⁻¹` in `ℤ⟦X⟧` via `PowerSeries.invOfUnit`, E₄³'s coefficients integral by
>   `E_qExpansion_coeff`) is recorded in the footer of `MMLevelOneCusp.lean`.  **It is not called
>   easy and it is not faked.**
> * **Nothing in these files shows `SL₂(ℤ)` has genus zero.**  `MM.HasGenusZero` is the cardinality
>   condition `Nonempty (ℍ/Γ ≃ ℂ)`; see the standing caveat in `MMLevelOneHauptmodul.lean`.

* Deliverable: for each `N` in the Conway--Norton list, a proof of `MM.HasGenusZero` for the
  relevant group (`Γ₀(N)`, `Γ₀(N)⁺`), via an explicit bijection with `OnePoint ℂ`.
* Acceptance: builds, no `sorry`.
* Risk: **very high** — but the recorded reason below was **wrong on two counts** (measured).
  Mathlib has no genus of a modular curve, no Riemann--Roch for modular curves, no modular curve at
  all.  The original paragraph said `fermats-last-theorem` has "~200 files of modular-curve
  infrastructure but also no genus theory"; in fact FLT has **1450 definition modules and 29511
  theorems**, and it **does have genus theory** — `Definitions/Def_AlgebraicCurve_CanonicalDivisor.lean:33`
  defines `genus`, and `Place`, `Divisor`, `LSpace`, `H1`, `indexOfSpecialty`, `HasCanonicalDivisor`
  and a Čech Riemann--Roch family under `Theorems/Thm_AlgebraicCurve_cechRiemannRoch_*` all exist
  (whether unconditional or under an unproved `...Reached`/`...Exists` hypothesis is what the survey
  had to settle).  It is also **importable from this package**: compiling FLT's
  `Definitions/Def_ModularCurve_ProjectiveLine.lean` takes ~5 s, after which MM can `import` it and
  `#check @ModularCurve.IsUnimodularRow`.  The recipe is `tools/build.ps1`'s `LEAN_PATH` **plus the
  FLT root directory** (and `lean -o` does not create directories); FLT's own modules are **not
  built** — only `P2M` has oleans — so any FLT module MM wants must be compiled to `.olean` first.
  `Def_ModularCurve_X0.lean` imports seven stock Mathlib modules and **no FLT-internal module**, so
  the closures are shallow.  The prerequisite sub-project is still: define the compactified modular
  curve `X(Γ)` as a Riemann surface, prove it is compact with finitely many cusps, and state/prove
  the genus formula; the practical first step (M0, below) is the *function field* characterisation of
  genus zero, which avoids Riemann surface theory entirely.

  > **SURVEY RESULT (dispatcher-verified where stated).**  The interface is built and working:
  > `Probe/build-flt-subtree.ps1` resolves FLT's internal imports (`Definitions|Theorems|P2M`),
  > topologically sorts them, compiles incrementally into the right `.olean` mirrors and skips what is
  > current; `Probe/build-mm-with-flt.ps1` wraps MM files that import FLT.  Two mechanisms only
  > measurement reveals: **`lean -o` resolves imports from the output path**, so `P2M.*` must land in
  > FLT's own `.lake/build/lib/lean` (why the first attempt's seven modules "failed"), and on this
  > machine `lean` returns exit code `-1`, not `1`, through MSYS2.  A closure of 8 modular-curve
  > targets is **30 modules**, 9 compiled / 17 skipped / 0 failed.  `Definitions.Def_CohCarrier_Level`
  > is **broken in FLT itself** (`Def_CohCarrier_Level.lean:198`), blocking `Def_ModularCurve_XH` —
  > do not try to fix it.
  >
  > What that buys M1:
  > * **`X₀(N)`'s genus formula is unconditionally proved in characteristic 0**:
  >   `Thm_ModularCurve_genusFF_modularFunctionFieldFullC_eq_genusFormula_algebraicClosure`, plus
  >   `CuspForm.finrank_gamma0_weight_two_eq_genusFormula (N) [NeZero N]`.  So the *genus computation*
  >   half of M1 drops from **very high risk to low**.
  > * `genusZeroLevels := [1,2,3,4,5,6,7,8,9,10,12,13,16,18,25]` (the genus-0 list for `Γ₀(N)`) is
  >   already computed at `P2M/Sol/S_ModularCurve_genusFormula_isNat.lean:957`.  Measured: neither
  >   `decide` nor `norm_num` can recompute it (`genusFormula` uses `noncomputable def`, `Nat.card`
  >   over `ZMod`, `totient`, `dedekindPsi`), so that 2297-line file was necessary — **refuted later
  >   for the arithmetic half** by `Probe/ProbeArithFull.lean` (140 lines, Mathlib only); see
  >   "M1's COST WAS MIS-STATED" above.
  > * **The other half does not drop at all.**  FLT has **no** "genus 0 ⟹ single generator /
  >   `≅ RatFunc`" theorem, and **no algebraic-to-analytic bridge**: FLT's genus is that of an
  >   algebraic function field, while MM's `HasGenusZero` is a statement about `ℍ/Γ`.  Level 1 is the
  >   only precedent (`WLight.levelOne_hauptmodul_package`, which has `j_surjective`).  `Γ₀(N)⁺` —
  >   most of the Conway--Norton table — is unexplored.
  > * **Important negative:** `FunctionFieldGeneration`
  >   (`Thm_ModularCurve_functionFieldGeneration.lean:8`) holds **for all `N`** and does not mention
  >   genus, so it is **not** a genus-zero criterion.  Do not use it as one.
  > * Cost reality: one genus theorem's closure is **1115 modules** (P2M 511 + Theorems 510 +
  >   Definitions 94), dragging in `EMD`/`ModuliPoint`/elliptic curves/Galois representations.

> **M1-L1g reconnaissance: `MM.LevelOneOrbitSeparation` is NOT provable in this environment, and the
> reason is one missing theorem.**  (Dispatcher-dispatched recon task; the dispatch report is at
> `Probe/ORBIT_SEPARATION_RECON.md` with probes `Probe/ProbeM1L1g{A..E}.lean` — **scratch, not
> committed**.  (This note was written by the reconnaissance task itself; the dispatcher has read the
> report and the probes, but has **not independently re-run** the compiled negatives it quotes — they
> are the task's evidence, not the dispatcher's.)
>
> **The single decisive gap:** nothing in Mathlib or `fermats-last-theorem` connects *"a modular form
> vanishes at an interior point `τ ∈ ℍ`"* to *"its `q`-expansion order at the cusp is high"*.  That
> link is the level-one **valence formula**, absent from both (grep-verified: no `def`/`theorem
> valence` anywhere in Mathlib, no `argumentPrinciple`; `ModularForm.valence`, `ModularForm.divisor`,
> `CuspForm.valence`, `UpperHalfPlane.j`, `ModularForm.j` are all unknown constants in this pin).
> Every route in the brief dies at that same wall.
>
> **A route recorded in this file is a hypothesis, and one of them was FALSE — the dispatcher's own.**
> The brief's route (D) — "multiply `j - c` by a power of `Δ` and violate the Sturm bound" — is dead,
> and the dispatching brief's stated reason for rejecting it was wrong.  The refutation, checked by the
> dispatcher by hand against the `PowerSeries.order` API (the note's claim that
> `(qExpansion 1 g_m).order = m - 1` is the arithmetic `1 + (m-1) = m > (m-1)`): for `g_m := (j - c)·Δ^m = Δ^{m-1}·(E₄³ - cΔ)`, the leading term is `Δ^{m-1}`
> with coefficient `1` and the correction `-cΔ^m` starts one order higher, so
> **`(qExpansion 1 g_m).order = m - 1` for every `c : ℂ` and every `m`** — while
> `ModularForm.sturm_bound_levelOne` (`LevelOne/DimensionFormula.lean:305`) forbids only
> `order > k.toNat / 12 = m`.  So an interior zero of `g_m` is Sturm-compatible at every `m`; taking
> `m` large cannot repair the route.  (At `m = 1` the constant term of `E₄³ - cΔ` is `1`, so the only
> `Δ`-elimination lemma, `qExpansion_eq_qExpansion_discriminant_mul`, cannot even be *applied* — its
> hypothesis is exactly that this coefficient vanishes, so using it to prove the cusp order is
> circular.)
>
> **Route (F) is not an alternative:** `ModularGroup.exists_smul_mem_fd` plus
> `eq_one_or_neg_one_of_mem_fdo_mem_fdo` give only `LevelOneOrbitSeparation ↔ (j injective on 𝒟ᵒ mod
> ±1)` — the same target, approached differently.  A **restatement, not progress**; it must not be
> reported as partial progress on the Hauptmodul conjunct.
>
> **Dispatcher verification of this note:** the `sturm_bound_levelOne` citation was re-checked and is
> correct (`LevelOne/DimensionFormula.lean:305`, and `:286` for the `ℕ`-weight form), and the `order`
> arithmetic in the route-(D) refutation was re-checked by hand and is correct.  The **"unknown
> constant" negatives** (`ModularForm.valence`, `ModularForm.divisor`, `CuspForm.valence`,
> `UpperHalfPlane.j`, `ModularForm.j`, `modularLambda`, `Gamma2`) and the probes
> `ProbeM1L1g{A..E}.lean` are the **task's** evidence and were not independently re-run.
>
> **Also corrected here:** `Definitions/MMLevelOneHauptmodul.lean`'s header says "the cheapest known
> route is Mathlib's modular-forms dimension/valence machinery".  Mathlib has the **dimension** half
> only, and it is proved *from* the isomorphism `S_k ≅ M_{k-12}` plus base cases, so it cannot be
> inverted into a zero count.  There is no valence machinery to use.  Route (L) (λ/Γ(2)) is confirmed
> dead: no `modularLambda`, no `Γ(2)`/`Γ_θ` in either repository.
>
> **What that costs, honestly.**  A real proof of `LevelOneOrbitSeparation` needs the analytic valence
> formula for level one (`∑_{z ∈ 𝒟ᵒ} ord_z f / |stab_z| + ord_∞ f = k/12`, with the `1/3` and `1/2`
> weights at `ρ` and `i`): **1,500--3,000 lines** by the reconnaissance estimate, mostly
> `import Mathlib`-class modules (~93 s each).  There is no partial credit — a valence formula with a
> wrong constant is worthless — and everything on MM's side of it (invariance, surjectivity, the cusp
> expansion, the fundamental domain, the dimension formula) is already available.  The alternative is
> FLT's algebraic route at the price already recorded above (606 modules, 585 to compile).
> **This is a scope decision for the repository owner, and it is recorded here rather than taken.**
>
> **It is on the critical path, and the dispatcher checked the conjunction chain rather than trusting
> a first reading** (a first reading of the headline got this *wrong*): the conclusion of
> `MoonshineConjectureStatementGenus` is `IsGenusZeroGroup Γ ∧ IsAnalyticNormalizedHauptmodul Γ f a`,
> and `MM.IsAnalyticNormalizedHauptmodul` (`MNHauptmodulUniqueness.lean:119`) has
> `IsHauptmodul Γ f` as its **first conjunct**, which is invariance ∧ surjectivity ∧ **orbit
> separation** (`MMModular.lean:148-151`).  So the valence formula is what stands between this
> repository and an unconditional level-one theorem; `MM.IsGenusZeroGroup` alone does **not** carry
> orbit separation, and `MM.IsGenusZeroGroup.exists_isHauptmodul_of_orbitSeparation` takes it as an
> explicit hypothesis for exactly that reason.
>
> **Flavour of the saved evidence, so the next task does not redo it:** `ModularForm.discriminant : ℍ
> → ℂ` is *not* a `ModularForm` (it is the coercion of `CuspForm.discriminant`; `rfl`, yet invisible to
> `rw`); `levelOne_weight_zero_const` is `ModularFormClass`-namespaced; `ρ`, `I` are `UpperHalfPlane`
> variables and `1 +ᵥ ρ` is a third boundary point (the `cases_of_mem_fd_smul_mem_fd` split has nine
> cases); the `1/3`/`1/2` elliptic-point weights are load-bearing; `orbitMk` acts on the **second**
> argument; and `tools/build.sh --timeout` **is** implemented after all — the reconnaissance reported
> it as documented-but-missing, and the dispatcher checked: `tools/build.sh` parses `--timeout SECS`
> before its file list and enforces it with `timeout` at both the file and vendor call sites, printing
> `--- TIMEOUT (${TIMEOUT}s): <file> ---` on expiry.  The trap is positional, not missing: the flag
> must come **first**, or it is taken for a filename.  (Recorded because a reported blocker is a
> hypothesis too — this one was wrong, and it had already been copied into this file.)

### [x] M0 — the modular predicates diagnosed and repaired — **ACCEPTED (a) + (b); (c) folded into M1**

### [x] D0 — repair the definitions `MoonshineConjectureStatement` is phrased in — **CLOSED (a), (b), (c); D0-iii closed the two remaining items and proved the optional rewiring cosmetic**

> **AUDIT VERDICT (dispatcher-verified: the file was rebuilt and every key declaration re-checked
> with `#print axioms` before this was written).  `Definitions/MMStatementAudit.lean`.**
>
> **`MM.MoonshineModule` has no inhabitant.**  Proved, with the three standard axioms:
>
> ```lean
> theorem MM.no_moonshineModule (M : MM.MoonshineModule) : False
> theorem MM.not_moonshineConjectureStatement : ¬ MM.MoonshineModule.MoonshineConjectureStatement
> ```
>
> So `moonshine_conjecture`'s `sorry` and `not_moonshineConjectureStatement` are **contradictory**,
> and every theorem stated for an `M : MoonshineModule` — including the two guarded in
> `FinalCheck.lean` and everything in `Challenge.lean` — is **vacuously true**.  A green build with
> green `#print axioms` guards no longer carries its old meaning: the guards certify proofs about an
> empty structure.  This is the third defect of the same family in this project, after
> `IsHauptmodul` (unsatisfiable: `MMModular.lean`) and `IsHauptmodul` again (vacuous:
> `MMGenusZeroRefute.lean`).
>
> **Two independent defects, both proved, both needing repair:**
>
> 1. **`MM.MoonshineModule.hauptmodul` demands `IsBoundedAtImInfty f` *and*
>    `IsNormalizedHauptmodul Γ f (M.thompsonSeries g)`.**  The paper's normalized Hauptmodul takes
>    `i∞` to `∞` — it has a pole there and is therefore **unbounded** at that cusp; Mathlib's
>    `IsBoundedAtImInfty` speaks about that marked cusp only.  Drop the conjunct, or replace it by
>    boundedness at the *other* cusps.
> 2. **`MM.GradedModule.FiniteSupport` is *finite total support*
>    (`∀ g, {n | V.traceCoeff g n ≠ 0}.Finite`) — not what its own docstring says** ("the homogeneous
>    pieces vanish for all sufficiently negative degrees").  Finite total support is **false of the
>    FLM module**: `j - 744` has infinitely many nonzero coefficients.  It is also what makes the
>    `hauptmodul` field unsatisfiable, by an argument that does not mention the cusp at all:
>    `MM.not_surjective_of_finite_support_coeff` — if `f` is 1-periodic, `MDiff`, bounded at the cusp
>    and `HasQExpansion f a` with `{m : ℕ | a.coeff m ≠ 0}` finite, then `f` is a **finite sum of
>    monomials** `c_m q^m` with `‖𝕢 τ‖ < 1`, so `∀ τ, ‖f τ‖ ≤ Σ ‖c_m‖` and `f` is bounded on all of
>    `ℍ` — contradicting `Function.Surjective f`, which `IsHauptmodul` contains.  Weaken to "support
>    bounded below", which is what `HahnSeries` actually needs and what is true of FLM.
> 3. **`MM.HasQExpansion` never inspects the negative part of `a` — now CHARACTERISED, not merely
>    reported.**  `Definitions/MMQExpansionGap.lean` proves the limitation: the one-sided condition
>    **does** pin `a.coeff 0` once `f` is periodic and bounded at the cusp
>    (`MM.coeff_zero_eq_valueAtInfty`), but it can never constrain the negative degrees
>    (`MM.hasQExpansion_of_neg_eq`), so **no series is determined by it**
>    (`MM.not_determined_by_one_sided`) and the `q⁻¹` term of a normalized series is invisible to the
>    only link `IsNormalizedHauptmodul` has between `f` and `a`.  **THE REPAIR IS NOW LANDED** (task
>    T2-i, this session): `MM.HasLaurentQExpansion f a` in `Definitions/MMQExpansionTwoSided.lean`
>    writes the pole out as `f = a.coeff (-1) * qInv + g` with `g` periodic, `MDiff` and bounded, and
>    the series is then **determined** by `f` (`MM.HasLaurentQExpansion.eq`) — the exact negation of
>    `MM.not_determined_by_one_sided`.  Normalization becomes a property of `f`
>    (`…isBoundedAtImInfty_sub_qInv`, and conversely `…coeff_neg_one_eq_one_of_isBoundedAtImInfty_sub_qInv`),
>    `MM.isNormalizedLaurentSeries_iff` matches it to `MM.IsNormalizedSeries` on integer coefficients,
>    and the level-one instance is proved (`MM.levelOneJ_sub_hasLaurentQExpansion`, `q⁻¹`-coefficient
>    `1`, `q⁰`-coefficient `0`) from `MM.levelOneJ_cusp_expansion`.  **What is still NOT done:** the
>    coefficients are `ℂ`-valued, so **integrality** is untouched (the missing Lean step is in
>    `MMLevelOneCusp.lean`'s footer), and **`MM.MoonshineModule` has not been rewired** onto the
>    two-sided predicate — that rewiring changes the statement of Theorem 1.1 and is a dispatcher
>    decision, exactly as D0's item (c) says.  (Original report, for the record: Mathlib's `qExpansion`
>    is a `PowerSeries`, so the degree-`n` conjuncts only bind `n : ℕ`, and a faithful treatment needs
>    a `LaurentSeries` / `HahnSeries ℤ ℂ` `q`-expansion.
>    `MM.not_hasAnalyticNormalizedHauptmodul_single` shows the field's existential fails for
>    `a = q⁻¹`, which *is* `IsNormalizedSeries` — so the conclusion is **not** free.)
>
> **A correction to this entry's own earlier text, kept for the record.**  The 20-minute-lived claim
> that "surjectivity is now immediate" from the third conjunct of `IsHauptmodulAnalytic` was already
> wrong (M0(b)); the further claim that **boundedness at the cusp trivialises the `q`-expansion**
> — i.e. that `(qExpansion 1 f).coeff n = 0` for every `n ≥ 1` — was also wrong, and it is wrong
> **as a compiled counterexample**: `MM.qExpansion_coeff_one_qParamFun` shows `q ↦ q` is periodic,
> `MDiff` and bounded at the cusp yet has `q¹`-coefficient `1`
> (`not_forall_qExpansion_coeff_eq_zero_of_one_le`).  The Cauchy-estimate argument for it was
> vacuous: boundedness bounds the cusp function on a *fixed* punctured disc, and `n!/R^n` with a
> bound uniform in `R` gives nothing as `R → 0`.  Boundedness at the cusp bounds the coefficients by
> *geometric* growth; it does not kill them.  **Four dispatcher hypotheses about this one field were
> wrong in a row; the file records all four.**  The rule stands and applied to the dispatcher: a
> recorded route is a hypothesis.
>
> **Scope of the repair (a decision, not a task):** it changes `MM.GradedModule.FiniteSupport`,
> `MM.MoonshineModule.hauptmodul` and `MM.HasQExpansion`, i.e. the statement of Theorem 1.1.  Streams
> S, T, A and the whole M0 diagnosis are unaffected — they do not go through `MoonshineModule`.
> (**Taken**: see D0-e and D0-g below, which carry the rewiring and its equivalence theorem.)

> **RECONNAISSANCE VERDICT (dispatcher-verified: the probes were recompiled before this was
> written).  The spec below must NOT be dispatched as written, and the M0 line in "Ordering" is
> wrong for the same reason.**
>
> **1. `MM.IsHauptmodul` carries no analytic content at all.**  Its three conjuncts are invariance,
> surjectivity onto `ℂ`, and orbit separation — and the last two are supplied free of charge by the
> quotient map.  Proof (`Probe/ReconC.lean`, compiles, axiom-free): for **every**
> `Γ : Subgroup (GL (Fin 2) ℝ)` and every bijection `e : ℍ/Γ ≃ ℂ`, the function
> `fun τ => e (MM.orbitMk Γ τ)` satisfies all three, because `MM.orbitMk_surjective`
> (`MMModular.lean:83`) gives surjectivity and `MM.orbitMk_eq_iff` (`MMModular.lean:74`) gives
> separation.  No discreteness of `Γ`, no cusp, no holomorphy, no meromorphy is used anywhere.
> Consequently:
> * the spec's candidate repair `HasGenusZeroFun Γ := ∃ f, IsHauptmodul Γ f` is **`True` in
>   disguise** — proved for every `Γ`, with `HasGenusZeroFun Γ ↔ HasGenusZero Γ` given the
>   cardinality input, so it neither excludes `Γ₀(11)` nor adds anything;
> * a cusp-aware variant `∃ f, IsHauptmodul Γ f ∧ ¬ IsBoundedAtImInfty f` **is also vacuous**
>   (`Probe/ReconE.lean`, compiles): it implies `HasGenusZero`;
> * "whose field of rational functions generates the invariant field" is not statable here at all:
>   there is **no** invariant field, no `Hauptmodul` anywhere in Mathlib (grep: zero occurrences),
>   and no analytic `genus`; attached to `IsHauptmodul` it degenerates to its third conjunct.
> There is therefore **nothing to prove** in the shape the old spec asks for, and the old
> "Risk: medium … `IsHauptmodul` is already an analytic statement" is exactly backwards.
>
> **2. What survives, and it is worth having.**  `MM.IsHauptmodul` should nonetheless be *repaired a
> second time*: the honest predicate adds the two analytic conjuncts the paper actually uses,
> holomorphy on `ℍ` and unboundedness at the cusp.  `Mathlib` has the input:
> `UpperHalfPlane.qExpansion_eq_zero_iff` — "a periodic `MDiff` function bounded at `i∞` is
> determined by its `q`-expansion" — is precisely the removable-singularity + Liouville content, and
> it needs **no hypothesis on `Γ` beyond periodicity**.  This is already compiled in
> `Probe/ReconD.lean` as `eq_of_qExpansion_eq_of_bounded`.  From it one gets a genuine theorem:
> *a non-constant `Γ`-invariant holomorphic function unbounded at the cusp is surjective onto `ℂ`.*
> That is the first statement in this project about Hauptmoduls a mathematician would recognise,
> and it is Mathlib-only.
>
> **3. What still does not come out of it, and must not be claimed.**  It is a **witness** predicate,
> not a **criterion**: it cannot show `Γ₀(11)` is *not* genus zero, and `HasGenusZero` remains a
> cardinality condition.  Anything that would decide genus zero needs the compactified quotient — a
> Riemann surface, cusps and Riemann–Roch — i.e. task M1, months of work, not a spike.
>
> **4. FLT cannot supply the missing bridge** (measured, `Probe/ReconImport.lean` compiles in
> 5.3 s).  FLT's **definitions** layer is importable — MM's `build/lib/lean/Definitions/` already
> holds 27 FLT `Definitions` oleans — but its genus-formula **theorems** and `genusZeroLevels` sit
> behind the **1115-module** closure (only 4 `Theorems` and 7 `P2M` oleans exist), and, decisively,
> **FLT has no `genus 0 ⟹ F ≅ RatFunc` theorem and no algebraic-to-analytic bridge.**  Its genus is
> that of an algebraic function field; `MM.HasGenusZero` is about `ℍ/Γ`.  Nothing in FLT connects
> them.  So "genus zero via the function field" cannot be finished by importing FLT, and the M1
> risk reduction recorded in the stream-M box applies to the *genus number* only.

**Revised spec.**

* **(a) Record the defect as theorems, not as a paragraph.**  New file
  `Definitions/MMGenusZeroRefute.lean`, mirroring the `IsHauptmodulOldShape` /
  `not_isHauptmodul_old_shape` pattern of `MMModular.lean:166--187`: `HasGenusZeroFun`, its
  vacuity theorem for every `Γ`, and the honest docstring saying that `IsHauptmodul`'s second and
  third conjuncts are supplied by the quotient map.  This is the deliverable that matters, because
  the README currently sells `IsHauptmodul`'s repair as content and it is not.
* **(b) The analytic predicate — DELIVERED, with its limits recorded.**  Two new files, both
  importing `Definitions.MMModular` only, both building clean with 0 `sorry`/`axiom`:
  `Definitions/MMHauptmodulAnalytic.lean` (310 lines) and
  `Definitions/MMHauptmodulAnalyticRefute.lean` (231 lines), which holds the refutations so the main
  file stays readable.

  ```lean
  IsHauptmodulAnalytic Γ f :=
    (∀ γ ∈ Γ, ∀ τ, f (γ • τ) = f τ) ∧ MDiff f ∧
      ∀ c : ℂ, ¬ (MDiff (fun τ => (f τ - c)⁻¹) ∧ IsBoundedAtImInfty (fun τ => (f τ - c)⁻¹))
  HasPoleAtCusp f           := ∀ c : ℂ, IsBoundedAtImInfty (fun τ => (f τ - c)⁻¹)
  HasBoundedInvariantConst Γ := every Γ-invariant holomorphic function bounded at the cusp is constant
  ```

  **THREE candidate predicates were tried and the first TWO are refuted — do not use either.**
  * `invariance ∧ MDiff f ∧ ¬ IsBoundedAtImInfty f`: refuted by `τ ↦ τ` on `Γ = ⊥`
    (`not_forall_isHauptmodulAnalyticWeak_surjective`).  Unboundedness at the cusp does not control
    *how* `f` grows there.
  * `∀ c, ¬ (MDiff (f - c)⁻¹ ∧ IsBoundedAtImInfty (f - c)⁻¹)`: **also refuted**, and this was the
    dispatcher's own correction of the first candidate — a clean illustration of the standing rule
    that a recorded route is a hypothesis, and that the dispatcher's summary is one too.  The
    mathematics is one line: **"`f` misses `c`" and "`f` blows up at the cusp" are compatible with
    "`f` approaches `c` at the cusp"**, and nothing requires `f` to *attain* `c`.  Counterexample
    `f = exp` on `Γ = ⊥` (`not_forall_isHauptmodulAnalytic_surjective`): its only missed value is
    `0`, and at `c = 0` the third conjunct *holds* because `(exp τ)⁻¹` is unbounded at the cusp.
    **So no growth condition at the cusp can force surjectivity**, and the "surjectivity is now
    immediate" argument that stood in this entry for twenty minutes was wrong.

  **What DOES close** (both landed, both guarded):
  * `IsHauptmodulAnalytic.surjective_of_hasPoleAtCusp` — elementary: a missed `c` makes `(f - c)⁻¹`
    holomorphic, `HasPoleAtCusp` makes it bounded, exactly what the third conjunct forbids.
  * `IsHauptmodulAnalytic.surjective_of_hasBoundedInvariantConst` — the classical route, isolating as
    one hypothesis the compactness input the compact Riemann surface supplies.  Mathlib has it only
    at level one (`ModularFormClass.levelOne_weight_zero_const`); in general it is M1.

  **The deliverable is therefore CONDITIONAL, and is stated as such:**
  `IsHauptmodulAnalytic.toIsHauptmodul` takes `HasPoleAtCusp f` **and orbit separation** as explicit
  hypotheses.  Orbit separation is a genuinely independent gap, not a convenience: even with
  holomorphy, the pole condition and surjectivity, `f = j²` on `SL(2,ℤ)` is not injective on orbits
  (`j τ = - j σ` in different orbits gives `j² τ = j² σ`).  That is the paper's degree-1 /
  simple-pole condition, and ruling `j²` out needs the argument principle on `X(Γ)` — M1, not M0.
  **There is no unconditional `IsHauptmodulAnalytic Γ f → IsHauptmodul Γ f` in this Mathlib**, and
  the docstring says so rather than leaving it to be discovered.
> **D0-e LANDED (dispatcher decision, this session): the genus-zero conjunct is now non-vacuous.**
> `Definitions/MMGenusZeroStatement.lean` (272 lines) defines
> `MM.IsGenusZeroGroup Γ := HasGenusZero Γ ∧ HasBoundedInvariantConst Γ ∧ ∃ f, IsHauptmodulAnalytic Γ f ∧ HasPoleAtCusp f`
> and `MM.MoonshineConjectureStatementGenus`, with the reduction
> `MM.moonshineConjectureStatement_of_genus` to the current statement (so nothing is lost).  The
> added conjunct is not decoration, and **both** directions are theorems: `MM.hasGenusZero_bot`
> (from new hand-built equivalences `ℍ/⊥ ≃ ℍ` and `ℍ ≃ ℝ × ℝ`) with
> `MM.not_hasBoundedInvariantConst_bot` (witness `τ ↦ 𝕢 1 τ`) gives
> `MM.hasGenusZero_not_isGenusZeroGroup_bot`; symmetrically `MM.hasBoundedInvariantConst_top` and
> `MM.not_hasGenusZero_top`.  **No inhabitant of `IsGenusZeroGroup` is proved**, so the strengthened
> conjecture must not be quoted as known-satisfiable; the expected first instance is level one
> `𝒮ℒ` (compactness from `ModularFormClass.levelOne_weight_zero_const`, the analytic Hauptmodul from
> `MM.levelOneJ` + `MM.levelOneJ_surjective`, cardinality for the first conjunct) and that is the
> next task — **AND IT IS NOW DONE**: `Definitions/MMLevelOneGenusZero.lean` (320 lines) proves
> `MM.levelOne_isGenusZeroGroup : IsGenusZeroGroup 𝒮ℒ`, so the strengthened hypothesis is
> known-satisfiable in at least one case, with each conjunct proved for real (compactness via
> `ModularFormClass.levelOne_weight_zero_const` on a packaged `ModularForm 𝒮ℒ 0`; the pole via the
> `MM.levelOneJ_cusp_expansion` epsilon bound; the analytic Hauptmodul's third conjunct via the
> constancy argument; and the cardinality conjunct via the fundamental domain's imaginary axis and
> Schröder--Bernstein).  **The headline is still not re-pointed**: `MM.MoonshineModule`, its
> `MoonshineConjectureStatement` and `moonshine_conjecture` still use `HasGenusZero`, on purpose —
> the rewiring (swap the conjunct in the structure's `hauptmodul` field and in `Challenge.lean`) is a
> separate, explicit dispatcher step, to be taken once an inhabitant exists so that the strengthened
> hypothesis is known satisfiable.  That sequencing was the decision, and the condition is now met,
> so **the rewiring was taken (task D0-g, this session) and is DONE**:
> `MM.IsGenusZeroGroup` moved to `Definitions/MMGenusZeroGroup.lean` (upstream of `MMMoonshine.lean`,
> which previously could not see it — the import cycle is what fixed where the predicate lives); the
> structure's `hauptmodul` field now assumes `IsGenusZeroGroup Γ`; the conclusion of the standing
> `sorry` is `MM.MoonshineModule.MoonshineConjectureStatementGenus`; the pre-repair statement is kept
> unchanged with a *proved* implication from the new one
> (`MM.MoonshineModule.moonshineConjectureStatement_of_genus`); the two spellings of the strengthened
> statement are proved equivalent (`MM.moonshineConjectureStatementGenus_iff`); and the new goal's
> **non-vacuity is itself a theorem**
> (`…MoonshineConjectureStatementGenus.genusZero_exists`, yielding `IsGenusZeroGroup` for every
> element, where the old goal yielded only the cardinality condition).  `Challenge.lean` follows the
> new statement, with `moonshine_existence_weaker` as the proved corollary.  **The open content is
> unchanged**: constructing the module (streams S and T).  Nothing about `Γ₀(N)` or orbit separation
> is claimed.

> **D0-iii LANDED (a fresh task agent, dispatcher-verified by a from-scratch rebuild on 2026-09): both
> items this entry still left open are closed, and the rewiring is now known to be cosmetic.**
>
> * **`Definitions/MMLevelOneLaurentIntegral.lean` (166 lines): the level-one two-sided expansion is
>   INTEGRAL.**  `MM.levelOneLaurentSeries_eq_map_levelOneA : levelOneLaurentSeries = levelOneA.map
>   (Int.castRingHom ℂ)` — the complex series of `MM.levelOneJ_sub_hasLaurentQExpansion` **is** the
>   image of the integral series, coefficientwise (`q⁻¹ = 1`, below zero, nonnegative degrees via
>   `MM.qExpansion_levelOneCuspBounded` against `MM.levelOneA_coeff_nat`).  `MM.hasLaurentQExpansion_eq_map_levelOneA`
>   then uses the uniqueness `MM.HasLaurentQExpansion.eq` to make the value **forced**, not witnessed,
>   and `levelOneLaurentSeries_coeff_one` / `_two` compute `196884` and `21493760`.  **Nothing about the
>   Jacobi product is reproved**: the whole input is `MM.levelOneA_hasQExpansion` (task M1-L1h), which is
>   why the "missing Lean step" footer of `MMLevelOneCusp.lean` and the matching footer of
>   `MMQExpansionTwoSided.lean` are superseded rather than confirmed.
> * **`Definitions/MMHauptmodulTwoSided.lean` (288 lines): the predicate of the `hauptmodul` field and
>   the two-sided predicate are EQUIVALENT.**
>   `MM.isAnalyticNormalizedHauptmodul_iff_hasLaurentQExpansion` (carrier `b.coeff 0 = 0`) and
>   `…_and_cusp` (carrier `IsZeroAtImInfty (f - qInv)`, the two interchangeable by
>   `MM.HasLaurentQExpansion.isZeroAtImInfty_sub_qInv_of_coeff_zero` and its converse), both taking
>   periodicity and holomorphy of `f` — two hypotheses `MM.IsAnalyticNormalizedHauptmodul` itself does
>   not carry, the same pair `MM.IsAnalyticNormalizedHauptmodul.coeff_zero_eq_zero` already takes.
>   **So the rewiring of `MM.MoonshineModule`'s field changes nothing but the spelling, exactly to the
>   extent that those two hypotheses and the constant term are carried along; dropping any of them
>   changes the statement**, and the file says so where it matters.
> * **The rewiring itself was deliberately NOT taken** (it is the dispatcher step this entry reserved;
>   the equivalence theorem is the reason it buys no content), and **two brief errors were caught by the
>   task and are recorded**: the brief asserted (i) that `tools/build.ps1` works (it did not: its
>   `LEAN_PATH` put this package's build dir LAST, so every module importing `P2M.*` failed with
>   "object file … does not exist" even though the olean exists here — **repaired by the dispatcher**,
>   the order now matches `tools/build.sh` and the rule in `AGENTS.md`), and (ii) that the forward
>   direction of the equivalence is provable without periodicity and holomorphy of `f` (it is not).
> * Dispatcher verification, from scratch and not by trusting the author: `tools/build.ps1` over the 15
>   prerequisites in dependency order plus the two new files plus the dispatcher's own axiom probe →
>   16/16 `--- OK ---`, exit 0; `Probe/forbidden_tokens.py` → `sorry=0 admit=0 axiom=0
>   native_decide=0`; the dispatcher's probe prints `[propext, Classical.choice, Quot.sound]` for all
>   eleven declarations; `FinalCheck.lean` carries the same eleven `#guard_msgs` guards and builds
>   green (exit 0).  **Nothing in this project's headline changes**: the `sorry` is still the existence
>   of the module (streams S, T), and no genus, orbit separation or `Γ₀(N)` claim is made here.

* **(c) Do NOT replace `MM.HasGenusZero`.**  A separate predicate added beside it, or the statement
  of Theorem 1.1 changes under the README's `genusZero_exists` guard.  That is a dispatcher
  decision, not a task-level one.
* Acceptance: builds, no `sorry`, `#print axioms` exactly the three standard axioms, `FinalCheck.lean`
  green.
* **D0, the consequence that makes M0 urgent.**  With the present definitions,
  `MM.MoonshineModule.MoonshineConjectureStatement` (`MMMoonshine.lean:194`) reduces to
  `IsNormalizedSeries (M.thompsonSeries g) ∧ HasQExpansion f (M.thompsonSeries g)`: its first
  component is the vacuous `IsHauptmodul Γ f`, and `HasGenusZero Γ` is the cardinality condition.
  **The formalized statement of Theorem 1.1 therefore does not require `Γ` to have genus zero**,
  which is exactly the Conway--Norton input.  The existing `genusZero_exists` guard
  (`MMMoonshine.lean:227`) does not catch this, being an `∃ Γ, HasGenusZero Γ`.  Repair: phrase the
  conclusion with the analytic predicate instead of `HasGenusZero` + `IsHauptmodul`.  That changes
  the statement of the theorem, so it needs an explicit dispatcher decision and a README note; it is
  not a change to make silently inside a task.
* Risk: **low-medium**, with **(b)'s surjectivity step named as the failure point** — it needs a
  holomorphic square root of a nowhere-vanishing `MDiff` function on `ℍ` (equivalently a log), which
  Mathlib does not package; budget that step on its own.  The rigidity lemma (2) is already compiled,
  so no Picard argument has to be redone by hand.
* Will **not** deliver: `Γ₀(11) ∉ HasGenusZero`, any genus statement, any bridge to FLT, or a cusp
  compactification.

### [ ] M1' — the seven ATLAS elements and Koike's theorem
* Deliverable: the paper's section 9 case check: seven explicit elements `2B, 3B, 5B, 7B,
  9B, 13B, 15D` and the nonsingularity of `χ_i(g_j)` (determinant `2²²·3⁵·5·7·17`), plus the
  tabulated first five coefficients.
* Depends on S2 (needs the monster) and on the monster's character table, which does not
  exist in Lean.  Recorded as blocked.

---

## Stream A — the monstrous Lie superalgebras (sections 11--14, not needed for Theorem 1.1)

### [x] A1 — the `E8` lattice and its theta series (the finite half of section 11's Lemma 11.1) — **ACCEPTED**

**Goal.**  Lemma 11.1 (and if budget allows 11.2) of the paper's section 11, as power series
identities.  The paper states it for the *Fourier series*, and proves it by multiplying by `Δ` and
comparing finitely many coefficients — so it is formalizable as algebra of formal series, with no
modular-form theory required.

**Definition, confirmed from the paper's TeX source and by the user:**
`eta_{2+}(q) := eta(q)^8 * eta(q^2)^8`, where `eta(q) = q^{1/24} ∏_{n>0}(1 - q^n)` and
`Delta = eta^24`.  Lemma 11.1:

```
theta_{2E8}(q) / Delta(q)      = 1/eta_{2+}(q) + 1/eta_{2+}(q^{1/2}) + 1/eta_{2+}(-q^{1/2})
theta_{2E8+v1}(q) / Delta(q)   = 1/eta_{2+}(q^{1/2}) - 1/eta_{2+}(-q^{1/2})
theta_{2E8+v2}(q) / Delta(q)   = 1/eta_{2+}(q^{1/2}) + 1/eta_{2+}(-q^{1/2})
```

**Corrected and re-verified by the dispatcher (2026-09, exact integer series arithmetic).  The block
that stood here was WRONG — see the correction of record after it:**

```
eta_{2+}(q)          = q - 8q^2 + 12q^3 + 64q^4 - 210q^5 + ...   (the series previously written here
                                                                  was eta_{2+}/q, not eta_{2+})
1/eta_{2+}(q)        = q^{-1} + 8 + 52q + 256q^2 + 1122q^3 + 4352q^4 + ...
1/eta_{2+}(q^{1/2})  = q^{-1/2} + 8 + 52q^{1/2} + 256q + 1122q^{3/2} + ...
1/eta_{2+}(-q^{1/2}) = -q^{-1/2} + 8 - 52q^{1/2} + 256q - 1122q^{3/2} + ...
three-term sum       = q^{-1} + 24 + 564q + 8960q^2 + 105570q^3 + 996096q^4 + ...
Delta x that sum     = 1 + 240q^2 + 2160q^4 + 6720q^6 + ...      (= theta_{2E8}, paper line 2153)
Delta/eta_{2+}(q)    = eta(q)^16 eta(q^2)^{-8} = 1 - 16q + 112q^2 - 448q^3 + 1136q^4 - 2016q^5 + ...
```

**The paper is NOT misprinted here.**  `eta(q)^{16}eta(q^{1/2})^{-8} = q^{1/2} + 8q + 28q^{3/2} +
64q^2 + 126q^{5/2} + 224q^3 + 344q^{7/2} + ...` (`.tex:2156`) is **exactly right** — recomputed
coefficientwise here — and the claim that stood in the earlier revision of this block ("the true
expansion is `q^{1/2} + 8q + 52q^{3/2} + 256q^2 + ...`, so that display is misprinted") was **false**:
those are coefficients of `q · (1/\ddp)`, a different object.  The earlier block's `three-term sum`
and `theta_{2E8}/Delta` lines were shifted by one power of `q` for the same reason, and its
`eta_{2+}(q)` line was `eta_{2+}/q`.  Kept as a correction of record: a dispatcher's numeric
"verification" is a hypothesis until it is redone, and this one was wrong for a whole session.

**Status at that round: delivered with four `sorry`s, since discharged on the M-form route (below).**
Two files were produced and merged: `Definitions/MMLevelTwo.lean` — `E8` as the union of the integral
coset `D8` and the half-integral coset, `IsLattice`, `normSq` (`normSq_nonneg`,
`normSq_half_integral`), `sum_odd_sq_dvd`, `isLattice_iff`, the pruned enumerator `boxAux`/`box`, and
`thetaCoeff`; and `Definitions/ZZCond.lean` — the parity arithmetic for `ℤ`, including
`even_sum_iff_even_pair` and `even_sufficient`, which makes `Even (Σ yᵢ)` the correct coset condition.

`thetaCoeff_zero` is **proved** (task D-d2, combinatorially); the other three (`= 240`, `= 2160`,
`= 6720`) were then `sorry`, and the module's `## TODO: sorries to discharge` records the **corrected**
diagnosis (task D-d): the original `decide` forms for `n = 0` and `n = 1` did not finish in ~18 min,
the suggested `countP`/`Bool`-predicate rewrite did not finish `n = 1` in ~10 min, and the earlier
"11 s / 497 s / 31 s" figures should not be relied on — **the cost is the pruned enumeration `boxAux`
itself**.  The counts are settled in exact arithmetic (`1`; `112 + 128`; `1136 + 1024`;
`3136 + 3584`), each verified twice (`#eval` and an independent Python enumeration of the two cosets),
and the combinatorial route is: a soundness lemma for `box`, constructors for the small vectors, and
the classification of `Σ yᵢ² = 2n` (resp. `8n` with all coordinates odd) for `n ≤ 3`.
**Superseded by M-form** (below): the owner fixed the *route* as modular forms, so these are no longer
enumeration debts.

**Correction found by the task, and independently checked by the dispatcher.**  The brief for A1
said the half-integral coset condition is `4 ∣ Σ yᵢ`.  That is wrong: for `⟨z/2, y⟩ ∈ ℤ` for every
`y ∈ D8` the correct condition is `Σ zᵢ ≡ 0 (mod 2)`, i.e. **`Even`, not `4 ∣`**.  With `4 ∣` the
count comes out `112 + 64 = 176` instead of the paper's `240`; with `Even` it is `112 + 128 = 240`.
`Definitions/ZZCond.lean` proves both directions, so the model is pinned down rather than asserted.

**Warning recorded for everyone doing finite verification in this project.**  The dispatcher
initially "disproved" Lemma 11.1 by computing both sides in a script that truncated the
*intermediate* eta products at the same cutoff as the final answer, which silently dropped
coefficients; with a correct cutoff the identity holds.  **When checking a power series identity
numerically, truncate every intermediate product strictly above the target precision**, or the
result is worthless — and a wrong check of this kind nearly blocked a correct theorem.

**Policy for the remaining `thetaCoeff_*` work (superseded by the route change below):** discharge
them in one pass; the kernel cost of an enumeration cannot be avoided, so the honest fix is a general
lemma that the pruned box covers all vectors of norm at most `B`.

> **ROUTE CHANGE for the four theta-coefficient `sorry`s (owner's instruction, this session).**
> `Definitions/MMLevelTwo.lean`'s `thetaCoeff_one/two/three` were being discharged by *counting*
> lattice vectors (`thetaCoeff_zero` is already proved that way, combinatorially).  The owner has
> directed that the computation formula be proved **directly from modular forms** instead — i.e. the
> classical identity `θ_{E8} = ½(θ₂⁸ + θ₃⁸ + θ₄⁸) = E₄`, from which `thetaCoeff n = 240 σ₃(n)` and all
> four values follow with no enumeration at all.  Task **M-form** is that route, in three stages —
> (1) the coefficient-level identity for the repository's own `MM.thetaCoeff` by parity classification
> of `ℤ^8`; (2) `½(θ₂⁸+θ₃⁸+θ₄⁸) = E₄` via the theta transformation laws and Mathlib's
> `ModularForm.levelOne_weight_four_rank_one`; (3) `thetaCoeff n = 240 σ₃ n` and the three `sorry`s as
> corollaries.  The machinery is grounded: Mathlib has `jacobiTheta` with
> `jacobiTheta_S_smul`/`jacobiTheta_T_sq_smul` (nome `e^{πiτ}`, i.e. `Σ q^{n²/2}`) and
> `EisensteinSeries.E_qExpansion_coeff`; `fermats-last-theorem` has E₄'s integral q-expansion
> (`Thm_EisensteinSeries_ramanujan_system_qExpansion_int`), the divisor-convolution/Ramanujan
> identities (`Def_NumberTheory_DivisorConvolution`) and a Jacobi theta product identity.  **Neither
> has a lattice theta series or the E8 lattice**, so the lattice↔theta bridge is built here.  The
> riskiest step was stage 2's θ₂ multiplier system.
>
> **STAGE 2 LANDED, IN THREE FILES (and it retired that risk).**
> `Definitions/MME8ThetaModular.lean` — **the half-period evaluation
> `MM.jacobiTheta₂_half : jacobiTheta₂ (1/2) τ = jacobiTheta (τ + 1)`**; the brief had listed it as an
> existing library fact and **it does not exist in Mathlib** (the dispatcher re-ran that grep to
> confirm), so it was *proved* from the two series instead, and the correction is recorded in the file
> header and in `AGENTS.md`.
> `Definitions/MME8ThetaS.lean` — **`MM.thetaTwo_S_smul : θ₂(S•τ) = (-Iτ)^{1/2}θ₄(τ)`**, the classical
> `θ₂(-1/τ)` law, from Mathlib's two-variable functional equation at `z = 1/2` with
> `jacobiTheta₂_neg_left` and a `Complex.cpow_add` cancellation.
> `Definitions/MME8ThetaSCombination.lean` — **`MM.thetaCombination_S_smul`**: the combination
> transforms with weight 4 under `S` as well as `T` (stage 1), so the modularity is complete at the
> **generator** level; supporting lemmas include `MM.cpow_half_pow_eight : (z^{1/2})⁸ = z⁴` (no branch
> hypothesis) and `MM.thetaFour_S_smul`.
> **A second brief correction** is recorded in that file: the θ₄-law bookkeeping had been written
> inverted — the law is `θ₄(S•τ) = B·θ₂(τ)` with `B = (-I(S•τ))^{1/2}`, `B⁸ = (I/τ)⁴ = (τ⁴)⁻¹`, and
> since the law carries `B⁻¹` the eighth power of the actual multiplier is `τ⁴`: same weight,
> different accounting, and the `B` form dodges the `cpow` branch.
> **The convention that makes the law usable was settled from the source** (now an `AGENTS.md`
> bullet): `ModularForm.SL_slash_apply` is `(f ∣[k] γ) τ = f(γ•τ)·denom γ τ^(-k)` with
> `ModularGroup.denom_S : denom S τ = τ`, so the `S`-statement *is* weight-4 slash-invariance for `S`
> verbatim.
> **STEP 4a LANDED** (`Definitions/MME8ThetaModularForm.lean`, 130 lines): the combination
> `MM.thetaCombination := θ₂⁸ + θ₃⁸ + θ₄⁸`, its slash-invariance at the two generators
> (`MM.thetaCombination_slash_S`, `…_slash_T`), the group identification
> `MM.closure_mapGL_generators : Subgroup.closure {mapGL ℝ S, mapGL ℝ T} = 𝒮ℒ`, and hence the **full
> statement `MM.thetaCombination_slash_invariant {γ} (hγ : γ ∈ 𝒮ℒ) : thetaCombination ∣[(4 : ℤ)] γ =
> thetaCombination`** by closure induction over `SL2Z_generators`.  Three more traps from this round
> are in `AGENTS.md` (the `JacobiTheta` import chain carries no modular-forms scopes, so no `∣[k]` and
> no `SL_slash_apply`; `Subgroup.closure_induction` takes the generator case first and the membership
> last, and `Subgroup.map_top` does not exist; there is no `denom_T`, and the `mapGL`/`toGL (map …)`
> defeq trap requires stating the `denom` lemma in the goal's form).
> **What remains:** `MDiff` of the three θ's and of the combination, boundedness
> at the cusp, the `ModularForm 𝒮ℒ 4` assembly, then `½(θ₂⁸+θ₃⁸+θ₄⁸) = E₄` by
> `ModularForm.levelOne_weight_four_rank_one` + `EisensteinSeries.E_qExpansion_coeff`; then stage 3's
> two coset bijections give `thetaCoeff n = 240 σ₃ n` and the three `sorry`s as corollaries.  None of
> the stage-2 files enumerates anything (the only `decide`/`box` strings in them are docstrings).
>
> **Recorded fallback, deliberately NOT on `main`.**  The branch `task/d-d5-counting` (commit
> `3eb86ee`) holds a complete **whnf-safe counting proof of `MM.thetaCoeff_one`** (that branch reads
> `sorry=2`).  The dispatcher audited it: its `decide` occurrences are `ZMod 8`-scale checks,
> `decide_eq_true_eq` rewrites and per-coordinate term construction — no searches — and its assembly
> uses `rfl` on lambdas, never unfolding `MM.box`, so it satisfies the no-brute-force rule.  It is held
> back because the owner's directive fixes the *route* for the formula, and mixing provenances (one
> value by counting, the rest by modular forms) would muddy the record.  If the modular route stalls at
> stage 2, landing that branch is a one-step 3 → 2 reduction.

> **A1b RECONNAISSANCE (2026-09-13): STOPPED ON A DEFINITIONAL INCONSISTENCY IN THE SOURCE.  Do not
> dispatch a proof task here until it is settled — and it is a question for the owner, not for a task
> agent.**
>
> The first A1b dispatch burned its budget on reconnaissance and produced no Lean file.  It reported
> **the paper's definition of `\eta_{2+}` (line 2166: `\ddp(q) = \eta(q)^8\eta(q^2)^8`) to be
> inconsistent with the paper's own Fourier expansion three lines earlier (line 2157)**: with
> `\eta_{2+} = \eta^8\eta(q^2)^8` one has `1/\eta_{2+} = 1 + 8q + 52q^2 + 256q^3 + \ldots`, whereas
> the displayed series is `1 - 16q + 112q^2 - 448q^3`; the two readings are related by
> `\eta_{2+} \cdot (\eta^{16}\eta(q^2)^{-8}) = \eta^{24} = \Delta/q`, **not** by `1`.
> **That finding is FALSE and is retracted by A1B-CONVENTION-RECON below** — it compared `1/\eta_{2+}`
> with `\Delta/\eta_{2+}`.  What stood in doubt was only which object `1/\ddp(q)` denotes (an eta
> PRODUCT with positive exponents as printed, or the RATIO whose expansion the paper tabulates); the
> distance-`q^2` arithmetic above is the measured content, and the resolution is below.  A1b is off the
> critical path for Theorem 1.1 either way.

### [ ] A1b — Lemma 11.1 itself, and Lemma 11.2

> **A1B-CONVENTION-RECON LANDED (fresh task agent; the dispatcher re-read the primary-source lines and
> redid the arithmetic from scratch, 2026-09): Lemma 11.1's convention is DECIDED, and the
> "definitional inconsistency" this stream stopped on was an artefact of the repository's own record.**
>
> * `\ddp(q) = \eta(q)^8\eta(q^2)^8` exactly as printed (`.tex:2166`), with
>   `\eta(q) = q^{1/24}\prod_{n>0}(1-q^n)` (`.tex:506`) and `\Delta(q) = \eta(q)^{24}` (`.tex:494`).
>   `1/\ddp(q)` is the honest **reciprocal** — an eta quotient with leading term `q^{-1}` and constant
>   term `8` — and that is the object Lemma 11.1 is stated with.
> * The paper's tabulated `\eta(q)^{16}\eta(q^2)^{-8} = 1 - 16q + 112q^2 - 448q^3 + \ldots`
>   (`.tex:2158`) is **not** the expansion of `1/\ddp(q)`: it is `\Delta/\ddp(q)`, which is exactly
>   what the proof's "multiply both sides by `\Delta(q)`" produces.  Recomputed here by exact integer
>   series arithmetic: `1/\ddp = q^{-1} + 8 + 52q + 256q^2 + 1122q^3 + \ldots`, the three-term sum is
>   `q^{-1} + 24 + 564q + 8960q^2 + 105570q^3 + \ldots`, and `\Delta \times` that sum is
>   `1 + 240q^2 + 2160q^4 + 6720q^6 + \ldots` — the paper's `\theta_{2E_8}` (`.tex:2153`).
> * **So the half-integral-shift, branch-choice and typo hypotheses are all refuted for Lemma 11.1**,
>   and the branch in `\eta(-q^{1/2})` is *forced* (`\mu = -1`) rather than free.  **Lemma 11.1 is
>   therefore unblocked as a statement** — the owner's confirmation of the reading is invited, since
>   this roadmap reserved that decision — and it is a well-posed formal power series identity needing
>   no modular-form theory, only `PowerSeries`/`HahnSeries` algebra of the kind T1 already provides.
> * **Lemma 11.2 stays BLOCKED, for a reason independent of any convention.**  The printed signs at
>   `.tex:2196` (four `-`) and `.tex:2198` (four `+`) add to
>   `\theta_{\Lambda_2} + \theta_{\Lambda_2+v_3} = \Delta/\ddm(q) = 1 - 32q + 480q^2 - \ldots`, but
>   both summands are coset theta series with non-negative coefficients and
>   `\theta_{\Lambda_2} = 1 + 4320q^2 + \ldots` has `q^1`-coefficient `0`: a sum of non-negative
>   series cannot have `-32` at `q^1`.  Independently, `\Delta/\ddm(q^{1/4})` read literally is a
>   `q^{1/12}`-series starting at `q^{3/4}`, whereas the tabulated partner (`.tex:2185`) is a level-2
>   series starting at `q^1`.  **No delivered source settles Lemma 11.2** (checked against Gannon,
>   FLM, Jurisich and Barraclough), so its first deliverable is the resolution of those two points —
>   by the owner, or against Borcherds' own later errata — **not** a Lean file.
> * **Corrections to this repository's record, all verified here and all corrected in place:**
>   (i) the A1b block's central claim ("the paper's definition of `\eta_{2+}` is inconsistent with the
>   paper's own Fourier expansions") is **false** — it compared `1/\eta_{2+}` with `\Delta/\eta_{2+}`;
>   (ii) the A1 row's claim that `.tex:2156` is misprinted is **false** — recomputed coefficientwise,
>   and that row now carries the corrected series; (iii) `README.md`'s eta-product form for
>   `\theta_{2E_8}` was false by weight (`\eta^8\eta(q^2)^8` is `\ddp`, of weight 8 and positive order)
>   and is corrected there; (iv) `AGENTS.md`'s source table called `魔群月光/RWBphd.pdf` "Borcherds'
>   thesis" — it is **Barraclough**, *Some Calculations Related To The Monster Group* (Birmingham
>   2005), while Borcherds' thesis is `魔群月光/THESIS.PDF` (*The Leech lattice and other lattices*) —
>   and it claimed `pdftotext` is installed, which it is **not** on this machine (`python` + `pypdf`
>   is the route); all four are fixed.
> * Full report, including Lemma 11.1 written out in Lean terms and the price of its proof:
>   `Probe/A1B_CONVENTION_RECON.md` (gitignored — this block is its committed substance).

> **M-FORM (owner-directed, this session): the `thetaCoeff` values are to be proved FROM MODULAR
> FORMS, not by counting.**  `Definitions/MME8Theta.lean` (180 lines, stage 1 done) defines the three
> Jacobi theta functions on top of Mathlib — `thetaThree = jacobiTheta`, `thetaFour = θ₃(·+1)`, and
> `thetaTwo = e^{πiτ/4}·jacobiTheta₂(τ/2) τ`, the bridge from the library's **two-variable**
> `jacobiTheta₂` (**not** the classical `θ₂`; the naming trap is recorded in the header) to
> `Σ q^{(n+1/2)²/2}` — and proves the `q`-expansions, the `T`-shift laws, the multiplier law
> `θ₂(T·τ) = e^{πi/4}θ₂(τ)`, and **`thetaCombination_T_invariant`**: `θ₂⁸+θ₃⁸+θ₄⁸` is `T`-invariant
> although no single term is.  **The `S`-side's engine is identified, not missing:**
> `jacobiTheta₂_functional_equation` (the two-variable Poisson identity) at `z = τ/2`, plus
> `jacobiTheta_S_smul` and `jacobiTheta₂ (1/2) σ = θ₄(σ)`.  Remaining stages: (2) the `S`-laws for
> `θ₂`/`θ₄` and hence `½(θ₂⁸+θ₃⁸+θ₄⁸) ∈ ModularForm 𝒮ℒ 4`, concluded to be `E₄` by
> `ModularForm.levelOne_weight_four_rank_one` (both sides weight 4, constant term 1); (3) the
> coefficient-level bridge to `MM.thetaCoeff` (a bijection between the two cosets and the supports of
> `½(θ₃⁸+θ₄⁸)` and `½θ₂⁸` — no search), and then `thetaCoeff_one/_two/_three` as corollaries of
> `thetaCoeff n = 240 σ₃ n`.  **Rule 2 of `AGENTS.md` (no brute-force enumeration) governs all of
> this**, and the superseded counting layer for `n = 1` stays preserved on `task/d-d5-counting` as
> evidence, not to be extended.

With the lattice and theta-series half in place, the remaining work of section 11 is to *discharge*
the four `thetaCoeff_*` sorries, then state Lemma 11.1 with `eta_{2+} := η^8 · (η ∘ q ↦ q²)^8` and
prove it by the paper's method (multiply by `Δ` and compare coefficients).  Lemma 11.2 has weight
`8` and involves `i = √-1`; it needs the weight-`8` analogue.  Neither is on the critical path for
Theorem 1.1 (stream A is not needed for it), so it stays behind T1b/T2 and M0/M1 in the ordering.

### [ ] A2 — a fake monster Lie algebra denominator formula
* Deliverable: the product identity of section 13 stated as a formal power series identity.
* Risk: high; depends on A1 and on root-multiplicity combinatorics.

---

## The FLM campaign (batches 151--229): status, compressed

The campaign to prove FLM Theorem 8.10.2 at FLM's own datum is planned here; its **per-batch
records live in `NOTES.md` Appendix A** (dispatcher narratives: files, exact statements, brief
errors) and its **topic-wise summaries and lessons in `NOTES.md` §§64--127**.  The actionable next
steps are `HANDOVER.md` §6; the exact remaining formulas, `HANDOVER.md` §1.  This section is the
plan's own view: what is closed, what is open, and where a new task entry belongs.

### Closed (do not redo; one row per phase)

| phase | batches | outcome |
| --- | --- | --- |
| alignment with the book (fields, prescriptions, the weight/translation axioms) | 157--165 | the definitions are the book's; `hL0` discharged; `hvir`/`htrans` reduced and partly discharged |
| the `z_0^j` tower `ZLine E j` | 177--205 | `ZAlignedGeneratorFlat` and `zLineModeAt_all` are THEOREMS (batch 202); the `l = 0`, `<a,b> <= -3` residue proved (batch 204) |
| the Jacobi faces (8.8.41) | 186--204 | the `l >= 0` faces proved at every state and pairing; every `l = -c` chamber landed; the `l = -1/-2/-3` slices unconditional at FLM's datum |
| the §8.6 engine | 206--219 | the nested Cauchy carrier at general `k`; the OPE/insertion step at all lengths; **`ModeFieldCommInput` (8.6.9)/(8.6.10) proved at all states** |
| the Fock front | 197--228 | the positive-pairing faces proved (batch 213); the honest negative-pairing residual is ONE one-mode step, lattice base proved (batch 228) |
| the boundary package | 216--228 | the delivery re-hung on the non-vacuous corrected package; residual #1 sharpened, absorbed, put in the display currency, and identified with the source's Theorem 8.6.1 (8.6.3) |
| the two Chapter-8 theorems as statements | 229 | FLM Theorem 8.6.1 and Theorem 8.8.9 + Remark 8.8.11 exist as theorems with one registered `sorry` each (holes = residuals #1 and #2) |

### Open (the campaign's frontier; this is the plan's live part)

| residual | what it is | where |
| --- | --- | --- |
| #1 | the display (8.6.23)/(8.6.24) = (8.5.13) at the (8.6.2) states = the source's (8.6.3): `DisplayAllStates` / `CommutatorInsertion8625` | `HANDOVER.md` §1 row 1; hole of `MM.FLM810T861S.displayAllStates_evenCocycle` |
| #2 | (8.8.41) `l < 0` faces at non-generator pairs: `NegativeResidual` | §1 row 2; hole of `MM.FLM88T889S.theorem889_jacobi` |
| #3 | the Fock half `FockStep` (the one-mode step on the normal-ordered blocks) | §1 row 3 |
| #4 | the `l >= 1` second slot `ResidueMatching8625NegSecondSlot` | §1 row 4 |
| #5 | the standing boundary inputs (`hnd hs C h2 S hpd hW hfin`): instantiate for a concrete positive-definite even lattice | §1 row 5 |

### How to add to this file

Add `[ ]` (todo) / `[~]` (dispatched) entries as plan items --- goal, deliverable, acceptance --- to
this section or to the stream sections above, and put the **record** of the batch that does the work
in `NOTES.md` (a `§` entry for the analysis and lessons; the dispatcher's narrative in Appendix A).
When a task completes, compress it into one row of the "Closed" table above: **do not paste batch
narratives back into this file** --- that is what `NOTES.md` is for.

