=== ROADMAP.md (8420 lines)
    1: # ROADMAP: from the conditional Theorem 1.1 to an unconditional one
   44: ## Stream S — the monster group (removes assumed input 1)
   51: ### Foundation: is that presentation the monster?  **Yes — it is a theorem** (settled 2026)
   76: ### [x] S1 — first attempt: **REJECTED**, superseded by S1b
  126: ### [x] S1-V — independent verification: verdict **WRONG**
  132: ### [x] S1b — the actual `Y4 4 3` Coxeter matrix (12 nodes, every edge labelled 3) — **ACCEPTED**
  160: ### [x] S2 — the spider relation and `Monster` — **ACCEPTED**
  234: ### [ ] S3 — `Monster` is finite, of the known order
  300: ### [x] S4 — retarget `MoonshineModule` to `MM.Monster` — **ACCEPTED (S4 + S4b, this session)**
  328: ## Stream T — the monster Lie algebra and (8.3) (removes assumed input 3)
  330: ### [x] T1 — formal power series infrastructure for (8.3) — **PARTIAL, merged**
  374: ### [x] T1b — the composition law `exp ∘ logOf f = f` — **ACCEPTED**
  425: #### Earlier history of this entry (kept: each revision was wrong in an instructive way)
  572: ### [~] T2 — the denominator identity (8.3): sections 6--8 (unproved), plus its self-contained §10 half (T2a, 
  777: ### [~] T3 — the recursion (9.1) from (8.3) — **first step landed (this session)**
  837: ### [ ] T4 — generalized Kac--Moody algebras (the long game)
  846: ## THE LONG CAMPAIGN — discharging the four assumed inputs outright
  852: ### Measured state of the foundations (COMPILED inventory, this revision)
  865: ### M1's COST WAS MIS-STATED: the arithmetic half is 140 lines and needs no FLT (measured)
  923: ### A THIRD EXTERNAL DEVELOPMENT — AND IT IS THE VERTEX-ALGEBRA FOUNDATION ITSELF
  960: ### EXTERNAL FOUNDATION, FOUND — TWO developments, both measured, neither ported
 1020: ### EXTERNAL FOUNDATION, FOUND — and why it changes Phases 3/4 (measured, port UNVERIFIED)
 1059: ### THREE CORRECTIONS THAT SHARPEN THE PLAN (one removes a library from the critical path)
 1144: ### LEECH LATTICE: CONSTRUCTION FOUND AND NUMERICALLY VERIFIED — and why two attempts failed
 1191: ### LEECH: MILESTONES, MEASURED TRAPS, AND A SOURCING WEAKNESS THAT MUST BE STATED
 1512: ### PHASE 0 DECIDED, AND PHASE 1's FIRST INCREMENT LANDED (both measured)
 1562: ### Phasing (each phase ends in a compiling, `sorry`-free increment)
 1584: ### Reporting rule for this campaign
 1591: ## Stream M — the Conway--Norton table (removes assumed input 4)
 1631: ### [paused] M1 — genus zero for the groups in the table — **PAUSED BY THE OWNER 2026-09-13**
 1857: ### [x] M0 — the modular predicates diagnosed and repaired — **ACCEPTED (a) + (b); (c) folded into M1**
 1859: ### [x] D0 — repair the definitions `MoonshineConjectureStatement` is phrased in — **CLOSED (a), (b), (c); D0-
 2136: ### [ ] M1' — the seven ATLAS elements and Koike's theorem
 2145: ## Stream A — the monstrous Lie superalgebras (sections 11--14, not needed for Theorem 1.1)
 2147: ### [x] A1 — the `E8` lattice and its theta series (the finite half of section 11's Lemma 11.1) — **ACCEPTED**
 2302: ### [ ] A1b — Lemma 11.1 itself, and Lemma 11.2
 2371: ### [ ] A2 — a fake monster Lie algebra denominator formula
 2377: ### Batch 151, final acceptance
 2422: ### Batch 152, final acceptance — **Theorem 8.6.1's display is a theorem, and its last input is one named `Pro
 2485: ### Batch 153, reconnaissance — **the residual is not a proof gap, it is a wrong field**, and Theorem 8.6.1 is
 2634: ### Batch 153, acceptance — **the corrected assembly boundary is landed, and the "repaired field" turned out t
 2713: ### Batch 154 — **the honest field's two-point product is landed, and the swap symmetry is the way past its si
 2796: ### Batch 155, part 1 — **`YFamOnGenerators` is REFUTED at `Yzero`: the dispatcher's own proposed identificati
 2849: ### Batch 155, part 2 — **the `z₁ ↔ z₂` swap does NOT remove the sign restriction, and the file as handed back
 2909: ### Batch 156 — four fronts opened toward Theorem 8.10.2
 3219: ### Batch 157 — **the owner's directive: align the definitions with the book first, then prove Theorem 8.10.2*
 3834: ### Batch 163 — the owner's standing instruction: **do not stop until Theorem 8.10.2 is complete**
 4542: ### Batch 173 — the §8.10 substitution σ is CONSTRUCTED (and `SubstForm`'s reformulation is REFUTED); (8.10.73
 4655: ### Batch 174 — (8.6.3) at the boundary field IS Corollary 8.5.1 at the (8.6.2) states; the honest-field (8.4.
 4739: ### Batch 175 — the Fock half reduces to the Fock MONOMIAL BASIS (and the book's (8.5.13) is the lattice case 
 4810: ### Batch 176 — `NegativeChamberExpansion` is a THEOREM in 11 lines (the wall moves to the Θ-collapse); (8.5.5
 4895: ### Batch 177 — the `k = 1` case of (8.6.10) is a FREE theorem from (8.5.23)+(8.10.13) (the tower collapses to
 4997: ### Batch 178 — `NonvacuumCreatedStep` is REFUTED (the `conv` carrier gates on two-sided finiteness, so the wh
 5073: ### Batch 179 — the one-sided product repair is landed (the previously refuted vacuum step is now a theorem); 
 5138: ### Batch 180 — `MiddleBlockDiagonal` (step 2 of `AssemblyDiagonal`) is LANDED; step 4 becomes the single resi
 5209: ### Batch 181 — MILESTONE: `AssemblyDiagonal` is a THEOREM (the `⟨a,b⟩ = −1` case of `hjac` is unconditional a
 5292: ### Batch 182 — `PairFinite` is PROVED on the honest pairs (the Fock fork closes in favour of the datum, and t
 5379: ### Batch 183 — the `−2` line needs the source cocycle: batch 182-B's `NegTwoBlockCollapse` is REFUTED as stat
 5451: ### Batch 184 — the `−2` residual is the `p = 1` line of the landed display family `diagFam` (a both-direction
 5521: ### Batch 185 — the `−2` case reduces to a DERIVATIVE normal-ordering identity (`NegTwoFirstDerivZero`; the `p
 5593: ### Batch 186 — the even-cocycle boundary theorem and the FACE AUDIT (only `l = 0` has producers; the `l ≠ 0` 
 5672: ### Batch 187 — the `l ≠ 0` front is OPENED (the degenerate `l ≥ 0` chamber at `0 ≤ ⟨a,b⟩` is a theorem; the `
 5745: ### Batch 188 — the `l = −1` face becomes a pure honest-lattice-VOA identity `(∗)` (both directions, all bound
 5820: ### Batch 189 — MILESTONE: `(∗)` and the `l = −1` slice are UNCONDITIONAL at FLM's datum; the `−2` assembly re
 5886: ### Batch 190 — the `l = −2` face's `1 ≤ ⟨a,b⟩` chamber is UNCONDITIONAL at FLM's datum; the `(8.4.23)` dictio
 5953: ### Batch 191 — the `z_0^1` line's missing half is DIAGNOSED (the (8.4.19) tail contraction) and unified as `Z
 6019: ### Batch 192 — the `l = −3` face at `2 ≤ ⟨a,b⟩` is UNCONDITIONAL at FLM's datum; the `(8.4.19)` premise is co
 6085: ### Batch 193 — general `l = −c`: the `ν ≥ c−1` chamber is UNCONDITIONAL for every `c`; and the `z_0^1` residu
 6144: ### Batch 194 — the `z_0^1` line at the FIRST FOCK LEVEL is LANDED (with the contraction and the right-hand-si
 6217: ### Batch 195 — 🎉 BREAKTHROUGH: the shared obligation `ZOneLineAllPairings` IS A THEOREM (the `z_0^1` line of 
 6268: ### Batch 196 — the general-`j` induction `ZLine E j` is LANDED conditional on the single `c`-independent base
 6331: ### Batch 197 — the order-2 line is reduced to exactly TWO statements (`zLine_two_iff`), and the Fock half is 
 6433: ### Batch 198 — 🎉 `ZLine E 2` IS A THEOREM: both halves of the order-two base landed (MODE2 + GEN2), and the `
 6491: ### Batch 199 — both halves of the general-`j` base are reduced to ONE named residual each; the left-hand side
 6560: ### Batch 200 — the Fock carrier input is discharged; the GEN-ALL computation is complete up to one finite-sum
 6629: ### Batch 201 — 🎉 the MODE-LAW half is UNCONDITIONAL (`zLineModeAt_all`), and the `l = 0`, `<a,b> <= -3` resid
 6692: ### Batch 202 — 🎉🎉 THE WHOLE `z_0^j` TOWER IS CLOSED: `ZAlignedGeneratorFlat` is a theorem, `ZLineGeneratorBas
 6769: ### Batch 203 — the Fock ledger is corrected (the carrier inputs are NOT inputs of Theorem 8.10.2), the `l = 0
 6846: ### Batch 204 — 🏆 the `l = 0`, `<a,b> <= -3` residual IS PROVED at FLM's datum (all pairings, all N), and the 
 6921: ### Batch 205 — ⚠️ THE FOCK CORNER IS **REFUTED** at honest data (and FLM itself flags the identity as formal)
 6997: ### Batch 206 — the §8.6 engine's honest layer, and the generator slice's `(0,0)` corner is a THEOREM; the exa
 7065: ### Batch 207 — the `k`-variable nested Cauchy carrier is BUILT ((8.6.6)/(8.6.8) at general `k`), and the Fock
 7134: ### Batch 208 — 🎯 (WAD) IS A THEOREM at every weight (the Fock residual's `j = 0` face closed at `0 <= <a,b>`)
 7196: ### Batch 209 — ⛔ THE FOCK RESIDUAL IS **REFUTED** AS SPELLED (two independent machine-checked routes): the ho
 7266: ### Batch 210 — the audit, the honest re-statement of the boundary, and the positive-pairing Fock residual red
 7340: ### Batch 211 — 🎯 the two-shift Fock face is PROVED from ONE derivation identity, and the negative-pairing obj
 7414: ### Batch 212 — the Fock bidegree (and its h-weight refinement) is LANDED, and the Fock residual's residual is
 7482: ### Batch 213 — 🏆 THE POSITIVE-PAIRING FOCK FACES ARE PROVED (no named residual left), and the h-weight separa
 7549: ### Batch 214 — the honest boundary REDUCED to the two negative-pairing Fock faces + the Jacobi step; the nega
 7606: ### Batch 215 — the general OPE/insertion step is LANDED (all lengths), and the negative-pairing faces are pin
 7661: ### Batch 216 — 🎉 item (iii) IS CLOSED (Display866SeriesStep is a theorem for every k), and item (i) is REFUTE
 7719: ### Batch 217 — item (i) reduced to THREE named residuals; the two negative-pairing faces reduced (both ways) 
 7782: ### Batch 218 — (i) reduced to ONE named annihilation input (its zero half closed); and the Fock negative-pair
 7840: ### Batch 219 — 🎯 ModeFieldCommInput IS PROVED (all states); the honest (8.6.25)/(8.6.27) coefficient is a BIN
 7894: ### Batch 220 — slice 2 (j >= 1) is REFUTED too; the honest residual is HonestNegPairingCoeff, whose proof red
 7950: ### Batch 221 — 🎯 FlatBinomialExpansion PROVED (with an honest correction), HonestNegPairingCoeff at l = 0 PRO
 8009: ### Batch 222 — 🎯 THE DELIVERY IS RE-HUNG ON A NON-VACUOUS CORRECTED PACKAGE; the Fock face reduces to the Foc
 8070: ### Batch 223 — 🎯 THE ASSEMBLY IS BUILT: the step reduces to TWO named statements (the windows conjunct + the 
 8141: ### Batch 224 — TARGET: residual #1 SHARPENED: the (8.5.13) window synchronization IS the grounded one-mode st
 8191: ### Batch 225 — TARGET: residual #1 IS FLM's display — the window synchronization is ABSORBED
 8245: ### Batch 226 — TARGET: residual #1 in the per-pair DISPLAY currency of (8.6.23)/(8.6.24); the per-pair bridge
 8291: ### Batch 227 — TARGET: residual #1 IS the source's Theorem 8.6.1 display (8.6.3), in the source's own carrier
 8333: ### Batch 228 — TARGET: the FOCK half of (8.6.25)/(8.6.27) is ONE one-mode step (the mode action on the blocks
 8372: ### Batch 229 — TARGET: FLM Theorem 8.6.1 and Theorem 8.8.9 + Remark 8.8.11 as THEOREMS, with the open input p
