# HANDOVER — FLM Theorem 8.10.2 (V_L is a vertex operator algebra)

State as of batch 230 (batch 224 is commit `42da30e`, batch 225 `34c5fdf`, batch 226 `6f1768c`, batch 227
`38eb09f`; batch 228 adds `Definitions/MMFLM86NegPairingFockStep.lean`; batch 229 adds the two
statement-only deliveries `Definitions/MMFLM810Theorem861Stated.lean` and
`Definitions/MMFLM88Theorem889Stated.lean`; batch 230 restructured the documentation: the per-batch
records moved to `NOTES.md` Appendix A, and `ROADMAP.md` keeps the plan and the compressed status
tables).  The campaign's chronological record is `NOTES.md` (`§§64--127` topic-wise, Appendix A per
batch); the plan is `ROADMAP.md`; **this file is the handover manual and the entry point**.

## 0. What is delivered, and with which hypotheses

* The acceptance gate is `FinalCheck.lean` (imports everything, guards the axiom footprints).  It is GREEN.
  There is no `axiom`, `admit` or `native_decide` anywhere.  **`sorry` policy (per batch; owner's standing
  instruction, 2026-09-22): a batch may land `sorry`s marking the parts that are not yet proved, provided each is
  registered in `README.md`'s `sorry` map and tied to the open item it belongs to here or in `ROADMAP.md`; the
  declarations that consume them are guarded with `sorryAx` printed, so the holes are always visible; "no `sorry`
  anywhere" is the completion criterion of the whole project, not of a batch.**  Currently there are **two** such
  holes --- the statement-only deliveries of batch 229-A (see the next bullet): `python3 Probe/forbidden_tokens.py
  <files>` reports all zeros for every other module, and every other public declaration carries a
  `#guard_msgs in #print axioms` guard whose footprint is exactly `[propext, Classical.choice, Quot.sound]`.
