## 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.
* `#guard_msgs in #print axioms` for EVERY public declaration, docstring = the printed message VERBATIM (the
  printer wraps at 120 chars, name-dependently).  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

* `ROADMAP.md` --- one entry per batch (173--223), each with the files landed, the exact statements, the brief
  errors and the accounting supersessions.
* `NOTES.md` --- §§70--120 topic-wise; §§105--120 are the Fock/assembly period and contain the refutation records.
* `Probe/` --- agent briefs, reports and falsification scripts (gitignored, not committed).