=== NOTES.md (3406 lines)
    1: # Notes: what a full formalization of the paper would take
    7: ## 0. Environment
   21: ## 1. The monster group
   89: ## 2. The FLM module
  108: ## 3. The replication identity (8.3)
  147: ## 4. The Conway--Norton table (section 9)
  173: ## 64. Batch 151, second half: `Hrel` is closed, and three ways a dispatched file lies about itself
  189: ### 64.1 An unproved declaration with no `sorry` in the file
  210: ### 64.2 A file written against an import closure that was never rebuilt
  218: ### 64.3 A name that resolves in a minimal probe and not in the file — cause unknown
  228: ### 64.4 What is still open, in one paragraph
  246: ## 65. Batch 152: Theorem 8.6.1's display is a theorem, and the finiteness it needed was an axiom all along
  248: ### 65.1 The display, at a fixed window, from two named inputs
  269: ### 65.2 Why the axiom's window suffices here, when it does not for `JacobiIdentity`
  291: ### 65.3 The uniform vanishing is (8.10.5)
  314: ### 65.4 A landed definition that is refutable: `WeightGrading.IsHomogeneousOp`
  345: ### 65.5 What Theorem 8.6.1 now rests on
  365: ## 66. Batch 153, reconnaissance: the residual of Theorem 8.6.1 is not open, it is **false** — and the repair 
  370: ### 66.1 The defect, in one line
  377: ### 66.2 Consequences, all landed and unconditional
  397: ### 66.3 The repair, landed since batch 80
  416: ### 66.4 What is *not* a gap, and what is
  432: ### 66.5 What the batch does about it
  448: ### 66.6 The empty-oscillator case of Theorem 8.6.1 is **one named `Prop`**, and the two mis-shaping defects a
  485: ## 67. Batch 153, acceptance: the corrected boundary is landed — and the "repaired" field is a **third** defec
  503: ### 67.1 A wrong-prescription statement with a prescription-free proof
  515: ### 67.2 `Yzero` still fails (8.10.13), so the zero mode was not the only defect
  545: ### 67.3 Corrections to the batch's own briefs
  566: ## 68. Batch 156: the `ι` maps exist, and the commutator's real dividing line is the cocycle, not the sign
  568: ### 68.1 FLM (8.10.37)–(8.10.42) for `n = 2`, and why the carrier had to be built
  597: ### 68.2 The commutator at the lattice generators: the cocycle is the dividing line
  621: ### 68.3 Theorem 8.10.2, field by field, after this batch
  631: ## 69. Campaign state at the end of the batch-157--164 run: what Theorem 8.10.2 now rests on
  639: ### 69.1 The alignment (the owner's directive), all four steps landed
  657: ### 69.2 `hL0` (8.10.12) — DISCHARGED
  662: ### 69.3 `hvir` (8.10.9) — discharged **modulo a hypothesis that is false on even lattices**
  682: ### 69.4 `htrans` (8.10.13) — the induction step and the state half proved, three pieces named
  698: ### 69.5 `hjac` (8.10.8) — open, with its faces mapped
  713: ### 69.6 Update after batches 163--165: the two fronts have MERGED into one computation
  764: ## 70. Batch 173: the §8.10 substitution, the Θ corollaries, and what the book's route to Jacobi is
  766: ### 70.1 What landed
  782: ### 70.2 The two false statements this batch found, and the repair
  798: ### 70.3 What the book's route to the Jacobi axiom actually is (read from the page images, batch 173)
  820: ## 71. Batch 174: what is left of Jacobi, and it is now one named `Prop`
  822: ### 71.1 The crux, reduced
  841: ### 71.2 The two halves that remain
  855: ### 71.3 FLM's §8.6 direct route, re-read at the repaired field (B174-A's map)
  868: ### 71.4 What the next batches must do, in order
  878: ## 72. Batch 175: the Fock half reduces to the Fock monomial basis; the negative pairing splits; one missing e
  880: ### 72.1 The book's (8.5.13) is the LATTICE case only
  888: ### 72.2 The reduction landed (B175-A, `Definitions/MMFLM85CorollaryFock.lean`)
  903: ### 72.3 The negative pairing (B175-B, `Definitions/MMFLM86ResidueNegative.lean`)
  919: ### 72.4 What is left, precisely
  930: ## 73. Batch 176: the two engines, and a free theorem the agents missed
  932: ### 73.1 `NegativeChamberExpansion` was a theorem waiting to be noticed
  943: ### 73.2 (8.5.5) coefficientwise, and the vacuum field of (8.6.10)
  958: ### 73.3 The free theorem (dispatcher)
  968: ### 73.4 The two residuals that remain for `hjac`
  977: ## 74. Batch 177: (8.6.10) at `k = 1` is free; the non-vacuum one-step and the antidiagonal collapse are what 
  979: ### 74.1 A structural theorem: (8.5.23) + (8.10.13) ⟹ (8.6.10) at `k = 1`
 1006: ### 74.2 `NegOneBlockCollapse` is REFUTED; the corrected residual is `c`-free
 1028: ### 74.3 The three residuals left for `hjac`
 1038: ## 75. Batch 178: the `conv`-form §8.6 chain is refuted (carrier defect); `AssemblyDiagonal` is the `−1` case'
 1040: ### 75.1 The refutation, and what it does and does not touch
 1065: ### 75.2 `AssemblyDiagonal`: the `⟨a,b⟩ = −1` case's single residual
 1076: ### 75.3 The three live residuals for `hjac`
 1082: ## 76. Batch 179: the one-sided repair, and `expField` multiplicativity (a new Leibniz rule)
 1084: ### 76.1 The repair (B179-B, `Definitions/MMFLM85OneSidedProduct.lean` + `MMFLM85OneSidedChain.lean`)
 1098: ### 76.2 `expField` multiplicativity (B179-A, `Definitions/MMFLM86ExpFieldMul.lean` + `MMFLM86ExpFieldMulLat.l
 1113: ### 76.3 The live residuals after batch 179
 1120: ## 77. Batch 180: `MiddleBlockDiagonal` landed; step 4 is one index-regrouping Prop; the OPE third family corr
 1122: ### 77.1 `AssemblyDiagonal` is now one measured regrouping away
 1142: ### 77.2 The OPE third family: a scalar mis-reading corrected, and the bridge landed
 1161: ### 77.3 The live residuals after batch 180
 1167: ## 78. Batch 181: `AssemblyDiagonal` is a theorem (the `−1` case closes); `PairFinite` is the Fock fork
 1169: ### 78.1 Milestone: the `⟨a,b⟩ = −1` case of `hjac` is closed at the boundary field
 1186: ### 78.2 The Fock fork: `PairFinite` is UNDECIDED
 1207: ### 78.3 The residuals after batch 181
 1217: ## 79. Batch 182: `PairFinite` PROVED (the Fock fork closes); `⟨a,b⟩ = −2` reduced to `NegTwoBlockCollapse`; c
 1219: ### 79.1 CORRECTION OF RECORD — the "infinite sum" claim of §§75--78 is FALSE
 1240: ### 79.2 What is now exact
 1250: ### 79.3 The `⟨a,b⟩ = −2` residue
 1267: ### 79.4 The residuals after batch 182
 1276: ## 81. Batch 184: the `−2` residual is the `p = 1` line of `diagFam`; the mode intertwining evaluates the Fock
 1281: ### 81.1 `NegTwoDisplayZOne`: the exact `⟨a,b⟩ = −2` residual
 1301: ### 81.2 The mode intertwining, and the Fock LHS evaluated
 1320: ### 81.3 The residuals after batch 184
 1328: ## 80. Batch 183: the `−2` line is WEIGHTED (and needs the source cocycle); the coherent-state field is a recu
 1330: ### 80.1 `NegTwoBlockCollapse` is refuted as stated; the corrected residual is `NegTwoDiagonalWeight`
 1352: ### 80.2 The coherent-state field is a recursion; `≤ −3` is expanded to the honest (8.5.5) form
 1365: ### 80.3 The residuals after batch 183
 1372: ## 82. Batch 185: the `−2` case is a DERIVATIVE identity; the Fock half is one dictionary
 1374: ### 82.1 `NegTwoFirstDerivZero`: the `⟨a,b⟩ = −2` residual, in derivative form
 1398: ### 82.2 The Fock half is one dictionary
 1408: ### 82.3 Correction of record
 1414: ### 82.4 The residuals after batch 185
 1421: ## 83. Batch 186: the boundary at the even cocycle and the FACE AUDIT
 1423: ### 83.1 The boundary, stated honestly
 1434: ### 83.2 The face audit (the batch's main product)
 1445: ### 83.3 The `−2` derivative residual, decomposed
 1455: ### 83.4 The fronts after batch 186
 1462: ## 84. Batch 187: the `l ≠ 0` front opened; the `−2` creation piece collapsed
 1464: ### 84.1 The `l ≠ 0` faces: first land at the boundary field
 1490: ### 84.2 `creationDerivPiece` collapsed; the `−2` residual is now sharply localised
 1508: ### 84.3 The fronts after batch 187
 1515: ## 85. Batch 188: the `l = −1` face becomes a pure VOA identity; the third Leibniz piece lands
 1517: ### 85.1 `(∗)`: the `l = −1` slice is one honest-lattice-VOA statement
 1537: ### 85.2 The third Leibniz piece: the `E⁺` mirror collapse
 1552: ### 85.3 The fronts after batch 188
 1559: ## 86. Batch 189: `(∗)` and the `l = −1` slice are unconditional at FLM's datum; the ordering question settled
 1561: ### 86.1 MILESTONE: the `l = −1` slice is closed at the even cocycle
 1580: ### 86.2 The ordering question, settled; the `−2` residual is now the (8.4.23) dictionary
 1598: ### 86.3 The fronts after batch 189
 1604: ## 87. Batch 190: the `l = −2` face lands; the `z_0^1` line is now the single shared blocker
 1606: ### 87.1 The `l = −2` face
 1625: ### 87.2 The (8.4.23) dictionary, and the relocation of the `−2` gap
 1643: ### 87.3 The state after batch 190
 1650: ## 88. Batch 191: the `z_0^1` obligation is unified as `ZOneLineAllPairings`; the moment picture corrected
 1652: ### 88.1 The single shared obligation
 1668: ### 88.2 The moment picture, corrected and landed
 1689: ### 88.3 The state after batch 191
 1695: ## 89. Batch 192: the `l = −3` face lands; the `(8.4.19)` premise corrected
 1697: ### 89.1 The `l = −3` face at `2 ≤ ⟨a,b⟩` is a theorem
 1712: ### 89.2 The `(8.4.19)` premise refuted; the annihilation/zero-mode laws landed
 1731: ### 89.3 The state after batch 192
 1738: ## 90. Batch 193: general `l = −c` chambers; the `z_0^1` residual on the generators and its linearity
 1740: ### 90.1 General `l = −c`: the `ν ≥ c−1` chamber is unconditional
 1754: ### 90.2 The `z_0^1` residual: generators landed, linearity landed
 1772: ### 90.3 The state after batch 193
 1779: ## 91. Batch 194: the `z_0^1` line at the first Fock level; the derivative ladder
 1781: ### 91.1 The first Fock level of the shared blocker
 1803: ### 91.2 The derivative ladder: no higher line is easier
 1820: ### 91.3 The state after batch 194
 1827: ## 92. 🎉 Batch 195: `ZOneLineAllPairings` IS A THEOREM
 1829: ### 92.1 The breakthrough
 1849: ### 92.2 What this unlocks
 1858: ### 92.3 The state after batch 195
 1864: ## §93 Batch 196 — the `ZLine` tower is one `c`-independent base from closed
 1866: ### 93.1 The harvest (A)
 1884: ### 93.2 The induction (B): one base, two halves
 1915: ### 93.3 Accounting after batch 196
 1933: ### 93.4 Brief errors (three, all consequential)
 1946: ## §94 Batch 197 — the order-2 line is two statements, and the Fock half is a display plus two carrier inputs
 1948: ### 94.1 The truncated base (A)
 1982: ### 94.2 The Fock half is two-layered (B)
 2008: ### 94.3 The next Fock step is probably cheap
 2017: ### 94.4 Corrections of record
 2031: ### 94.5 Accounting after batch 197
 2042: ## §95 Batch 198 — `ZLine E 2` is a theorem: the order-two base is closed on both halves
 2044: ### 95.1 What closed
 2067: ### 95.2 The mathematics that was actually new
 2077: ### 95.3 The `sorryAx`-from-elaboration-error trap (campaign-level)
 2088: ### 95.4 Corrections and traps of record
 2100: ### 95.5 Accounting after batch 198
 2112: ## §96 Batch 199 — both halves of the general-`j` base are one named residual away
 2114: ### 96.1 The two residuals of record
 2129: ### 96.2 The new mathematics of batch 199
 2143: ### 96.3 Accounting after batch 199
 2155: ### 96.4 Corrections and traps of record (batch 199)
 2168: ## §97 Batch 200 — the Fock span is discharged; the all-order generator line is complete up to one finite-sum 
 2170: ### 97.1 Fock: one carrier input left, and it is `PairFiniteAll`
 2186: ### 97.2 GEN-ALL: everything but one finite-sum identity
 2205: ### 97.3 Traps of record (batch 200)
 2216: ### 97.4 Accounting after batch 200
 2226: ## §98 Batch 201 — the mode-law half is unconditional; `ZLineGeneratorBase` now rests on the generator half al
 2228: ### 98.1 `zLineModeAt_all` (unconditional)
 2246: ### 98.2 The `l = 0`, `<a,b> <= -3` residual, reduced to `normOrdered2` alone
 2261: ### 98.3 Corrections of record
 2278: ### 98.4 Accounting after batch 201
 2290: ## §99 Batch 202 — the tower is closed; every `l = -c` face is unconditional
 2292: ### 99.1 The three-step composition
 2306: ### 99.2 Why the face consumer was cheap
 2314: ### 99.3 Corrections and traps of record (batch 202)
 2327: ### 99.4 Accounting after batch 202
 2339: ## §100 Batch 203 — the Fock ledger corrected; the `l = 0` face assembled at all states; the `<= -3` residual'
 2341: ### 100.1 The Fock front is ONE statement
 2354: ### 100.2 The `<a,b> <= -3` residual cannot be reformulated into something easier
 2368: ### 100.3 The all-states assembly, and its one named residual
 2377: ### 100.4 Traps of record (batch 203)
 2386: ### 100.5 Accounting after batch 203
 2397: ## §101 Batch 204 — the `<= -3` residual is proved; the Fock front is the shift-zero corner
 2399: ### 101.1 The residual that was called hard
 2414: ### 101.2 The Fock front, sharpest form
 2427: ### 101.3 A warning worth keeping
 2435: ### 101.4 Accounting after batch 204
 2446: ## §102 Batch 205 — the Fock corner is refuted; the `l = 0` face is one mode step
 2448: ### 102.1 A refuted target, and FLM warned us
 2462: ### 102.2 What survives, and the honest Fock front
 2472: ### 102.3 The `l = 0` all-states face, precisely
 2486: ### 102.4 Accounting after batch 205
 2497: ## §103 Batch 206 — the generator slice's `(0,0)` corner proved; the two exact residuals named
 2499: ### 103.1 The Fock front, now precise
 2518: ### 103.2 The §8.6 engine: what it now has, and the one carrier it lacks
 2528: ### 103.3 Corrections (B206-B)
 2538: ### 103.4 Accounting after batch 206
 2548: ## §104 Batch 207 — the nested Cauchy carrier is built; the Fock residual is (WAD) at `r >= 1`
 2550: ### 104.1 The dictionary (both ways)
 2566: ### 104.2 The nested Cauchy carrier, and (8.6.6)/(8.6.8) at general k
 2582: ### 104.3 Traps of record
 2590: ### 104.4 Accounting after batch 207
 2600: ## §105 Batch 208 — (WAD) is a theorem; (8.6.6)'s second equality is a named Prop at `k >= 3`
 2602: ### 105.1 Reading the tower backwards
 2621: ### 105.2 (8.6.6)'s second equality
 2633: ### 105.3 Accounting after batch 208
 2644: ## §106 Batch 209 — the Fock residual is refuted as spelled; the honest slice is `0 <= <a,b>`
 2646: ### 106.1 The refutation, two independent routes
 2663: ### 106.2 What this costs, and what it does not
 2671: ### 106.3 The corrected accounting
 2685: ### 106.4 The lesson (recorded for the whole campaign)
 2693: ### 106.5 Accounting after batch 209
 2704: ## §107 Batch 210 — the honest boundary is landed; the Fock residual is one two-shift statement
 2706: ### 107.1 The Fock residual, final shape
 2721: ### 107.2 The honest boundary, and why it is not vacuous
 2735: ### 107.3 The one object still missing
 2742: ### 107.4 Accounting after batch 210
 2753: ## §108 Batch 211 — the two-shift face proved from a derivation identity; the shifted normal-ordered object bu
 2755: ### 108.1 `CoherentCreatedStepShifted` reduced to `ShiftedCreationDerivation`
 2772: ### 108.2 `pairBlock`: the (8.6.25) object, built
 2779: ### 108.3 Two defects of record (batch 210-B's spelling)
 2789: ### 108.4 What still blocks the negative-pairing faces
 2795: ### 108.5 Accounting after batch 211
 2804: ## §109 Batch 212 — the bidegree and its h-weight refinement; the residual pinned to the `YFam` modes
 2806: ### 109.1 The residual, corrected and pinned
 2820: ### 109.2 The grading, and why the coarse one is not enough
 2827: ### 109.3 Accounting after batch 212
 2837: ## §110 Batch 213 — the positive-pairing Fock faces are theorems; the h-weight separation is landed
 2839: ### 110.1 The residual is closed
 2850: ### 110.2 The h-weight separation, and what it corrects
 2858: ### 110.3 Milestone: the honest residual package is two Fock faces
 2871: ### 110.4 Traps of record (batch 213)
 2880: ## §111 Batch 214 — the boundary reduced to two Fock faces + the Jacobi step; the negative-pairing faces at pe
 2882: ### 111.1 The reduced boundary (the campaign's current frontier)
 2896: ### 111.2 The negative-pairing faces, corrected and assembled
 2909: ### 111.3 Corrections of record
 2915: ### 111.4 Accounting after batch 214
 2926: ## §112 Batch 215 — the general insertion step landed; the negative-pairing faces off-vacuum
 2928: ### 112.1 The last two mathematical residuals of the campaign
 2937: ### 112.2 What landed this batch
 2946: ### 112.3 Traps and corrections of record
 2956: ### 112.4 Accounting after batch 215
 2966: ## §113 Batch 216 — (iii) closed; (i) refuted as spelled
 2968: ### 113.1 Item (iii) is CLOSED
 2976: ### 113.2 Item (i) is false as spelled
 2985: ### 113.3 What the remaining (i) residual contains
 2991: ### 113.4 Accounting after batch 216
 3000: ## §114 Batch 217 — (i) to three residuals; the negative-pairing faces in block form
 3002: ### 114.1 Item (i), final shape
 3012: ### 114.2 The negative-pairing faces in block form
 3018: ### 114.3 Corrections and traps of record
 3026: ### 114.4 Accounting after batch 217
 3035: ## §115 Batch 218 — (i) to one annihilation input; the Fock j = 0 face refuted
 3037: ### 115.1 Item (i)
 3045: ### 115.2 The Fock j = 0 face is false in every spelling
 3055: ### 115.3 Accounting after batch 218
 3064: ## §116 Batch 219 — the honest (8.6.25) coefficient; ModeFieldCommInput proved; the honest Fock package refute
 3066: ### 116.1 The honest coefficient (the answer to the Fock question)
 3075: ### 116.2 Refuted spellings (do not consume)
 3082: ### 116.3 The corrected residual
 3089: ### 116.4 Item (i): the mode-field commutator is PROVED
 3096: ### 116.5 Accounting after batch 219
 3107: ## §117 Batch 220 — slice 2 refuted; the residual is a reindexing identity
 3109: ### 117.1 Fock: the corrected face and its single gap
 3117: ### 117.2 Item (i): the matching is unnamed
 3122: ### 117.3 Accounting after batch 220
 3132: ## §118 Batch 221 — the flat identity proved; the generator slice of the Fock residual proved; the matching na
 3134: ### 118.1 The honest identity (corrected window)
 3141: ### 118.2 The Fock residual's current shape
 3149: ### 118.3 Ledger after batch 221
 3160: ## §119 Batch 222 — the boundary re-hung (non-vacuous); the Fock half named; the lattice factor proved
 3162: ### 119.1 The corrected package (the new delivery frontier)
 3173: ### 119.2 The Fock side
 3179: ### 119.3 Accounting after batch 222
 3192: ## §120 Batch 223 — the assembly built; the ledger halves again
 3194: ### 120.1 The assembly's residual
 3204: ### 120.2 The insertion conjunct is redundant
 3209: ### 120.3 Accounting after batch 223
 3224: ## §121 Batch 224 — residual #1 sharpened: the window synchronization is the grounded one-mode step
 3226: ### 121.1 The sharpened residual and the theorem corner
 3240: ### 121.2 The delivery re-hung
 3244: ### 121.3 Accounting after batch 224
 3254: ## §122 Batch 225 — the window synchronization is absorbed: residual #1 IS the display
 3256: ### 122.1 The bridge between the grounded and the threshold currencies
 3262: ### 122.2 The display gives the descendant windows outright
 3273: ### 122.3 The accounting, both ways
 3278: ### 122.4 Accounting after batch 225
 3289: ## §123 Batch 226 — residual #1 in the per-pair display currency
 3291: ### 123.1 The display at a pair, and the per-pair bridge
 3304: ### 123.2 The step, and the residual
 3312: ### 123.3 Accounting after batch 226
 3323: ## §124 Batch 227 — residual #1 IS the source's (8.6.3)
 3325: ### 124.1 The carriers coincide at one window
 3333: ### 124.2 Residual #1 at a labelled pair, and at all pairs
 3340: ### 124.3 Accounting after batch 227
 3352: ## §125 Batch 228 — the Fock half is ONE one-mode step; its lattice base is a theorem
 3354: ### 125.1 The face at a family, and the step
 3367: ### 125.2 Accounting after batch 228
 3377: ## §126 Batch 229 --- the two Chapter-8 theorems delivered with one registered `sorry` each
 3393: ## §127 Policy: per-batch `sorry` is the sanctioned marker of unfinished work (2026-09-22)
=== HANDOVER.md (192 lines)
    1: # HANDOVER — FLM Theorem 8.10.2 (V_L is a vertex operator algebra)
    9: ## 0. What is delivered, and with which hypotheses
   87: ## 1. Remaining book formulas (the exact list)
   97: ## 2. What is already proved (by book formula) --- do not redo
  115: ## 3. Refuted spellings --- BLACKLIST (never consume; cite the refutation)
  126: ## 4. Module map (start here)
  139: ## 5. Build and verification discipline (mandatory)
  160: ## 6. Next steps in priority order
  187: ## 7. Where the history lives
=== README.md (427 lines)
    1: # Monstrous moonshine in Lean 4
  119: ## Build and verification
  136: #print axioms MM.moonshine_conjecture
  140: ## What is in the repository
  212: ## The `sorry` map: what is not proved
  277: ## What is actually proved, and what is assumed
  282: ### Proved unconditionally (no hypotheses)
  353: ### Assumed (the fields of `MM.MoonshineModule`)
  393: ### Also not formalized
  416: ## Relation to the other repositories in this workspace
  425: ## Licence
