# Monstrous moonshine in Lean 4

A Lean 4 formalization of the statement and the formalizable core of

> R. E. Borcherds, *Monstrous moonshine and monstrous Lie superalgebras*,
> Invent. Math. **109** (1992), 405--444.

Lean 4.33.1, Mathlib pinned at `db584cd6d46c92f209a44c0f1c829460d327499d`. **No added `axiom`,
no `native_decide`**: every declaration in this repository is checked by the Lean kernel, and
`FinalCheck.lean` (the default build target) verifies through `#guard_msgs` that each proved
declaration depends on nothing beyond Lean's three standard axioms
`[propext, Classical.choice, Quot.sound]`.

**`sorry` policy (per batch).**  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 `sorry`
must be *registered and linked*: it appears in the `sorry` map below **and** is tied to the open
task/residual it belongs to in `ROADMAP.md` or `HANDOVER.md`; the declarations that consume it are
guarded with `#guard_msgs`, printing `[propext, sorryAx, Classical.choice, Quot.sound]`, so the
hole is never hidden behind a passing build.  **"No `sorry` anywhere" is the completion criterion
of the whole project — the formalization of monstrous moonshine is finished when the map below is
empty — not an invariant of a batch.**

`sorry` currently marks three things — one open mathematical goal and two statement-only
deliveries of FLM Chapter 8 (Theorem 8.6.1 and Theorem 8.8.9 + Remark 8.8.11, batch 229-A); the
three bounded enumerations that used to sit here were discharged from modular forms (task M-form).
See [The `sorry` map](#the-sorry-map-what-is-not-proved).

---

> # THE MODULAR HYPOTHESES WERE DEFECTIVE — DIAGNOSED, REPAIRED, AND RECORDED
>
> Two rounds of audit (`Definitions/MMStatementAudit.lean`, `Definitions/MMGenusZeroRefute.lean`)
> found that the predicates this repository's main theorem is phrased in were broken, in three
> separate ways.  Two are now repaired; one remains.  This box is the answer to "what should I not
> believe", and the repairs are recorded rather than silent.
>
> ### Repaired: `MM.MoonshineModule` was uninhabited
>
> For a period the repository contained **both** `moonshine_conjecture` (proved by `sorry`) and
> `MM.not_moonshineConjectureStatement` — a proof of its negation, with the three standard axioms.
> Every theorem stated for an `M : MM.MoonshineModule` was therefore **vacuously true**, including
> the two guarded in `FinalCheck.lean` and everything in `Challenge.lean`.  Two defects caused it:
>
> 1. **`MM.GradedModule.FiniteSupport` was *finite total support*, not what its docstring said.**
>    The docstring said "the homogeneous pieces vanish for all sufficiently negative degrees"; the
>    definition said `∀ g, {n | V.traceCoeff g n ≠ 0}.Finite`.  The stronger condition is **false of
>    the module the paper is about** — the FLM module's graded dimension `j - 744` has infinitely
>    many non-zero coefficients.  **Repaired**: it is now support bounded below
>    (`∀ g, ∃ N, ∀ n < N, V.traceCoeff g n = 0`), which is what `HahnSeries` actually needs
>    (`MM.isWF_of_bddBelow`).
> 2. **`MM.MoonshineModule.hauptmodul` required `IsBoundedAtImInfty f` alongside a normalized
>    Hauptmodul.**  Those are contradictory: the paper's normalization *is* the `q⁻¹` term, i.e. a
>    **pole at `i∞`**, so a normalized Hauptmodul is **unbounded** at that cusp.  By (1) it also
>    forced `f` to be a finite sum of monomials `c_m q^m`, hence bounded on all of `ℍ`, hence not
>    surjective — contradicting the `Function.Surjective f` inside `IsHauptmodul`.
>    **Repaired**: the conjunct is gone, and the field now uses
>    `MM.IsAnalyticNormalizedHauptmodul Γ f a`, which states the paper's normalization *analytically*
>    (`f - q⁻¹` vanishes at the cusp) instead of asserting a formal series and leaving `f`
>    unconstrained.
>
> **The `sorry` of `moonshine_conjecture` is therefore an honest open problem again** — the
> *existence* of a module with the paper's properties (streams S, T) — rather than an artefact of a
> broken definition.
>
> ### Also repaired: the uniqueness theorem was vacuous
>
> `MM.IsNormalizedHauptmodul.eq_of_qExpansion` took `IsBoundedAtImInfty f` together with
> `IsNormalizedHauptmodul Γ f a`, so **no `f` satisfied its hypotheses** and the theorem said
> nothing.  `Definitions/MNHauptmodulUniqueness.lean` supplies the correct statements, whose content
> is that the *difference* of two functions with the same `q`-expansion is bounded at that cusp
> because the `q⁻¹` poles cancel: `MM.eq_of_qExpansion_of_bounded`,
> `MM.IsAnalyticNormalizedHauptmodul.eq_of_qExpansion`, and the paper's "unique up to addition of a
> constant" (`MM.exists_const_add_of_qExpansion_coeff_eq`).
>
> ### Repaired: `MM.HasQExpansion` cannot see the negative part of a series
>
> Mathlib's `qExpansion` is a `PowerSeries` built from the Taylor coefficients of the cusp function
> at `q = 0`, so `MM.HasQExpansion f a` binds only the degrees `n : ℕ` and **nothing links
> `a.coeff (-1)` to `f`**.  In particular `MM.IsNormalizedHauptmodul Γ f a` yields *no* analytic
> information about `f` at all — which is why the repaired uniqueness theorem states the
> compatibility it needs explicitly, and why the repaired `hauptmodul` field uses the analytic
> predicate.  A faithful treatment needs a two-sided (`HahnSeries ℤ ℂ` / `LaurentSeries`)
> `q`-expansion; that is supplied by **`MM.HasLaurentQExpansion`** in
> `Definitions/MMQExpansionTwoSided.lean` (task **D0**'s repair, landed), where the series **is**
> determined by `f` (`MM.HasLaurentQExpansion.eq`) and the normalization is a property of `f`.
> Task **D0-iii** then closed the two items this box used to leave open:
>
> * **Integrality at level one — CLOSED.**  `MM.levelOneLaurentSeries_eq_map_levelOneA`
>   (`Definitions/MMLevelOneLaurentIntegral.lean`) proves that the complex two-sided expansion of
>   `j - 744` **is** the image of the integral series `MM.levelOneA` under `Int.castRingHom ℂ`, and
>   `MM.hasLaurentQExpansion_eq_map_levelOneA` — via the uniqueness `MM.HasLaurentQExpansion.eq` —
>   that it is the **only** two-sided expansion of `j - 744`; the coefficients are therefore the
>   integers `q⁻¹ = 1`, `q⁰ = 0`, `q¹ = 196884`, `q² = 21493760`, not complex numbers that merely
>   happen to be integral.  The footer of `Definitions/MMLevelOneCusp.lean` saying that this step is
>   missing is superseded by `MM.levelOneA_hasQExpansion` in `Definitions/MMLevelOneHq.lean`, which
>   is the whole input used.
> * **The rewiring of `MM.MoonshineModule` is a change of spelling, and that is PROVED.**
>   `MM.isAnalyticNormalizedHauptmodul_iff_hasLaurentQExpansion` and
>   `…_iff_hasLaurentQExpansion_and_cusp` (`Definitions/MMHauptmodulTwoSided.lean`) prove the
>   predicate of the `hauptmodul` field equivalent to its two-sided form — carried by the constant
>   term `b.coeff 0 = 0`, equivalently by `IsZeroAtImInfty (f - qInv)` — and taking periodicity and
>   holomorphy of `f`, two hypotheses `MM.IsAnalyticNormalizedHauptmodul` itself does not carry.  The
>   field has **not** been rewritten; the point of the equivalence is that rewriting it changes
>   nothing except the spelling, while dropping any of those three carried hypotheses would change
>   the statement (the file says so where it matters).
>
> `MM.statement_audit_summary` records the surviving consequence: not every normalized series is the
> `q`-expansion of a bounded Hauptmodul, so any revision that re-imposes boundedness at `i∞` is
> unsatisfiable again.
>
> **Related, and also diagnosed:** `MM.IsHauptmodul` itself has no analytic content
> (`Definitions/MMGenusZeroRefute.lean`: the `∃ f` repair of `HasGenusZero` is *equivalent* to
> `HasGenusZero`), and `MM.HasGenusZero` is a cardinality condition rather than genus zero
> (`Definitions/MMModular.lean`).  The honest analytic predicate is
> `MM.IsAnalyticNormalizedHauptmodul` / `MM.IsHauptmodulAnalytic`.  Deciding genus zero for any
> specific group needs the compactified quotient — task M1.> 1.1 until these are repaired.**  The modular and power-series parts (streams S, T, A, and the
> M0 diagnosis) are unaffected and remain as described.

## Build and verification

The package reuses an already-built Mathlib (8312 `.olean` files) through a directory junction
to `../fermats-last-theorem/.lake/packages/mathlib`.  On Windows, Lake does not resolve the
transitive package paths (batteries, aesop, ...) through that junction, so `lake build` cannot
be used directly; use the checked-in build driver, which passes an explicit `LEAN_PATH` and
compiles each module with `lean` (~1 s per module), writing `.olean` files under `build/`:

```
powershell -NoProfile -File tools/build.ps1 Definitions/MMBasic.lean Definitions/MMModular.lean Definitions/MMMoonshine.lean Definitions/MMCoxeter.lean Challenge.lean FinalCheck.lean
```

All six modules compile with exit code 0 and no diagnostics.  `FinalCheck.lean` carries
`#guard_msgs` checks, and `lean` fails if the printed axiom sets differ from the expected
ones, so a passing build *is* the axiom verification:

```
#print axioms MM.moonshine_conjecture
-- 'MM.moonshine_conjecture' depends on axioms: [propext, Classical.choice, Quot.sound]
```

## Documentation map

| file | role |
| --- | --- |
| `README.md` | **this file**: the project description, what is proved and what is assumed, the `sorry` map, and the index of everything else |
| `AGENTS.md` | conventions for any agent (human or LLM) working here: ground rules (incl. the per-batch `sorry` policy), traps, build and verification, git, sources |
| `ROADMAP.md` | the **plan**: front matter = index + project status (the four assumed inputs, the FLM campaign's frontier); Part II = the branches (streams S/T/M/A, the long campaign, the FLM campaign) with one entry per task.  No batch narratives here |
| `NOTES.md` | the **work log**: what each batch did and taught --- topic-wise sections, and Appendix A with the dispatcher's per-batch records (batches 151--229) |
| `HANDOVER.md` | the **handover manual** for the long-running FLM Theorem 8.10.2 campaign: delivery and hypotheses, the exact remaining formulas, the blacklist, the module map, next steps, and the build discipline |
| `refs/FLM-CH8-MAP.md` | the book map: every numbered item of FLM Chapter 8 with its page, dependencies and landed status (`refs/` holds the auxiliary evidence: the book map, the FLT asset surveys, `refs/README.md`) |
| `FinalCheck.lean` | the build gate: imports every module and guards the axiom footprint of every declarative claim (proved = the three standard axioms; a registered `sorry` shows `sorryAx`) |

## What is in the repository

| Module | Contents | `sorry` |
| --- | --- | :---: |
| `Definitions/MMBasic.lean` | `MM.GradedModule`: a `ℤ`-graded complex vector space with finite dimensional homogeneous pieces, an action of a monoid by graded linear maps, and integral traces `c_g(n) = Tr(g\|V_n)`; `MM.thompsonSeries`, the Thompson series `T_g(q) = ∑_n c_g(n)qⁿ` as a formal Laurent series with finite support; `thompsonCoeff_one` (`T_1` is the graded dimension). | 0 |
| `Definitions/MMModular.lean` | The orbit projection `MM.orbitMk` (`orbitMk_eq_iff`, `orbitMk_surjective`) and the predicates `MM.HasGenusZero`, `MM.IsHauptmodul`, `MM.IsModularFunction`, `MM.HasQExpansion`; a Hauptmodul is invariant, modular, separates orbits (a bijection `ℍ/Γ → ℂ`), and the normalized one is **unique** (`IsNormalizedHauptmodul.eq_of_qExpansion`, the step section 9 needs). **Caveats, proved and not repaired**: `IsHauptmodul` holds for *every* `Γ`; the earlier **unsatisfiable** shape is kept as a checked theorem (`IsHauptmodulOldShape`, `not_isHauptmodul_old_shape`); `MM.HasGenusZero` is **only a cardinality condition** (`Nonempty (ℍ/Γ ≃ ℂ)`, satisfied by `Γ₀(11)`) and **must be replaced, not repaired** (defect block; `ROADMAP.md` M0). | 0 |
| `Definitions/MMMoonshine.lean` | `MM.IsReplicable` (the paper's (8.3) in coefficient form) and the structure `MM.MoonshineModule` — the FLM module with graded character `j - 744`, (8.3) and the Conway--Norton table as fields (genus conjunct `MM.IsGenusZeroGroup` since D0-g); plus `MM.MoonshineModule.IsMonsterModule` and Theorem 1.1 in three spellings, `…Monster` being **the type of the standing `sorry`** since S4b, with monster ⟹ genus ⟹ pre-repair proved. | 1 |
| `Definitions/MMCoxeter.lean` | The diagram `Y₄₄₃` as `MM.Y443Vertex` (a `torso` plus arms `4, 4, 3` — **12 nodes**), its 11 bonds, the matrix `MM.Y443Matrix` (`1`/`3`/`2`), the non-vacuous count `MM.Y443Matrix_multiset` (144 entries = `replicate 12 1 + replicate 22 3 + replicate 110 2`), the group `MM.Y443` and the seven spider generators. Provenance: Lean 3 `formalabstracts`'s `matrix_of_graph (coxeter_edges [4,4,3])`, which **discards the annotations** — all bonds are `3` and `[4,4,3]` only fixes arm lengths. **Not yet wired to the monster**; `ROADMAP.md` S2. | 0 |
| `Definitions/MMMonster.lean` | The Fischer--Griess monster by presentation: `MM.Y443Quotient` (`Y443` modulo the normal closure of the spider generators) and `MM.Monster := Y443Quotient ⧸ Subgroup.center`, with `MM.Monster_eq` proving by `rfl` that this is *definitionally* the reference quotient. **A definition, not a theorem**: that the presentation presents `M × C₂` is Norton--Ivanov 1990 (`refs/README.md`), not formalized. Non-triviality, finiteness and the order are open (task S3); the abelianisation cannot settle non-triviality because the monster is perfect. | 0 |
| `Definitions/MMMonsterOrder.lean` | **What finiteness and the order of `MM.Monster` need (task S3-D):** `MM.Y443QuotientFinite` is a normal-form certificate with `2·\|M\| ≈ 1.6 × 10^54` entries, and `MM.NortonIvanovPresentation` **transports** the order question without answering it — both sides may be infinite, so it carries no finiteness (a correction to the task's brief, recorded in the file). Proved: `card_monster_eq_monsterCenter_index`, `card_monsterCenter_eq_two_of_nortonIvanov` (the centre **is** the `C₂`), and `MM.monsterOrder` (the **54-digit** numeral) with `MM.monsterOrder_ne_wrongLiteral`, refuting in Lean the 51-digit literal of an earlier brief. **No finiteness, no order and no non-triviality of `MM.Monster` is claimed**: the order is a third, independent input. 244 lines. | 0 |
| `Definitions/MMPowerSeries.lean` | The algebra of (8.3)/(9.1): `MM.ThompsonCoeffFamily`/`MM.FiniteSupportCoeff`, the monomials and truncations, `MM.EulerSeries` and its formal logarithm `MM.adamsLog`. `MM.AdamsLogIsLog` (the Möbius-inversion step, task **T2**) is **not the paper's identity**: `MMLogCoeff.lean` proves it **false** in general (`MM.not_adamsLogIsLog`), because (8.3) has a **two-sided** `q`-side that `MM.EulerSeries` does not provide — restate it, do not quote it as a target. `MM.expOp_logOf` (task **T1b**, `∘` = substitution) is a `Prop` here, **proved** as `MM.expOp_logOf_eq` in `MMExpLog.lean`. | 0 |
| `Definitions/ZZCond.lean` | The parity arithmetic behind the half-integral coset of `E8`, proved for `ℤ` with explicit witnesses (Mathlib does not give `ℤ` the `Even.add` / `Odd.mul` names of the `Nat` instances): `even_add`, `odd_add`, `even_add_odd`, `odd_mul`, `even_tail`, `sum_eq_pair_add_tail`, `even_sum_iff_even_pair`, and the two directions `even_sufficient` / the necessity half, which together show that `Even (Σ yᵢ)` — and **not** `4 ∣ Σ yᵢ` — is the correct condition for `⟨z/2, y⟩ ∈ ℤ` for every `y ∈ D8`. | 0 |
| `vendor/vertexAlg/` | **A vendored axiom layer for vertex algebras, with no models.** `class VertexAlgebra`/`VertexAlgebra1` (the Borcherds identity), with the equivalences between Borcherds-at-zero, associativity, the commutator formula and weak associativity **proved**, plus a hom/subalgebra API; vendored at commit `bd8adbb` (its Mathlib pin is **our pin's direct child**; 35/35 modules compile, no API delta). **What it is not**: the **locality half of the equivalence is not proved** (those theorems sit in comment blocks with `sorry` bodies), and **no instance of either class exists anywhere** — upstream's `Affine.lean`, `Lattice.lean`, `ChevalleyEilenberg.lean`, `Lie/Basic.lean` are 100 % doc-comment. | 0 |
| `vendor/virasoro/` | **The Virasoro/Heisenberg/Fock/Sugawara layer at `c = 1`** (29/29 modules here), from `kkytola/VirasoroProject` branch `bump-202606` commit `e3e08a3b`, Apache-2.0: the Witt algebra and bracket, the Virasoro 2-cocycle, `H²(Witt)` one-dimensionality, the Heisenberg algebra, Fock and charged Fock spaces, and the bosonic **Sugawara construction**. **What it is not**: no `TensorProduct`, no coalgebra, no lattice/VOA machinery, nothing moonshine — and `c = 1` where moonshine needs `c = 24`, pinned by the no-ghost hypotheses with the Lorentzian rank the only freedom (`c ∈ {24,16,8,0}`). It also supplies `Gamma0GL N`, **the first definition of `Γ₀(N)` here** (previously prose only), with `periodic_of_invariant_Gamma0GL`. See `vendor/virasoro/README.md`. | 0 |
| `Definitions/MMGolay.lean` | **The extended binary Golay code** from `[I₁₂ \| B]`: `4096` words, doubly even, minimum weight `8`, weight enumerator `1, 759, 2576, 759, 1`, self-dual (`G.rank = 12`, `golayCode = dualCode`); the combinatorial input to the Leech construction `Λ = 2^{-3/2}·A`. **The sharp divisibility is `4 ∣ wt`, not `8 ∣ wt`**: `2576` words of weight `12`, so triple-evenness is false (a claim in the task brief, refuted by the proof and recorded). **The twelve generator masks' provenance is not formalized** (literals from the length-23 QR code plus a parity bit); re-proved: they generate a `[24,12,8]` doubly-even self-dual code matching the parity-block enumeration on all `4096` messages. 746 lines, 58 theorems, ~3 m 25 s to build. | 0 |
| `Definitions/MMLeech.lean` | **The Leech carrier, its structure theorem and its index** (M2a/M2b/M3/M3b): `MM.IsLeechVec a` is Conway--Sloane's condition on `a : ℤ²⁴` (same parity, `Σa ≡ 4a₀ mod 8`, each mod-4 class word Golay), which `MM.isLeechVec_iff` splits into `2·lift d + 4t` with `Σt` **even** and `1 + 2·lift d + 4t` with `Σt` **odd**. **M3b proved**: `MM.leech_index : [ℤ²⁴ : A] = 2³⁶`, from the parametrisation `key d τ = Στ + 2·lift d + 4τ` of a class mod `8ℤ²⁴` (`4096 · 2²⁴ = 2³⁶` classes), agreeing with `Probe/leech_verify.py`. **Not claimed**: the parity conditions on `Σt` are *forced by* the mod-8 congruence and contradict the reconnaissance's recorded shape (`x₀ + 2(d+2t)` with `Σt` even is never in `A`). Split into `MMLeech.lean` (1018 lines) and `MMLeechIndex.lean` (457 lines); no `decide +kernel`, ~3 s each. | 0 |
| `Definitions/MMLeechForm.lean` | **The integral structure on the Leech carrier** (M4a/M4b): `MM.leech_sum_mul_dvd : 8 ∣ ∑ aⱼbⱼ`, `MM.leech_sq_dvd`, and `MM.normSq_spec : 8 * normSq a = ∑ aⱼ²`, so the form `(x,y) = (Σxᵢyᵢ)/8` is integral on `A`. **What the proof needs** is that Golay is doubly even **and closed under addition**; **M3's parity correction is load-bearing** — `4·ca·S` and `4·cb·T` are each `4 mod 8` in the odd branch and cancel only via the parity conditions, so integrality independently confirms the corrected M3 shape. Also `4eᵢ ∉ A`. 301 lines, ~2 s. | 0 |
| `Definitions/MMLeechMinNorm.lean` | **The Leech lattice is rootless** (M6, the crux): `MM.leech_min_norm : IsLeechVec a → a ≠ 0 → 32 ≤ ∑ aⱼ²`, with the minimiser `x₀ − 4eⱼ` (`−3` in one coordinate, `+1` elsewhere); so `Λ` has **no vector of norm 1 or 2** and minimum norm `4`, the arithmetic that forces the moonshine module to use a rootless lattice (`j − 744` has `c(0) = 0`; the weight-1 space of `V_Λ` is `24 + #{λ : λ² = 2}`). **The odd branch is two lines**: with `b = d + 2t` and `Z := Σⱼ(tⱼ+dⱼ)(1+2tⱼ)`, `Σbⱼ + b·b = 2Z`, `Z ≥ 0` pointwise for every integer `tⱼ` (the factors share a sign) and `Z` odd — superseding the reconnaissance's case split and the dispatcher's replacement. **Not claimed**: `16 ∣ ∑ aⱼ²` (`Λ` even), reserved for M8. 455 lines, no `decide +kernel`. | 0 |
| `Definitions/MMLeechEven.lean` | **`Λ` is an even lattice**: `MM.leech_sq_dvd_sixteen : 16 ∣ ∑ aⱼ²` and `MM.two_dvd_normSq`, so every norm is an **even** integer. **Evenness follows from M3's parity correction, not from Golay alone**: the even branch needs only `4 ∣ wt d`, 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₀`, `normSq = 3`). Third confirmation of the corrected M3 shape, after M4's integrality and M6's minimum. 215 lines, 1.6 s. | 0 |
| `Definitions/MMLeechUnimodular.lean` | **`Λ` is unimodular** (M5): `MM.isLeechVec_iff_eight_dvd` and `MM.leech_dual_eq_eighth`, i.e. `A* = (1/8)A` — literally `Λ* = Λ` under the scaling `x = y/√8`. **The unscaled statement `A* = A` is FALSE**: `x = x₀/4` pairs integrally against every `a ∈ A` (since `Σⱼ aⱼ ∈ 4ℤ`, being `0` or `4` mod `8`) yet `x ∉ A`, so the scaling is load-bearing, as `1/√8` was for `A` itself. The odd generator used is `x₀ − 4e₀`, **not** `x₀` (`24 ≢ 4 mod 8`). 546 lines, 2.8 s. | 0 |
| `Definitions/MMLeechKissing.lean` | **The kissing number of the Leech lattice** (M7, 1373 lines): `MM.leech_kissing_number : {a \| IsLeechVec a ∧ ∑ aⱼ² = 32}.ncard = 196560`, with `MM.leech_min_iff_shape` classifying the minimal vectors and the three family counts `1104`, `97152`, `98304`. **The `2⁷` of the `(2⁸)` family is M3's parity condition, not subset counting** — `Even (Σt)` says `\|u\|` is even, and an 8-set has `2⁷` even subsets: the fourth place M3's parity correction is load-bearing. The odd family's parity hypothesis is **automatic** (`Σt = −wt d + 2d_{j₀} − 1`), so that lemma assumes less than the brief asked. 88 declarations, no enumeration. | 0 |
| `Definitions/MMLevelOneHauptmodul.lean` | **Level one, the paper's own worked example** (M1's first increment): for `MM.levelOneGamma := 𝒮ℒ` and `MM.levelOneJ := E₄³/Δ`, **invariance** (`levelOneJ_invariant`) and **surjectivity** (`levelOneJ_surjective`, inherited from the sibling repo's `WLight.j_surjective`) are proved and `q⁻¹ + 744 + 196884q + ⋯` matches `IsNormalizedSeries`; **the cusp conjunct is now a theorem** (`levelOneJ_cusp_expansion`). **The third conjunct, orbit separation, is NOT obtained**: it is the explicit hypothesis `MM.LevelOneOrbitSeparation`, the level-one **order-1 valence statement**, in neither Mathlib nor the sibling repo. **Nothing here shows `SL₂(ℤ)` has genus zero.** | 0 |
| `Definitions/MMLevelOneDiscUnit.lean` | **The unit part of `Δ` at the cusp, and `Δ = q − 24q² + ⋯`** (task M1-L1c, first half): Mathlib's `discriminant_eq_q_prod` gives `Δ = 𝕢·P` with `MM.levelOneDiscTprod := ∏' n, (1 − eta_q n)^24`, and `MM.qExpansion_levelOneDiscTprod` identifies that unit part with the unit of `qExpansion 1 Δ` — the proof needs `MM.qExpansion_qParam_one` (that `q` **is** the local parameter) and goes through `Filter.EventuallyEq.iteratedDeriv`, as `cuspFunction 1 (𝕢 1 ·)` is only *eventually* `id`. The missing coefficient is `levelOneDiscUnit.coeff 1 = −24`, equivalently `(qExpansion 1 Δ).coeff 2 = −24`, from `discriminant_eq_E₄_cube_sub_E₆_sq` plus `E_qExpansion_coeff` (`E₄ = 1 + 240q + 2160q²`, `E₆ = 1 − 504q − 16632q²`). 229 lines; `PowerSeries.inv` of `qExpansion 1 Δ` is never formed (it is `0`). | 0 |
| `Definitions/MMLevelOneCusp.lean` | **The cusp expansion `j = q⁻¹ + 744 + O(q)`, as a theorem** (task M1-L1c, second half: it discharges the hypothesis `hz` of the level-one conditional theorems), via `MM.isBoundedAtImInfty_div_qParam_pow` (the first `n` coefficients vanish ⟹ `f/𝕢ⁿ` bounded at `i∞`; **not** via `HasFPowerSeriesAt`) and `𝕢/P → 0`, giving `MM.levelOneJ_cusp_expansion : IsZeroAtImInfty ((j − 744) − q⁻¹)`. **`HasQExpansion` is NOT obtained *here* and NOT weakened**: unwound it is exactly the **integrality** of the coefficients of `j − 744 − q⁻¹` (`196884, 21493760, …`), and the missing step it records is now `MM.qExpansion_levelOneDiscTprod_eq_formal` (`MMLevelOneDiscProduct.lean`, M1-L1f), with `hq` proved in `MMLevelOneHq.lean` (M1-L1h); this file is deliberately untouched, so its theorems still carry `hq`. 285 lines. | 0 |
| `Definitions/MMLevelTwo.lean` | The level-2 half of the paper's section 11: `E8` as `D8` plus the half-integral coset, `MM.E8.IsLattice`, `MM.E8.normSq` (`8 ∣ Σ yᵢ²` is what makes the division by `4` integral), the pruned enumerator `box`/`boxAux`, and `MM.thetaCoeff n`. The four values `1`, `240`, `2160`, `6720` are **stated correctly**; the `4` in this row's count column is the task-D-d state (proved by `sorry`, kernel enumeration cost), and task M-form then discharged all of them from modular forms — the file now reads `sorry=0` and the three statements are corollaries (see the `sorry` map). | 4 |
| `Definitions/MMQBinomial.lean` | **Euler's q-binomial theorem, PROVED (batch 3, task JTP run 1).** `MM.qPoch` is `(q;q)_n` over `PowerSeries ℤ`; `MM.zProd M = ∏_{j≤M}(1 + z q^j)`, `MM.zErr n M = (q;q)_n · zCoeff n M − q^{n(n−1)/2}`; the theorem `MM.euler_qbinomial` is the **coefficientwise stabilisation** (`∃ M0, ∀ M ≥ M0, zErr n M = 0`), with `MM.euler_qbinomial_tendsto` its `X`-adic form and the checks `MM.euler_qbinomial_one_coeff`, `MM.euler_qbinomial_two_coeff_one`. `MM.tri n = n.choose 2`. 294 lines. | 0 |
| `Definitions/MMJacobiTripleProduct.lean` | **The Jacobi triple product as a TARGET, with its proved fragments (batch 3, JTP run 1) — the identity itself was NOT proved here.** `MM.JacobiTripleProductStatement` and `MM.GaussDurfeeStatement` are `Prop`s whose docstrings say in capitals that they are **not** proved and why (pentagonal is a *specialisation*; the missing input is Gauss/Durfee); proved are `MM.jtpProd_succ`, `MM.jtpProd_coeff_zero` and `MM.euler_qbinomial_shifted`. **Correction of the brief, in the header: the correct exponent is `k(k+1)/2`; `k(k−1)/2` is the same identity under `z ↦ z/q`.** 343 lines. **Superseded:** proved in batch 6 (`MMJacobiTripleProductMain.lean`). | 0 |
| `Definitions/MMHeisenbergFockBasic.lean` | **The Heisenberg Fock space, its grading and its vacuum — the first stone of the FLM construction (batch 3, task FOCK run 1)**: `MM.Heisenberg.Mode n = Fin n × ℕ+`, `FockSpace = SymmetricAlgebra R (Mode n →₀ R)`, `vacuum = 1`, `GradedPart n N`; every graded piece is **finite**, the vacuum lies in weight `0`, and **`F_0 = R·\|0⟩`**. 263 lines. **The oscillator operators are deliberately NOT here:** `MMHeisenbergFock.lean` is parked on branch `task/fock-i` because its `annihilate` came out an algebra homomorphism rather than a derivation — a defect the agent found and reported itself — so `MM.Osc.canonicalCommutationRelation` is **false** for that operator. | 0 |
| `Definitions/MMHeisenbergOscillator.lean` + `MMHeisenbergOscillatorComm.lean` | **Run 2 of the Fock program: the oscillator operators built correctly, with the FULL Heisenberg commutation relations (batch 4).** Annihilation is a genuine **`Derivation`** (`MM.Heisenberg.deriv`), fixing run 1's defect; creation raises the weight, annihilation lowers it. All three cases: `annihilate_comp_annihilate` (`[a_e,a_f] = 0`), `create_comp_create`, `annihilate_comp_create` (`a_e·a_{−f} = a_{−f}·a_e + δ_ef·m·id`), with `ccr_ring`. **Correction of record:** run 1's claim that `SymmetricAlgebra.equivMvPolynomial` needs a finite index type is **false** — it takes an arbitrary basis, which is what made this work; `dim F_N = p(N)` holds only at rank 1 (rank `n` gives `∏(1−q^m)^{−n}`). **Not proved:** the graded character (missing: a bijection `WeightVec 1 N ≃ Nat.Partition N`). 270 + 229 lines. | 0 |
| `Definitions/MMGaussBinom.lean` | **The Gaussian binomial machinery for the finite triple product (batch 4, task JTP run 2).** `MM.qbin` with the inversion normalisation, division-free over `ℤ`, with `MM.qbin_pascal`, `MM.qbin_symm`, the recurrence `MM.qbin_step` (and its `k = 0` case), and the limits `MM.qbin_limit` / `MM.qbin_limit_coeff` (the only step that uses `PowerSeries.isUnit_iff_constantCoeff`). 586 lines, complete. | 0 |
| `Definitions/MMJacobiTripleProductProof.lean` | **The triple product's recurrence — run 2's partial result (batch 4); `MM.jtpC_main` is NOT proved here.** Proved: `MM.jtpC_succ` (the recurrence), `MM.jtpC_zero` (base case), `MM.jtpC_symm`. **Where it stopped, verbatim from the file:** the base case `M = 1` is defeated by the `↑k : ℤ` coercions inside `jtpC_zero`'s `if`-conditions ("Did not find an occurrence of the pattern"), and the inductive step is one `ring` identity after `qbin_step`; the agent removed the unfinished proof rather than leave a marker, and there is no `sorry`. 344 lines. **Superseded:** `MM.jtpC_main` is proved in batch 6 (`MMJacobiTripleProductMain.lean`). | 0 |
| `Definitions/MMLevelOneOrbitSeparation.lean` | **`MM.LevelOneOrbitSeparation` reduced to equivalent forms — the target itself is NOT proved (batch 5, M1-FLT).** Proved: the quotient map `MM.levelOneJQuotient : ℍ/𝒮ℒ → ℂ` induced by `j`, and the chain `_iff_injective`/`_iff_bijective`/`_iff_isHauptmodul`/`_iff_analyticNormalized`/`_iff_fd` — injectivity on the **closed** fundamental domain `ModularGroup.fd` suffices. **The open-domain form is NOT equivalent** (counterexample recorded: `ρ` and `ρ − 1 = T⁻¹•ρ` lie in `𝒟∖𝒟ᵒ` with equal j-values), correcting `Probe/ORBIT_SEPARATION_RECON.md` §4. The owner-directed FLT route is blocked by three Mathlib-drift compile errors inside `../fermats-last-theorem` (file:line in `ROADMAP.md`'s BATCH 5 block), not by mathematics. 265 lines. | 0 |
| `Definitions/MMJacobiTripleProductMain.lean` | **THE JACOBI TRIPLE PRODUCT, PROVED (batch 6, JTP run 3):** `MM.jtpC_main` — the induction runs 1 and 2 could not close — with **`MM.jacobiTripleProduct : MM.JacobiTripleProductStatement`** inhabiting run 1's `Prop` verbatim, the coefficient corollaries `jtp_coeff_one_one` … `jtp_coeff_zero_one`, and `MM.jtpProd_coeff_stable` (the bound `d + 1 ≤ M` is not a restriction). **This is the eta-theta bridge**: the obstruction that stopped Lemma 11.1 (task A1b) is gone. Run 3's corrections of run 2's notes: the `j = 0` step is *not* the blocker (`jtpC_symm`), the induction must be stated for all `j` (or needs boundary cases at `j = M, M+1`), and the coefficient identity is genuinely false without `d + 1 ≤ M`. 486 lines, 21 declarations, no `sorry`. | 0 |
| `Definitions/MMLevelOneOrbitSeparationProof.lean` | **The level-one affine/valence reduction, and the sibling project's asset re-exported (batch 6, M1-FLT-2); `MM.LevelOneOrbitSeparation` is still NOT proved.** Proved: `MM.levelOne_affine_of_bounded_mul_discriminant` (the sibling's `levelOne_holFn_eq_polynomial_j` at `m = 1`: level-one functions with at most a simple pole at the cusp are exactly `a·j + b`), `MM.LevelOneValenceInput` with `levelOneOrbitSeparation_iff_valenceInput`, `MM.exists_two_fd_fibre_points_of_not_orbitSeparation`, and `MM.flt_levelOne_isPrincipal_of_degree_eq_zero_charLOne` — the **first MM theorem resting on a repaired `fermats-last-theorem` module**. Remaining gaps, named in the header: (B1) the `ComplexPlaceDictionary` `pt` (167 modules) / `pt_eq_pt_iff` (345 modules, ≈35–40 min, unblocked but not built), (B2) `Gamma0 1 = ⊤ = 𝒮ℒ`, (B3) the order bridge `(pt τ).ord (jqModC ℂ − jqModC ℂ τ) > 0`. 259 lines. | 0 |
| `Definitions/MMExpLog.lean` | Task **T1b, proved**: `exp ∘ logOf f = f` for `constantCoeff f = 1` (with `∘` read as substitution, see the `MM.expOp` docstring) is `MM.expOp_logOf_eq`, resting on the uniqueness lemma `MM.eq_zero_of_derivative_eq_mul`. Also here: `MM.expOp_logOf_holds` (the `Prop` of `MMPowerSeries.lean` is inhabited), `MM.seriesIdentity_of_adamsLogIsLog` (the paper's identity with T1b discharged, so only T2 and a constant-term hypothesis remain), `MM.instIsAddTorsionFreeHahnSeries` (not synthesizable; the cancellation of `n + 1` needs it), `MM.deriv_log_eq_inv`. Its docstrings record why the substitution route of an earlier `ROADMAP.md` revision is **circular** rather than bookkeeping — the identity it needed, `subst (log A) (exp A) = 1 + X`, is the statement to be proved. | 0 |
| `Definitions/MMLogCoeff.lean` | **The T2 pre-work: `coeff_logOf`, and the refutation of `MM.AdamsLogIsLog`.** Mathlib has no coefficient formula for `logOf`, so **`MM.coeff_logOf`** supplies one (`(logOf f).coeff n = Σ_{d ∈ Icc 1 n} ((-1)^{d+1}/d)·((f−1)^d).coeff n` when `constantCoeff f = 1`), and **`MM.adamsLogIsLog_iff`** reduces the `Prop` to a per-degree equality (divisor sum versus alternating sum of powers); **`MM.not_adamsLogIsLog` refutes it** at the coefficient of `p²`, by a counterexample (trivial group, `c(1) = 1`, `bound = 1`) satisfying `FiniteSupportCoeff`. **Scope, stated in the file:** that counterexample is **not** `MM.IsReplicable`, so whether replicability implies the `Prop` is *not* settled, and on the primary source (`../mm_text.txt`, section 8) the shape is not refuted either — (8.3)'s right-hand side is **two-sided in `q`** (`−p·q⁻¹`), while `MM.EulerSeries` keeps positive `q`-powers only and adds an `m = 0` term. So T2's first requirement is the two-sided `q`-expansion whose absence task D0 records, not a hypothesis on `c`. 354 lines. | 0 |
| `Definitions/MMQExpansionTwoSided.lean` | **The two-sided `q`-expansion — task D0's repair, in the form (8.3) needs.** `MM.HasQExpansion` cannot see negative degrees (`MM.not_determined_by_one_sided`), so the `q⁻¹` term of a normalized series was invisible; **`MM.HasLaurentQExpansion f a`** writes the pole as `f = a.coeff (-1) * qInv + g` with `g` periodic, `MDiff` and bounded. So the series is **determined** by `f` (`MM.HasLaurentQExpansion.eq` — the opposite of the one-sided defect), normalization is a property of `f` (the coefficient is *forced*), and `MM.isNormalizedLaurentSeries_iff` identifies it with `MM.IsNormalizedSeries` on integer coefficients; the analytic input is `MM.not_isBoundedAtImInfty_const_mul_qInv` (from `‖q⁻¹‖ = e^{2π im τ}`). `hasQExpansion_of_map` recovers the old predicate on the bounded part, so this **extends** rather than replaces. 293 lines. | 0 |
| `Definitions/MMQExpansionTwoSidedLevelOne.lean` | **The level-one instance of the repaired predicate**: `MM.levelOneJ_sub_hasLaurentQExpansion : HasLaurentQExpansion (levelOneJ - 744) MM.levelOneLaurentSeries`, with `coeff (-1) = 1`, `coeff 0 = 0` — the classical `j - 744 = q⁻¹ + 0 + 196884q + ⋯` with the pole term tied to the function (it rests on `MM.levelOneJ_cusp_expansion`) — plus the reusable `MM.mdifferentiable_levelOneJ`, `MM.periodic_levelOneJ`. **The coefficients are complex numbers: integrality is a separate gap** *here* and is not claimed; the classical `196884` is read off, not computed. 178 lines. **Superseded in part (D0-iii):** integrality is now `MM.levelOneLaurentSeries_eq_map_levelOneA` (`MMLevelOneLaurentIntegral.lean`); this file's own text still describes the gap as open because the dispatcher does not rewrite accepted files to trail later work. | 0 |
| `Definitions/MMLevelOneLaurentIntegral.lean` | **Task D0-iii (a): the level-one two-sided `q`-expansion is INTEGRAL.** `MM.levelOneLaurentSeries_eq_map_levelOneA : MM.levelOneLaurentSeries = MM.levelOneA.map (Int.castRingHom ℂ)` — the complex expansion of `j - 744` **is** the image of the integral series, coefficientwise (`q⁻¹` both `1`, below `q⁻¹` both zero, nonnegative degrees via `MM.qExpansion_levelOneCuspBounded` against `MM.levelOneA_coeff_nat`); `MM.hasLaurentQExpansion_eq_map_levelOneA` upgrades a witness to a **forced** value by `MM.HasLaurentQExpansion.eq`, and `levelOneLaurentSeries_coeff_one`/`_two` are the classical `196884`, `21493760` (`q⁰ = 0` being the FLM fact `V_0 = 0`). Nothing about the Jacobi product is reproved: the whole input is `MM.levelOneA_hasQExpansion`. 166 lines, no `decide`, no enumeration. | 0 |
| `Definitions/MMHauptmodulTwoSided.lean` | **Task D0-iii (b): the `hauptmodul` predicate and the two-sided predicate are EQUIVALENT**, so the pending rewiring of `MM.MoonshineModule`'s field is a change of spelling: `MM.IsAnalyticNormalizedHauptmodul.toHasLaurentQExpansion` (taking periodicity and holomorphy of `f` — two hypotheses the predicate itself does not carry) and `MM.HasLaurentQExpansion.toIsAnalyticNormalizedHauptmodul` (taking `IsHauptmodul Γ f`, the normalization, and `b.coeff 0 = 0`, which `MM.IsNormalizedSeries` does **not** pin — without it the expansion only bounds `f - qInv` at the cusp instead of making it vanish there). The constant-term and analytic conditions are interchangeable here; assembled as `MM.isAnalyticNormalizedHauptmodul_iff_hasLaurentQExpansion` and `…_and_cusp`. 288 lines. | 0 |
| `Definitions/MMGenusZeroStatement.lean` | **The genus-zero hypothesis, stated non-vacuously (D0-e; a dispatcher decision).** `MM.HasGenusZero Γ` is `Nonempty (ℍ/Γ ≃ ℂ)` — **cardinality**, true for `⊥` — so the conjecture as phrased did not require `Γ` to have genus zero, exactly the Conway--Norton input; **`MM.IsGenusZeroGroup Γ`** keeps that conjunct and adds the **compactness** input `MM.HasBoundedInvariantConst Γ` and an analytic Hauptmodul with a pole at the cusp, and `MM.moonshineConjectureStatement_of_genus` reduces the genus form (`…StatementGenus`) to the current statement, so nothing is lost. **Both directions are proved**: `MM.hasGenusZero_bot` (with `ℍ/⊥ ≃ ℍ ≃ ℝ × ℝ`) versus `MM.not_hasBoundedInvariantConst_bot` (witness `τ ↦ 𝕢 1 τ`), and symmetrically `hasBoundedInvariantConst_top` / `not_hasGenusZero_top`. **Not claimed:** no inhabitant of the new predicate is proved here, and `MM.MoonshineModule`, `MM.MoonshineModule.MoonshineConjectureStatement` and `moonshine_conjecture` are **deliberately untouched**. 272 lines. | 0 |
| `Definitions/MMGenusZeroGroup.lean` | **The honest genus-zero predicate, upstream of the headline** (task D0-g moved it here from `MMGenusZeroStatement.lean`, breaking an import cycle so that `MM.MoonshineModule`'s field can use it). `MM.IsGenusZeroGroup Γ` and its projections: `hasGenusZero`, `hasBoundedInvariantConst`, `exists_hauptmodulAnalytic`, `exists_surjective`, `toHasGenusZeroFun`, `exists_isHauptmodul_of_orbitSeparation`. Imports only `MMGenusZeroRefute` and `MMHauptmodulAnalytic`. 141 lines. | 0 |
| `Definitions/MMDenominatorIdentity.lean` | **The paper's (8.3), faithfully stated (task T2-ii), and its coefficient reduction.** `PowerSeries` has no negative `p`-exponents, so it is stated multiplied through as `MM.DenominatorIdentity c hc g bound : expOp (−(adamsLogTwoSided c g bound)) = moonshineRHS c hc g`. **Both reformulations are forced and recorded:** the `p⁻¹` becomes content at `p⁰`, and the `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` — why the earlier one-sided `MM.AdamsLogIsLog` was the wrong target. Proved: `MM.DenominatorIdentity.iff_coeff` (identity ↔ explicit per-degree equalities), **`coeff_zero` derives the normalization `c(g,-1) = 1`**, **`coeff_one` derives `c(g,0) = 0`** (the FLM fact `V_0 = 0`). **Not proved:** `DenominatorIdentity` itself (paper §6--8 — that is what T2 now is); the `p²`/`p⁴` comparisons are the recursion (9.1) = T3; the Möbius inversion (10.4) is a *definition* of `mult`, not a coefficient of (8.3). 374 lines. | 0 |
| `Definitions/MMRootMultiplicity.lean` + `MMRootMultiplicityArith.lean` | **Section 10 counted as done: the Möbius inversion (10.3) ⇒ (10.4), proved** (task T2a). `MM.moebiusSum_adamsSum : 0 < k → moebiusSum (adamsSum B) k = B k` holds for `B : ℕ → R` with `R` a `ℚ`-algebra and **no hypothesis on `B`**, so the paper's `mult(m,n) = Σ_{ds \| (m,n)} (μ(s)/(ds))·Tr(g^d\|V_{mn/d²s²})` follows; the old target `MM.moebiusSum_adamsSum_holds` keeps its name as a **theorem of the same statement** (the earlier version left the `Prop` unproved, so nothing could be built on it). **No series occurs** in either file, so nothing here is a claim about `MM.adamsLog`, `MM.EulerSeries` or `MM.DenominatorIdentity`; the (10.4) ⇒ (10.5) step is proved too (`MM.moebiusBlock_eq_zero_of_not_dvd` is the paper's *"the sum `Σ_{ds=k} μ(s)f(d)` is 0 unless `k \| N`"*). **Note the subscript**: the paper **defines** `(m,n)` as `gcd(m,n)` (after (2.3)) — mis-reading it as `ds \| m` produced the wrong `mult(2,1)` expectation of an earlier brief. 261 + 201 lines, no `sorry`, six `#print axioms` guards each exactly `[propext, Classical.choice, Quot.sound]`. | 0 |
| `Definitions/MMMonsterMoonshine.lean` | **The headline can name the monster (task S4)**: `MM.MoonshineModule.IsMonsterModule M := Nonempty (M.G ≃* MM.Monster)` — until this existed nothing tied the abstract group `M.G` to the Fischer--Griess group. **`MM.MoonshineModule.reindex` transports a whole `MoonshineModule` along a group isomorphism** (graded pieces, traces, `charCoeff_spec` through `map_one`, `replication` through `map_pow` — replicability is isomorphism-invariant), so `MM.isMonsterModule_reindex` makes `IsMonsterModule` a property of the **isomorphism class**. `…StatementMonster` is the headline in that form, with **proved** reductions to the genus and pre-repair statements and the unpacking `…Monster.exists_module`. **Not bought:** no finiteness, order or non-triviality of `MM.Monster` (task S3), no formalized identification with Griess's group, and the module is still not constructed — `IsMonsterModule` is not even known satisfiable. 207 lines. | 0 |
| `Definitions/MMReplicationRecursion.lean` | **The `p²` comparison of (8.3), the first step of the paper's recursion (9.1)** (task T3): `MM.coeff_expOp_two` (`(expOp f).coeff 2 = f.coeff 2 + ½(f.coeff 1)²` for `constantCoeff f = 0`) and **`MM.DenominatorIdentity.pTwo`**, which equates it with `c(g,1)` — the paper's comparison at `p²` — from which its first and third formulas (`c_g(4k)`, `c_g(4k+2)`) are read off; **both readings are verified numerically** (the first at `k = 1, 2`, the third at `k = 1`, against the true `j`-coefficients; re-checked by the dispatcher). **Everything here is conditional on `MM.DenominatorIdentity`**, which is *not* proved (paper §6--8, task T2). **Not landed, with the blockers named in the header:** the four formulas as statements, and the determination theorem — blocked by (a) the `HahnSeries` convolution extraction over `coeff_mul`'s antidiagonal and (b) explicit truncation hypotheses for `bound`, both bookkeeping rather than mathematics. 145 lines. | 0 |
| `Definitions/MMReplicationFormulas.lean` | **The paper's recursion formulas (9.1) for `c_g(4k)` and `c_g(4k+2)`** (task T3, second step): `MM.DenominatorIdentity.cg_four_mul` / `…cg_four_mul_add_two` are the paper's first and third formulas **verbatim**, at its own ranges and its `k ≥ 1`, read off the `p²` comparison. The hypotheses the paper leaves implicit are **explicit**: the FLM grading `c(g,n) = 0` for `n < −1` (*not* derivable from `MM.FiniteSupportCoeff`; it confines the convolution to the paper's finite ranges), `c(g,0) = 0`, and the truncation bound — while `c(g,-1) = 1` is *derived* from (8.3) by `MM.DenominatorIdentity.coeff_zero`, not assumed. **Everything is conditional on `MM.DenominatorIdentity`** (task T2). **Not landed, with the reason in the header:** the second and fourth formulas (task T3d settled where they come from, and it is **not** the `p⁴` comparison) and the determination theorem, needing a joint induction over `g, g², g⁴, …` because formula 1 determines `c(g,4k)` partly through `c(g²,k)`. 498 lines (over the ~300 convention; the interval machinery dominates). | 0 |
| `Definitions/MMReplicationFormulasOdd.lean` | **The `p⁴` comparison of (8.3), and a correction to the paper's second formula** (task T3c): `MM.coeff_expOp_four` (`f₄ + f₁f₃ + ½f₂² + ½f₁²f₂ + (1/24)f₁⁴`) and **`MM.DenominatorIdentity.pFour`** (`−L₄ + L₁L₃ + ½L₂² − ½L₁²L₂ + (1/24)L₁⁴ = single 0 (c g 3)`), conditional on `MM.DenominatorIdentity`. **The correction, recorded and deliberately NOT applied:** the paper's second formula *as extracted* is false at `k = 1` — the paper says the recursion degenerates there (`c_g(5) = c_g(5)`), but the extracted sign gives `c_g(5) + c_g(2)²`; with `(cg2(2k) − cg(2k)²)/2` in place of the first square term it degenerates exactly and then holds at `k = 2, 3` (author-checked, **independently re-checked by the dispatcher**: extracted `462314921578200` against `c(5) = 333202640600`; corrected gives `c(5)` and `c(9) = 3176440229784420`). **Not stated here, and why:** formulas 2 and 4 themselves — they cannot both come from a coefficient comparison of `exp(−L) = p(T(p) − T(q))`, since the alternating sums `Σ(−1)^j` have no source there and point to the reciprocal/product form. 303 lines. | 0 |
| `Definitions/MMReplicationPThree.lean` | **The `p³` comparison of (8.3), and the settled provenance of all four formulas** (task T3d): `MM.coeff_expOp_three` and **`MM.DenominatorIdentity.pThree`** (`−L₃ + L₁L₂ − (1/6)L₁³ = single 0 (c g 2)`), conditional on `MM.DenominatorIdentity`; the first comparison in which `c(g,4k+1)`/`c(g,4k+3)` occur, and it settled where the paper's `p⁻¹` shift puts "compare the coefficients of `p²` and `p⁴`" — at this repository's `p²`, `p³`, `p⁴`. **Verdict, computed as an exact polynomial identity in the symbols `c(n)`:** the `p²` comparison at `q^{2k+1}` **is minus** the paper's third formula (verified at `k = 1..4`, so odd `q`-degrees carry no new information); `c(g,4k+1)`/`c(g,4k+3)` **do not appear at all** in the `p²` comparison at `q^{4k+1}`, `q^{4k+3}` (so formulas 2, 4 cannot come from `p²` — why the earlier `p⁴` route failed); they **first appear here**; and no single comparison *is* the formula — at `q⁹` it has 26 monomials against the formula's 11, whose elimination is the paper's "elementary algebra" and the source of the alternating sums (equal to `[q^N](T(q)·T(−q))`, impossible in a raw coefficient of `exp(∓L)`) and of the formula-2 sign correction. All four hold numerically with the corrected sign; the header also **refutes** the guess that formulas 2 and 4 are read off from here. 195 lines. | 0 |
| `Definitions/MMReplicationFormulaTargets.lean` | **The paper's formulas 2 and 4 as `Prop`-valued targets** (task T3e; the `MM.AdamsLogIsLog` pattern — the obligation visible as a declaration, not hidden in a proof): `MM.RecursionFormulaTwo` (sign-corrected), `MM.RecursionFormulaFour`, **not** theorems. **Why not: the derivation does not exist.** As exact polynomials in the symbols `c(g^i,n)` they lie in **no** linear combination of (8.3)'s coefficient relations (residual 7--8 terms for `p`-degree `≤ 6`, `q ∈ [−8,26]`); the same for the reciprocal presentation `exp(L)·p(T(p)−T(q)) = 1` and after adjoining products of relations. **Both natural repairs failed too:** adjoining (8.3) for `g, g², g³, g⁴` (60 → 240 relations) leaves residuals at 19 and 9 terms, and the **replicability** relations (divisor recursion, `k ≤ 6`, `\|P\| ≤ 12`) do not span them. What validates the probes: **formulas 1 and 3 are single relations** (`F1(k) = −R[2][2k]`, `F3(k) = −R[2][2k+1]`), matching T3b's Lean proofs, and the formulas are **true** (checked at `k = 1…5`). So "compare the coefficients of `p²` and `p⁴` of 8.3 and carry out some elementary algebra" is **not reproduced by any route tried**, and the stream is stopped rather than fitted: the extra input yielding formulas 2 and 4 is unidentified. 124 lines. | 0 |
| `Definitions/MME8Theta.lean` | **The three Jacobi theta functions and the `T`-side of the modularity of `½(θ₂⁸+θ₃⁸+θ₄⁸)`** (task M-form, stage 1 — the owner-directed route to the three `thetaCoeff` values **from modular forms**, not by counting). `MM.thetaThree` is Mathlib's `jacobiTheta`; `MM.thetaFour = θ₃(·+1)`; `MM.thetaTwo = e^{πiτ/4}·jacobiTheta₂(τ/2) τ` bridges the library's **two-variable** `jacobiTheta₂` (which is **not** the classical `θ₂` — a naming trap the header records) to `Σ q^{(n+1/2)²/2}`. Proved: the `q`-expansions, `MM.exp_pi_mul_I_mul_sq`, the `T`-shift laws, `thetaTwo_add_one_mul`, and **`MM.thetaCombination_T_invariant`** — the combination is `T`-invariant although no single term is. **The `S`-side's engine is identified in the header** (`jacobiTheta₂_functional_equation`, `TwoVariable.lean:465`, at `z = τ/2`, with `jacobiTheta_S_smul`, `jacobiTheta₂ (1/2) σ = θ₄(σ)`): the first two exist as stated, **the third did not** (stage 2, next row). **No enumeration of lattice points appears anywhere.** 180 lines. | 0 |
| `Definitions/MME8ThetaModular.lean` | **Stage 2 of task M-form: the half-period evaluation, and a correction to the *dispatcher's* brief.** `MM.jacobiTheta₂_half : jacobiTheta₂ (1/2) τ = jacobiTheta (τ + 1)` — `θ₄` is the two-variable theta at `z = 1/2` — proved from the two series (the `n`-th term of `jacobiTheta₂ (1/2) τ` is `(-1)ⁿe^{πin²τ}`, which is `θ₄`'s), with `MM.exp_pi_mul_I_int`. **Why it had to be proved:** the stage-1 report named three library facts as the `S`-side engine; two exist exactly as stated and **the third did not** — there is no lemma in `Mathlib/NumberTheory/ModularForms/JacobiTheta/` evaluating the two-variable theta at `z = 1/2` (the dispatcher re-ran that grep and confirms it). Treating a recorded route as a fact is what `AGENTS.md` warns against; the fix was to make the missing piece a theorem. 76 lines. | 0 |
| `Definitions/MME8ThetaS.lean` | **Stage 2 of task M-form: the `S`-side.** **`MM.thetaTwo_S_smul : θ₂(S•τ) = (-Iτ)^{1/2}·θ₄(τ)`** — the classical `θ₂(-1/τ) = (-iτ)^{1/2}θ₄(τ)` — from Mathlib's two-variable functional equation at `z = 1/2`, with `jacobiTheta₂_neg_left` and a `Complex.cpow_add` cancellation of the two prefactors. **No enumeration, no `decide`, no `MM.box`** (the only such strings in either new file are inside comments). With stage 1's `T`-side, `½(θ₂⁸+θ₃⁸+θ₄⁸)` has both transformation laws; what remains for stage 3 is θ₄'s `S`-law, the `ModularForm 𝒮ℒ 4` assembly, the identification with `E₄` by `levelOne_weight_four_rank_one`, and the two coset bijections to `MM.thetaCoeff`. 81 lines. | 0 |
| `Definitions/MME8ThetaSCombination.lean` | **Stage 2 of task M-form, second partial: the `S`-half of the modularity, weight 4** — `MM.thetaCombination_S_smul : θ₂⁸(S•τ)+θ₃⁸(S•τ)+θ₄⁸(S•τ) = τ⁴·(θ₂⁸+θ₃⁸+θ₄⁸)(τ)` — so with stage 1's `T`-half the combination transforms with weight 4 under **both** generators of `SL₂(ℤ)`; supporting `MM.cpow_half_pow_eight : (z^{1/2})⁸ = z⁴` (no branch hypothesis), `MM.neg_I_mul_pow_four`, `MM.thetaFour_S_smul`. **A second correction to the dispatcher's brief is in the header**: the `θ₄`-law bookkeeping had been written inverted — the law is `θ₄(S•τ) = B·θ₂(τ)`, `B = (-I(S•τ))^{1/2}`, and since `B⁸ = (τ⁴)⁻¹` while the `θ₄`-law carries `B⁻¹`, the actual multiplier's eighth power is `(B⁸)⁻¹ = τ⁴`: same conclusion (weight 4), different accounting, and the `B` form dodges the `cpow` branch. **The convention was settled by reading the source**: Mathlib's slash is `(f ∣[k] γ) τ = f(γ•τ)·denom γ τ^(-k)` with `denom_S : denom S τ = τ`, so the statement **is literally** weight-4 slash-invariance for `S`. 149 lines. | 0 |
| `Definitions/MME8ThetaModularForm.lean` | **Step 4a of task M-form: weight-4 slash-invariance for all of `𝒮ℒ`.** Generator cases `MM.thetaCombination_slash_S`/`_slash_T`, the group identification **`MM.closure_mapGL_generators : Subgroup.closure {mapGL ℝ S, mapGL ℝ T} = 𝒮ℒ`** (from `SpecialLinearGroup.SL2Z_generators` through `MonoidHom.map_closure`), and **`MM.thetaCombination_slash_invariant`** by closure induction. **This is slash-invariance, not yet a `ModularForm`**: what remains is `MDiff` of the three θ's and of the combination, boundedness at the cusp (θ₃, θ₄ → 1, θ₂ → 0), and the `ModularForm 𝒮ℒ 4` assembly (weight-0 template `MM.levelOne_modularForm_of_invariant`), after which `½(θ₂⁸+θ₃⁸+θ₄⁸) = E₄` follows from `levelOne_weight_four_rank_one` + `E_qExpansion_coeff`. No enumeration. 130 lines. | 0 |
| `Definitions/MMLevelOneGenusZero.lean` | **The first inhabitant of `MM.IsGenusZeroGroup`: level one, `Γ = 𝒮ℒ`.** **Compactness** `MM.levelOne_hasBoundedInvariantConst`: `MM.levelOne_modularForm_of_invariant` packages an `𝒮ℒ`-invariant holomorphic function bounded at the cusp as a `ModularForm 𝒮ℒ 0` (`isCusp_SL2Z_iff'` + `IsBoundedAtImInfty.slash`), and `ModularFormClass.levelOne_weight_zero_const` makes it constant. **The pole**: an explicit `ε` bound from `MM.levelOneJ_cusp_expansion` with `MM.norm_qInv : ‖q⁻¹ τ‖ = e^{2π im τ}`. **The analytic Hauptmodul** `MM.levelOne_isHauptmodulAnalytic`, whose third conjunct is a *constancy* argument (an invariant holomorphic bounded inverse would be constant, forcing `j` constant against `levelOneJ_surjective`), deliberately not a differentiability argument since `(0 : ℂ)⁻¹ = 0`. **The cardinality conjunct** is genuine: `Cardinal.mk_le_of_surjective`, and for `≥` the injection `MM.fdAxisEquiv : fdAxis ≃ (1,∞)`, then Schröder--Bernstein. **Not claimed:** nothing about `Γ₀(N)`; orbit separation for `𝒮ℒ` still open; `MM.HasGenusZero` remains a cardinality condition. 320 lines. | 0 |
| `Definitions/MMLevelOneIntegrality.lean` | **The formal Jacobi product over `ℤ` — the first half of the level-one integrality gap** (task M1-L1d): `MM.formalDiscTprod := ∏' n, (1 − X^(n+1))^24`, `MM.multipliable_formalDiscPow` (from `a^24 − 1 = (a−1)·Σ_{i<24} a^i`) and `MM.formalDiscTprod_coeff_isInt`, the integrality `MM.HasQExpansion` consumes. **What is NOT there, and the header says so:** the comparison with `qExpansion 1 levelOneDiscTprod`, splitting into a **formal stabilisation** lemma (route identified, ~40 lines) and the **analytic half** (the expensive part), for which the header names the tool the original footer did not: `TendstoLocallyUniformlyOn.deriv`, iterated by hand since there is no `iteratedDeriv` version, fed by `multipliableLocallyUniformlyOn_eta`. 94 lines. **Superseded in part (M1-L1h):** the comparison is now `MM.qExpansion_levelOneDiscTprod_eq_formal` (`MMLevelOneDiscProduct.lean`) and the `hq` built on it is **proved**; this file's text still describes the gap as open because the dispatcher does not rewrite accepted files to trail later work. | 0 |
| `Definitions/MMLevelOneDiscProduct.lean` | **The analytic Jacobi product *is* the formal one** (task M1-L1f): `MM.qExpansion_levelOneDiscTprod_eq_formal` — verbatim the comparison `MMLevelOneIntegrality.lean` records as *the* obstruction, for which no Mathlib lemma existed — with consequences `levelOneDiscUnit_coeff_isInt`, `qExpansion_discriminant_eq_X_mul_formal`. **The route, and the library gap it exposed:** the engine is `PowerSeries.eval₂`, **unusable at `ℂ`** — `eval₂Hom` needs `IsLinearTopology S S` and there is **no `IsLinearTopology ℂ ℂ`** (the field's `ℂ`-submodules are `⊥`/`⊤`, so a linear topology on `ℂ` is discrete) — so the locally uniform limit is genuinely needed: `hasProdLocallyUniformlyOn_nat_one_add` on `ball 0 (1/2)`, the bound `MM.norm_one_sub_pow_pow_sub_one_le : ‖(1-q^m)^24 - 1‖ ≤ 24·2^24·‖q‖^m` (hypothesis `‖q‖ ≤ 1`, **not** `< 1`, false at `m = 0`), and `TendstoLocallyUniformlyOn.deriv` iterated by hand (no `iteratedDeriv` version); `UpperHalfPlane.qExpansion_coeff_unique` was **not** needed. **What this is NOT:** the integrality of the **unit part** of `Δ` only — `HasQExpansion ((j-744) - qInv) a` comes later (`MMLevelOneHq.lean`, M1-L1h) — and it says nothing about `MM.LevelOneOrbitSeparation`, which needs the valence formula (M1-L1g reconnaissance, `ROADMAP.md`). 364 lines, no `sorry`, four `#print axioms` guards each exactly `[propext, Classical.choice, Quot.sound]`. | 0 |
| `Definitions/MMLevelOneJCoeffs.lean` + `MMLevelOneHq.lean` | **The level-one integrality input `hq` is PROVED** (task M1-L1h, both files in `FinalCheck.lean`): `MM.levelOneA : HahnSeries ℤ ℤ` is the integral ladder of `j − 744 − q⁻¹`, with `levelOneA_isNormalized` and **`levelOneA_hasQExpansion : HasQExpansion ((levelOneJ - 744) - qInv) levelOneA`**, discharging the hypothesis of `MMLevelOneCusp.lean`'s two theorems in `MM.levelOne_hauptmodul_of_orbitSeparation_discharged` / `…isAnalyticNormalizedHauptmodul_of_orbitSeparation_discharged` (**still taking `MM.LevelOneOrbitSeparation` explicitly**; the valence formula is still missing). **The route took five attempts.** The first four failed on an *impossible* intermediate: `qExpansion 1 MM.qInv = 0` is **not provable**, since `cuspFunction h f` updates the 0-th coefficient with `limUnder (𝓝[≠] 0) (f ∘ invQParam h)` (`Mathlib/Analysis/Complex/Periodic.lean:119`) and `q ↦ q⁻¹` is unbounded near `0`, so that limit is `Classical.epsilon (fun _ : ℂ => False)` — an arbitrary complex number. The working route never touches it: expand the analytic `(j − 744) − q⁻¹` as a whole, get `qExpansion 1 Δ = X·map P_Z`, divide **in `ℤ⟦q⟧` before mapping** (`invOfUnit`), cancel `X`. Coefficients: `0`, `196884`, `21493760` (`c(g,0) = 0` is the FLM fact `V_0 = 0`). Ten `#print axioms` guards, each exactly `[propext, Classical.choice, Quot.sound]`; no `sorry`. | 0 |
| `Definitions/MMHauptmodulAnalytic.lean` | **The analytic content `MM.IsHauptmodul` lacks, and what it does not give.** `MM.IsHauptmodulAnalytic Γ f` is `Γ`-invariance, `MDiff f` and "no missed value has a holomorphic inverse bounded at the cusp"; `MM.HasPoleAtCusp f` is the paper's "takes `i∞` to `∞`"; `MM.HasBoundedInvariantConst Γ` isolates the compactness input the compact Riemann surface supplies (Mathlib has it only at level one). Proved: `surjective_of_hasPoleAtCusp`, `surjective_of_hasBoundedInvariantConst`. **`toIsHauptmodul` is conditional** — it takes `HasPoleAtCusp` and orbit separation as explicit hypotheses, because neither is implied: the pole condition is needed for surjectivity (`MMHauptmodulAnalyticRefute.lean`), and orbit separation does not follow even with it (`f = j²` on `SL(2,ℤ)` has holomorphy, the pole condition and surjectivity but is not injective on orbits). Ruling `j²` out is the degree-1/simple-pole condition and needs the argument principle on `X(Γ)` — task M1. | 0 |
| `Definitions/MMHauptmodulAnalyticRefute.lean` | **Both analytic predicates refuted as sources of surjectivity** — neither `MM.IsHauptmodulAnalytic` nor the earlier `MM.IsHauptmodulAnalyticWeak` (invariance + `MDiff` + unboundedness at the cusp) implies `Function.Surjective`: `not_forall_isHauptmodulAnalytic_surjective` (`f = exp` on `Γ = ⊥`, whose only missed value is `0`, and there the third conjunct *holds*) and `not_forall_isHauptmodulAnalyticWeak_surjective` (`f = τ ↦ τ`, missing `0`). The moral, recorded in the docstrings: **"`f` misses `c`" and "`f` blows up at the cusp" are compatible with "`f` approaches `c` at the cusp"**, so no growth condition at the cusp forces surjectivity. | 0 |
| `Definitions/MMGenusZeroArith.lean` | **The arithmetic genus formula of `X₀(N)`, evaluated at the Conway--Norton levels**: `nuTwo`/`nuThree`, `cuspCount`, `dedekindPsi` (`∑ d ∈ divisors with Squarefree d, N/d` — **not** the tempting `if Squarefree d then d else 0`, which is not Dedekind psi and gives `-1/4` at `N = 4`), `genusFormula : ℕ → ℚ`, `genusZeroLevels := [1,2,3,4,5,6,7,8,9,10,12,13,16,18,25]`, `genusFormula_eleven`. Mathlib-only, ~6 s to build; it refutes the recorded claim that `decide`/`norm_num` cannot recompute the list (the obstacles were `Nat.card` and `Squarefree`, neither of which kernel-reduces). **It is arithmetic about a definition and asserts nothing about `Γ₀(N)`**: the identification "this formula = the genus of `X₀(N)`" is untouched, and completeness ("no other `N`") is checked only numerically for `N ≤ 300` and is **not** formalized. | 0 |
| `Definitions/MMLatticeDoubleCover.lean` | **The algebraic skeleton of the lattice vertex algebra**, needing no vertex-algebra API: for an *arbitrary* even lattice with an arbitrary finite ordered basis, `MM.IntegralLattice` (evenness a field — Mathlib's `ZLattice` has no form and `BilinForm.dualSubmodule` still carries a TODO), the cocycle `ε(x,y) = (-1)^(F(x,y))` with the **2-cocycle condition** and `ε(x,y)ε(y,x) = (-1)^((x,y))`, the double cover `MM.LatticeDoubleCover` as a group with central kernel, and the twisted group ring on `L →₀ ℤ` with `e^x * e^y = ε(x,y) • e^{x+y}`, associativity proved. `MM.II11` supplies `II^{1,1}` with Gram matrix **`((0,1),(1,0))`** (so `(λ,λ) = 2mn`) and `det = -1`; this is what the no-ghost operators `K_i`, `V_L` are built on. Deliberately no `Ring`/`Group` instances, so every axiom is a named theorem keeping the cocycle hypothesis visible; 620 lines against the ~300 guideline, ~245 of them doc comments. | 0 |
| `Definitions/MMGenusZeroRefute.lean` | **The modular predicates diagnosed, as theorems rather than as prose.** `MM.HasGenusZeroFun` (the `∃ f, IsHauptmodul Γ f` repair task M0 proposed) is proved **equivalent to `MM.HasGenusZero` with no hypotheses** (`MM.hasGenusZeroFun_iff_hasGenusZero`) — the repair is the predicate it was meant to repair, not a strengthening. The general form of the defect is `MM.isHauptmodul_comp_orbitMk`: for *every* `Γ` and every bijection `e : ℍ/Γ ≃ ℂ`, `τ ↦ e (orbitMk Γ τ)` is a Hauptmodul, using no discreteness, cusp, holomorphy or meromorphy. Both hypotheses on `e` are needed — with `Function.Injective e` alone the shape is false, refuted at `Γ = ⊤` (`not_forall_isHauptmodul_comp_orbitMk_injective`) — and `MM.not_hasGenusZeroFun_top` shows the predicate is not literally `True`, so the equivalence has content. | 0 |
| `Challenge.lean` | Theorem 1.1 as a standalone statement, with the objects it mentions explained. | 0 |
| `FinalCheck.lean` | Default target: imports everything and guards the axiom footprint of every proved declaration it imports. | 0 |
| `ROADMAP.md`, `NOTES.md`, `AGENTS.md` | Task list with acceptance criteria; what each unformalized input of the paper would require; repository conventions. | — |

Everything above is machine-checked, and every declaration's axiom footprint is exactly
`[propext]`, `[propext, Quot.sound]`, or `[propext, Classical.choice, Quot.sound]` depending on
whether it uses `Classical.choice` — **except** the declarations listed in the `sorry` map below.

## The `sorry` map: what is not proved

`sorry` marks what is unfinished.  By the policy above (and `AGENTS.md`), every `sorry` in the
repository must be registered in this map **and** tied to the open item it belongs to in `ROADMAP.md`
or `HANDOVER.md`; the map is the project's completion meter.  `sorry` is used for three kinds of
unfinished business, listed separately because they have nothing in common but the keyword.

**One open mathematical goal** — the construction half of Theorem 1.1:

| location | what it marks | what discharging it requires |
| --- | --- | --- |
| `MM.MoonshineModule.moonshine_conjecture` (`Definitions/MMMoonshine.lean`) | **existence** of a module `M` with the properties of `MM.MoonshineModule` — the construction half of the paper's Theorem 1.1.  Its type is **`MM.MoonshineModule.MoonshineConjectureStatementMonster`** (task S4b): the module's group is required to be `MM.Monster` — the group this repository defines — and every Thompson series must be the normalized Hauptmodul of a group satisfying the honest `MM.IsGenusZeroGroup` of task D0-e, not the cardinality condition used before D0-g. The weaker spellings are kept and **proved** to follow, so the chain monster ⟹ genus ⟹ pre-repair is visible in the names (`moonshineConjectureStatementGenus_of_monster`, `moonshineConjectureStatement_of_genus`), and each level's non-vacuity is a theorem (`…Monster.exists_module` — a witness may even be taken with `M.G = MM.Monster` literally, `…monster.exists_module_literal`; `MoonshineConjectureStatementGenus.genusZero_exists`; `MoonshineConjectureStatement.genusZero_exists`) | the FLM module (vertex algebras, §3), the monster Lie algebra and the replication identity (8.3) (§4, §6–8), and the Conway--Norton case check (§9) — tasks **S3, S4, T2, M1'**. **This row was briefly superseded**: while the `hauptmodul` field carried a `IsBoundedAtImInfty` conjunct that the paper's normalization contradicts, `MM.MoonshineModule` had no inhabitant and `MM.not_moonshineConjectureStatement` proved this proposition *false*. The field and `MM.GradedModule.FiniteSupport` are now repaired (see the box at the top), so this is an open problem again — and the audit that exposed it is kept in `Definitions/MMStatementAudit.lean`. |

**Two statement-only deliveries of FLM Chapter 8** (batch 229-A) — the theorem statements
themselves, with their one open input each registered as `sorry`.  Everything else in the two files
is a composition of landed theorems, and every declaration in them carries a `#guard_msgs`
footprint printed *with* `sorryAx`, so the hole cannot hide behind a passing build:

| location | what it marks | what discharging it requires |
| --- | --- | --- |
| `MM.FLM810T861S.displayAllStates_evenCocycle` (`Definitions/MMFLM810Theorem861Stated.lean`) | **FLM Theorem 8.6.1** ((8.6.1)--(8.6.3), printed p. 205) at the boundary field of Theorem 8.10.2: the display (8.6.23)/(8.6.24), equivalently Corollary 8.5.1 (8.5.13) at the (8.6.2) states — the campaign's **residual #1** | the (8.4.25) cross contraction of the normally-ordered (8.6.9) object of `α_c(-r)u` with `Y(v,z2)`, i.e. FLM's proof (8.6.4)--(8.6.27); `HANDOVER.md` §1 row 1 and §6 item 1 |
| `MM.FLM88T889S.theorem889_jacobi` (`Definitions/MMFLM88Theorem889Stated.lean`) | **FLM Theorem 8.8.9** ((8.8.29)/(8.8.30), printed p. 231) at the same field; **Remark 8.8.11**'s three residue faces and the engine link to Theorem 8.6.1 are then *proved* corollaries in the same file | its `l = 0` face is residual #1 (above); its `l >= 0` faces and `l = -c` generator chamber are proved, so the hole is exactly **residual #2** — `MM.FLM810ASM.NegativeResidual`, the `l < 0` faces at non-generator pairs |

The theorems named above (`theorem861_source`, `theorem861_all_pairs`, `theorem861_residual`,
`theorem889_delta`, `remark8811_res_z0`/`_res_z1`, `remark8812_res_z2`) carry `sorryAx` in their
footprint exactly through these two declarations.  The engine link in the other direction,
`MM.FLM88T889S.theorem861_of_theorem889`, is a genuinely proved theorem (three standard axioms): the
book's own proof of 8.8.9 repeats 8.6.1's, and this is that repetition, machine-checked.

**The theta coefficients, too, are PROVED, from modular forms (task M-form).**  The
three remaining values used to be carried as "delivery debt" with a counting route.  The owner
redirected the approach, and the computation formula is now a theorem:

> **`MM.thetaCoeff_of_ne_zero : m ≠ 0 → thetaCoeff m = 240 * σ 3 m`** — the classical
> `θ_{E8} = ½(θ₂⁸ + θ₃⁸ + θ₄⁸) = E₄`, built in six steps across `Definitions/MME8Theta*.lean`:
> `MDiff` of the three theta functions and the combination, their cusp behaviour (θ₃, θ₄ → 1 and
> θ₂ → 0), the `ModularForm 𝒮ℒ 4` assembly from task M-form's slash-invariance, its identification
> with `E₄` by `ModularForm.levelOne_weight_four_rank_one`, and then the identification of
> `MM.thetaCoeff` with that form's `q`-expansion.  **No enumeration anywhere**: every count is a
> cardinality from `MM.box_complete`/`MM.box_nodup` plus explicit bijections and involutions (two
> `Finset.card_bij`, one `Set.indicator` fibre argument), and the only `decide`s are the single
> values `σ 3 1 = 1`, `σ 3 2 = 9`, `σ 3 3 = 28` and `B₄ = -1/30` — the idiom
> `Definitions/MMLevelOneDiscUnit.lean` already uses.  The three statements in
> `Definitions/MMLevelTwo.lean` are unchanged and are now **corollaries**; that file reads `sorry=0`.
> The compliant counting proof of `MM.thetaCoeff_one` alone, preserved on the branch
> `task/d-d5-counting`, is therefore superseded outright and is no longer needed as a fallback.

`Definitions/MMLevelTwo.lean` ends with a `## TODO: sorries to discharge` section recording the task-D-d diagnosis, which now trails the file's true state: neither the original `decide` forms nor the suggested `countP`/`Bool`-predicate rewrite finish, because the pruned enumeration `boxAux` — not the predicate — is what does not scale (the "31 s" figure in that file should not be relied on), while the four counts are settled in exact arithmetic (`1`, `112 + 128`, `1136 + 1024`, `3136 + 3584`).  Task D-d2 then proved `MM.thetaCoeff_zero` combinatorially and task M-form discharged the other three, so no `thetaCoeff` declaration is a `sorry` and none was ever reachable from a declaration that `FinalCheck.lean` guards.

Two declarations sit next to it and are easy to confuse with it, so they are named apart:

| declaration | status |
| --- | --- |
| `MM.MoonshineModule.moonshine_uniqueness` | **proved unconditionally.** Given that `T_g` is the normalized Hauptmodul of a genus zero group, it is the unique one with that `q`-expansion. This is the step §9 of the paper actually uses. |
| `MM.MoonshineModule.moonshine_existence_for_fixed_module` | **proved, but it restates the `hauptmodul` field** — no content beyond its hypothesis. Kept so that the boundary is visible in a name rather than buried. |

`FinalCheck.lean` guards the axiom footprint of the proved declarations and deliberately leaves
`moonshine_conjecture` unguarded, so that `sorryAx` stays visible rather than being hidden behind a
passing build.  The wider list of *assumed* inputs (as opposed to `sorry`) is the four items under
"What is actually proved, and what is assumed" below.

A note for anyone reading a build log: a clean `#print axioms` output is **not** evidence that
moonshine has been formalized.  It is evidence that the declarations it was run on do not use
`sorry`, and the point of the table above is to say exactly which parts those are.

## What is actually proved, and what is assumed

The paper proves more than can currently be formalized, and it is important to say exactly
where the boundary lies in this repository.

### Proved unconditionally (no hypotheses)

> **DEFECT OF RECORD (task D0; the box at the top of this file is the current account of it).**
>
> `MM.IsHauptmodul` as originally written was **unsatisfiable** — false for every `Γ` and every `f`,
> with no hypothesis on `Γ` — hence so was `MM.IsNormalizedHauptmodul`, `MM.MoonshineModule` had
> **no inhabitant**, and `MM.MoonshineModule.MoonshineConjectureStatement` was a **false
> proposition**: the `sorry` at `FinalCheck.lean:221` was an artefact of a broken definition, not a
> mathematical gap.  The definition asked for a bijection from the **cusp-less** quotient `ℍ/Γ` onto
> `OnePoint ℂ`, and `∞` had nowhere to come from: `orbitMk` is surjective (`MMModular.lean:77`), so
> such an `e` would have to take the value `OnePoint.infty`, while the definition pinned every value
> to `OnePoint.some (f τ)` and `OnePoint.some ≠ OnePoint.infty`.  **Repaired** to invariance **and**
> surjectivity onto `ℂ` **and** orbit separation — equivalently, that the induced map `ℍ/Γ → ℂ` is a
> bijection; the old shape is kept as a checked theorem (`MM.IsHauptmodulOldShape`,
> `MM.not_isHauptmodul_old_shape`), not as a comment.
>
> **Two things must be read with it.**  (i) `MM.HasGenusZero Γ` is still only the *cardinality*
> condition `Nonempty (ℍ/Γ ≃ ℂ)`, which `Γ₀(11)` (genus 1) satisfies as well: a correct replacement
> must speak about the **compactified** quotient, and until then **no claim in this repository should
> be read as establishing that any group has genus zero** (`ROADMAP.md` task M0).  (ii) **The repair
> is not content**: for **every** subgroup `Γ ≤ GL(2,ℝ)` and every bijection `e : ℍ/Γ ≃ ℂ`,
> `τ ↦ e (orbitMk Γ τ)` satisfies all three conjuncts, so the predicate holds for `Γ₀(11)` exactly as
> much as for `SL₂(ℤ)` — it uses no discreteness, no cusp, no holomorphy and no meromorphy — and the
> `∃ f` repair task M0 proposed is **equivalent to `HasGenusZero` with no hypotheses**
> (`MM.hasGenusZeroFun_iff_hasGenusZero`, machine-checked and guarded in `FinalCheck.lean`); the
> general form is `MM.isHauptmodul_comp_orbitMk`, and the predicate is not literally `True`
> (`MM.not_hasGenusZeroFun_top`), which is what gives that equivalence content.  So "surjectivity is
> not decoration" is true only of the old *unsatisfiable* shape; against the present one all three
> conjuncts are free, and the honest predicate adds the analytic conjuncts the paper uses (`MDiff`,
> unboundedness at the cusp) — the revised task M0 — though even then it is a **witness** predicate,
> not a **criterion**.
>
> **Why this is not cosmetic: it weakens the statement of Theorem 1.1.**  The conclusion of
> `MM.MoonshineModule.MoonshineConjectureStatement` (`Definitions/MMMoonshine.lean:194`) is
> `HasGenusZero Γ ∧ IsNormalizedHauptmodul Γ f (M.thompsonSeries g)`, which with the present
> definitions reduces to `IsNormalizedSeries (M.thompsonSeries g) ∧ HasQExpansion f
> (M.thompsonSeries g)` — the first component of `IsNormalizedHauptmodul` is the vacuous
> `IsHauptmodul Γ f`, and `HasGenusZero Γ` is the cardinality condition.  **So the formalized
> "Theorem 1.1" does not require `Γ` to have genus zero at all**, which is exactly the missing
> Conway--Norton input; the `genusZero_exists` guard named above does **not** catch this, being an
> `∃ Γ, HasGenusZero Γ`.  The repair is to phrase the conclusion with the analytic predicate
> (`MM.IsHauptmodulAnalytic`, task M0) rather than `HasGenusZero` plus `IsHauptmodul` — a change to
> the *statement of the theorem*, hence a dispatcher decision recorded here rather than a change made
> silently under a task.

* **The representation-theoretic data is well defined.**  Traces on finite dimensional graded
  pieces, the Thompson series as a genuine formal Laurent series with finite support, and `T_1` =
  graded dimension (`MM.GradedModule.thompsonCoeff_one`, `MM.MoonshineModule.thompson_one_coeff`).

* **The modular bookkeeping.**  The orbit projection and its universal property (`MM.orbitMk_eq_iff`,
  `MM.orbitMk_surjective`); a Hauptmodul is `Γ`-invariant (`MM.IsHauptmodul.invariant`), a modular
  function (`…isModularFunction`), implies genus zero (`MM.HasGenusZero.of_isHauptmodul`), is constant
  on orbits (`…map_eq`) and **separates** orbits (`…eq_orbit_of_apply_eq`).  **Read this bullet with
  the defect block above, not on its own**: every theorem named here is true, and every one is
  *unconditional in the wrong direction* — they all take `MM.IsHauptmodul Γ f` as a hypothesis, and
  that hypothesis is satisfiable for every `Γ` — so "implies genus zero" is a statement about the
  *cardinality* predicate `HasGenusZero`, not a proof that any group has genus zero.

* **Uniqueness of the normalized Hauptmodul** (`MM.IsHauptmodul.eq_of_qExpansion`,
  `MM.IsNormalizedHauptmodul.eq_of_qExpansion`): two Hauptmoduls for `Γ` and `Γ'` with the same
  `q`-expansion, periodic of period `1`, holomorphic on `ℍ` and bounded at the cusp, are equal, via
  Mathlib's `UpperHalfPlane.qExpansion_eq_zero_iff` applied to the difference.  This is the one
  modular input section 9 of the paper actually uses, and *what makes its case-by-case comparison of
  five coefficients sufficient.*

* **Theorem 1.1 for a monster module.**  The statement (`MM.MoonshineModule.moonshine_conjecture`):
  for every `g`, `T_g` is the normalized Hauptmodul of a genus zero group, and it is the unique one
  with that `q`-expansion.  This declaration **is** the standing `sorry` — `FinalCheck.lean` leaves
  it unguarded — so it is listed here as the *statement* that the four assumed inputs below make
  conditional, not as a proved theorem; what is proved outright is its uniqueness half.

### Assumed (the fields of `MM.MoonshineModule`)

These are exactly the places where the paper's argument is not yet formalized; each is a
field of the structure, so the conditional status is visible in the type of the theorem.

1. **The monster group is defined, but its theory is not proved.**  Since tasks S1b/S2 this
   repository *does* define `MM.Monster` (the `Y₄₄₃` Coxeter group modulo the spider relation, then
   modulo the centre — the same definition the Lean 3 `formalabstracts` used), and since **S4b** the
   standing goal names it: `MoonshineConjectureStatementMonster` requires
   `Nonempty (M.G ≃* MM.Monster)`.  What is still missing is everything one wants to know about that
   group: its **finiteness and order** (task **S3** — the smallest faithful permutation degree is
   196883, so this is a project of its own; Seysen's computer-friendly constructions are in
   `../魔群月光/`), the **identification of the presented group with Griess's monster** (cited:
   Norton--Ivanov, recorded in `refs/README.md`, *not* formalized — see the header of
   `Definitions/MMMonsterMoonshine.lean`), and its **representation theory**, which M1' needs.

2. **The Frenkel--Lepowsky--Meurman module is not constructed.**  `V` is abstract data
   satisfying the graded-character condition.  Mathlib's vertex-operator material is 259
   lines of experimental, unmerged code (`Mathlib/Algebra/Vertex/`).

3. **The replication identity (8.3)** is the field `MM.MoonshineModule.replication`
   (`MM.IsReplicable`).  Sections 6--8 of the paper derive it from the monster Lie algebra
   and its twisted denominator formula (via `Λ(E) = H(E)`, the no-ghost theorem, and the
   product formula for `j`).  None of that (vertex algebras, generalized Kac--Moody
   algebras, Lie algebra homology, the no-ghost theorem) is formalized here.

4. **The Conway--Norton table** is the field `MM.MoonshineModule.hauptmodul`, whose genus conjunct
   is **`MM.IsGenusZeroGroup Γ`** since task D0-g (it was the cardinality condition `HasGenusZero Γ`,
   which `⊥` satisfies — see `MM.hasGenusZero_not_isGenusZeroGroup_bot`): for each `g`,
   the normalized Hauptmodul of a genus zero group exists with `q`-expansion `T_g`.  This
   packages the paper's section 9 (Koike's theorem that the tabulated functions are
   completely replicable, plus the explicit check of the first five coefficients for the
   seven ATLAS classes `2B, 3B, 5B, 7B, 9B, 13B, 15D`) together with the genus-zero
   computations for the relevant modular groups.

So the theorem `MM.moonshine_conjecture` is *not* the unconditional Theorem 1.1.  It is
Theorem 1.1 conditional on (1)--(4), with the modular uniqueness step — the part section 9
uses — proved outright.  A formalization that discharges (3) or (4) is a self-contained
project; `NOTES.md` records what each would require.

### Also not formalized

Section 11 is **partly** formalized: `Definitions/ZZCond.lean` and `Definitions/MMLevelTwo.lean`
build the `E8` lattice, its lattice condition and its theta series, and state the first four
coefficients `θ_{E8}(q) = 1 + 240q + 2160q² + 6720q³ + ...`.  Those four values are no longer
`sorry`: task M-form proved the identification `MM.thetaCoeff_of_ne_zero : thetaCoeff m = 240·σ₃ m`
from modular forms (see the `sorry` map), and **batches 11--12 of the 2026-09 session closed
Lemma 11.1 itself** — `MM.JacobiQuartic` (`Definitions/MMThetaDuplication.lean`) and
`MM.E8ThetaInput` (`Definitions/MME8ThetaBridge.lean`, on the analytic-to-formal transport of
`Definitions/MME8ThetaTransport.lean`) are both theorems, hence **`MM.lemma11_1 :
MM.Lemma11_1Statement`**, the paper's `.tex:2166`--`2172`, unconditionally.  **Correction of record (2026-09, task A1B-recon,
re-verified by the dispatcher with exact series arithmetic): an earlier revision of this line gave
the eta-product form as `θ_{2E8} = η(q)^8 η(q^2)^8`, which is false twice over** —
`η(q)^8η(q^2)^8` is the paper's `\ddp(q) = \eta_{2+}(q)`, it has **weight 8**, not 4, and it equals
`q - 8q² + ⋯`, of positive order, while `θ_{2E8} = 1 + 240q² + 2160q⁴ + ⋯`.  The paper's own relation
(Lemma 11.1, `.tex:2166`--`2172`) is
`θ_{2E8}(q)/Δ(q) = 1/\ddp(q) + 1/\ddp(q^{1/2}) + 1/\ddp(-q^{1/2})`, equivalently
`Δ/\ddp(q) = η(q)^{16}η(q²)^{-8}`; **it is now formalized** — that is exactly the content of
`MM.lemma11_1` (see above, and `ROADMAP.md`'s A1b entry with the BATCH 11--12 blocks).  Sections
12--14 (the fake monster Lie algebra and the monstrous Lie superalgebras) and
section 15 (the open problems) are untouched.  The paper's auxiliary arithmetic (`c(1) = 196884`,
`c(2) = 21493760`, the values of `σ₃`) is not formalized either.

## Relation to the other repositories in this workspace

`fermats-last-theorem/` and `HopfProblem/` use the same toolchain and Mathlib revision.  The
modular-forms API needed here (`ModularForm`, `CuspForm`, `CongruenceSubgroup.Gamma0`,
`UpperHalfPlane.qExpansion`, `ModularForm.eta`, `ModularForm.discriminant`) is stock Mathlib;
`fermats-last-theorem` builds much further on it (`Definitions/Def_ModularCurve_*`,
`Def_ModularForm_*`) and is the natural source of material for the modular-group side of
items (4) above.

## Licence

Apache License 2.0 (see `LICENSE`).