* **Batch 229-A: Theorem 8.6.1 and Theorem 8.8.9 + Remark 8.8.11 are THEOREMS, with one registered `sorry` each**
  (`README.md`'s `sorry` map).  `Definitions/MMFLM810Theorem861Stated.lean` (`MM.FLM810T861S`) delivers
  `theorem861_source` / `theorem861_all_pairs` / `theorem861_residual`: FLM Theorem 8.6.1 ((8.6.1)--(8.6.3)) at
  the boundary field, with (8.6.1) discharged and every layer composed from landed theorems; its single hole is
  `displayAllStates_evenCocycle`, i.e. residual #1.  `Definitions/MMFLM88Theorem889Stated.lean`
  (`MM.FLM88T889S`) delivers `theorem889_jacobi` ((8.8.29)/(8.8.30)), `theorem889_delta`, Remark 8.8.11's three
  residue faces `remark8811_res_z0`/`_res_z1`/`remark8812_res_z2`, and the engine link
  `theorem861_of_theorem889` --- the last one **proved outright** (three standard axioms), the book's "repeat the
  proof of Theorem 8.6.1" made machine-checked; its single hole is at the `l < 0` non-generator faces, i.e.
  residual #2.  The residual list below is unchanged: the holes now sit at named, guarded locations.
* FLM Theorem 8.10.2 is landed as a REDUCTION (the honest conditional form):
    `MM.FLM810BC.theorem8102_of_correctedResiduals` / `MM.FLM810BC.theorem8102_of_correctedNormal`
    `MM.FLM86M8625P.theorem8102_of_matching_and_windows`   (the sharpest spelling)
  with hypotheses: the boundary inputs `hnd hs C h2 S hpd hW hfin` + `EvenCocycleResidualsCorrected C h2` +
  `EvenCocycleJacobiStepCorrected C h2`.
* The residual package was REDUCED (both ways) in batches 222--223 to:
    `MM.FLM86M8625.ResidueMatching8625 E`      (the (8.6.25)/(8.6.27) matching, whose NONNEG half is a theorem)
    `MM.FLM86SL.Corollary851SpanningEventualWindows (ZAligned E)`   (the (8.5.13) window synchronization)
  because the insertion conjunct of the older package is IMPLIED by the windows conjunct
  (`MM.FLM86M8625P.insertionConjunct8625_of_spanningEventual`, `evenCocycleResidualsCorrected_iff_matching_and_windows`).
* Residual #1 was SHARPENED and localized (batch 224): `Corollary851SpanningEventualWindows (ZAligned E)` is
  EQUIVALENT, both ways and unconditionally, to the single grounded one-mode step
  `MM.FLM86WS.GroundedModeStepAtStates (ZAligned E)` (`MM.FLM86WS.spanningEventual_zAligned_iff_groundedStep`) ---
  a step that consumes its own grounded input, the (8.5.4) lattice corner being a THEOREM at the even cocycle
  (`MM.FLM86WS.groundedLatticeCorner_evenCocycle`, from the proved `MM.FLM86NTP.residueNegativeAligned_evenCocycle`
  + (8.5.11)).  The delivery is re-hung on that spelling (`MM.FLM86WSD.theorem8102_of_matching_and_groundedStep`).
* The window-synchronization layer was ABSORBED (batch 225): the honest commutator half of FLM's display
  (8.6.23)/(8.6.24) --- `MM.FLM86M8625.CommutatorInsertion8625 E (MM.FLM86M8625P.honestIns8625 E)` --- implies
  `MM.FLM86WS.GroundedModeStepAtStates (ZAligned E)` with NO hypothesis at all
  (`MM.FLM86WSA.groundedModeStep_of_commutatorInsertion`: the (8.10.5) threshold of the DESCENDANT pair is
  itself a grounded window, so no window is ever raised and no input window is consumed), and at an even
  cocycle the two are equivalent (`MM.FLM86WSA.groundedModeStep_iff_commutatorInsertion_of_evenCocycle`).
  So residual #1 IS the display: no groundedness quantifier, no window raising and no finiteness input is
  left outside it.  The general bridge between the grounded and the threshold currencies is
  `MM.FLM86WSA.groundedPairWindow_iff_aboveThreshold`; the delivery is re-hung on the display
  (`MM.FLM86WSA.theorem8102_of_matching_and_commutatorHalf`).
* Residual #1 was put in its per-pair DISPLAY currency (batch 226, `MMFLM86DisplayPair.lean`):
  `MM.FLM86DP.DisplayAtPair Y u v` is (8.6.23)/(8.6.24) at ONE pair (the inert (8.6.4) labels dropped),
  `DisplayAllStates` is its all-pairs form, and the per-pair bridge
  `MM.FLM86DP.displayAtPair_zAligned_iff_groundedPairWindow` shows the display at a pair IS a grounded
  window at that pair (at the honest field, via the (8.10.5) threshold; the general form keeps the
  threshold as a parameter).  The residual is now the single step `MM.FLM86DP.DisplayModeStep` (the
  display is inherited by the two one-creation-mode descendants), and
  `MM.FLM86DP.honestDisplay_iff_displayModeStep_of_evenCocycle` (both ways) plus
  `displayAllStates_iff_commutatorInsertion8625` /
  `displayAllStates_iff_spanningEventual_of_evenCocycle` identify it with the previous spellings.  The
  display at the lattice pairs is a THEOREM (`displayAtPair_lattice_evenCocycle`).
* The FOCK half was isolated as ONE one-mode step (batch 228, `MMFLM86NegPairingFockStep.lean`):
  `MM.FLM86NPFS.FaceAtFamily` (the (8.6.25) face at one family of (8.5.4) states), `FockStep E` (the face
  is inherited when a list of creation modes is appended to each state; one-mode instance
  `fockStep_imp_oneMode`), the lattice base as a THEOREM (`faceAtFamily_lattice`, the union of the
  canonical windows), and the both-way identification
  `MM.FLM86NPFS.honestNegPairingCoeffAtStates_iff_fockStep`:
  `HonestNegPairingCoeffAtStates E ↔ FockStep E`.  So residual #3 is now exactly the mode action on the
  normal-ordered blocks; the lattice factor, the generator slice and the (8.5.4) induction are out.
* Residual #1 was identified with the SOURCE's own display (batch 227, `MMFLM86SourceBridge.lean`): the
  spine's carriers are the campaign's (`MM.FLM86SG.sourceResidue861Unshifted_eq_corollary851Residue` is
  `rfl`, the operator-valued grading factor is inert), and
  `MM.FLM86SB.displayAllStates_iff_sourceStatements_of_evenCocycle` (both ways, at an even cocycle) says
  `DisplayAllStates (ZAligned E)` IS `MM.FLM86SG.Theorem861SourceStatement` (8.6.3) at every labelled
  (8.6.2) pair and every window above the vanishing bound.  So the campaign's residual #1 and the spine's
  named next step are ONE statement, and the source's route (8.6.4)--(8.6.27) with the spine file's
  per-step status table is available as a map.
* The Jacobi step was reduced (batch 223) to: `Corollary851SpanningEventualWindows` +
  `MM.FLM810ASM.NegativeResidual E` (`MM.FLM810ASM.stepCorrected_of_spanningEventual`), where the `l >= 0` faces
  of (8.8.41) are PROVED not residual (`crossBracket_eq_crossIterate_of_nonneg_of_grounded`).

## 1. Remaining book formulas (the exact list)

| # | FLM (printed page) | what is still missing | named Lean residual |
| --- | --- | --- | --- |
| 1 | (8.5.13) Corollary 8.5.1 (p. 200), through the proof of Theorem 8.6.1 | the DISPLAY (8.6.23)/(8.6.24): the cross contraction of the normally-ordered (8.6.9) object of `alpha_c(-r)u` with `Y(v,z_2)` (the (8.4.25) contraction producing the (8.6.25) pairing factor on the commutator side) --- the window synchronization is ABSORBED (batch 225), the display needs no mode labels or groundedness (batch 226), and it IS the source's (8.6.3) (batch 227) | `MM.FLM86DP.DisplayModeStep (ZAligned E)` ⟺ `MM.FLM86DP.DisplayAllStates (ZAligned E)` ⟺ `MM.FLM86M8625.CommutatorInsertion8625 E (MM.FLM86M8625P.honestIns8625 E)` ⟺ `MM.FLM86SL.Corollary851SpanningEventualWindows` ⟺ `MM.FLM86WS.GroundedModeStepAtStates` ⟺ `MM.FLM86SG.Theorem861SourceStatement` at the labelled (8.6.2) pairs (`MM.FLM86SB.displayAllStates_iff_sourceStatements_of_evenCocycle`); the implication from the landed commutator half to the grounded step holds with NO hypothesis (`MM.FLM86WSA.groundedModeStep_of_commutatorInsertion`) |
| 2 | (8.8.41) at `l < 0` (p. 234) | the `l < 0` faces at pairs that are NOT lattice generators with `0 <= <a,b>` (batch 202's `negCFaceAligned_evenCocycle` covers only that generator chamber); needs the `(z_1-z_2)^l`/normal-ordering engine at non-generator states and negative pairings | `MM.FLM810ASM.NegativeResidual` |
| 3 | (8.6.25)/(8.6.27) (p. 210), the FOCK half | the mode action on the normal-ordered blocks: the face at a family is inherited when creation modes are appended to the test states (batch 228 isolated it; the lattice base, the generators, the windows and the (8.5.4) induction are PROVED) | `MM.FLM86NPFS.FockStep E` (⟺ `MM.FLM86NPCL.HonestNegPairingCoeffAtStates` ⟺ `MM.FLM86NPGC.HonestNegPairingCoeff`) |
| 4 | (8.6.25)/(8.6.27), second slot `l >= 1` | the `l >= 1` coefficient `honestBlockCoeffJL a b j l m Q = binomCoeff (blockFirstIdx j l m <a,b> - Q) (j + (-<a,b>).toNat)` (NOT implied by #3) | `MM.FLM86M8625.ResidueMatching8625NegSecondSlot` |
| 5 | the theorem's standing hypotheses | `hs` (7.1.1 symmetry), `hnd` (nondegenerate), `hpd` (positive definite), `S`/`hW` (weight grading), `hfin` (weight pieces finite) --- inputs of `theorem8102_of_...`; instantiating them for a concrete lattice is a separate stream | (arguments, not a residual) |

## 2. What is already proved (by book formula) --- do not redo

| FLM | Lean |
| --- | --- |
| (8.4.20)/(8.4.25) assembly | `MM.FLM810NOC.assemblyDiagonal_antidiagonal`, `MM.FLM86AR.assemblyDiagonal` |
| (8.4.36)/(8.4.40) `z_0^j` tower, all `j` | `MM.FLM810NCFC.zLine_all`, `MM.FLM86GLC.zLineGeneratorBase`/`zAlignedGeneratorFlat` |
| (8.5.11)/(8.5.24) anchor/coherent dictionary | `MM.FLM86NTR.ZAligned_anchorVL`, `MM.FLM86MLA.anchorField` |
| (8.5.13) at generators, all `N` | `MM.FLM86NTP.negThreeExpandedResidualAligned_evenCocycle`, `residueNegativeAligned_evenCocycle` |
| (8.5.13) window and display currencies | `MM.FLM86WSA.groundedPairWindow_iff_aboveThreshold` (grounded ⟺ every window above a (8.10.5) threshold), `MM.FLM86DP.displayAtPair_zAligned_iff_groundedPairWindow` (the display at a pair ⟺ a grounded window there), `displayAllStates_iff_groundedAllStates`; the lattice corners `MM.FLM86WS.groundedLatticeCorner_evenCocycle` / `MM.FLM86DP.displayAtPair_lattice_evenCocycle`; `MM.FLM86WSA.groundedModeStep_of_commutatorInsertion`, `descendantsGrounded_of_commutatorInsertion` |
| (8.5.14) at the `z_0^j` coefficient | `MM.FLM86CCN.createdStepAt_shiftZero` |
| (8.6.6) second equality, all `k` | `MM.FLM86D866.display866SecondEqK_all` (via `MM.FLM86NC.normOrderedK`) |
| (8.6.9)/(8.6.10) mode-field commutator, all states | `MM.FLM86MFC.ModeFieldCommInput` |
| (8.4.22)/(8.4.36) general insertion step | `MM.FLM86D866T.powerFam_nestedExp`, `annihExp_nestedExp` |
| (8.6.25)/(8.6.27) nonneg face; coefficient extraction; lattice factor | `MM.FLM86M8625.residueMatching8625Nonneg`; `MM.FLM86FlatBinomial.flatBinomialExpansion`; `MM.FLM86NPCA.honestNegPairingCoeff_on_latticeSpan` |
| (8.8.41) `l >= 0` faces, every state/pairing | `MM.FLM810ASA.crossBracket_eq_crossIterate_of_nonneg_of_grounded` |
| (8.8.41) `l = -c`, generator `0 <= <a,b>` chamber | `MM.FLM810NCFC.negCFaceAligned_evenCocycle` |
| (8.10.5)/(8.10.8)'s finiteness | `MM.FLM86RI.exists_iterateOf_zAligned_eq_zero`, `MM.FLM810ASM.faceWindows_zAligned` |

## 3. Refuted spellings --- BLACKLIST (never consume; cite the refutation)

`CoherentCreatedStep`; `EvenCocycleResiduals` (old) and `EvenCocycleResidualsHonest`; `FockResidualHonest`,
`FockResidualHonestCorrected`, `FockResidualHonestCoeff`; `HonestNegPairingPos`, `HonestNegPairingZero(IdxHw)
(Nonvac)(Block)`, `HonestNegPairingZeroIdxHwNonvacBlock`; `CreatedStepAtZeroNegPairingHonest(+Corrected)`;
`FockShiftZeroStep`, `FockCreatedStep`, `Display8610TwoOneSided`; `PairFiniteAll`, `FockPairDatum`,
`ShiftedPairFiniteGenerators`; `NegOneBlockCollapse`, `NegTwoBlockCollapse`; the batch-220
`Finset.range (TOT.toNat+1)` spelling of the flat identity (the honest window is `Finset.Icc 0 TOT`).
The audit script `Probe/b222a_audit.py` (comment-stripped, word-boundary, negative-controlled) checks them; the
header of `Definitions/MMFLM810BoundaryCorrected.lean` carries the table of refutation names.

## 4. Module map (start here)

* delivery: `Definitions/MMFLM810BoundaryCorrected.lean`, `Definitions/MMFLM86Insertion8625Prove.lean`,
  `Definitions/MMFLM810Assembly{,Aux,Slices,Grounded}.lean`
* the tower (8.4.36)/(8.4.40): `MMFLM86ZMoments`, `MMFLM86ZLineInduction`, `MMFLM86ZLineBaseUpTo`,
  `MMFLM86GeneratorLineAll{,Ind,Close}`, `MMFLM86ModeLawAll{,Step}`, `MMFLM86FockInduction`
* the faces (8.8.41): `MMFLM810NegCFace{,J,Closed}`, `MMFLM86HarvestAllPairings{,Faces}`, `MMFLM810Assembly*`
* the residue (8.5.13): `MMFLM86NegTwoResidue`, `MMFLM86NegThree{Chamber,Prove}`, `MMFLM86HarvestAllPairings*`
* the Fock front: `MMFLM86FockShiftZero`, `MMFLM86NegPairing{Nonvac,Final,Honest,CoeffGeneral,BlockProve}`,
  `MMFLM86FlatBinomial{,Apply}`, `MMFLM86Matching8625{,Aux}`, `MMFLM86SpanningLift`, `MMFLM86ResidueInsertion`
* the section 8.6 engine: `MMFLM86Engine86`, `MMFLM86NestedCauchy*`, `MMFLM86Display866*`,
  `MMFLM86ModeFieldComm*`

## 5. Build and verification discipline (mandatory)

* `cd /home/li/Downloads/mm/MM && tools/build.sh Definitions/<F>.lean` (prerequisites BEFORE dependents on the same
  command line --- a dependent built before its prerequisite fails with "object file ... does not exist", which has
  cost the dispatcher three rounds).  Success = `--- OK: ... ---` AND driver exit 0; read the FULL log (`| tail`
  hides the exit code).
* `python3 Probe/forbidden_tokens.py <explicit file list>` -> all zeros **except** the files carrying a
  registered `sorry` (see §0 and `README.md`'s map).  **Per-batch `sorry` policy (owner's standing instruction,
  2026-09-22): a batch may leave `sorry`s for the unproved parts, provided each is registered in `README.md`'s
  `sorry` map and tied to an open item here or in `ROADMAP.md`; "no `sorry` anywhere" is the completion
  criterion of the whole project, not a per-batch invariant.**
* `#guard_msgs in #print axioms` for EVERY public declaration, docstring = the printed message VERBATIM (the
  printer wraps at 120 chars, name-dependently).  A proved declaration prints the three standard axioms; a
  declaration that consumes a registered `sorry` prints `[propext, sorryAx, Classical.choice, Quot.sound]` ---
  the hole is never hidden.  MEASURED TRAP: an elaboration failure becomes `sorryAx` and the
  guard mismatch is the only symptom --- this fired in batches 198, 208, 209 and 216 and was caught every time.
* Acceptance: `tools/build.sh --timeout 3600 FinalCheck.lean` once per batch (add the new imports first).
* ONE `lean` process at a time (~4.2 GB each).  Rebuild from deleted `.olean`s; re-verify an agent's files AFTER its
  last write (batch 217 had two files still being written during the first verification pass).
* Subagents never commit and never edit existing files; the dispatcher commits by explicit path.

## 6. Next steps in priority order

1. Residual #1 = the source's Theorem 8.6.1 display (8.6.3) = `MM.FLM86DP.DisplayModeStep (ZAligned E)` =
   `DisplayAllStates` = the honest commutator half = the spanning eventual windows = the batch-224 grounded
   step (batches 225--227 landed the absorptions, the per-pair bridge, the display currency and the
   identification with the spine; `MMFLM86WindowSyncAbsorbed.lean`, `MMFLM86DisplayPair.lean`,
   `MMFLM86SourceBridge.lean`).  The source's route is the map: the OPE (8.6.12), the (8.6.4)--(8.6.10)
   series/shifted-field layer (NOT landed; the spine file's status table) and (8.6.21)--(8.6.27), with the
   mode--field commutator (8.6.9)/(8.6.10) PROVED (batch 219-B, `MMFLM86ModeFieldCommAnn*`) and the
   contraction engines landed for lattice monomials (`MMFLM84Contraction`, `MMFLM86ExpProduct`,
   `MMFLM86CommIota`, `MMFLM86MLA`); alternatively the direct cross-contraction route via the anchor
   dictionary (`MMFLM86MLA`), `MMFLM86RI.*`.
2. The Fock half (residual #3) = `MM.FLM86NPFS.FockStep E` (batch 228: the one-mode step, the lattice
   base PROVED, the (8.5.4) induction PROVED, the uniform-support bookkeeping out of the way).  Its proof
   is the mode action on the normal-ordered blocks: the left side of the step is the PROVED
   (8.6.9)/(8.6.10) mode--field commutator at the inserted state (`MM.FLM86MFC.ModeFieldCommInput`, batch
   219-B), the right side moves the mode through `blockOfShift = normOrdered2` (creation-exponential
   commutation `MM.FLM84TV.creationExpVL_comm`, `MM.FLM86RWC.annihExp_mul_creationExpVL_eq_sum_of_subset`,
   `MM.FLM86D866T.powerFam_nestedExp`), and the coefficients are compared by the landed
   `MM.FLM86FB.flatBinomialExpansion` (batch 221-A); the recorded route also uses
   `MM.FLM86MLA.zLineModeAt_all`/`AnchorModeComm`.
3. `NegativeResidual` (residual #2) --- the `l < 0` faces at non-generator pairs; the `l >= 0` translate engine
   (`MMFLM810AssemblyAux`) is the model, and the Fock half (#3) is expected to be its main input.
4. The `l >= 1` slot (residual #4) --- `honestBlockCoeffJL`; its generator LHS is available through
   `MM.FLM86MI.ZAligned_createdState` as a ratio sum of `coherentFieldNat` self-recursions.
5. The six boundary inputs (#5) --- instantiate for a concrete positive-definite even lattice.

## 7. Where the history lives

* `NOTES.md` --- **the work log**: `§§64--127` topic-wise (analysis, accounting, corrections of record,
  refuted spellings) and **Appendix A**, the dispatcher's per-batch records for batches 151--229, moved
  verbatim out of `ROADMAP.md` in batch 230 (files landed, exact statements, brief errors, supersessions).
* `ROADMAP.md` --- **the plan**: the four assumed inputs, the streams' tasks with status, and the campaign's
  compressed "closed / open" tables.  Completed work is one row there, never a batch narrative.
* `README.md` --- the project description, the `sorry` map and the documentation index; `AGENTS.md` --- the
  conventions (ground rules, traps, build and verification, git).
* `Probe/` --- agent briefs, reports and falsification scripts (gitignored, not committed).
