## 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.FLM810ASM.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.

