### 8.4.25
Definitions\MMFLM810BoundaryCorrected.lean:14: (printed p. 199); (8.4.25) (printed pp. 192--193); (7.2.22)/(7.2.23) (printed p. 146);
Definitions\MMFLM810BoundaryCorrected.lean:41: | ModeFieldCommInsertionStep8625 E Ins | (8.6.23)/(8.6.24), printed p. 210, the commutator half | batch 221-B, MMFLM86Matching8625.lean | its input ModeFieldCommInput is a THEOREM 
Definitions\MMFLM810NegCFace.lean:10: (8.4.22)/(8.4.25) (printed pp. 192--193); (8.4.36)/(8.4.40) (the `z_0`-lines); (8.5.11), (8.5.24) and
Definitions\MMFLM810NegOneChambers.lean:9: (8.4.25) (printed pp. 192--193), (8.4.20) (printed p. 192), (8.4.17), (8.5.11) (printed p. 204),
Definitions\MMFLM810NegOneFace.lean:10: (8.10.8) (printed p. 244), and the (8.4.25) product of printed pp. 192--193.
### 8.5.13
Definitions\MMFLM810Assembly.lean:10: Corollary 8.5.1 (8.5.13) (printed p. 200), the finiteness (8.10.5) and the identity (8.10.8)
Definitions\MMFLM810AssemblyAux.lean:10: (printed p. 234), Corollary 8.5.1 (8.5.13) (printed p. 200), and the finiteness (8.10.5)
Definitions\MMFLM810AssemblyGrounded.lean:9: Corollary 8.5.1 (8.5.13) (printed p. 200), the finiteness (8.10.5) (printed p. 244), Corollary 8.5.4
Definitions\MMFLM810AssemblySlices.lean:9: Corollary 8.8.17 (8.8.41) (printed p. 234), Corollary 8.5.1 (8.5.13) (printed p. 200), the
Definitions\MMFLM810BoundaryCorrected.lean:13: Remark 8.6.4 (printed p. 211); Corollary 8.5.1 (8.5.13) (printed p. 200) at the states (8.5.4)
### 8.5.15
Definitions\MMFLM810Fields.lean:130: FLM (8.5.15), printed p. 200, verbatim:
Definitions\MMFLM810NegTwoFace.lean:10: pp. 192--193); (8.5.11), (8.5.15), (8.5.24) (printed pp. 204, 207, 208); the finiteness gloss of
Definitions\MMFLM84VacuumField.lean:20: **Printed p. 200 (PDF page 255).**  The component indexing is introduced in (8.5.15)
Definitions\MMFLM85ConvAdditive.lean:13: **Printed p. 200** (PDF page 255).  (8.5.15), verbatim:
Definitions\MMFLM85ConvProduct.lean:35: FLM (8.5.15), printed p. 200, verbatim: `Y(v,z) = Σ_{n∈Q} v_n z^{−n−1} = Σ_{n∈Q} v_{n−1} z^{−n}`.
### 8.6.23
Definitions\MMFLM810BoundaryCorrected.lean:41: | ModeFieldCommInsertionStep8625 E Ins | (8.6.23)/(8.6.24), printed p. 210, the commutator half | batch 221-B, MMFLM86Matching8625.lean | its input ModeFieldCommInput is a THEOREM 
Definitions\MMFLM86DisplayPair.lean:11: (8.6.23)/(8.6.24) (printed p. 210); Corollary 8.5.1 (8.5.13) (printed p. 200); (8.5.4) (printed
Definitions\MMFLM86Insertion8625Prove.lean:12: (8.6.23)/(8.6.24) (printed p. 210), (8.6.25)/(8.6.27) (printed p. 210) and the closing sentence
Definitions\MMFLM86Insertion8625Prove.lean:18: FLM's (8.6.23)/(8.6.24) (printed p. 210): the coefficient of P = prod w_i^{r_i} x_j^{s_j} in
Definitions\MMFLM86Insertion8625ProveAux.lean:11: (8.6.23)/(8.6.24) (printed p. 210) and (8.6.25)/(8.6.27) (printed p. 210); Corollary 8.5.1
### 8.6.24
Definitions\MMFLM810BoundaryCorrected.lean:41: | ModeFieldCommInsertionStep8625 E Ins | (8.6.23)/(8.6.24), printed p. 210, the commutator half | batch 221-B, MMFLM86Matching8625.lean | its input ModeFieldCommInput is a THEOREM 
Definitions\MMFLM86DisplayPair.lean:11: (8.6.23)/(8.6.24) (printed p. 210); Corollary 8.5.1 (8.5.13) (printed p. 200); (8.5.4) (printed
Definitions\MMFLM86Insertion8625Prove.lean:12: (8.6.23)/(8.6.24) (printed p. 210), (8.6.25)/(8.6.27) (printed p. 210) and the closing sentence
Definitions\MMFLM86Insertion8625Prove.lean:18: FLM's (8.6.23)/(8.6.24) (printed p. 210): the coefficient of P = prod w_i^{r_i} x_j^{s_j} in
Definitions\MMFLM86Insertion8625ProveAux.lean:11: (8.6.23)/(8.6.24) (printed p. 210) and (8.6.25)/(8.6.27) (printed p. 210); Corollary 8.5.1
### 8.6.12
Definitions\MMFLM86Contraction8612.lean:12: (8.6.12) (printed p. 208) is
Definitions\MMFLM86FockBidegreeAux.lean:18: with (8.6.12), printed p. 208:
Definitions\MMFLM86SpineGap.lean:86: * **(8.6.12)** [p. 208] `Y(A,z₁)Y(B,z₂) = 𝟙Y(A,z₁)Y(B,z₂)𝟙 ∏_{i,j}(z₁−z₂+w_i−x_j)^{⟨ā_i,b̄_j⟩}`.
Definitions\MMFLM86SpineGap.lean:158: * **(8.6.28)/(8.6.29)/(8.6.30)** [p. 211, Remark 8.6.4] the formal combination of (8.6.12) and
.\HANDOVER.md:63: | 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)` ---
