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

State as of batch 241.  The three source theorems of the chapter are delivered as Lean theorems with
their open inputs registered as `sorry` (batch 229: Theorem 8.6.1, Theorem 8.8.9 + Remark 8.8.11;
batch 231: Theorem 8.10.2).  **This file is the handover manual for the campaign**: what is
delivered, the exact gaps that remain before it is `sorry`-free, the proved inventory, the blacklist,
the module map, the build discipline and the next steps.  The plan is `ROADMAP.md`; the work log
(per-batch records, topic-wise analyses and corrections) is `NOTES.md` (`§§64--129` + Appendix A).

## 0. The delivery in one screen

* **Acceptance gate**: `FinalCheck.lean` (imports every module, guards the axiom footprints).  GREEN.
  No `axiom`, `admit` or `native_decide` anywhere.  **`sorry` policy (owner's standing instruction,
  revised 2026-09-22, batch 241): this file is the SINGLE REGISTRY of the registered `sorry`s; one
  batch does exactly one of (a) eliminate ONE registered `sorry`, or (b) eliminate ONE registered
  `sorry` and create ONE new `sorry` in a NEW file, entered in `§1.1` below, which the next batch
  attacks.**  Declarations that consume a registered `sorry` print `sorryAx` in their guarded
  footprint; "no `sorry` anywhere" is the completion criterion of the whole project, and when the
  `§1.1` registry is empty, `ROADMAP.md` marks the live item (Theorem 8.10.2) resolved.  **There are exactly TWO holes** (batch 239-A: the 8.10.2 file's matching package --- residuals #3/#4 and their four consumers --- left the ledger; its content lives inside the 8.8.9 hole's proof, and the two TARGET Props stay in the tree) (batch 237-A: the 8.10.2 copy of residual #2 was a duplicate of the 8.8.9 hole, and the 8.8.9 hole was the vacuous uniform-window form --- both fixed, `NOTES.md` §137) (§1).
* **The statements exist as theorems** (composed from landed theorems; the holes are the residuals):

  | file (namespace) | theorem | holes |
  | --- | --- | --- |
  | `Definitions/MMFLM810Theorem861Stated.lean` (`MM.FLM810T861S`) | `theorem861_source`, `theorem861_all_pairs`, `theorem861_residual`: FLM Theorem 8.6.1 ((8.6.1)--(8.6.3), printed p. 205) at the boundary field | #1 |
  | `Definitions/MMFLM88Theorem889Stated.lean` (`MM.FLM88T889S`) | `theorem889_jacobi` ((8.8.29)/(8.8.30)), `theorem889_delta`, Remark 8.8.11's faces `remark8811_res_z0`/`_res_z1`, `remark8812_res_z2`; `theorem861_of_theorem889` (the engine link) is **proved outright** | #2 (for the Jacobi passage) |
  | `Definitions/MMFLM810Theorem8102Stated.lean` (`MM.FLM810T8102S`) | **`theorem8102_evenCocycle`** concluding `FLM810.Theorem8102 form ((Fintype.card κ : ℕ) : ℚ)`, plus `corollary851AllStatesExists_evenCocycle` and `evenCocycleResidualsCorrectedNormal_evenCocycle` | **no hole of its own** (batch 239-A: the matching package --- #3/#4 and their four consumers --- was removed from this file; `NOTES.md` §139).  `theorem8102_evenCocycle` goes through the 8.8.9 hole below  **Batch 238-A**: `theorem8102_evenCocycle` now follows the BOOK's route --- (8.10.8) = Theorem 8.8.9 --- through the landed `MM.FLM810CFC.theorem8102_of_hs` + the 8.8.9 hole `MM.FLM88T889S.theorem889_faithful`; the matching (#3/#4) is OFF its dependency path (`NOTES.md` §138) |

* **The reduction the theorem uses** is the landed, fully proved
  `MM.FLM86WSA.theorem8102_of_matching_and_commutatorHalf` (equivalently
  `MM.FLM86WSD.theorem8102_of_matching_and_groundedStep`, `MM.FLM86M8625P.theorem8102_of_matching_and_windows`,
  `MM.FLM810BC.theorem8102_of_correctedNormal`), whose hypotheses are the six boundary inputs plus
  the matching and the display---Jacobi pair.  Every batch-231 step that connects the holes to those
  hypotheses is a landed theorem: `residueMatching8625_evenCocycle`,
  `honestNegPairingCoeff_evenCocycle`, `commutatorInsertion_evenCocycle`,
  `jacobiStep_evenCocycle`.
* **What "`sorry`-free" would mean**: close the TWO registered `sorry`s of §1.1 --- both are holes in
  other files, not here --- and instantiate the six boundary inputs of §1.2.  (The 8.10.2 file itself
  has no `sorry`: batch 239-A removed the matching package.)  Nothing else: the reductions, the equivalences between the currencies,
  the finiteness (8.10.5), the lattice corners and the `l >= 0` faces are all theorems.

## 1. What still separates the three statements from `sorry`-freeness

### 1.1 The registered `sorry`s (the exact statements) --- the SINGLE REGISTRY

```lean
-- #1 (ELIMINATED, batch 242-A): the (8.4.25) cross contraction is no longer open ---
-- \MM.FLM810T861S.crossContraction_evenCocycle\ is now a THEOREM, derived from the grounded l = 0 face
-- below through the landed batch-223-B equivalence
-- (MM.FLM86M8625P.modeFieldCommInsertionStep8625_iff_spanningEventual) and
-- MM.FLM810CCG.corollary851SpanningEventualWindows_of_groundedZeroFace.
--
-- #1-old (the all-states grounded face, batch 242-A's entry) is ELIMINATED (batch 245-A): it is the
-- (8.6.2)-pair computation below lifted to all states by the book's own spanning step (Remark 8.3.9)
-- --- \MM.FLM810CCG.groundedZeroFace_of_spanningDisplay\ --- with the iterate's vanishing supplied by
-- the landed (8.10.5).  \groundedZeroFace_evenCocycle\ is now a THEOREM (sorry = 0 in its file).

-- #1-bis (batch 244-A, the book's own location of the remaining computation): the coefficient-of-P
-- argument of (8.6.15)--(8.6.21) AT the (8.6.2) pairs, registered in the window-synchronized (8.5.13)
-- currency at the (8.5.4) states.  Everything downstream is landed: the lift to all states is batch
-- 223-B's backward direction (Remark 8.3.9's spanning via `MM.FLM85Fock.corollary851_of_mem_span`), the
-- (8.4.25) step and the commutator half (8.6.24) follow in `MM.FLM86SDA`, and the display chain
-- (`commutatorHalf` -> `displayAllStates`) is the 8.6.1 file's proved composition.  So this entry is
-- the book's Theorem 8.6.1 computation itself; `groundedZeroFace_evenCocycle` above awaits absorption
-- into it by the all-states bilinear lift (`NOTES.md` §143).
MM.FLM86SDA.spanningDisplay_evenCocycle (hs : ∀ a b : L, form a b = form b a)
    (C : EvenCocycle L form) (h2 : (2:F) ≠ 0) :
    MM.FLM86SL.Corollary851SpanningGroundedWindows (F := F) bL form
      (MM.FLM810JF2.ZAligned (F := F) bL form (C.toCentralExtension (F := F) h2))

-- #2 (ELIMINATED, batch 243-A): `MM.FLM88T889S.theorem889_faithful` (`FacesAtStates`) is now ASSEMBLED
-- from the two entries below, through the landed slices
-- (`MM.FLM810ASM.faces_of_groundedZeroFace`, `MM.FLM810ASM.negativeFaces_of_residual`): the l = 0 slice
-- is the grounded display and the l > 0 slice is a theorem from it plus (8.10.5).
--
-- #2-new (the SHARPENED entry it was replaced by, batch 243-A, in a NEW file): the l < 0 faces of
-- (8.8.41) at the honest field, OFF the landed generator chamber (batch 202) --- the (8.6.25)/(8.6.27)
-- matching's free-field half, the mode action on the normally-ordered blocks.
MM.FLM810NRA.negativeResidual_aligned (C : EvenCocycle L form) (h2 : (2:F) ≠ 0) :
    MM.FLM810ASM.NegativeResidual (F := F) bL form (C.toCentralExtension (F := F) h2)
```

The 8.10.2 file's own copy of #2 (`MM.FLM810T8102S.negativeResidual_evenCocycle`) is a definitional
projection from #2; it carries `sorryAx` through that hole and is not a separate register.

| # | FLM (printed page) | what the hole is | what its proof needs | ledger |
| --- | --- | --- | --- | --- |
| 1 | (8.6.23)/(8.6.24), the proof of Theorem 8.6.1 (pp. 205--210) | the DISPLAY: the cross contraction of the normally-ordered (8.6.9) object of `alpha_c(-r)u` with `Y(v,z_2)` --- with the window synchronization ABSORBED (batch 225), no mode labels or groundedness needed (batch 226), and identified with the source's (8.6.3) (batch 227).  All its currencies are one statement: `DisplayAllStates` = `DisplayModeStep` = `CommutatorInsertion8625 E (honestIns8625 E)` = `Corollary851SpanningEventualWindows` = `GroundedModeStepAtStates` = `Theorem861SourceStatement` at the labelled (8.6.2) pairs | Route A (source, `MMFLM86SpineGap.lean` PHASE A `:36`--`:213` is the per-step map): land the general-`k` multi-variable series of states (8.6.5) and the (8.6.8) layer, the OPE (8.6.12), the coefficient extraction (8.6.15)--(8.6.21), and the contraction (8.6.23)/(8.6.24); already proved on that route: (8.6.6)'s second equality all `k` (`display866SecondEqK_all`), the mode--field commutator (8.6.9)/(8.6.10) at all states (`ModeFieldCommInput`), (8.6.11)/(8.6.13)/(8.6.14)/(8.6.22).  Route B (direct): the anchor dictionary (`MMFLM86MLA`, `MMFLM86NTR`), the contraction engines for lattice monomials (`MMFLM84Contraction`, `MMFLM86ExpProduct`, `MMFLM86CommIota`), `MMFLM86RI.*`, plus the landed lattice/display corners | `HANDOVER` §1 (this row), §6 item 4; `HANDOVER` §6 item 1   **Batch 234 (`Definitions/MMFLM810Theorem861Stated.lean` §2)**: the book's own steps (8.6.11)--(8.6.27) are absorbed at this datum --- the proved ones as THEOREMS (`modeFieldCommInput_evenCocycle`, the (8.6.9)/(8.6.10) input of batch 219-B; `commutatorHalf_of_step`, (8.6.23)/(8.6.24) from the proved input plus the ONE named (8.4.25) step; `modeStepExists_of_twoHalves`, the landed bridge to the (8.5.13) mode step) --- and the hole is now machine-visibly the conjunction of TWO named halves: the ITERATE half `IterateInsertion8625` (the (8.6.25)/(8.6.27) matching = nonneg PROVED + residual #3 + residual #4) and the COMMUTATOR half `CommutatorInsertion8625` (the (8.4.25) cross contraction = `ModeFieldCommInsertionStep8625`).  (`NOTES.md` §132)   **Batch 235 (`Definitions/MMFLM810Theorem861Stated.lean`)**: the single `sorry` of Theorem 8.6.1 is SHARPENED to the book's own (8.4.25) cross contraction --- `MM.FLM810T861S.crossContraction_evenCocycle`, i.e. `ModeFieldCommInsertionStep8625` at the honest insertion --- and the DISPLAY itself is now PROVED from it (through the landed both-way `MM.FLM86DP.displayAllStates_iff_commutatorInsertion8625`), with the proved (8.6.9)/(8.6.10) input in between; the matching (residuals #3/#4) is NOT part of Theorem 8.6.1's display.  (`NOTES.md` §133)   |
| 2 | (8.8.41) at `l < 0` (p. 234) | the `l < 0` faces at pairs that are NOT lattice generators with `0 <= <a,b>`; the generator chamber is a theorem (batch 202), as are the `l >= 0` faces at every state/pairing and the finiteness conjuncts | the `(z_1-z_2)^l`/normal-ordering engine at non-generator states and negative pairings, with the `l >= 0` translate argument of `MMFLM810AssemblyAux` as the model; the Fock half (#3) is its expected main input.  Once this falls, `faces_iff_split` closes the whole Jacobi identity at the boundary field | `HANDOVER` §6 item 2  **Batch 237-A**: the registered hole is the SOURCE-FAITHFUL form `MM.FLM88T889S.theorem889_faithful` (`FacesAtStates`); the batch-229 uniform-window statements were vacuous (`MM.FLM810JBAux.jacobiIdentity_zero_window`) and are now proved + marked (`NOTES.md` §137) |
| 3 | (8.6.25)/(8.6.27) (p. 210), the Fock half | the mode action on the normal-ordered blocks | **REMOVED from the ledger (batch 239-A)**: it was off Theorem 8.10.2's path (batch 238-A) and its content is part of #2's proof (the book proves 8.8.9 by repeating 8.6.1's proof, whose iterate side is (8.6.25)/(8.6.27)); the Prop `MM.FLM86NPFS.FockStep`, every landed bridge and batch 233's reindexing (`MMFLM86ModeBlockReindex.lean`, `NOTES.md` §131) stay in the tree (`NOTES.md` §139) |
| 4 | (8.6.25)/(8.6.27), second slot `l >= 1` | the `l >= 1` coefficient `honestBlockCoeffJL`; strictly additional to #3 (machine-checked, `honestBlockCoeffJL_one_rankOne`) | **REMOVED from the ledger (batch 239-A)** (same reading as #3; the Prop stays).  **Batch 240-A**: the slot's `l`-general SUPPORT/ARITHMETIC layer is landed (`Definitions/MMFLM86SlotWindowL.lean`, `MM.FLM86SWL`: the `l`-general canonical window, the block's vanishing outside it, the coefficient shift `coeff_{l1+l2}(Q) = coeff_{l1}(Q-l2)`, the reindexed `p`-form --- `NOTES.md` §140); what remains is the LHS evaluation, i.e. the mode-crossing engine --- the same one #1 needs |

### 1.2 The one non-mathematical gap: the six boundary inputs

`hnd` (nondegenerate form), `hs` (the (7.1.1) symmetry), `C` (an even cocycle), `h2` (`(2:F) ≠ 0`,
free under `[CharZero F]`), `S`/`hW` (a weight grading agreeing with the lattice weight pieces) and
`hfin` (the weight pieces finite).  They are parameters of every boundary theorem
(`HANDOVER` §6 item 3).  Instantiating them for a concrete positive-definite even lattice turns
`theorem8102_evenCocycle` from its hypothesis form into the unconditional statement.

### 1.3 What is NOT part of the gap (do not redo)

Everything in §2, and in particular: the equivalence of all currencies of #1; the split of the
Jacobi identity into faces (`faces_iff_split`) with the finiteness (8.10.5) and the `l >= 0` faces
proved; the nonnegative-pairing face of the matching; the lattice corner of (8.5.13); the insertion
conjunct of the package (redundant, `insertionConjunct8625_of_spanningEventual`); the reduction
from the package to the matching + windows (both ways).

## 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`, `MM.FLM86DP.displayAtPair_zAligned_iff_groundedPairWindow`, `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) finiteness | `MM.FLM86RI.exists_iterateOf_zAligned_eq_zero`, `MM.FLM810ASM.faceWindows_zAligned` |
| the delivery (both ways, no hypotheses) | `MM.FLM810BC.theorem8102_of_correctedResiduals`/`_correctedNormal`; `MM.FLM86M8625P.theorem8102_of_matching_and_windows`; `MM.FLM86WSD.theorem8102_of_matching_and_groundedStep`; `MM.FLM86WSA.theorem8102_of_matching_and_commutatorHalf` |

## 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.
The legacy scalar proxies `MM.FLM86.theorem861Residue`, `MM.FLM86.Theorem861`,
`MM.FLM86.Theorem861Statement` are NOT Theorem 8.6.1 (their `p = 0` slice is the genuine (8.5.13)).

## 4. Module map (start here)

* the three statement-only deliveries: `MMFLM810Theorem861Stated.lean` (`MM.FLM810T861S`),
  `MMFLM88Theorem889Stated.lean` (`MM.FLM88T889S`), `MMFLM810Theorem8102Stated.lean` (`MM.FLM810T8102S`);
* delivery/reduction: `MMFLM810BoundaryCorrected.lean`, `MMFLM86Insertion8625Prove.lean`,
  `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`,
  `MMFLM86NegPairingFockStep.lean`, `MMFLM86ModeBlockReindex.lean` (batch 233: the reindexing of the `MMFLM86SlotWindowL.lean` (batch 240: the (8.6.27) second slot's `l`-general window/coefficient layer);
  two landed engines --- corrects the batch-232 `FockStepRecon` reading, `NOTES.md` §131);
* the section 8.6 engine: `MMFLM86Engine86`, `MMFLM86NestedCauchy*`, `MMFLM86Display866*`, `MMFLM86ModeFieldComm*`;
* the window currencies: `MMFLM86WindowSync{,Delivery,Absorbed}.lean`, `MMFLM86DisplayPair.lean`,
  `MMFLM86SourceBridge.lean`.

## 5. Build and verification discipline (mandatory)

* On THIS machine the driver is
  `powershell -NoProfile -ExecutionPolicy Bypass -File tools/build.ps1 <file.lean> [...]`; `tools/build.sh`
  is the Linux port (it hard-codes `/home/li/...` and is not usable here).  Pass prerequisites BEFORE
  dependents on the same command line.  Success = `--- OK: <file> ---` AND driver exit 0; read the FULL log.
* `python3 Probe/forbidden_tokens.py <explicit file list>` -> all zeros **except** the files carrying a
  registered `sorry` (see §0/§1 and `README.md`'s map).  The per-batch `sorry` policy is in §0.
* `#guard_msgs in #print axioms` for EVERY public declaration, docstring = the printed message VERBATIM.
  A proved declaration prints `[propext, Classical.choice, Quot.sound]`; one that consumes a registered
  `sorry` prints `[propext, sorryAx, Classical.choice, Quot.sound]`.  **`#guard_msgs` does NOT normalise
  whitespace**: long messages wrap (name-dependently, at 120 chars) and the guard text must be the wrapped
  form --- measure first, then write (batches 156/157/231 measured it).
  MEASURED TRAP: an elaboration failure silently becomes `sorryAx` and the guard mismatch is the only
  symptom --- this fired in batches 198, 208, 209, 216 and was caught every time.
* Acceptance: build `FinalCheck.lean` once per batch (add the new imports first).
* ONE `lean` process at a time (~4.2 GB each); re-verify an agent's files AFTER its last write.
* Subagents never commit and never edit existing files; the dispatcher commits by explicit path.

## 6. Next steps in priority order

**The registry is §1.1: TWO `sorry`s, and both are the SAME engine** --- the §8.6 mode-crossing /
normal-ordering engine (moving one creation mode past the other side's field):
`crossContraction_evenCocycle` IS the window-synchronized (8.5.13) (batch 223-B, both ways), and
`theorem889_faithful`'s `l = 0` face is that same (8.5.13)/display while its `l < 0` slice is the
negative (Fock) face of the (8.6.25)/(8.6.27) matching.

1. **The assembly at the face (the recorded shape, batch 233 §3 + batch 240-A).**  Engine (L) is the
   guarded `MM.FLM86MLA.actionFamily_factorFactorZero_modeVL` (the (8.6.9)/(8.4.16) law at an
   arbitrary accumulated field) and engine (R) is the guarded
   `MM.FLM86ZOF.normOrdered2_modeVL_sub` (the (8.6.6) law at every block); the reindexing they perform
   is proved (`MMFLM86ModeBlockReindex.lean`: the shifted copies at `m-r`, `honestBlockCoeffJ_shift`,
   `blockSum_shift_image`, `blockSum_modeVL_creation`), and the second slot's `l`-general
   window/coefficient layer is proved (`MMFLM86SlotWindowL.lean`, batch 240-A).  Next sub-target:
   instantiate (L) at the face's field (`Yt = YzeroField baseAligned (iota b)`, `gamma = <c,b>`,
   `delta = 0`), read it through `MM.FLM84TV.reflectFam` (`k ↦ -k-1`), cancel the `gamma`-half against
   `blockSum_shift_image`, and match the `kappa`-half against the MIXED sum (coefficients at `m`,
   blocks at `m-r`).  The step consumes the face at `m-r`, so the induction runs on the all-`m`
   strengthened face.
2. **`theorem889_faithful`, the `l < 0` slice** --- after the engine is assembled, the `l < 0`
   faces at non-generator pairs follow the `l >= 0` translate argument of `MMFLM810AssemblyAux`;
   `faces_iff_split` then closes the whole Jacobi identity at the boundary field, making Theorem 8.8.9
   `sorry`-free.
3. **The six boundary inputs** --- instantiate for a concrete positive-definite even lattice (the
   unconditional statement of Theorem 8.10.2).

## 7. Where the history lives

* `NOTES.md` --- **the work log**: `§§64--129` topic-wise (analysis, accounting, corrections of
  record, refuted spellings, the `sorry` policy of §127, this batch's records of §128/§129) and
  **Appendix A**, the dispatcher's per-batch records for batches 151--229, moved verbatim out of
  `ROADMAP.md` in batch 230.
* `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); `refs/` --- the auxiliary
  evidence (the book map `refs/FLM-CH8-MAP.md`, the FLT asset surveys, `refs/README.md`).
* `Probe/` --- agent briefs, reports and falsification scripts (gitignored, not committed).
