   14: `sorry` marks exactly what is not finished, and it is used for two quite different things — one
   15: open mathematical goal and **no other `sorry`** — the three bounded enumerations that used to sit
   16: here were discharged from modular forms (task M-form), see the `sorry` map
   17: below, and the distinction matters: see [The `sorry` map](#the-sorry-map-what-is-not-proved).
   30: > For a period the repository contained **both** `moonshine_conjecture` (proved by `sorry`) and
   52: > **The `sorry` of `moonshine_conjecture` is therefore an honest open problem again** — the
  133: | Module | Contents | `sorry` |
  137: | `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 Conw
  143: | `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
  155: | `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
  161: | `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), `M
  163: | `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.jacobiTripleProduc
  174: | `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 → mo
  188: | `Definitions/MMLevelOneDiscProduct.lean` | **The analytic Jacobi product *is* the formal one** (task M1-L1f): `MM.qExpansion_levelOneDiscTprod_eq_formal` — verbatim the comparison `MMLevelOneIntegra
  189: | `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
  201: whether it uses `Classical.choice` — **except** the declarations listed in the `sorry` map below.
  203: ## The `sorry` map: what is not proved
  205: `sorry` marks what is unfinished, and in this repository it is used for two different things,
  214: **No other `sorry`s: the theta coefficients are PROVED, from modular forms (task M-form).**  The
  228: > `Definitions/MMLevelTwo.lean` are unchanged and are now **corollaries**; that file reads `sorry=0`.
  232: `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 
  242: `moonshine_conjecture` unguarded, so that `sorryAx` stays visible rather than being hidden behind a
  243: passing build.  The wider list of *assumed* inputs (as opposed to `sorry`) is the four items under
  248: `sorry`, and the point of the table above is to say exactly which parts those are.
  262: > proposition**: the `sorry` at `FinalCheck.lean:221` was an artefact of a broken definition, not a
  322:   with that `q`-expansion.  This declaration **is** the standing `sorry` — `FinalCheck.lean` leaves
  371: `sorry`: task M-form proved the identification `MM.thetaCoeff_of_ne_zero : thetaCoeff m = 240·σ₃ m`
  372: from modular forms (see the `sorry` map), and **batches 11--12 of the 2026-09 session closed
