# Notes: what a full formalization of the paper would take

This file records, for each unformalized input of `MM.moonshine_conjecture`, what the paper
proves, what Mathlib has, and what would have to be built.  It is written so that work can be
resumed at any point.

## 0. Environment

* Lean `leanprover/lean4:v4.33.1`; Mathlib pinned to
  `db584cd6d46c92f209a44c0f1c829460d327499d` (`master-2026-08-10`, v4.33.0).
* `.lake/packages/mathlib` is a junction to the already-built Mathlib of this workspace, so no
  Mathlib rebuild is needed.  Lake does not resolve the transitive package paths through the
  junction, so `lake build` (and `lake env lean`) fail with "object file ... does not exist"
  for `Batteries`/`Aesop`; `tools/build.ps1` works around this by passing an explicit
  `LEAN_PATH` built from every package's `.lake/build/lib/lean` directory plus the project's
  own `build/lib/lean`.  Use that driver, or replicate its `LEAN_PATH` construction.
* If the package is ever moved inside a Mathlib workspace (for example to
  `fermats-last-theorem/MonstrousMoonshine/`), plain `lake build` works with no changes,
  since Lake then resolves every package through the manifest of that workspace.

## 1. The monster group

The paper's `M` is the Fischer--Griess sporadic simple group of order
`2⁴⁶·3²⁰·5⁹·7⁶·11²·13³·17·19·23·29·31·41·47·59·71`, acting on the FLM module.

**Mathlib status.**  Nothing.  No sporadic group of any kind; the string "monster" occurs
once in Mathlib, in a bibliography comment in `Mathlib/Algebra/Vertex/HVertexOperator.lean`.

**Least-effort route.**  The Lean 3 project `formalabstracts/formalabstracts` (unmaintained
since 2019) defines it in four lines:

```lean
noncomputable def Y443 : Group := coxeter_group $ matrix_of_graph (coxeter_edges [4,4,3])
private def a  : Y443 := generated_of torso
private def b₁ : Y443 := generated_of $ arm (by to_dfin 0) (by to_dfin 0)
-- ... b₂,c₂,b₃,c₃
noncomputable def spider : Y443 := (a * b₁ * c₁ * a * b₂ * c₂ * a * b₃ * c₃)^10
noncomputable def Monster : Group :=
  mk_ob $ quotient_group.quotient $ is_subgroup.center $ Y443/⟪{spider}⟫
```

i.e. the Coxeter group of the `Y₄₄₃` diagram modulo the spider relation (which yields
`M × C₂`) and then modulo the centre.  Porting this needs
`coxeter_group`, `matrix_of_graph`, `coxeter_edges`, `coxeter_vertices.arm/torso`, and a
quotient of a finitely presented group.  Mario Carneiro called this "the right definition"
on Zulip; Johan Commelin proposed porting it to Lean 4, which has not happened.

**Is that presentation the monster?  Yes — it is a theorem** (verified 2026, this used to be the
project's largest risk):

* **Ivanov, *Y-groups via transitive extension*, J. Algebra 218 (1999) 412--435**: Conway
  conjectured (c. 1980) that the Coxeter diagram `Y555` plus the single spider relation
  `(ab₁c₁ab₂c₂ab₃c₃)¹⁰ = 1` presents `M ≀ C₂`; "**This conjecture was proved by S. P. Norton and
  the author in 1990.**"  Second treatment: Ivanov, *The Monster Group and Majorana Involutions*,
  CUP 2009.
* **Borcherds, *Problems in moonshine* (2001), Problem 5** independently calls it the "Y
  presentation" of the monster [ATLAS], "conjectured by Conway and Norton and finally proved by
  Ivanov ... roughly the presentation of a Coxeter group with one extra relation".  Borcherds
  lists the *connection between this presentation and moonshine* as an **open problem** — the
  presentation is not in doubt, the conceptual link was.
* **Bray's 1997 tables** record the 12-generator `Y₄₄₃` form we use: arms 4, 4, 3; 79 relators
  `12 + 11 + 55 + 1`; same spider relation; with the remark that `Y₅₅₃` and `Y₅₄₃` present the
  same group.  Bray also warns: "There is more than one definition of `Y_pqr` in existence" —
  our convention (arm lengths = components of `[4,4,3]`, every bond labelled `3`) is fixed
  explicitly in `Definitions/MMCoxeter.lean`.

So the `formalabstracts` attribution to a MathOverflow comment should not be propagated as the
justification.  Full quotes are in `refs/README.md`.

**What would still be needed after the port.**  `M` finite, of order
`2⁴⁶·3²⁰·5⁹·7⁶·11²·13³·17·19·23·29·31·41·47·59·71` (task S3).  Because the presentation is now a
theorem, the obligation is "does the presented group have this order" rather than "is the
presentation correct" — still very hard (the monster's smallest faithful permutation degree is
196883), and Lean 3 never proved it.  After that: the conjugacy classes, the character table of
the first seven irreducible representations (used at the end of section 3 of the paper), and the
identification `2²⁴·2·Co₁ = Aut(Λ̂)` used in sections 12--14.

**The Griess-algebra cross-check is not feasible in Mathlib.**  Defining `M` as the isometry
group of the Griess algebra (the note `魔群月光.pdf` suggests exactly this) is a genuinely
*non-circular* route — unlike `M := Aut(V^♮_1)` from the FLM module, which presupposes the
monster action, since FLM construct the module together with the action — but it needs the Leech
lattice, the Griess product on a 196884-dimensional commutative non-associative algebra, and
`Aut` of that.  Mathlib has no Leech lattice and no usable non-associative algebra API.  The cheap
sanity check that *is* available is a nontriviality/abelianisation argument (in the S2 brief).
Two conventions not to mix: the Griess algebra has dimension **196884**, while Griess constructed
the monster as automorphisms of a **196883**-dimensional space, and `196884 = 196883 + 1` is the
first moonshine decomposition.

## 2. The FLM module

**Paper.**  Frenkel--Lepowsky--Meurman, *Vertex operator algebras and the monster* (1988).
`V = ⊕_{n∈ℤ} V_n` with `dim V_n = c(n)`, `V_{−1} = 1`, `V_0 = 0`, and the monster acting and
preserving the vertex algebra structure, the conformal vector and the bilinear form.

**Mathlib status.**  `Mathlib/Algebra/Vertex/VertexOperator.lean` (98 lines) and
`HVertexOperator.lean` (161 lines), by Scott Carnahan, define `HVertexOperator` as
`V →ₗ[R] HahnModule Γ R W` and its `coeff`/`of_coeff` API.  There is **no** vertex algebra
structure (no locality, vacuum, translation axioms), no Virasoro algebra, no module theory,
no Zhu algebra.  The related Mathlib PR #25822 is open and self-described as a testbed.

**What would be needed.**  A vertex algebra structure with the three axioms listed in section
3 of the paper (in the paper's own formulation: a family of bilinear products `u_n v` with
`u_n v = 0` for `n ≫ 0`, the Borcherds identity, and a vacuum `1`), a conformal vector of
central charge 24, the graded pieces as `L₀`-eigenspaces, and the FLM construction itself.
Also needed for sections 6--8: the no-ghost theorem (Goddard--Thorn), which is nowhere in
Lean.

## 3. The replication identity (8.3)

**Paper.**  Sections 6--8:
1. build the monster Lie algebra `M = ⊕_{m,n} M_{m,n}` from `V` as the space of physical
   states of a bosonic string, with `M_{m,n} ≅ V_{mn}` for `(m,n) ≠ (0,0)`;
2. identify it as a generalized Kac--Moody algebra with root lattice `II^{1,1}`, simple roots
   `(1,n)` of multiplicity `c(n)`, and Weyl group of order 2;
3. write its denominator formula `p⁻¹ ∏ (1 − p^m q^n)^{c(mn)} = j(p) − j(q)` and use the
   product formula for `j` to compute the simple roots (Theorem 7.2);
4. compute `H(E)` for the positive-root subalgebra: `H₀ = ℝ`, `H₁ = ∑_{n∈ℤ} V_n p q^n`,
   `H₂ = p ∑_{m>0} V_m p^m`, `H_i = 0` for `i ≥ 3`;
5. substitute into `Λ(E) = H(E)` and take the trace of `g` to get

   `p⁻¹ exp(−∑_{i>0} ∑_{m>0,n∈ℤ} Tr(g^i|V_{mn}) p^{mi} q^{ni}/i) = ∑_m Tr(g|V_m)p^m − ∑_n Tr(g|V_n)q^n`  (8.3).

**Mathlib status.**  Lie algebra homology, exterior powers of graded vector spaces, and
generalized Kac--Moody algebras are all absent.  The trace identity (8.3) itself is formal
power series algebra over `ℚ⟦p,q⟧`, for which Mathlib has `PowerSeries.exp` (`PowerSeries/Exp.lean`)
and `PowerSeries.log` (`PowerSeries/Log.lean`, with `logOf`); note that **`MvPowerSeries.exp`
does not exist**, so a two-variable statement has to be set up as power series in `p` with
coefficients in `HahnSeries ℤ ℚ` (Laurent series in `q`), which does have the needed
`Algebra ℚ` instances.  That was the plan of the (removed) `MMPowerSeries.lean` draft; the
declaration to prove there is, for a finitely supported `c : ℤ → ℤ → ℤ`,

```
PowerSeries.exp _ (∑' n, C (mult m n / m) * X m ...) = 1 + (F - 1)
```

where `F = ∑_m c 1 m p^m − ∑_n c 1 n q^n` and `mult` is the Möbius-inversion expression
(10.4) of the paper.

**What a partial formalization could achieve today.**  Steps (4) and (5) are elementary once
the objects are set up: the homology computation is a statement about exterior powers of a
graded vector space with the degrees given, and (8.3) is a formal power series identity.  A
reasonable intermediate theorem is: *if* the monster Lie algebra has the stated simple roots
and homology, *then* `c` is completely replicable in the sense of `MM.IsReplicable`.  That
would remove the paper's single largest gap (the no-ghost theorem) from the conditional
statement, leaving the Lie-theoretic part.

## 4. The Conway--Norton table (section 9)

**Paper.**
* (8.3) determines the coefficients `c_g(n)` from `c_g(1), c_g(2), c_g(3), c_g(5)` and the
  coefficients of all the powers `g^j` — this is the recursion (9.1), obtained by comparing
  the coefficients of `p²` and `p⁴` of (8.3);
* Koike proved that the modular functions of Conway--Norton's table satisfy the same
  relations;
* seven monster elements of ATLAS type `2B, 3B, 5B, 7B, 9B, 13B, 15D` have a nonsingular
  character matrix `χ_i(g_j)` (determinant `2²²·3⁵·5·7·17`), so the first five coefficients
  of every `T_g` are determined; the first five coefficients of the tabulated functions are
  equal to them.

**What is formalizable here.**  The recursion (9.1) is an identity between integer sequences
and is a candidate for a real proof: it needs the formal power series expansion of (8.3) to
order `p⁴`, which is finite combinatorics.  Once `MM.IsReplicable` is connected to the
recursion, `MM.moonshine_conjecture`'s uniqueness step could be replaced by "the coefficients
agree with the tabulated function's", which is a finite verification per conjugacy class.

**What is not.**  The genus-zero computations for `Γ₀(N)` and its normalizer `Γ₀(N)⁺`
(Riemann surface theory for modular curves; Mathlib has no genus, no modular curve, no
`IsHauptmodul`), and the construction of the `Γ₀(N)⁺` Hauptmoduls as modular functions.  The
`fermats-last-theorem` repository in this workspace has roughly 200 files of modular-curve
infrastructure (`Definitions/Def_ModularCurve_*`) that would be the starting point, but it
also has no genus theory.

## 64. Batch 151, second half: `Hrel` is closed, and three ways a dispatched file lies about itself

**The result.**  `Definitions/MMFLM85HrelClose.lean` (297 lines, 9 guards) proves

    MM.FLM85HrClose.hrel (bL) (form) (base) : MM.FLM85Hr.Hrel (F := F) bL form base

with **no hypothesis on `base`** — FLM (8.5.6), the well-definedness of the (8.5.5) normal-ordered
prescription on the spanning states (8.5.4).  The route is the landed
`MM.FLM85PS.permSpanningStatement` (`ker stateOfVL ≤ permRel ⊔ labelRel`) plus one new lemma for each
summand: the exchange at an *arbitrary* position (`normalOrderedFam_swap_at`, generalising the landed
head-only `MM.FLM85Hr.normalOrderedFam_swap`) and the label additivity at an arbitrary position
(`normalOrderedFam_label_add_at`).  With it, `MM.FLM85Un.generalVertexOperator_existsUnique` produces
the general vertex operator of (8.5.5)–(8.5.6) on all of `V_L` with nothing left to assume, and
`MM.FLM810F.theorem8102_of_hrel_modelBase` loses its last input on the relation side.  Batch 122's
head-only `RelSpanningStatement` stays refuted and is not used.

### 64.1 An unproved declaration with no `sorry` in the file

The file as delivered by the dispatched agent contained a proof whose first line failed to synthesize
`Module.Free ℤ L` (the instance is not derivable from an explicit `bL : Module.Basis κ ℤ L`
parameter).  Lean's diagnostic was one line at that line number; the *consequence* was that the
declaration and everything downstream — including the theorem the file is named for — acquired the
axiom footprint

    [propext, sorryAx, Classical.choice, Quot.sound]

**`Probe/forbidden_tokens.py` reports `sorry=0` on that file and is right to**: there is no `sorry`
token anywhere in the text.  The `sorryAx` enters through the failed elaboration.  So the two checks
this repository treats as acceptance are not redundant and not ordered by strength:

* the token stripper catches a *declared* gap;
* the `#guard_msgs` axiom guards catch a *failed* proof that produced a gap.

A file that passes only the first is a file with an unproved theorem in it, and the guard is the only
thing that says so.  Both were run here; had the guards been written *after* the last green build
instead of carried from the author's intent, the file would have been committed as proved.

### 64.2 A file written against an import closure that was never rebuilt

Two imports were missing — `MMFLM85Action` (for `MM.FLM85Ac.factorFamily`) and `MMFLM85LabelLinearity`
(for `MMFLM85LL.factorFamily_add`).  The author had them in its working closure; the interrupted run
never rebuilt the file from disk.  The lesson is the ordinary one and is recorded only because it
compounded: **the dispatcher's first action on any handed-back file is a build from the file as it
stands on disk, not a read of its header.**

### 64.3 A name that resolves in a minimal probe and not in the file — cause unknown

After the two structural fixes, `MM.FLM85Ac.factorFamily` still failed as a *simple* identifier under
`open FLM85Ac` inside this file (`unknown identifier factorFamily`, with `autoImplicit` suggested),
while the same term resolved in a minimal probe with byte-identical imports, options and `open` list
(`Probe/b151_probe4.lean`, `--- OK ---`, exit 0).  Fully qualifying the two occurrences fixes it.
The cause is **not known** and is recorded as unknown rather than explained away; the practical rule
that follows is cheap and worth keeping: *in a file that references another namespace's value,
qualify it — an `open` that works in a probe is not evidence that it works in the file.*

### 64.4 What is still open, in one paragraph

`Hrel` closed the relation side of the general vertex operator; it did **not** close Theorem 8.6.1.
By `MM.FLM86TDA.residue863_iff_corollary851` the display is *equivalent* to `MM.FLM85Co.Corollary851`
at the states of (8.6.2) — a statement whose every symbol is landed and which mentions no
normal-ordered product — and by `MM.FLM86TDA.display863_of_jacobiIdentity` it follows from a Jacobi
identity plus the finiteness `hvan`.  Two things stand between the repository and it: the **concrete**
field on `V_L` (`annihExp · actVL · creationExpVL`, all landed, unlike the abstract carrier
`MM.FLM87.LatticeElement` which has no annihilation half — §63.2) and its two-point product identity;
and the **uniform-in-`(m,n)`** vanishing `hvan`, which the VOA axioms supply only per component.  Both
are stated with exact types in `Probe/briefs/B151-W3-vacuum851.md` and
`Probe/briefs/B151-W4-assembly.md`.

> **§65 supersedes the last sentence of §64.4.**  The uniform vanishing is *not* a gap: it is the axiom
> (8.10.5) at the pair `(a,b)`, one line (`MM.FLM86UV.exists_uniform_bracketTerm_vanishing`).  What the
> axioms supply only per component is the *operator-valued* `MM.FLM88.JacobiIdentity` window, which the
> display does not consume.

## 65. Batch 152: Theorem 8.6.1's display is a theorem, and the finiteness it needed was an axiom all along

### 65.1 The display, at a fixed window, from two named inputs

`MM.FLM86DVS.display863_fixed_window` (`Definitions/MMFLM86DisplayVOASplit.lean`):

    FaithfulJacobi Y u v  →  (∀ m n i, K ≤ i → bracketTerm (toVertexOp Y) u v m n i = 0)
                          →  1 ≤ K  →  Display863 form E Y u' v' a b K

with `u = stateOf u' a`, `v = stateOf v' b` the states of (8.6.2).  Neither hypothesis restates the
conclusion:

* `MM.FLM810JF.FaithfulJacobi Y u v` is **verbatim the `jacobi` field** of the landed
  `MM.FLM810.VertexOperatorAlgebra` (`MMFLM810Axioms.lean:585`, the field's type being `JacobiAxiom Y`
  = `∀ u v, FaithfulJacobi Y.coeff u v`, `:438`).  So the display is a *consequence of the axiom
  (8.10.8)* for any field that satisfies it — no construction of the field, no normal ordering, no
  two-point product identity.
* the finiteness hypothesis is the source's own parenthetical of (8.5.26).

`display863_of_voa_self` is the same at a structure's own field; `display863_of_remainingFields` states
it at the boundary of `MM.FLM810CA.theorem8102_of_remainingFields` and consumes **only** the
`JacobiAxiom` conjunct of the four `ActionRemainingFields`.

### 65.2 Why the axiom's window suffices here, when it does not for `JacobiIdentity`

`corollary851_of_jacobiIdentity` consumes `MM.FLM88.JacobiIdentity Y u v N`: **one** window for all
monomials, with `MM.FLM88.CrossWindow` (operator-valued vanishing).  The axiom gives neither — it gives
a window per monomial *and per element* — which is why earlier batches recorded a "uniform vs
per-component" gap (§61.2) and why the history of that field records `CrossWindow` as equivalent in
characteristic zero to the vanishing of every component product
(`MMFLM810JB.jacobi8108_iff_zeroProduct`).

The display does not need that.  It is the **`l = 0`** face, and at `l = 0` the two cross sums collapse:
`deltaExpCoeff i 0 = 0` for `i ≥ 1` (`MM.FLM85Ex.deltaExpCoeff`, with `binomCoeff 0 i = 0`), so

    crossBracket Y u v N 0 m n  =  u_m v_n − v_n u_m  =  commutatorFamily Y u v m n

at **every** `N ≥ 1` — the landed `MM.FLM88.crossBracket_zero_eq_commutatorFamily`, whose window
hypothesis is only `1 ≤ N`.  The cross side therefore carries no window at all, the axiom's per-element
freedom has nothing to act on, and the single remaining obligation is the *iterate* side:
`crossIterate Y u v N 0 m n = bracketSum Y u v N m n`, which stops moving once `bracketTerm` vanishes
past `N`.  That is exactly the finiteness hypothesis, and `residue863_of_faithfulJacobi` is the
three-line proof.  **This is the structural reason batch 152's route is short where five earlier batches
were long**: those batches read (8.5.13) at general `l`, where the two windows genuinely differ.

### 65.3 The uniform vanishing is (8.10.5)

FLM's parenthetical at (8.5.26), printed p. 201, is *"`ι(a)_i·ι(b) = 0` for `i` sufficiently large"* —
a statement about the **state**, not about the operator family.  That is verbatim the axiom (8.10.5)
`u_n v = 0 for n sufficiently large` (`MM.FLM810.ComponentTruncation`) at the *pair* `(u,v) = (a,b)`.
`MM.FLM86UV.exists_uniform_bracketTerm_vanishing` is the one-line consequence:

    obtain ⟨N, hN⟩ := A.componentTruncation a b
    ...  bracketTerm = binomCoeff m i • (a_i·b)_{m+n−i} = binomCoeff m i • 0 = 0

with no grading, no homogeneity, no weight, and the window `N.toNat` **independent of `m` and `n`**
because what is killed is the state `a_i·b` and the outer component is linear in it.  The earlier
framing — "the VOA axioms supply truncation *per component*, not uniformly in `(m,n)`" — is therefore
wrong for the pair-indexed form the display consumes.  The window that is genuinely per-component is the
one of the operator-valued `JacobiIdentity`; the display does not use it.

A **second, independent** route is landed for the record:
`bracketTerm_vanishing_of_gradingOn_uniform` gets the same uniform window from the grading (8.5.22) plus
the nonnegativity of (8.10.3), the window being `(S.wt a + S.wt b).toNat`.  Note that the brief's sketch
of this route — "take the maximum of the binomial window `m+1` and the state window" — is
**unnecessary**: the state window alone is already uniform in `(m,n)`, and the binomial `binomCoeff m i`
(which for `m < 0` never vanishes) never enters.

### 65.4 A landed definition that is refutable: `WeightGrading.IsHomogeneousOp`

`MM.FLM85.WeightGrading.IsHomogeneousOp S T p` is

    ∀ a, S.IsHomogeneous a → S.IsHomogeneous (T a) ∧ S.wt (T a) = S.wt a + p.

The weight clause is demanded at `a = 0` too, where it reads `S.wt 0 = S.wt 0 + p`.  Hence
`MM.FLM86UV.isHomogeneousOp_eq_zero`: **`p = 0` for every operator `T`**; `not_isHomogeneousOp`
refutes the predicate at every `p ≠ 0`; and `not_forall_isHomogeneousOp_component` refutes the `∀ n`
form used as the landed (8.5.22) hypothesis.  So every landed lemma whose hypothesis is an
`IsHomogeneousOp` is **vacuous**:

* `MM.FLM85Br.bracketTerm_vanishing_of_grading` (the lemma the (8.5.12) contraction work was built on),
  `MM.FLM85Br.component_eq_zero_of_toNat_le`, `component_eventually_zero`,
  `component_apply_eq_zero_of_weight_lt`;
* `MM.FLM85Br.weightOfComponents_of_isHomogeneousOp` and the whole Corollary 8.5.6 chain
  (`corollary856_iff_componentBracket_of_isHomogeneousOp`, `MMFLM85Corollary.lean:781`);
* the `hOp` parameters of `MMFLM88`'s grading lemmas
  (`componentBracket_of_jacobiIdentity_grading`, `corollary854_of_jacobiIdentity_grading`).

**The repair** is `MM.FLM86UV.IsHomogeneousOpOn`: the same statement with the `T a = 0` case dropped —
precisely the case where `WeightGrading.wt_eq_of_mem` has no content, since it constrains `wt` only on
*nonzero* elements of a graded piece.  `IsHomogeneousOp.isHomogeneousOpOn` records that the landed
predicate implies the repaired one, so the repaired theorems generalise their landed counterparts, and
`*_on` versions of the engine and of the uniform vanishing are landed under it.  Nothing in batch 152's
files consumes `IsHomogeneousOp`.

*The moral, and it is the third of its kind in this project: a hypothesis that has never been
instantiated is a hypothesis that has not been read.  `IsHomogeneousOp` was carried through six batches
of ledger entries as "the landed (8.5.22)" without anyone writing down its `a = 0` instance.*

### 65.5 What Theorem 8.6.1 now rests on

By §65.1 and §65.3 the display for the corrected action prescription is conditional on
`FaithfulJacobi` for that field — i.e. on (8.10.8) — and **nothing else**.  The repository already
reduces that to generators:

    MM.FLM810RR.JacobiOnStateTargets bL form Y   →   MM.FLM810RR.jacobiAxiom_of_stateTargets
                                                 →   JacobiAxiom Y
                                                 →   FaithfulJacobi Y u v

(`Definitions/MMFLM810RemainingReduction.lean:166`, `:180`).  So the chapter's "main commutator result"
is now conditional on **one landed `Prop`**, `MM.FLM810RR.JacobiOnStateTargets`, whose type is a
per-monomial, per-*spanning-state* window plus the component identity.  The two-point product identity of
the concrete field, the normal-ordering identities (8.5.11)/(8.5.12) and the `DiagOrdinary` dictionary —
five batches' worth of residual — are consumed **nowhere** in this route.

Not claimed: FLM's own proof of (8.6.3) through (8.6.11)--(8.6.27).  The display is reached through the
Jacobi axiom, which is the source's own Remark 8.8.11 (*"Theorem 8.6.1 is `Res_{z₀}` of the Jacobi
identity"*), not through the coefficient extraction of §8.6.

## 66. Batch 153, reconnaissance: the residual of Theorem 8.6.1 is not open, it is **false** — and the repair is already landed

Two reconnaissance agents (fresh, self-contained briefs; reports `Probe/B153_R1_PROVED.md`,
`Probe/B153_R2_VOA.md`), plus the dispatcher's own re-verification of every cited line.

### 66.1 The defect, in one line

`MM.FLM85Cp.heisFam a = fun m => modeVL a (−m−1)` is the (8.4.7) Heisenberg field **without its zero
mode**: at the power `m = −1` it evaluates `modeVL a 0`, and `modeVL a 0 = 0` by construction —
whereas FLM (7.1.33)/(7.1.41) has `a(0)` act on the lattice factor by the pairing.  Everything else in
this section follows from that one missing term.

### 66.2 Consequences, all landed and unconditional

* `MM.FLM810MD.l0OnWeightGenerators_forces_zero` (`Definitions/MMFLM810ModesL0.lean:370`): for *any*
  base whose field at `0` is the identity field — in particular the (8.4.17) model base of the §8.10
  assembly — `L0OnWeightGenerators` **forces `k = 0`** at every generator of weight `k`.
  `not_l0OnWeightGenerators_modelBase` (`:398`) is the instance: the predicate is **false** as soon as a
  lattice vector of nonzero even norm exists, which for the Leech lattice (and every nonzero positive
  definite even lattice) it does.
* `MM.FLM810MD.not_translationOnStateData_modelBase`
  (`Definitions/MMFLM810TranslationStateObstruction.lean:271`): `TranslationOnStateData` is false there
  for the same reason (`L(−1)ι(a) = 0` while (8.10.13) demands the derivative of a non-constant field).
* Therefore `MM.FLM810AFT.ActionRemainingFields` is **unsatisfiable** at that field, and
  `MM.FLM810RR.JacobiOnStateTargets` — batch 152's "single named residual" — is *not* a proof
  obligation one can discharge: two of its three sibling conjuncts are false at the same object.

**This retracts, for cause, the closing claim of §65.5** ("Theorem 8.6.1 is now conditional on that one
landed `Prop` and nothing else").  The `Prop` is landed; it is refuted; the correct statement is that
Theorem 8.6.1 is conditional on a field that satisfies the §8.10 axioms, and the repository's assembly
boundary does not produce one.

### 66.3 The repair, landed since batch 80

* `MM.FLM85ZM.heisFamZero` (`Definitions/MMFLM85ZeroModeField.lean:116`): (8.4.7) with
  `hZeroVL (ofLattice a)` at the power `−1`, agreeing with the landed field at every other power
  (`heisFamZero_apply_of_ne`).
* `MM.FLM85ZP.actionPrescriptionTAZero`, and **unconditionally**
  `existsUnique_actionPrescriptionTAZero` (`Definitions/MMFLM85ZeroPrescriptionSpanning.lean`): (8.5.1)
  with (8.5.6) for the corrected prescription.  The relation-spanning input is literally the *same
  proposition* as the landed one — `PermSpanningStatement` has no prescription argument, and `stateOfVL`
  reads only strictly negative modes — so no re-proof was needed and no zero-mode hypothesis enters.
* `MM.FLM810ZMU.Yzero` + `Yzero_spec` + `Yzero_unique`
  (`Definitions/MMFLM810ZeroModeL0Uncond.lean:82`, `:87`, `:107`): the unique concrete `Y` of the
  corrected (8.5.5), with no hypothesis.  **This is the field of the moonshine-module construction.**
* `MM.FLM810ZMW.L0OnWeightGenerators_zero` (`Definitions/MMFLM810L0General.lean:301`): (8.10.12) at the
  vacuum generators for that field, where the landed prescription gave `0`.

`MM.FLM810CA.theorem8102_of_remainingFields` still consumes `actionPrescriptionTA`, and no assembly
line for `actionPrescriptionTAZero` exists.  Batch 153's task P2 builds it.

### 66.4 What is *not* a gap, and what is

* **Not a gap**: the finiteness conjuncts.  `crossWindowVectorwise_of_truncation` and
  `iterateWindowVectorwise_of_truncation` (`MMFLM810JacobiFaithful.lean:186`, `:213`) need only
  `ComponentTruncation`, which is a theorem for the concrete field
  (`MMFLM85ActionTruncationTA.componentTruncation_of_actionPrescriptionTA:63`).
* **Not a gap, but a named open `Prop`**: the display *is* the `l = 0` face of the Jacobi identity
  (`MM.FLM86TDA.display863_iff_corollary851`), and that face is *equivalent* to
  `MM.FLM85Co.Corollary851` (`MMFLM88Jacobi.lean:588`, `corollary851_iff_jacobiIdentity_zero_face`).
* **A gap**: every `l ≠ 0` face.  `Definitions/MMFLM88Jacobi.lean:189` records that the objects FLM
  uses — the localisation `F[z₁,z₂]_S` and the maps `ι_{i₁⋯iₙ}` of (8.10.36)--(8.10.42) — do not exist
  in the repository.
* **A dead route**: the weight/grading route through `IsHomogeneousOp` (unsatisfiable, batch 152), and
  the vendored `VertexAlg` route (a class field with no construction upstream; its carrier is not `VL`;
  its one concrete field is refuted).

### 66.5 What the batch does about it

Two proof tasks on disjoint files, dispatched together:

* **P1** `Definitions/MMFLM86ExpProduct.lean` — the concrete exponential two-point product on `V_L`,
  `Y(ι(a),z₁)Y(ι(b),z₂) = ε(a,b)·:Y(ι(a),z₁)Y(ι(b),z₂):·(z₁−z₂)^{(a,b)}`, and its commutator corollary.
  This is FLM's own engine for Theorem 8.6.1, independent of the §8.10 rationality layer.
* **P2** `Definitions/MMFLM810CorrectedZeroAssembly.lean` — the corrected four-field package and the
  `theorem8102` boundary at `Yzero`, reusing the landed generator reductions verbatim.

The meta-lesson, and it is the fourth of its kind here: **a residual carried across batches as "one
landed `Prop`" had never been instantiated either.**  Batch 152's `IsHomogeneousOp` lesson (a
hypothesis that has never been instantiated has not been read) applies verbatim to the *conclusion*
side: a target that has never been attempted at the object it names has not been read either.  Both
refutations that killed it were already in the repository, in files whose headers say so.

### 66.6 The empty-oscillator case of Theorem 8.6.1 is **one named `Prop`**, and the two mis-shaping defects are now distinct

Measurement agent M1 (`Probe/B153_M1_EXPAPI.md`) mapped the concrete exponential layer.  Three results
change the plan:

1. **The concrete exponentials exist and their contractions are landed.**  `MM.FLMLatSt.creationExpVL`
   (`Definitions/MMFLMLatticeState.lean:199`) is the creation half `E^-`, `MM.FLM84CM.annihExp`
   (`MMFLM84Completion.lean:682`) the annihilation half `E^+`; the five lemmas that move a Heisenberg
   mode or the zero mode past `E^-` are all landed (`modeVL_comm_creationExpVL` at `:375` and `:436`,
   `MMFLM84TwoVarProduct.lean:600`, `hZeroVL_comm_creationExpVL` at `:639`, `hZeroVL_contraction` at
   `:659`, `creationExpVL_mul_actVL` at `:333`).  **No normal-ordered product formula for two creation
   exponentials exists**; the only product statement is the commutation `creationExpVL_comm`
   (`MMFLM84TwoVarProduct.lean:624`).  That is exactly the gap batch 153's task P1 was aimed at, and
   the flat form of it (`creationExpVL a i * creationExpVL b j = creationExpVL b j * creationExpVL a i`)
   is now landed there.
2. **The object mismatch is named.**  `actionPrescriptionTA` folds factors built from
   `heisFam a m = modeVL a (−m−1)` (`MMFLM85Compat.lean:213`), the (8.4.36) display uses
   `modeFam Y a m = Y (iotaVL a) (−m−1)` (`MMFLM8512Done.lean:403`), and the two are identified only by
   `MMFLM8512H.ModeFamHeisShift` (`MMFLM8512Heis.lean:221`) — a `Prop` with **no producer anywhere**.
   So the construction carries *two* independent mis-shaping defects: the missing zero mode (§66.1) and
   this missing dictionary.  Any future plan that assumes the prescription's factors are the field's
   modes is wrong by this `Prop`.
3. **The reduction that matters.**  `theorem842Concrete_iff_corollary851` (`MMFLM8512Done.lean:805`)
   with `theorem842Concrete_iff_apply` (`:793`) makes `Theorem842Concrete Y E a b (form a b) K`
   *equivalent* to `Corollary851 Y (iotaVL a) (iotaVL b) K`; `stateOf_one_eq_iotaVL` is `rfl`, so this is
   `Display863Unshifted form E Y 1 1 a b K` (`MMFLM86TheoremDisplay.lean:163`), the empty-oscillator
   case of (8.6.3)'s second sentence.  **Theorem 8.6.1's `(1,1)` case is therefore a single named
   `Prop`.**  It does **not** lift to general `u', v''`: `theorem861Source_of_coeffFamily_and_spanning`
   (`MMFLM86SpineGap.lean:632`) is proved but needs spanning families with their own coefficient
   conditions, the pure lattice generators do not span `V_L = M(1) ⊗ F{L}`, and the spanning input
   (Remark 8.3.9) is not landed.

Priced remainder, in FLM's own steps: (a) (8.5.12) at `k ≥ 1`, i.e. (8.5.5) at the Fock states
`E_k·ι(a+b)`, plus `ModeFamHeisShift`; (b) the (8.4.35) commutator identity with its contraction
factor; (c) the `z_1 = z_0 + z_2` shifted resummation (`MMFLM86MixedProduct.jointNO:345` lands the
object, `DiagOrdinary` its identification with the iterate, unproved); (d) the Fock half of (8.5.5).

## 67. Batch 153, acceptance: the corrected boundary is landed — and the "repaired" field is a **third** defect

Both proof tasks of §66.5 are accepted, after the dispatcher's own verification: each file was
rebuilt **from a deleted `.olean`** (`tools/build.sh` → `--- OK ---`, exit 0), passes
`Probe/forbidden_tokens.py` at `sorry=0 admit=0 axiom=0 native_decide=0`, and every in-file
`#guard_msgs in #print axioms` guard printed `[propext, Classical.choice, Quot.sound]`; an independent
probe over the headline declarations confirmed the footprints and the exact type of
`MM.FLM810CZA.theorem8102_of_generatorFieldsZero`.

* `Definitions/MMFLM86ExpProduct.lean` (349 lines, `MM.FLM86EP`): `creationExpVL_mul_comm`; the
  concrete two-point product `Yzero_iotaVL_mul_Yzero_iotaVL`; its state form
  `Yzero_iotaVL_apply_iotaVL` ((8.5.11) at `p = 0`); and the commutator family
  `commutatorFamily_Yzero_iotaVL = E.eps a b • X − E.eps b a • X`, `…_eq_c = ((E.c a b − 1) * E.eps b a) • X`.
* `Definitions/MMFLM810CorrectedZeroAssembly.lean` (299 lines, `MM.FLM810CZA`): `componentTruncationZero`,
  `vacuumOperatorZero`, `creationRegularZero`, `creationPropertyZero`,
  `actionRemainingFieldsZero_of_generators`, `theorem8102_of_remainingFieldsZero`,
  `theorem8102_of_generatorFieldsZero` — the corrected Section 8.10 assembly line at `Yzero`.

### 67.1 A wrong-prescription statement with a prescription-free proof

`MM.FLM85ATT.componentTruncation_action_modelBase` / `componentTruncation_of_actionPrescriptionTA`, and
`MM.FLM810AFT.vacuumOperator_action_modelBase` / `creationRegular_action_modelBase` /
`creationProperty_action_modelBase`, all carry a compatibility hypothesis **for
`actionPrescriptionTA`**, although their proofs consume only the underlying `TruncatedField` datum and
its factor list.  So they do not transfer to `Yzero`, and `MMFLM810AFT`'s docstring — which calls them
the fields "of the corrected object" — overstates what the statements say.  (8.10.5) had to be ported
(~40 lines).  The bridges that are generic in the factor list
(`MM.FLM85TAV.actionFold_vacuumNonnegative`, `…_eq_cutOff`, `…_zero`) transferred with no work, and the
four generator reductions transferred verbatim.

### 67.2 `Yzero` still fails (8.10.13), so the zero mode was not the only defect

`MM.FLM810TR.not_translationOnStateData_modelBase`
(`Definitions/MMFLM810TranslationStateObstruction.lean:271`): `TranslationOnStateData` is **false** for
`vertexOpOfField (Yzero … (modelBaseField E weight))` at the conformal vector whenever
`(form a b : F) ≠ 0` and `actVL E a (iotaVL b) ≠ 0`.  The uniform statement is
`translationOnStateData_modelBase_forces_zero`, whose conclusion is
`(form a b : F) • actVL E a (iotaVL b) = 0`.  So `theorem8102_of_generatorFieldsZero` at that base is
**vacuous**, and the obstruction is the *vacuum-supported base field*, not the missing `a(0)`.

This is the correction of record for §66: the construction carries **three** stacked defects —

1. the missing (7.1.33)/(7.1.41) zero mode in `heisFam` (repaired: `heisFamZero` →
   `actionPrescriptionTAZero` → `Yzero`, all unconditional);
2. the missing grading shift `z^{a(0)}` in the base field.  P1 measured the honest assembled (8.4.17)
   field `MM.FLM84LF.YFam` (`Definitions/MMFLM84LatticeField.lean:720`, the three-factor
   `E^-(z)·(az^∂)·E^+(z)`) and proved `Yzero_iotaVL_apply_iotaVL_eq_YFam`: the model base **is**
   `YFam` at a pairing-shifted index.  `Yzero` is creation-half only and has neither `z^{a(0)}` nor
   `E^+`, which is why no contraction and hence no scalar `(z₁−z₂)^{(a,b)}` appears in its two-point
   product;
3. the missing dictionary `MM.FLM8512H.ModeFamHeisShift` (`MMFLM8512Heis.lean:221`) between the
   prescription's factors `heisFam a m = modeVL a (−m−1)` (`MMFLM85Compat.lean:213`) and the field's
   modes `modeFam Y a m = Y (iotaVL a) (−m−1)` (`MMFLM8512Done.lean:403`).

**The object the next tasks must be stated about is therefore `YFam`, not `Yzero` and not
`modelBaseField`.**  P1's `## What this file does not prove` block names the landed next steps:
`MM.FLM84CT.fullPlus_contraction`, `MM.FLM84RWC.annihExp_mul_creationExpVL_eq_sum_of_subset`
(= `MM.FLM84TV.halfPair2_eq_window_of_subset` with `MM.FLM84RW.ratioCoeff`/`ratioWindow`),
`MM.FLM84LF.YFam_iotaVL_eq_exp`, `MM.FLM85Co.Corollary851`, `MM.FLM86MXP.Display8625One`.

### 67.3 Corrections to the batch's own briefs

* `Yzero` is at `MMFLM810ZeroModeL0Uncond.lean:81`, `Yzero_unique` at `:100` (the briefs said `:82`
  and `:107`).
* The two batch-79 refutations are `MM.FLM810MD.exists_not_l0OnWeightGenerators` (identity base) and
  `MM.FLM810MD.exists_not_translationOnStateData` (counterexample base `translationTestBase`), in
  `Definitions/MMFLM810ModesL0Trans.lean` — **not** at the (8.4.17) model base.  The model-base
  refutation is the separate `MM.FLM810TR.not_translationOnStateData_modelBase` of §67.2.
* The corrected `hL0` of the assembly boundary is already a theorem
  (`MM.FLM810ZMW.L0OnWeightGenerators_zero`, `MMFLM810L0General.lean:301`), so the boundary needs only
  `hjac`/`htrans`/`hvir`.
* Namespaces: `creationExpVL`/`creationExpVL_comm_actVL` are `MM.FLMLatSt.*`
  (`Definitions/MMFLMLatticeState.lean:333`, `:341`); `modeVL_comm_creationExpVL` and
  `hZeroVL_comm_creationExpVL` are `MM.FLM84CT.*`.  `E.eps` is the section 2-cocycle (7.1.12) and
  `E.c` the commutator cocycle (7.1.8), with `E.eps_mul_comm : E.eps a b = E.c a b * E.eps b a`
  (7.1.26) — the product carries `eps`, the commutator's scalar is `(E.c a b − 1) * E.eps b a`.
* API trap, recorded for the next agent: `rw [← sub_smul]` / `simp only [sub_smul]` **fail** on
  `Module.End F V` (the Algebra/Module `smul` instance diamond) even though both sides print
  identically; the fix is `LinearMap.ext` plus `LinearMap.sub_apply`/`smul_apply` with `sub_smul`
  pointwise on `V_L`.

## 68. Batch 156: the `ι` maps exist, and the commutator's real dividing line is the cocycle, not the sign

### 68.1 FLM (8.10.37)–(8.10.42) for `n = 2`, and why the carrier had to be built

`Definitions/MMFLMIotaVar.lean` (`MM.FLMIotaVar`, 852 lines).  FLM's target
`F[[z₁,z₁^{-1},z₂,z₂^{-1}]]` is **not a ring in FLM's use**, and the reason is a landed theorem:
`no_ringHom_monomial` shows that no ring homomorphism into the product model can send `z₁ − z₂` to a
unit, although `z₁ − z₂ ∈ S` by (8.10.36) and the localisation `F[z₁,z₂]_S` inverts it.  So the honest
object is an `F`-linear map into the product space; but each **ordering** does live in a ring, because
expanding first in negative powers of `z_{i_1}` makes the outer exponents well-founded.  The carrier is

    IotaVar F := HahnSeries (OrderDual ℤ) (HahnSeries ℤ F)      -- a field

with two variable assignments, and both incarnations are landed: the ring homs
`iota12Ring`/`iota21Ring : F[z₁,z₂]_S →+* IotaVar F`, and the `F`-linear
`iota12`/`iota21 : F[z₁,z₂]_S → AllSeriesN F 2` that Prop. 8.10.3–8.10.5 consume.

**Injectivity is proved at all three levels**, not cited: the polynomial embeddings (including
`polyToOnePoly_injective`, which the landed `MMFLMLocalization` lacked), the ring homs out of the
localisation (`IsLocalization.lift_injective_iff` plus `IsLocalization.injective` with the landed
`S_le_nonZeroDivisors`), and the readings.  The source says "it is clear that the maps `ι_{i₁⋯i_n}` are
injective"; given that `MM.FLM81.KerThetaStatement` exists because such statements can fail, this is
worth having as a theorem.

**The bound on what the `l ≠ 0` faces can say.**  The delta series is supported on the whole
antidiagonal — unbounded above in the outer exponent — so it is **not an element of the carrier**.  In
the carrier the two readings of `(z₁−z₂)^{-1}` differ by a sign: `iota12_invShift = expand12`,
`iota21_invShift = expand21`, `iota12_sub_iota21_invShift = deltaRatio`.  This is the `n = 2` form of
FLM's Remark 8.10.1, and it is the same phenomenon batch 155 met on the product: the two expansion
orders are not related by a constant, and the difference lives only in the target.

### 68.2 The commutator at the lattice generators: the cocycle is the dividing line

`Definitions/MMFLM86CommIota.lean` (`MM.FLM86CI`, 421 lines).

* `commutator_YFam_eq_twoVarField_sub_swap2` writes the commutator through
  `twoVarField a b − swap2 (twoVarField b a)` **for every pairing** — no sign hypothesis.
* `commutator_YFam_eq_smul_mul_of_nonneg`: at `0 ≤ ⟨a,b⟩` it is the **constant**
  `1 − E.c b a · (−1)^⟨a,b⟩` times the product; **no delta term** in this carrier.
* `evenCocycle_c_mul_neg_one_zpow`: for the source's own even-lattice cocycle
  (`MM.FLMLattice.EvenCocycle`, from the landed `C.c_eq_signPow`) that constant is `1`.  Hence
  `commutator_YFam_eq_zero_of_even`: `[YFam a m, YFam b n] = 0` for `0 ≤ ⟨a,b⟩` at the honest fields and
  the intended cocycle, **unconditionally**.  *This is the compatibility `c(a,b) = (−1)^⟨a,b⟩` that the
  landed `CentralExtension` does not assume and `EvenCocycle` supplies — and it is exactly the
  hypothesis under which Theorem 8.6.1's (8.6.1) is stated.*
* `not_YFamOnGenerators_and_corollary851_rankOne`: the pair `(hY, h851)` is **refuted** at the rank-one
  datum `a = b = 1`, where the constant is `2` for the trivial cocycle and the product is nonzero on the
  vacuum.  So `MM.FLM86II.commutatorFamily_lattice_eq_zero_of_nonneg` is not "the `0 ≤ ⟨a,b⟩` case of
  (8.4.41)" in landed generality: its hypothesis pair is empty at that datum.
* `commutator_rankOne_negTwo_ne_zero`: the commutator is genuinely nonzero at `⟨a,b⟩ = −2`, which is why
  the missing range `⟨a,b⟩ ≤ −2` is not a defect of the formalization: the finite-support carrier cannot
  express `contrFam N` for `N < 0`, and no scalar makes the exchange law hold there
  (`MM.FLM86TS.not_swap2_twoVarField_rankOne`).  The only route to that range is the residue sum of
  (8.5.13) itself.

### 68.3 Theorem 8.10.2, field by field, after this batch

`L0` (8.10.12) is **proved** (`MM.FLM810ZMW.LOf_conformalVectorZero_on_weightPiece`,
`L0OnWeightGenerators_zero`), so it is not an open field.  `Virasoro` (8.10.9) is reduced to two named
`Prop`s (`MM.FLM87ZBC.virasoroOnStateData_of_named`; the honest form is
`MM.FLM87SA.FreeBosonSugawaraBracketZero`, FLM (8.7.9), whose header records it is **not refuted**).
`translation` (8.10.13) is false at the model base and is being tested at the repaired base.  `Jacobi`
(8.10.8) is the only field with no finite reduction, and its `l ≠ 0` faces are now unblocked by §68.1
while its `l = 0` face at negative pairing is blocked by §68.2.

## 69. Campaign state at the end of the batch-157--164 run: what Theorem 8.10.2 now rests on

This section is the **handover**: it lists, for each of the four inputs of
`MM.FLM810TA2.theorem8102_of_generatorFieldsAligned` (Theorem 8.10.2 at the book's field), exactly what
is proved, what is named, and what has no route in the repository.  Everything named here is landed,
verified by the dispatcher by a rebuild from a deleted `.olean` plus token and axiom-guard checks, and
wired into `FinalCheck.lean`.

### 69.1 The alignment (the owner's directive), all four steps landed

1. **The base field**: `MM.FLM85BA.baseAligned` / `genFam E a m := YFam E a (−m−1)`, with
   `baseAligned_zero` (8.5.3) and the **sharp** truncation `genFam_lower_truncation_iotaVL`
   (`m < ⟨a,c⟩ ⇒ 0`), which is the `z^{−(a,a)/2}` of (8.4.17).  The old `modelBase`/`heisFam` are
   defective (no zero mode, no `a z^∂`, no `E^+`) and are **refuted on the sibling axioms**
   (`MM.FLM810MD.not_l0OnWeightGenerators_modelBase`,
   `MM.FLM810TR.not_translationOnStateData_modelBase`).
2. **The canonical field**: `MM.FLM85CF.canonicalField := heisFamZero`, with the defect itself a theorem
   (`splitPlus_defect_at_zero`) and a migration block plus pointer lemmas (the `deprecated` attribute is
   **impossible** cross-module in this pin).
3. **The `^+`-side counterparts**: `MM.FLM85SP`, 17 declarations, with a consumption table.
4. **The assembly**: `MM.FLM810TA2.theorem8102_of_generatorFieldsAligned(_l0)`.

**Why this mattered, in one line each**: with the old field, (8.4.23) is **false** at `p = −1`
(`MM.FLM84DY`), and the "tail Leibniz" shape that two landed files asserted is **false**
(`MM.FLM84TLP.not_tailLeibnizResidual`) — two theorems that would have been "proved" and then built on.

### 69.2 `hL0` (8.10.12) — DISCHARGED

`MM.FLM810TA2.l0OnWeightGenerators_aligned`, from `MM.FLM810ZMW.L0OnWeightGenerators_zero` (which is
base-generic given `(base 0).fam = 1`) plus `baseAligned_zero`.  Needs only `hnd` and symmetry of `form`.

### 69.3 `hvir` (8.10.9) — discharged **modulo a hypothesis that is false on even lattices**

* The bracket FLM (8.7.9) at `c = dim 𝔥` **was already a theorem** (batch 117,
  `MM.FLM87ZBF.freeBosonSugawaraBracketZero_of_orth`), from `hOrth : OrthonormalBasis bL form`.
* `MM.FLM87SBC.not_orthonormalBasis_of_even` proves `hOrth` **false** whenever `2 ∣ (a,a)` — i.e. on the
  Leech lattice, because FLM (8.7.3) asks for an orthonormal basis of the **`F`-space `𝔥 = L ⊗ F`**
  (scaling by `1/√(b_i,b_i)` allowed) while the repository demands it of the **`ℤ`-basis `bL`**.
* Hence `theorem8102_of_generatorFieldsAligned_dimH` has **no Virasoro hypothesis** but does carry
  `hOrth`.  The residual is exactly `MM.FLM87SBC.SugawaraBracketAtDimH` (no `hOrth`).
* `MM.FLM87GS` **refutes the only shortcut**: the Gram twist is not a transport
  (`form_eq_of_gramTwist`: conjugation preserves the CCR coefficient `m⟨a,b⟩`, so the form cannot change;
  `not_gramTwist_rankOne_even`; and `2c² = 1` has no rational solution, so "extend `F`" *is* (8.7.3)).
* **What is needed**: a new **two-contraction** Sugawara computation, the dual pair `(b_i, u^i)` of
  (8.7.2).  Landed starting points are cited in `MM.FLM87GS` §5 — `MM.FLM810CV.dualCoeff`,
  `MM.FLM810ZM.dualHBasis_sum`, `MM.FLM810ZMT.dualCoeff_sum_smul_hBasis`, the unconditional
  decomposition `MM.FLM87ZDG.sugawaraModeZero_apply_eq_regular_add_zeroCorr` with
  `MM.FLM87SG.zeroCorrPart`, and the Gram-weighted `[Z,Z]` bracket `MM.FLM87ZBK.zeroPart_comm`.  **The
  missing piece is the bracket of the regular inverse-Gram part.**  Smallest open case:
  `MM.FLM87GS.RankOneEvenSugawaraBracket` (`rankOneEvenSugawaraBracket_iff` is `Iff.rfl`).

### 69.4 `htrans` (8.10.13) — the induction step and the state half proved, three pieces named

* **Proved**: the corrected-fold Leibniz rule (`MM.FLM810TG.actionFold_deriv_field`,
  `actionFold_deriv_dFold`, with the derivative field `dField`); the **state half**
  `MM.FLM810TG.LMinusOneCreationMode` (`MM.FLM810SHC.lMinusOneCreationMode`, at arbitrary `b` and
  arbitrary vector, no symmetry hypothesis); and the **creation intertwining at arbitrary `w`**
  (`MM.FLM810CI.Yzero_modeVL_eq_actionFamily_nat`), whose enabling tool is `Yzero_trunc` — (8.5.6) at an
  arbitrary vector.
* **Named and open**: (i) the `dFold` assembly of the induction step needs `dFactor (factor n b) =
  n • factor (n+1) b` as bundled `Factor`s (there is no scalar action on `Factor` and no `actionFamily`
  congruence in `Factor.bound`) and the derivation form of the state half at `sugawaraModeZero`;
  (ii) the base case, landed as `MM.FLM810CI.BaseResidual`, **equivalent** to the base-field identity
  `actionFamily (baseFactor a) (base a) = dField (base a)` — i.e. to `MM.FLM84LT.generalStateDeriv`,
  which is the one genuinely open analytic input on this front.
* The reduction is recorded as `MM.FLM810SHC.translationOnStateData_iff_translationResidual`.

### 69.5 `hjac` (8.10.8) — open, with its faces mapped

* The display (Theorem 8.6.1) is a theorem **given** the axiom (batch 152).
* The `l = 0` face is **equivalent** to `MM.FLM85Co.Corollary851`; at the lattice generators the
  commutator vanishes at the intended even cocycle **unconditionally**
  (`MM.FLM86CI.commutator_YFam_eq_zero_of_even`, from `evenCocycle_c_mul_neg_one_zpow`), and the missing
  range is exactly `⟨a,b⟩ ≤ −2`, where the finite-support carrier cannot express the contraction series
  (`commutator_rankOne_negTwo_ne_zero` shows the commutator is genuinely nonzero there).
* The `l ≠ 0` faces have their prerequisite: the several-variable `ι` maps for `n = 2`
  (`MM.FLMIotaVar`), with injectivity proved at three levels and the carrier `IotaVar F :=
  HahnSeries (OrderDual ℤ) (HahnSeries ℤ F)`.
* `MM.FLM810RR.JacobiOnStateTargets` has **no producer** for any field, and the field it used to be
  stated about (`modelBase`/`heisFam`) is refuted on the sibling axioms — so the Jacobi work must be
  done at the aligned field.

### 69.6 Update after batches 163--165: the two fronts have MERGED into one computation

The single most useful thing to know before resuming: **the Virasoro field and the translation field now
depend on the same open input.**

* `MM.FLM810SHC.lMinusOneCreationMode` — the state half of translation, which batch 162 *thought* it had
  closed — carries `hOrth : OrthonormalBasis` (`Definitions/MMFLM810StateHalfClose.lean:226`--`:228`,
  verified by the dispatcher), and `MM.FLM87SBC.not_orthonormalBasis_of_even` shows that hypothesis is
  **false on every even lattice**, the Leech lattice included.
* Batch 165's Y2 then proved `sugawaraDerivation_iff_lMinusOneCreationMode`: the derivation form needed by
  the `dFold` assembly is **exactly** that same statement.  So closing the non-orthonormal Sugawara
  computation discharges the state half of `htrans` **and** `hvir` at once.

**What is landed on that computation** (`MM.FLM87TC`, batch 165 Y1, verified):

    sugawaraModeZero_mul_modeZ_sub : [sugawaraModeZero m, modeZ (bL l) n]
                                   = (((−n : ℤ)) : F) • modeZ (bL l) (m + n)

for an **arbitrary `ℤ`-basis and arbitrary symmetric form, with no `OrthonormalBasis`** — the first
non-orthonormal Sugawara result in the repository, and the whole `[L, mode]` half of (8.7.9).  Plus the
corrected (7.1.33) CCR `modeZ_mul_modeZ_sub` (with the lattice zero mode), the one-contraction pair
identity `normalOrderedHeisPairZero_mul_modeZ_sub`, the Gram collapses `inverseGram_collapse_left`/`_right`,
and the two contraction coefficients `gramContraction`/`gramContraction_transpose`/`normContraction`.

**The one computation that remains** (named in `MM.FLM87TC` §7 as `RegularInverseGramBracket`): the
**double commutator** `[:b_i(m−p)b_j(p):, :b_k(n−q)b_l(q):]`, where *both* contractions occur at once.
The contraction bookkeeping is already measured and is not guesswork any more:

* the **Gram contraction** `Σ_j (M⁻¹)_{ij}⟨b_j,b_l⟩ = δ_{il}` (and its transpose, needing
  `dualCoeff_symm`) is the only contraction in `[L,mode]`, entering **twice** — at `k = −n` against the
  first factor (coefficient `M_{il}`) and at `k = m+n` against the second (`M_{jl}`) — each half giving
  `−n·b_l(m+n)/2`, so that the outer `(1/2)` of (8.7.5) makes the halves sum to `−n·b_l(m+n)`;
* the **trace** `Σ_{ij}(M⁻¹)_{ij}⟨b_i,b_j⟩ = card κ` occurs **only** in the double commutator, and **that
  is where the central charge `dim 𝔥` comes from.**

**Two secondary gaps were measured while doing this, and both are worth stating so they are not
re-discovered:**

1. brackets mixing `sugawaraMode` with `zeroCorrPart` are **not statable today**: `zeroCorrPart` is a plain
   function rather than an endomorphism, and the landed decomposition
   (`MM.FLM87ZDG.sugawaraModeZero_apply_eq_regular_add_zeroCorr`) is pointwise, so a linearity statement
   for it is missing;
2. `Factor`-level scalar bookkeeping is now available (`MM.FLM810DFA.factorSmul`), so the `dFold`
   assembly's piece (1) is closed; the brief's literal `dFactor (factor n b) = n • factor (n+1) b` is not
   even type-correct, and the library's recurrence is the chain-rule orientation
   `X_{n+1} = (n:ℚ)⁻¹ • deriv X_n`.

**And a warning worth keeping**: `MM.FLM87TC` is 509 lines against a 300-line target because the task
forbade a second file; **And a warning worth keeping**: `MM.FLM87TC` is 509 lines against a 300-line target because the task
forbade a second file; the coefficient/CCR layer should be split into a sibling file on the next pass.

## 70. Batch 173: the §8.10 substitution, the Θ corollaries, and what the book's route to Jacobi is

### 70.1 What landed

* `Definitions/MMFLM810RatSubst.lean` (`MM.FLM810RSub`): the substitution σ of (8.10.66), i.e.
  `locSubst : F[z_1,z_2]_S → F[z_1,z_2]_S` with `z_1 ↦ z_0+z_2`, `z_2 ↦ z_2` (source and target are
  the same localisation; index 0 reads `z_1` in the source and `z_0` in the target), by
  `IsLocalization.lift`; its two `@[simp]` generator equations; uniqueness among constants-fixing
  homs; and `rationalForm_locSubst`: (8.10.51)'s shape maps to (8.10.63)'s shape.  **The ledger item
  "the construction of σ is infrastructure of its own" of `MMFLM810RatCoef.lean:258`--`:267` is
  discharged.**
* `Definitions/MMFLM810ThetaKill.lean` (`MM.FLM810TK`): (8.10.73) verbatim; the reusable Laurent
  membership lemma; the general (8.10.46) for a Laurent-polynomial multiplier; and (8.10.72) as
  `recoverySplit_exists`.
* The Θ-side of the §8.10 formal calculus is therefore **complete** for the recovery: (8.10.45) both
  halves (`MMFLM810ADMain`, `MMFLM810IotaEq.lean:127`), (8.10.46) (`MMFLM810ThetaZero.lean:262` plus
  the new general form), (8.10.47) (`MMFLM810IotaEq.lean`), (8.10.72), (8.10.73).

### 70.2 The two false statements this batch found, and the repair

1. **`SubstForm` is too strong.**  It quantifies over *all* ring homs σ with the two generator
   equations, and such a σ need not fix the constants of `F`: for any field endomorphism φ the
   φ-semilinear substitution satisfies the same two equations and sends `locC a` to `locC (φ a)` (the
   side condition survives because φ is injective).  Hence `SubstForm f (locSubst f)` fails for `f`
   with constants over any field with a nontrivial endomorphism (`ℚ(x)`, `𝔽_p(t)`, ...), and
   **`Proposition8104b`/`Proposition8105`, whose conclusion is `SubstForm f h`, are false in that
   generality**.  The correct form is `SubstFormAlg` (constants fixed, equivalently `F`-linear), for
   which `SubstFormAlg f h ↔ h = locSubst f` **is** proved; for `F = ℚ` the two coincide, so the
   moonshine target is unaffected.  **Next pass on the rationality layer must restate those two Props
   with `SubstFormAlg`.**
2. **The "ι-bridge for an arbitrary `VertexOp`" is false** (`not_productRationality`), and the landed
   implication is vacuous (`Jacobi8108 ↔ ZeroProduct`).  This is not an obstacle: in the book the
   bridge is a consequence of **Theorem 8.6.1**, so it must be stated under that hypothesis.

### 70.3 What the book's route to the Jacobi axiom actually is (read from the page images, batch 173)

* Theorem 8.10.2 (printed 245) is the **summary of Chapter 8**; its Jacobi axiom (8.10.8) is
  **Theorem 8.8.9**.
* Theorem 8.8.9's proof (printed 231) is "**We repeat the proof of Theorem 8.6.1** except for the
  following changes: ..." — i.e. the same `P`-coefficient computation, with `x_n` reducing the pole
  order.
* (8.8.39) (printed 233) is "**an interesting alternate form of Theorem 8.6.1**" — so §8.10's forward
  direction (Prop 8.10.3 from the `Res_{z_0}` face) has Theorem 8.6.1 as its input, **not** the Jacobi
  identity.  The ledger sentence at `MMFLM810Rationality.lean:263`--`:269` reading it as circular is
  corrected here.
* **Consequence for the plan.**  The single crux is **Theorem 8.6.1 at the repaired honest field for all
  states** (`Yaligned (C.toCentralExtension h2)`, `C : EvenCocycle`).  From it the book offers two
  continuations: §8.8's repeat of the proof (Jacobi directly), or §8.10's Props 8.10.3--8.10.5 + 8.10.7.
  The campaign's §8.10 infrastructure (ι/Θ/σ/rationality Props) is the second continuation and is now
  nearly complete on the formal-calculus side; the first is untouched.
* **What Theorem 8.6.1 needs, per the batch-153 ledger and this batch's measurements**: the (8.4.25)
  two-point product at the honest field (the landed `MMFLM86ExpProduct` is the creation half only —
  `Yzero (ι(a))_m = actVL a · E^-(a)_m`, missing the grading shift and the annihilation half), the
  `x_n` calculus of (8.6.17)--(8.6.24), and the transfer of the batch-152 display from the old field to
  `baseAligned`.  Batch 153's measured cost of the remaining chapter was ~3.5--6.5 kLoC.

## 71. Batch 174: what is left of Jacobi, and it is now one named `Prop`

### 71.1 The crux, reduced

`Definitions/MMFLM810Theorem861Aligned.lean` (`MM.FLM810T861A`, B174-A) proves, at `1 ≤ K`, the
**equivalence** (`source861Aligned_iff_residual`)

    Theorem861SourceStatement form (C.toCentralExtension h2) (ZAligned E) u' v' a b K
      ↔  Corollary851 (ZAligned E) (stateOf u' a) (stateOf v' b) K,

with `ZAligned E = (vertexOpOfField (Yaligned E)).coeff` the boundary field of Theorem 8.10.2.  So the
whole of `hjac` (8.10.8) — hence the last field of Theorem 8.10.2 — is **Corollary 8.5.1 (8.5.13) at the
(8.6.2) states**, a single named `Prop` (`Residual861Aligned`).  Discharged at that field: (8.6.1) (a
theorem there, `hypothesis861_of_evenCocycle`), integrality (by type), the base (a definition), and the
grading factor (redundant in this carrier).  Proved: the corner `u' = v' = 1`, `0 ≤ ⟨a,b⟩`, every window.

**The old-field obstruction is not applicable**: `not_l0OnWeightGenerators_modelBase` and
`not_translationOnStateData_modelBase` are stated with `hY` about `actionPrescriptionTA … modelBaseField`,
while `Yaligned E` has base `baseAligned E`; the two fields are provably distinct
(`Yaligned_ne_Yzero_modelBaseField`) and both predicates are theorems at the aligned field.

### 71.2 The two halves that remain

1. **The Fock half**: `u', v' ∈ M(1)` arbitrary.  `MMFLM86ExpProductAligned.lean` (B174-B) lands the
   honest-field (8.4.25) product at the lattice states by **reindexing** the already-landed engine
   (`MMFLM86YFamProduct`, B154-Q1; `MMFLM86CommIota`, B156-T2) to `Yaligned`, with
   `Yaligned_mul_eq_sum_ratioCoeff` (`0 ≤ ⟨a,b⟩`, contraction series `ratioCoeff`) and
   `commutatorFamily_Yaligned_eq_smul`.  What is missing for general `u'` is the outer evaluation
   `YFam E a m (creationExpVL b j (anchorVL E b c))` — evaluated nowhere (B154-Q1 residual (i)) — i.e.
   FLM (8.6.10)/(8.5.12): the field at a *created* state.
2. **The negative-pairing lattice case** `ResidueNegativeAligned`: `form a b < 0` at the lattice
   generators.  The finite-support carrier cannot express the contraction series `contrFam N` for
   `N < 0` (refuted: `not_prodExpTwoVarEnd_rankOne`, `not_locallyFinite2_contrFam_of_neg`,
   `ratioCoeff_ne_zero_of_neg`), so this is a carrier-extension question, not a bookkeeping one.

### 71.3 FLM's §8.6 direct route, re-read at the repaired field (B174-A's map)

The repair changes exactly one prerequisite: the (8.5.2) link `Y(ι(a),z) = Y(a,z)`, refuted at the old
model base and now the theorem `yFamOnGenerators_vertexOpOfField_Yaligned`.  Of FLM's proof
(8.6.4)--(8.6.27): proved source-faithful are (8.6.4), (8.6.7), (8.6.11), (8.6.13), (8.6.14) per monomial
and (8.6.22); absent are (8.6.5) (multi-variable series of *states*), (8.6.23)/(8.6.24) (scalar bookkeeping
only) and (8.6.25)--(8.6.27); stated-not-proved are (8.6.6), (8.6.8)--(8.6.10), (8.6.12), (8.6.15),
(8.6.17), and (8.6.20)/(8.6.21) whose commutator side is (8.6.3)'s extraction itself; legacy proxies are
(8.6.16), (8.6.18), (8.6.19).  **The direct route is blocked by three objects the repository does not
have**: the multi-variable series of states (8.6.5), the shifted field `Y(a,z+w)`
((8.6.9)/(8.6.10)), and the `k`-fold normal-ordered product ((8.6.6)/(8.6.8)).  Remark 8.3.9's spanning
for `u, v ∈ V_L` is also unlanded.

### 71.4 What the next batches must do, in order

* **B175-A**: the Fock half of (8.5.13) at `0 ≤ ⟨a,b⟩` — extend
  `corollary851_Yaligned_lattice_of_nonneg` from `u' = v' = 1` to arbitrary `u'`, or land the exact
  obstruction (the created-state evaluation).
* **B175-B**: `ResidueNegativeAligned` — the `⟨a,b⟩ < 0` carrier extension, or the exact statement of
  what the carrier must become.
* Then: the boundary restatement at the even cocycle (`theorem8102_of_hs` carries `E` free and is
  refuted at the trivial cocycle), and the §8.10 or §8.8 continuation from the completed (8.6.3).

## 72. Batch 175: the Fock half reduces to the Fock monomial basis; the negative pairing splits; one missing engine remains

### 72.1 The book's (8.5.13) is the LATTICE case only

FLM p. 195 Theorem 8.4.2 is for `a, b ∈ L̂`, and p. 200 Corollary 8.5.1 says "In the notation of Theorem
8.4.2, [Y(a,z₁),Y(b,z₂)] = Res_{z₀} z₂^{−1}Y(Y(a,z₀)ι(b),z₂)e^{−z₀(∂/∂z₁)}δ(z₁/z₂) (8.5.13)" — no
quantification of its own.  **So (8.5.13) is the lattice states; general `u, v ∈ V_L` is Theorem 8.6.1**,
and the repository's `MM.FLM85Co.Corollary851` at arbitrary `u v : V_L` is *strictly stronger* than the
book's (8.5.13) — it is Theorem 8.6.1's content.

### 72.2 The reduction landed (B175-A, `Definitions/MMFLM85CorollaryFock.lean`)

* Both sides of `Corollary851` are `F`-linear in each state, so it transports along spans:
  `corollary851_of_mem_span`, `corollary851_of_spanning`, `corollary851_iff_spanningStates` (with the
  landed `spanningStatement`).
* **The Fock half is equivalent to its values on the Fock monomial basis**
  (`residual861Aligned_fockBasis_iff`, `corollary851_stateOf_basis`): it suffices to prove
  `Corollary851 (ZAligned E) (stateOf (fockMonomialBasis bL d) a) (stateOf (fockMonomialBasis bL d') b) K`
  for all `d, d'`.  `corollary851_vl_iff_residual861Aligned` shows the general-`V_L` statement is
  equivalent to the Fock-half residual.
* **What does NOT work**: bilinearity alone gives only a spanning family, not a single-oscillator law; no
  lemma computes `Corollary851` at `b_i(−n)·x` from `x`; FLM (8.5.5) coefficientwise at `u = a(−n)x` is
  nowhere landed; and the residue itself contains `Y ((Y (stateOf u' a)) k (stateOf v' b)) j` — the field
  of a created state — which nothing computes.  The mixed case `u' = 1, v'` arbitrary is not free either.

### 72.3 The negative pairing (B175-B, `Definitions/MMFLM86ResidueNegative.lean`)

* The residue is the exact finite (8.5.26) sum, with the `i`-th summand a **positive-degree created
  state** `creationExpVL a ((N:ℤ)−1−i) (anchorVL E a b)`; the top summand `i = N−1` is closed
  (`ι(ab)`), and `residueNegative_split` separates them.
* `ResidueNegativeAligned ↔ NegOneResidualAligned ∧ NegTwoAndBelowResidualAligned`
  (`residueNegativeAligned_iff_negOne_and_below`); the `⟨a,b⟩ = −1` case is *equivalent* to the honest
  commutator (8.4.42) at `YFam` (`negOne_iff_commutator`), so `YFamOnGenerators` being a theorem does
  **not** make it unconditional.
* **The carrier is not the wall.**  `negContraction_tail` proves the contraction series is finite at
  every vector; the (8.4.26)/(8.4.27) two-chamber identity is named `NegativeChamberExpansion (E)`, its
  finiteness half is a theorem and its scalar split is landed
  (`MM.FLM87.expansionA_sub_expansionB_of_neg`).
* The `≤ −2` gap is **not** (8.6.10)/`Display8610List` (that display needs a product the carrier lacks)
  but the two-point (8.5.12) `:Y(a,z₂+w)Y(b,z₂): w^{⟨a,b⟩}` at negative `w`-powers.

### 72.4 What is left, precisely

`hjac` (8.10.8) at the boundary field = `Corollary851 (ZAligned E) u v K` for all `u, v ∈ V_L`
(equivalently the Fock basis), plus the even-cocycle restatement of the boundary.  Both the Fock half and
the negative chamber need **the field at a created state**: FLM (8.5.5) coefficientwise at `Yaligned E`,
equivalently the shifted field (8.6.10) `Y(Y(a,w)ι(1),z) = Y(a,z+w)`.  The named unproved Props for it
are `MM.FLM86SF.Display8610One`/`Display8610List`, `MM.FLM85IS.IterateProductStepAt`/
`IterateProductStepOnCreated`, and `MM.FLM85Co.ProductExpansion` = `MM.FLM85Ext.iterateStatement`
(8.5.12).  Landed starting points for (8.5.5): `Yzero_spec`, `Yzero_unique`,
`generalVertexOperator_existsUnique`.

## 73. Batch 176: the two engines, and a free theorem the agents missed

### 73.1 `NegativeChamberExpansion` was a theorem waiting to be noticed

`MM.FLM86NC.negativeChamberExpansion : NegativeChamberExpansion E` is proved in **11 lines**, because
the equality is the landed `MM.FLM86RX.threshold_holds` (`MMFLM86Reindex8612.lean:880`, for **every**
pairing) and the finiteness is the landed `MM.FLM86RN.negContraction_tail`.  **The wall is not the
chamber expansion but the Θ-collapse**: the landed chain is
`NegOneResidualAligned ↔ NegOneChamberCollapse ↔ NegOneBlockCollapse` (the (8.4.27)
`Θ((1−z)^{−1}) = δ(z)` step on the antidiagonal `P+Q+1`), and
`NegTwoAndBelowResidualAligned ↔ NegTwoChamberResidueIdentity` (which keeps the
`ZAligned`-at-created-states summands and so meets B176-A's gap).

### 73.2 (8.5.5) coefficientwise, and the vacuum field of (8.6.10)

* `Definitions/MMFLM85PrescriptionCoeff.lean` (`MM.FLM85PC`): the (8.5.5) prescription coefficientwise at
  `ZAligned E` (`ZAligned_spec`, `ZAligned_spec_cons` = the (8.4.16) `headOp`+`tailOp` form,
  `ZAligned_creationStep` at an arbitrary vector).  **Already landed at an arbitrary base** as
  `MM.FLM810CI.Yzero_modeVL_eq_actionFamily(_nat)` and `actionPrescriptionTAZero_cons`; these are the
  `ZAligned`-indexed transports.  The `Yzero_unique` route does **not** apply to (8.6.10) (it compares
  state-linear maps, while (8.6.10) constrains one state's value).
* **`vacuumFieldAt_ZAligned : VacuumFieldAt (ZAligned E) vacuumVL` is a theorem**, so at the honest field
  `Display8610List`/`Display8610One` follow from the single input
  `IterateProductStep (ZAligned E) conv` ⟺ `MM.FLM85IS.CreatedStepResidual`
  (`createdStep_ZAligned_iff`), and the k=1 case is the landed (8.5.12) `iterateStatement`.
* The levels: `j = 0` theorem; `j = 1` ⟺ `BaseResidual (baseAligned E)`, and proved on the lattice
  generators; `j ≥ 2` open.

### 73.3 The free theorem (dispatcher)

`MM.FLM810TNO.baseRepaired_eq_baseAligned` (`MMFLM810TheoremNoOrth.lean:97`) and batch 172's
`MM.FLM810CFC.baseResidual_of_currentFieldComm : BaseResidual (baseRepaired E)`
(`MMFLM810CurrentFieldComm.lean:392`) together give **`BaseResidual (baseAligned E)`**, hence by
`display8610One_one_level_iff_baseResidual` the **`j = 1` level of (8.6.10) at `ZAligned E` is
unconditional**.  Neither B176 agent noticed (B176-A calls `BaseResidual` still open).  This is the fifth
"already landed under another name" case of the campaign, and the first one the dispatcher found rather
than a task agent.

### 73.4 The two residuals that remain for `hjac`

1. `MM.FLM85IS.CreatedStepResidual` (equivalently `IterateProductStep (ZAligned E) conv`, i.e. the
   one-step (8.4.25) at created states / (8.6.10)) — levels `j ≤ 1` unconditional after batch 177-A,
   `j ≥ 2` untouched;
2. `MM.FLM86NC.NegOneBlockCollapse` and `NegTwoChamberResidueIdentity` — the Θ-collapse telescoping
   along the antidiagonal, whose scalar shadow is `MM.FLM87.expansionA_sub_expansionB_of_neg`
   (`MMFLMY87.lean:910`).

## 74. Batch 177: (8.6.10) at `k = 1` is free; the non-vacuum one-step and the antidiagonal collapse are what remain

### 74.1 A structural theorem: (8.5.23) + (8.10.13) ⟹ (8.6.10) at `k = 1`

`Definitions/MMFLM85LevelShift.lean` (`MM.FLM85LS`) proves the **base-shifted** recurrence and the tower
collapse, for an arbitrary `VertexOp` with a translation axiom and a creation property:

* `creationCoeff_lminusOne : state_j(L(-1)v) = (j+1)·state_{j+1}(v)` — a pure reindexing of (8.10.13),
  footprint `[propext, Quot.sound]` (strictly smaller than the three-axiom set);
* `levelAt_succ_iff_levelAt_lminusOne : LevelAt Y vac v (j+1) ↔ LevelAt Y vac (L(-1)v) j` (**both**
  directions), `levelAt_succ_iterate_iff_levelAt_one : level (k+1) at v ↔ level 1 at (L(-1))^[k] v`;
* level 0 is the creation property `CreationProperty` (8.5.23), landed for every state at the honest field;
* hence `display8610One_of_creation_translation : CreationProperty Y vac → TranslationAxiom Y om →
  Display8610One Y.coeff a vac` — **(8.5.23) + (8.10.13) ⟹ (8.6.10) at `k = 1`**, with no Jacobi, no
  (8.4.25), no base residual and no uniqueness argument.  (`Yzero_unique` does not apply: it compares
  state-linear maps, while the display constrains one state's value.)  The other recurrence
  `L(-1)·state_j = (j+1)·state_{j+1}` is neither landed nor needed.

At `ZAligned E` (only `hnd`, `hs`): `display8610One_ZAligned`, `levelAt_ZAligned`,
`iterateStatement_ZAligned` ((8.5.12) at `b = ι(1)`) and `iterateProductStepAt_vacuum_ZAligned` — the
**vacuum half** of `IterateProductStep` is a theorem.  The free `j = 1` slice
(`display8610One_one_level_ZAligned`) also follows from batch 172's `BaseResidual` via
`baseRepaired_eq_baseAligned` (the dispatcher's batch-176 finding), as
`baseResidual_baseAligned_of_symm`.

**New exact residual**: `NonvacuumCreatedStep E` — the one-step (8.4.25) at non-vacuum created states
(equivalently `k ≥ 2` of (8.6.10)) — with `createdStepResidual_ZAligned_iff_nonvacuumStep` and
`display8610List_ZAligned_iff_nonvacuumStep` both directions.

### 74.2 `NegOneBlockCollapse` is REFUTED; the corrected residual is `c`-free

`Definitions/MMFLM86NegOneCollapse.lean` + `MMFLM86NegOneCollapseDiag.lean` (`MM.FLM86NOC`):

* `negOneBlockCollapse_eps_add_smul_eq_zero`: if the batch-176 residual held, then
  `(E.eps a b + E.eps b a) • YFam E (a+b) (m+n) v = 0`, because the instances at `(a,b,m,n)` and
  `(b,a,n,m)` are the same two window sums; at `a = b` this kills `YFam E (2a)` with `c a a = 1`.
  `not_negOneBlockCollapse_rankOne` refutes it at the landed rank-one datum (and the general obstruction
  applies to an even form, e.g. hyperbolic `ℤ²` with the trivial cocycle).  **The missing hypothesis is
  the source's (8.6.1) `c(b,a) = −1`.**
* **No pointwise telescoping exists**: the two chamber sums are the two complementary half-lines
  `p ≥ −m` and `p ≤ −m−1` of the same antidiagonal.  The corrected residual is `AntidiagonalCollapse`
  (both half-sums of the single family `normOrdered2 E a b` add to `ε(a,b)·YFam E (a+b)(m+n)`), and
  `negOneBlockCollapse_iff_antidiagonalCollapse (hs) (E) (hc : NegOneSourceCocycle E)` is proved in
  **both** directions.  `NegOneSourceCocycle` holds at the boundary field (`CocycleCompatible` at
  `⟨a,b⟩ = −1` gives `c(b,a) = −1`).
* What remains there is the assembly `(:YY:_{ab})(z,z) = ε(a,b)·Y(a+b,z)` (creation exponentials add,
  annihilation adds, the middle block gives `ε(a,b)(a+b)z^{(a+b)(0)}`).
* `≤ −2`: its summands are `ZAligned` at the (8.5.11) created states = `IterateProductStepOnCreated`;
  **the `−1` case is the first step of that induction and the `≤ −2` case its iterate**, so both agents'
  residuals meet at the same created-state evaluation.

### 74.3 The three residuals left for `hjac`

1. `NonvacuumCreatedStep E` (the non-vacuum one-step);
2. `AntidiagonalCollapse` under `NegOneSourceCocycle` (the `c`-free antidiagonal delta collapse; its
   remaining assembly `(:YY:_{ab})(z,z) = ε(a,b)Y(a+b,z)`);
3. the `≤ −2` iterate, which meets (1).

Everything else — the boundary field, (8.6.1), the Fock spanning reduction, the pairing split, the vacuum
step, the k=1 display — is landed.

## 75. Batch 178: the `conv`-form §8.6 chain is refuted (carrier defect); `AssemblyDiagonal` is the `−1` case's single residual

### 75.1 The refutation, and what it does and does not touch

`Definitions/MMFLM85NonvacuumStep.lean` + `MMFLM85NonvacuumRefute.lean` (`MM.FLM85NV`/`MM.FLM85NVR`):

* `NonvacuumCreatedStep E ↔ SingletonCreatedStep E` (FLM (8.5.23) alone — no list induction) and
  `↔ IterateProductStep (ZAligned E) conv`, and with `hnd/hs` `↔ Display8610Two E` (8.6.10 at `k = 2`,
  which implies every `k`).
* **The one-factor case is FALSE**: `ZAligned E (ι(a)) j ι(1) ≠ 0` for every `j ≤ −1` and `a ≠ 0`, so
  `¬ LocallyFiniteCoef (ZAligned E (ι(a)))`; `conv` is a `dite` on `LocallyFiniteCoef` of its second
  argument, so `conv A (YFam E a) = 0`, and the step at `ι(a)` demands `YFam E a = 0`.  Hence
  `not_nonvacuumCreatedStep_of_ne_zero`, `not_createdStepResidual_ZAligned`,
  `not_iterateProductStep_ZAligned`, `not_display8610List_ZAligned`, `not_display8610Two_of_ne_zero`.
* **Defect class**: the carrier's two-sided `LocallyFiniteCoef` gating (batch 133 refuted the two-sided
  `LocallyFinite2` for `normOrdered2`).  The fix is a **one-sided** product notion consuming (8.10.5)
  (`MM.FLM84LF.YFam_eq_zero_of_gt`) and/or the joint `8…8` object of (8.6.25); the missing FLM object is
  **(8.6.6)'s third family** (`MM.FLM86KF.Display866Family3`) — the ordinary-vs-normal-ordered OPE
  contraction — not the already-landed (8.6.5)/(8.6.9)/`kFoldNormalOrder`.
* **What is NOT touched**: `hjac`/`JacobiAxiom`, and the target `Corollary851 (ZAligned E) u v K`
  (a statement about `commutatorFamily` and the residue, not about `conv`).  Batch 177's `k = 1` theorem
  and the vacuum step stand.  `display8610List_ZAligned_iff_nonvacuumStep` is a valid equivalence between
  two false statements.
* **Trap**: `Definitions/MMFLM85StepLinear.lean` is imported by nothing although `MMFLM85IS`'s header
  cites its `iterateProductStepAt_iff_apply` as landed; without the explicit import the statement
  elaborates with `sorryAx` (the guards catch it).

### 75.2 `AssemblyDiagonal`: the `⟨a,b⟩ = −1` case's single residual

`Definitions/MMFLM86AntidiagonalAssembly.lean` (`MM.FLM86AA`) lands `AssemblyDiagonal (E)` — the
pairing-free (8.4.20) at `z₁ = z₂ = z`: the two half-sums of `normOrdered2 E a b` along the antidiagonal
add to `ε(a,b)·YFam E (a+b)(m+n)` — and proves
`assemblyDiagonal_iff_collapse : NegOneAssemblyDiagonal E ↔ AntidiagonalCollapse E` (both directions),
plus the consumer chain to `negOneResidualAligned_evenCocycle_of_assemblyDiagonal`.  **The hard step is
`expField` multiplicativity** (`E⁻_a(z)E⁻_b(z) = E⁻_{a+b}(z)`), landed nowhere; the landed
`creationExpVL_mul_comm` is commutation only.  Finiteness is already handled by
`normOrdered2_locallyFinite2OneSided`.

### 75.3 The three live residuals for `hjac`

1. `AssemblyDiagonal` (the `⟨a,b⟩ = −1` case), gated by `expField` multiplicativity;
2. the `≤ −2` iterate (`NegTwoChamberResidueIdentity`);
3. the Fock half, whose `conv`-form route is dead and must be rebuilt on a one-sided product.

## 76. Batch 179: the one-sided repair, and `expField` multiplicativity (a new Leibniz rule)

### 76.1 The repair (B179-B, `Definitions/MMFLM85OneSidedProduct.lean` + `MMFLM85OneSidedChain.lean`)

* Defect verbatim: `conv A B` is a `dite` on the **two-sided** `LocallyFiniteCoef B`; the honest field
  only satisfies the upper half ((8.10.5), `YFam_eq_zero_of_gt`), so `conv A (YFam E a) = 0`.
* Repair: `PairFinite A B` (a **pair** datum, not one-sidedness of one argument) and the total
  `convOneSided`, with `convOneSided_eq_conv` (agreement where `conv` was defined),
  `convOneSided_vacuumField(_left)` unconditional, `convOneSided_assoc` on the locally-finite class.
* **`vacuumShiftStep_ZAligned_convOneSided`**: the instance batch 178 refuted for `conv`
  (`not_iterateProductStepAt_ZAligned_iotaVL`) is now a **theorem**, for every `v`.
* New shortest residual: `Display8610TwoOneSided` / `SingletonCreatedStepOneSided`.
* **Two honest fields still do not form a `PairFinite` pair** (`PairFiniteHonestFields` recorded, not
  asserted): the general two-factor display is the **OPE gap** `MM.FLM86KF.Display866Family3`, not a
  carrier problem.

### 76.2 `expField` multiplicativity (B179-A, `Definitions/MMFLM86ExpFieldMul.lean` + `MMFLM86ExpFieldMulLat.lean`)

* `flatMul_expField_of_commute : flatMul (expField Om) (expField Om') = expField (Om + Om')` for
  coefficient-commuting exponents, over an arbitrary `Ring A`/`Algebra ℚ A`.
* **The missing engine was the Leibniz rule** `deriv_flatMul : deriv (flatMul X Y) =
  flatMul (deriv X) Y + flatMul X (deriv Y)` — recorded as open in `MMFLM84Diag`/`MMFLM84Subst` and
  landed here for the first time.
* Steps 1 and 3 of `AssemblyDiagonal` are landed in antidiagonal form
  (`flatMul_creationExpVL`, `sum_creationPair2_antidiagonal`, `flatMul_annihExp`,
  `sum_annihPair2_antidiagonal` — the `E⁺` half on the mirrored families).
* **Steps 2 and 4 are still open**, so `AssemblyDiagonal` stays a `Prop`; step 2 is the named
  `MM.FLM86EFM.MiddleBlockDiagonal` (route recorded: collapse on `F{L}` via `zPowH_iota` and
  `form a c + form b c = N`, then the tensor-factor transfer; three build rounds failed on `iota` defeq
  and induction-motive normalisation).

### 76.3 The live residuals after batch 179

1. `AssemblyDiagonal` — steps 2 (`MiddleBlockDiagonal`) and 4 (nested `convWith2` → `convWith`);
2. the `≤ −2` iterate (`NegTwoChamberResidueIdentity`);
3. the Fock half — its repaired one-sided chain reduces to `Display8610TwoOneSided`, i.e. the OPE third
   family `Display866Family3`.

## 77. Batch 180: `MiddleBlockDiagonal` landed; step 4 is one index-regrouping Prop; the OPE third family corrected and bridged

### 77.1 `AssemblyDiagonal` is now one measured regrouping away

`Definitions/MMFLM86MiddleBlockDiag.lean` + `MMFLM86MiddleBlockDiagStep4.lean` (`MM.FLM86MBD`):

* Step 2 = `middleBlockDiagonal` **is a theorem** (the middle block on the antidiagonal collapses to
  `ε(a,b)·(a+b)z^N`).  The route that works: on `F{L}`, `zPowH_iota` + `form a c + form b c = form (a+b) c`
  for the eigenvalue, then `TensorProduct.induction_on` + `zPowHVL = TensorProduct.map id` +
  `actVL_mul_actVL`; the induction tool is `Finsupp.induction_linear` (add/single) with
  `Finset.sum_subset`, **not** extensionality.
* Step 4 is reduced to the single `def AssemblyDiagonalResidual (E) : Prop` (the double-window sum equals
  `ε(a,b)·YFam (a+b) (−N−1) v`), with `assemblyDiagonal_of_residual : AssemblyDiagonalResidual E →
  AssemblyDiagonal E` **proved** and the reindexing lemmas `diagSum_convWith2`,
  `diagSum_convWith2_nested`, `sum_creationPair2_window` landed.
* **Recipe for the next task**: use a **uniform** middle window `w' q = ⋃_{q∈w}(canonical window)`
  (per-`q` windows leave incomparable `K'`-ranges); group by `J = q.1+q.2` (step 3), then by
  `K' = q'.1+q'.2` (step 2, now a theorem); read `(J,K')` as `YFam`'s `(j,i) = (−J−1,−K'−1)` via
  `YFam_eq_sum_three_factor`.
* So the `⟨a,b⟩ = −1` case at `ZAligned (C.toCentralExtension h2)` is unconditional modulo
  `AssemblyDiagonalResidual` alone.

### 77.2 The OPE third family: a scalar mis-reading corrected, and the bridge landed

`Definitions/MMFLM86OPEThird.lean` (`MM.FLM86OPE`):

* (8.6.6) verbatim (printed p. 206): `A = 8Y(a₁,w₁)…Y(a_k,w_k)8 ι(1) = Y(a₁,w₁)…Y(a_k,w_k)ι(1)
  ∏_{i<j}(w_i−w_j)^{−⟨ā_i,ā_j⟩}`, the factor being the binomial expansion in non-negative powers of
  `w_j`.
* **`MM.FLM86KF.Display866Family3` is not the landed two-variable product**: it reads the printed *series*
  factor as a *scalar* (true only at null exponents) and its type reads the multidegree only in the first
  coordinate.  Landed instead: `Display866Family3TwoIdx` (+ the proved null-pair instance) and
  `Display866Family3Two` (the printed third family at `k = 2`, unconditional for `0 ≤ ⟨a,b⟩`).
* **The bridge**: `shiftedField_ZAligned_apply_eq_sum_ratioCoeff` — (8.4.25) at the **shifted** honest
  fields, i.e. the display's right-hand side evaluated by the landed `normOrdered2`+`ratioCoeff`
  expansion.
* The display's generator slice is `Display8610TwoGenerators`, equivalent (both directions) to the ratio
  form given the **recorded, not asserted** datum `ShiftedPairFiniteGenerators`.  The Fock half stays
  open: the created-state equation, the datum (or a carrier-free replacement), and the arbitrary-`x y`
  display.

### 77.3 The live residuals after batch 180

1. `AssemblyDiagonalResidual` (the measured regrouping) → the `⟨a,b⟩ = −1` case;
2. the `≤ −2` iterate;
3. the Fock half's two-factor created-state display, with the OPE bridge landed.

## 78. Batch 181: `AssemblyDiagonal` is a theorem (the `−1` case closes); `PairFinite` is the Fock fork

### 78.1 Milestone: the `⟨a,b⟩ = −1` case of `hjac` is closed at the boundary field

`Definitions/MMFLM86AssemblyResidualFibers.lean` + `MMFLM86AssemblyResidualAux.lean` +
`MMFLM86AssemblyResidual.lean` (`MM.FLM86AR`):

* `assemblyDiagonalResidual` proved **verbatim** (batch 180-A's def, no weakening), with the new fiber
  lemmas `sum_filter_fiber_eq`, `sum_annihPair2_fiber`, `sum_midBlock2_fiber` and
  `sum_sum_window_regroup`.
* `assemblyDiagonal (hs) (E) : AssemblyDiagonal E` — **a theorem**; with the landed
  `negOneResidualAligned_evenCocycle_of_assemblyDiagonal` this gives
  **`negOneResidualAligned_evenCocycle`**: `NegOneResidualAligned` at `ZAligned (C.toCentralExtension h2)`
  for every symmetric form.  Together with batch 170's `0 ≤ ⟨a,b⟩` corner, **two of the three
  lattice-pair pairing cases are closed**.
* **Method of record**: the middle window must be **one common window for all `q`** (a rectangle
  `WP ×ˢ WQ` of the projections of the per-`q` windows), not a `q`-dependent `⋃`; and pinning the landed
  canonical-window collapses to an arbitrary window needed the fiber lemmas.

### 78.2 The Fock fork: `PairFinite` is UNDECIDED

`Definitions/MMFLM86TwoFactorDisplay.lean` (`MM.FLM86TFD`):

* The display's LHS is evaluated at the `j = l = 0` slice
  (`createdState_zero_zero_apply : ZAligned E (…) (−1) vac = ε(a,b)·ι(a+b)`,
  `createdState_zero_zero_ne_zero`), and `iteratedCreation_two` identifies the LHS state.
* **`convOneSided_eq_zero : ¬ PairFinite A B → convOneSided A B = 0`** (definitional), hence
  `display8610TwoGenerators_false` and `not_display8610TwoOneSided`: at any null pair, a failing
  `PairFinite` **refutes** the display.  The generator slice is exactly
  `[PairFinite datum] ∧ [(8.4.25) ratio form]`.
* **`PairFinite (ZAligned E (ι a)) (ZAligned E (ι b))` is undecided**: batch 179-B's reason for expecting
  failure (a `j`-independent weight summand) only shows all summands lie in one weight space, which is
  infinite-dimensional and compatible with both behaviours.
* **The fork**: if `PairFinite` holds on the needed slices, the Fock half is exactly the created-state
  evaluation — the (8.5.5) prescription of the coherent state
  `YFam E a (−j−1)(creationExpVL b l (ι b))`, **not** a (8.5.4) state for `l > 0`; if it fails, the display
  is false and the honest replacement is the OPE product `Display866Family3Two` (landed for `0 ≤ ⟨a,b⟩`).
* The span reduction cannot be transported through the `dite` carrier (linearity holds only with the datum
  fixed), so the arbitrary-`x y` half is blocked by the carrier, not by spanning.

### 78.3 The residuals after batch 181

1. the `⟨a,b⟩ ≤ −2` case (`NegTwoAndBelowResidualAligned` / `NegTwoChamberResidueIdentity`);
2. the Fock half — decide `PairFinite` (fork above), then either the created-state evaluation or the OPE
   replacement;
3. the final boundary restatement at the even cocycle.

**Superseded by §79 (batch 182): `PairFinite` is PROVED on the honest pairs with `0 ≤ ⟨a,b⟩`; the
"infinite sum" reading above is FALSE.**

## 79. Batch 182: `PairFinite` PROVED (the Fock fork closes); `⟨a,b⟩ = −2` reduced to `NegTwoBlockCollapse`; corrections of record

### 79.1 CORRECTION OF RECORD — the "infinite sum" claim of §§75--78 is FALSE

The paragraphs in §§75--78 (and in `MMFLM85OneSidedProduct.lean`, `MMFLM85OneSidedChain.lean`,
`MMFLM86OPEThird.lean`, `MMFLM86TwoFactorDisplay.lean`) that assert that two honest fields do **not**
form a `PairFinite` pair, on the grounds that the summand weight is `j`-independent, are **wrong**:

* `MM.FLM85PFD.pairFinite_ZAligned_iotaVL` / `pairFinite_yFam` /
  `pairFinite_shiftedField_ZAligned_iotaVL` / `pairFiniteHonestFields_of_nonneg` **prove** the datum
  whenever `0 ≤ ⟨a,b⟩`; the key identity is (8.4.25) along the diagonal `(m−1−j, j)`, where the two
  `normOrdered2` indices move **oppositely** in `j`, and the per-state (8.10.5) bounds give the window
  `Icc (K1+m+1) (−K2−2)`.  Weight-independence is compatible with finite support, and the support is
  finite.
* The citation of "FLM Remark 8.5.2" was a misreading: that Remark (printed p. 200) says the
  *created-state* identity (8.5.14) is not rigorous; **Corollary 8.5.4 (printed p. 201) records "the sum
  being finite"**.
* Consequently `not_display8610TwoGenerators`, `display8610TwoGenerators_false` and
  `not_display8610TwoOneSided` have an **unsatisfiable** hypothesis where `0 ≤ ⟨a,b⟩` — they are
  vacuous, not refutations (`not_not_pairFinite_ZAligned_iotaVL`).
* The dispatcher rewrote the five false docstring paragraphs in place as "CORRECTION OF RECORD (batch
  182)" blocks and rebuilt the four modules.

### 79.2 What is now exact

* `shiftedPairFiniteGenerators_of_nonneg` — batch 180-B's recorded datum is a **theorem** (symmetric
  form, `∀ a b, 0 ≤ form a b`).
* `display8610TwoGenerators_iff_ratioForm_of_nonneg` — the display's generator slice **is** the landed
  (8.4.25) ratio form, in both directions, with the datum discharged.
* **The Fock residual is the created-state evaluation** (`display8610TwoGenerators_iff_createdState`):
  the (8.5.5) reading of `YFam E a (−j−1) (creationExpVL b l (ι b))` for `l > 0`; plus `PairFinite`
  for `form a b < 0`, where the honest replacement is the OPE third family `Display866Family3Two`.

### 79.3 The `⟨a,b⟩ = −2` residue

`Definitions/MMFLM86NegTwoResidue.lean` (`MM.FLM86NTR`): the whole `N = 2` residue equals two closed
terms (`residueSum_negTwo_two_terms`, via `coherentField_one` and `ZAligned_anchorVL`), so the exact
residual is the commutator side, named `NegTwoBlockCollapse` (the (8.4.26) chamber difference at
`⟨a,b⟩ = −2`), with `negTwoExactResidualAligned_iff_blockCollapse` both directions.  Composition with
the closed `−1` chain: `residueNegativeAligned_evenCocycle_iff_negTwoAndBelow` — at
`C.toCentralExtension h2` the negative-pairing residue is exactly `NegTwoBlockCollapse` +
`NegThreeAndBelowResidualAligned`.

**Source-language finding**: the residue's states are the coefficients of the **negative** powers
`z_0^{−N}…z_0^{−1}` of `Y(a,z_0)ι(b)`, while the landed display language is `ℕ`-indexed and *defines*
the negative-power coefficients to be `0` (`creationCoeffZ_of_neg`) — the landed (8.6.10) cannot state
the evaluations the residue needs.  Also `MM.FLM8512.rhsFam`/`MM.FLM84T.coeff40Family` use
`opOpenBox`/`openBoxCoeff`, which **drop the `^+` tail** of (8.4.16); residuals must use the honest
`actionFamily` form.

### 79.4 The residuals after batch 182

1. `NegTwoBlockCollapse` (`⟨a,b⟩ = −2`) — the batch-181 machinery one order higher;
2. `NegThreeAndBelowResidualAligned` (`≤ −3`) — needs a closed form for the iterated (8.5.5) at degree
   `≥ 2`;
3. the Fock half's created-state evaluation `ZAligned E (creationExpVL a k (anchorVL E a b))` for general
   `k` (shared with (2));
4. the boundary restatement at the even cocycle.

## 81. Batch 184: the `−2` residual is the `p = 1` line of `diagFam`; the mode intertwining evaluates the Fock LHS

*(File order note: this section sits before §80 (batch 183) in the file; §80 is the batch that precedes it
chronologically.  The `ROADMAP.md` log is in order.)*

### 81.1 `NegTwoDisplayZOne`: the exact `⟨a,b⟩ = −2` residual

`Definitions/MMFLM86NegTwoWeighted.lean` (`MM.FLM86NTW`):

* The batch-183-A weighted line is **equivalent, both directions**, to the `p = 1` coefficient of the
  **landed display family** `MM.FLM86D86.diagFam`/`displayP`:
  `NegTwoDisplayZOne (E)` — for `form a b = −2`, `diagSumWeighted (fun p ↦ (p:F)) (normOrdered2 E a b)`
  on a window equals `iteratePow (ZAligned E) (ι a) (ι b) (form a b + 1) (m+n) v`.
* Landed equivalences: `zOneLine_iff_displayZOne`, `negTwoDiagonalWeight_iff_displayZOne`,
  `negTwoExactResidualAligned_iff_displayZOne` (under `c(b,a) = 1`), and
  **`negTwoExactResidualAligned_evenCocycle_iff_displayZOne`** with the cocycle discharged at
  `C.toCentralExtension h2`; consumer `residueNegativeAligned_evenCocycle_of_displayZOne`.
* `diagFam_zero_eq_diagSum` shows **the `p = 0` line IS the landed `assemblyDiagonal`** — so a
  recursion in `p` for `diagFam` would close `p = 1` from landed material (the batch-185-A target).
* **Route corrections**: the weight is the (8.2.14) falling factorial `m`, not a differentiated (8.4.25)
  expansion (the "derivative" is only the trivial `p = m+1` reindexing,
  `diagSumWeighted_eq_diagSum_firstDeriv`); and the landed (8.4.40) `z_0^1` lemmas carry a negative-power
  vanishing `hX` that is **false** for `YFam E a` (component `−1` is nonzero at pairing `−1`), so they do
  not apply at the boundary field.

### 81.2 The mode intertwining, and the Fock LHS evaluated

`Definitions/MMFLM86ModeIntertwine.lean` (`MM.FLM86MI`):

* `modeIntertwine : YFam E a M1 (ZAligned E (ι b) M2 v) = Σ_{i ≤ ⟨a,b⟩} ratioCoeff ⟨a,b⟩ i •
  normOrdered2 a b (−M1−1+i−⟨a,b⟩) (−M2−1−i) v` — the honest mode of `a` on an honest-mode-created state
  is the finite (8.4.25) ratio sum of normal-ordered blocks.
* `ZAligned_createdState` evaluates the **Fock LHS** `ZAligned E (YFam E a (−j−1)(creationExpVL b l (ι b)))`
  as a finite ratio sum of batch 183-B's `coherentFieldNat` at the **coherent anchors**;
  `display8610TwoGenerators_iff_coherentForm` (both directions) identifies the display's generator slice
  with `CoherentCreatedForm`.
* `normOrdered2_vacuum` / `ZAligned_normOrdered2_vacuum`: the block on `ι(1)` is the double coherent
  state, and its field is the coherent recursion.
* **`ZAligned_JZF_eq : FLM810JZF.ZAligned = FLM810JF2.ZAligned`** — the two definitionally equal but
  syntactically distinct copies of `ZAligned`; `rw` cannot cross them (CF2 speaks JZF, the (8.6.10) chain
  speaks JF2).  Successors must use this bridge.
* Correction: the Fock mode is the assembled `YFam` (an infinite mode combination on a lattice
  generator), so the (8.5.5) step lemmas `ZAligned_creationStep`/`ZAligned_spec_cons` do **not** apply.

### 81.3 The residuals after batch 184

1. `NegTwoDisplayZOne` — the `p = 1` line of `diagFam` (a `p`-recursion would give it from the landed
   `p = 0` = `assemblyDiagonal`);
2. the `≤ −3` case (coherent-recursion form `NegThreeExpandedResidualAligned`);
3. `CoherentCreatedForm` — the (8.6.9)/(8.6.10)-at-`k = 2` re-expansion (the Fock half);
4. the boundary restatement at the even cocycle.

## 80. Batch 183: the `−2` line is WEIGHTED (and needs the source cocycle); the coherent-state field is a recursion

### 80.1 `NegTwoBlockCollapse` is refuted as stated; the corrected residual is `NegTwoDiagonalWeight`

`Definitions/MMFLM86NegTwoDiagonal.lean` + `MMFLM86NegTwoBlockCollapse.lean` +
`MMFLM86NegTwoBlockCollapseAux.lean` (`MM.FLM86NTD`/`MM.FLM86NTB`):

* The batch-182-B residual carries no cocycle hypothesis, and that is fatal: it forces
  `(E.eps a b − E.eps b a) • YFam E (a+b) (N−1) v = 0` for all `N,v`, i.e. `c(a,b) = 1` or
  `YFam E (a+b) ≡ 0` — the analogue of batch 177-B's refutation of `NegOneBlockCollapse`.  At
  `⟨a,b⟩ = −2` the source's (8.4.34) `c(a,b) = (−1)^{⟨a,b⟩}` **is** `c(a,b) = 1`.
* The corrected `c`-free residual is **`NegTwoDiagonalWeight (E)`** (the `z_0^1` line of (8.4.36)): a
  **weighted** antidiagonal sum, weight `p + m`, equals the two closed terms of
  `residueSum_negTwo_two_terms`; `ZOneLineNegTwo` is the unweighted form at degree `−N`, and
  `negTwoDiagonalWeight_iff_zOneLine` holds both ways (using only `AssemblyDiagonal`).
* Bridge to the batch-182 residual: `negTwoBlockCollapse_iff_diagonalWeight` under `hs` and
  `hc : form a b = −2 → E.c b a = 1`; consumer at FLM's datum:
  `residueNegativeAligned_evenCocycle_of_diagonalWeight (h) (h3) : ResidueNegativeAligned`.
* **Why it is new mathematics**: `ratioCoeff (−2) k = k+1` (`ratioCoeff_neg_two`), so the `−2` chamber
  difference is a weighted antidiagonal sum — the batch-181 `AssemblyDiagonal` (`z_0^0` line) cannot
  close it.  `MM.FLM86TPS.diagSumWeighted` is reused; `MM.FLM84DG.opOpenBox_deriv_modeFam`/`_heis` are
  the `z_2`-derivative at a **free** vertex operator (with `DiagCollapse`/`DerivNormalOrdered` as
  hypotheses), not the carrier identity.

### 80.2 The coherent-state field is a recursion; `≤ −3` is expanded to the honest (8.5.5) form

`Definitions/MMFLM86CoherentField.lean` (`MM.FLM86CF2`): `coherentStep` + `coherentFieldNat` with
`coherentField_recursion : ZAligned E (creationExpVL a ((k:ℤ)+1) w) = coherentStep E a w k` —
**degree `k+1` = one (8.5.5) step against the fields of the lower coherent states** (`^+` tail
included), bottoming out at `ε(a,b)•YFam E (a+b)`.  No induction on `k` collapses it: the needed
identity `Y(E⁻(z₀)w,z) = 8E⁻(z₀)Y(w,z)8` is not landed (`NonvacuumCreatedStep`-adjacent; `conv` is
forbidden).  `NegThreeExpandedResidualAligned` with `negThreeResidualAligned_iff_expanded` (both ways)
is the `≤ −3` residual in this honest form, and `residueDegree_eq` identifies the `i`-th summand's
degree.  The Fock display is **not** reachable this way: its left-hand object is
`ZAligned E (YFam E a (−j−1) (creationExpVL b l (ι b)))` — an honest **mode of `a`** on the coherent
state of `b` — so it needs a mode intertwining, not the coherent recursion.

### 80.3 The residuals after batch 183

1. `NegTwoDiagonalWeight` (the weighted `z_0^1` line);
2. `NegThreeExpandedResidualAligned` (the `≤ −3` recursion);
3. the Fock half — an honest-mode intertwining;
4. the boundary restatement at the even cocycle.

## 82. Batch 185: the `−2` case is a DERIVATIVE identity; the Fock half is one dictionary

### 82.1 `NegTwoFirstDerivZero`: the `⟨a,b⟩ = −2` residual, in derivative form

`Definitions/MMFLM86NegTwoPOne.lean` (`MM.FLM86NPO`):

* **The `p`-recursion route is refuted**: `diagFam` is the diagonal Taylor family of `X(z₂+z₀,z₂)`, and
  its `p = 0`/`p = 1` coefficients read **different** coefficients of `X` — the counterexample
  `exists_diagFam_zero_eq_zero_one_ne_zero` shows a family with vanishing `p = 0` line and nonvanishing
  `p = 1` line.  So the landed `p = 0` line (`assemblyDiagonal`) cannot give `p = 1`.
* **The complete `p`-recursion is landed** instead: `diagFam_succ_eq_diagFam_firstDeriv` —
  `(p+1) • diagFam X M1 M2 (p+1) j = diagFam (firstDeriv X) (M1−1) M2 p j`; every step replaces `X` by
  `∂_{z₁}X` and only the `p = 0` line is evaluated.  The `−2` case therefore needs the `p = 0` line of
  `∂_{z₁}normOrdered2 a b`.
* **The exact residual `NegTwoFirstDerivZero (E)`** (with both directions:
  `zOneLine_iff_firstDerivZero`, `negTwoDisplayZOne_iff_firstDerivZero`,
  `negTwoExactResidualAligned_evenCocycle_iff_firstDerivZero` at `C.toCentralExtension h2`) is the
  **Leibniz/normal-ordering identity** `∂_{z₁}|_{z₁=z₂} 8Y(a,z₁)Y(b,z₂)8 = 8a(z₂)Y(ab,z₂)8` — source
  reading `∂_z Y(u,z) = Y(L₋₁u,z)`, `L₋₁ι(a) = a(−2)1` — i.e. a **weight-two Fock field times a lattice
  field**, outside the batch-180/181 two-lattice-label fibre computation.
* The only landed statement with a `z_0^1` line, `MM.FLM8512Done.productExpansion8512_apply_one`, is not
  a route (it assumes the whole display and a negative-power vanishing `hX` that is false at `ZAligned`).
* Successor routes: (i) the (8.4.36) substitution at `z_0^1` through the resummation layer
  (`MM.FLM84Taylor.resumCoeff`/`taylorCoeff`, `MMFLM86TaylorOperator`) applied to the `E⁻`/block/`E⁺`
  decomposition; (ii) generalise the fibre computation to `8Y(u,z₁)Y(b,z₂)8` for a general Fock `u`.

### 82.2 The Fock half is one dictionary

`Definitions/MMFLM86CoherentCreated.lean` + `MMFLM86CoherentCreatedStep.lean` (`MM.FLM86CCF`/`MM.FLM86CCS`):
the two sides of `CoherentCreatedForm` are **not** the same normal-ordered object (a ratio sum of *fields
at* blocks versus a window sum of blocks *applied to a state*), and the exact residual is
`CoherentCreatedStep (E)` with the both-directions dictionary `coherentCreatedForm_iff_createdStep`,
`…_iff_normOrdered2`, `…_iff_ratioForm(_nonneg)`.  The sibling lands
`IterateProductStep (ZAligned E) convOneSided ⇒ … ⇒ CoherentCreatedForm`; the four Fock statements are
one dictionary, all implied by that already-named gap.

### 82.3 Correction of record

Batch 178-A's "imported by nothing" for `Definitions/MMFLM85StepLinear.lean` is **false**:
`FinalCheck.lean:343` has imported it since batch 128 (commit `94b9097`), and
`MMFLM85NonvacuumStep.lean:47` does too.

### 82.4 The residuals after batch 185

1. `NegTwoFirstDerivZero` — the derivative normal-ordering identity;
2. the `≤ −3` case;
3. `CoherentCreatedStep` — the Fock comparison;
4. the boundary restatement at the even cocycle.

## 83. Batch 186: the boundary at the even cocycle and the FACE AUDIT

### 83.1 The boundary, stated honestly

`Definitions/MMFLM810TheoremEven.lean` (`MM.FLM810TE`): `theorem8102_of_residuals` takes
`hstep : EvenCocycleJacobiStep C h2` and `hres : EvenCocycleResiduals C h2` at
`E := C.toCentralExtension h2`, where
`EvenCocycleResiduals := NegTwoFirstDerivZero E ∧ NegThreeExpandedResidualAligned E ∧ CoherentCreatedStep E`.
Also landed: `theorem8102_of_evenJacobi`, `theorem8102_of_jacobiResidual` (the §8.10 form),
`FockCreatedStep`, and **`jacobiAxiom_iff_stateTargets`** — the converse of batch 169 R1's documented
equivalence, now formalized, so `JacobiAxiom` (the §8.10 output) feeds the boundary's
`JacobiOnStateTargets`.

### 83.2 The face audit (the batch's main product)

* `Res_{z_0}` = Corollary 8.5.1: closed for `0 ≤ ⟨a,b⟩` and `⟨a,b⟩ = −1`; the rest are the named
  residuals.
* `Res_{z_1}`/`Res_{z_2}` (`MM.FLM88.res_z1_face`/`res_z2_face`): **extractions from the Jacobi
  hypothesis**, not theorems; only conditional content in `MM.FLM810JacobiRoute`.
* **`l, m, n ≠ 0`: nothing landed** — `hjac` is strictly more than `Corollary851`; the `l ≠ 0` faces are
  the campaign's largest untouched gap.
* §8.8: the identity itself and the §8.6 engine are missing; §8.10: the `ι`-bridge, `RecoveryDisplay`,
  the `RecoverySplit` use and 8.10.7 are missing (calculus landed and consumable).

### 83.3 The `−2` derivative residual, decomposed

`Definitions/MMFLM86FirstDerivLine.lean` (`MM.FLM86FDL`): the `convWith2` Leibniz rule
`firstDeriv_convWith2` (the flat `deriv_flatMul` does not apply to the two-variable product) and the
three-piece decomposition `firstDeriv_normOrdered2_eq = creationDerivPiece + blockDerivPiece +
annihDerivPiece`, with the factor derivatives.  The `−2` residual becomes `FirstDerivThreeFactorLine`
(equivalent, both directions): three explicit per-state diagonal collapses of landed `convWith2`
expressions.  Attack `creationDerivPiece` first; the line is **weighted**, so the batch-181 regrouping
does not apply verbatim.

### 83.4 The fronts after batch 186

1. the `l ≠ 0` faces of (8.8.41) at the boundary field (untouched; `MMFLM810Route` is the entry point);
2. the `l = 0` residuals: `NegTwoFirstDerivZero` (now in three-piece form), `≤ −3`, the Fock half;
3. the continuation to full Jacobi: §8.8 (Theorem 8.8.9) or §8.10 (Props 8.10.3--8.10.7, `ι`-bridge);
4. the six boundary inputs `hnd/hs/S/hpd/hW/hfin`.

## 84. Batch 187: the `l ≠ 0` front opened; the `−2` creation piece collapsed

### 84.1 The `l ≠ 0` faces: first land at the boundary field

`Definitions/MMFLM810JacobiNonzeroFaces.lean` (`MM.FLM810JNF`):

* **Inventory**: every general-`l` statement in the tree is either a `def … : Prop` or **conditional on
  `h : JacobiIdentity`** (extractions: `res_z1_face`, `res_z2_face`,
  `corollary8818_of_jacobiIdentity`, `crossBracket_eq_of_window`).  At the boundary field nothing was
  landed for `l ≠ 0`; the only `l ≠ 0` identity anywhere is the scalar toy model
  (`MMFLM810ScalarJacobi.lean:542`, not a VOA field).
* **Landed** at `ZAligned (C.toCentralExtension h2)`, lattice generators, `0 ≤ ⟨a,b⟩`:
  `crossTerm_ZAligned_lattice` (+ swap), `yFam_mul_comm_of_nonneg`, the binomial reflection
  `deltaExpCoeff_reflect_of_nonneg`, the (8.8.21) swap-sum identity
  `sum_crossTerms_eq_smul_sum_crossTermSwaps`, and **the first `l ≠ 0` face**:
  `crossBracket_ZAligned_lattice_of_nonneg = 0`, `crossIterate_ZAligned_lattice_eq_zero_of_nonneg = 0`,
  hence `crossBracket_eq_crossIterate_ZAligned_lattice_of_nonneg` — equal for every `l ≥ 0`, every
  `m, n`, every `N ≥ l.toNat+1` (degenerate: both sides vanish).
* **The `l < 0` iterate side** is computed: `crossIterate_ZAligned_lattice_eq_sum_of_nonpos` (the finite
  sum over `i < (−l).toNat` of `binom(m,i) • iterateOf (ι a) (ι b) (l+i) (m+n−i)`).
* **The named residual `FirstNegativeFaceAligned (E)`** — (8.8.41) at `l = −1`, per monomial, cross side
  terminating (the δ-term of the formal (8.6.28)) — with the consumer
  `jacobiIdentity_neg_one_slice_of_firstNegativeFace`.
* **Route correction**: the shift display is **(8.6.28)** (which the source calls "formal ... suggestive"),
  not (8.6.29)/(8.6.30); no landed reduction of a general `l ≠ 0` face to `l = 0` exists, and for
  `l ≥ 0` the face reduces to a **commutator sum**, not to `l = 0` plus a shift.  Next target: `l = −1`
  through the landed (8.4.25) product.

### 84.2 `creationDerivPiece` collapsed; the `−2` residual is now sharply localised

`Definitions/MMFLM86CreationDerivPiece.lean` + `MMFLM86CreationDerivPieceLine.lean`
(`MM.FLM86CDP`/`MM.FLM86CDPL`):

* `sum_creationDerivPair_window` (the `E⁻` fibre collapse) and
  `flatMul_deriv_creationExpVL_add : deriv E⁻_{a+b} = flatMul (deriv E⁻_a) E⁻_b +
  flatMul (deriv E⁻_b) E⁻_a`: **each ordering contributes half**, so no single piece equals the target's
  right-hand side.
* `diagSum_creationDerivPiece(_regrouped)`, `diagSum_blockDerivPiece` (block first layer), and
  `sum_sum_window_regroup_factor` (batch 181's regrouping with an arbitrary factor; its
  `C = creationExpVL (a+b)` instance is syntactically the landed one).
* **Pieces**: creation **LANDED**; block **to the first layer** (the second layer — the weighted
  antidiagonal sum of the differentiated `a(0)` block, value `⟨a,c⟩` on `x ⊗ ι(c)` — open);
  annihilation **NOT landed** (the mirrored flat recursion `(d/dz)E⁺ = −a(z)⁺E⁺` is absent).
* **Weight correction**: `dE⁻_a`'s extra index `i = −1` has weight `0`, so the window hypothesis is
  verbatim batch 181's and the regrouping is reusable (proved).

### 84.3 The fronts after batch 187

1. the `l = −1` face (`FirstNegativeFaceAligned`) — the first genuinely nonzero `l ≠ 0` face;
2. the annihilation derivative piece (the `−2` case's remaining piece);
3. the `l = 0` residuals (`≤ −3`, the Fock half);
4. the continuation to full Jacobi (§8.8 / §8.10) and the six boundary inputs.

## 85. Batch 188: the `l = −1` face becomes a pure VOA identity; the third Leibniz piece lands

### 85.1 `(∗)`: the `l = −1` slice is one honest-lattice-VOA statement

`Definitions/MMFLM810NegOneFace.lean` (`MM.FLM810NOF`):

* The cross side is the **whole diagonal**: `crossBracket (ZAligned E) (ι a) (ι b) N (−1) m n =
  Σ_{i<N} YFam a (m−1−i)·YFam b (n+i) + Σ_{i<N} YFam b (n−1−i)·YFam a (m+i)` (`deltaExpCoeff i (−1) = 1`
  in char 0, the factorial hypothesis discharged).
* The iterate side is closed: `iterateOf (ZAligned E) (ι a) (ι b) (−1) (m+n) = if ⟨a,b⟩ = 0 then
  ε(a,b)·YFam (a+b) (m+n) else 0` — **the boundary-field repair drops out of this face**.
* `NegOneFaceAligned (E)` (the source's per-element reading) is **equivalent, both directions**, to the
  pure VOA identity
  `(∗) Σ_{p+q=m+n−1} YFam a p · YFam b q = (0 if ⟨a,b⟩ ≠ 0 else ε(a,b)·YFam (a+b) (m+n))`.
  `(∗)` mentions no `ZAligned`, so an honest-VOA proof of it gives the `l = −1` slice outright.
* **Chambers still open**: `1 ≤ ⟨a,b⟩` (cross side 0) and `⟨a,b⟩ = 0` (cross side `ε·YFam (a+b)`).
* **Corrections**: the "reduce `l = −1` to the landed `l = 0` face" advice is unsupported (there the
  `l = 0` face is commutativity with both sides 0); batch 187-A's `FirstNegativeFaceAligned` window is
  **operator-valued**, which is not the source's per-element reading (only 187-A ⟹ the per-element form
  is proved); and `MM.FLM86RN.NegOneResidualAligned` (the `⟨a,b⟩ = −1` pairing at `l = 0`) is a
  **different object** — a naming collision to remember.

### 85.2 The third Leibniz piece: the `E⁺` mirror collapse

`Definitions/MMFLM86AnnihDerivPiece.lean` + `MMFLM86AnnihDerivPieceLine.lean`
(`MM.FLM86ADP`/`MM.FLM86ADPL`): `deriv_annihExpField`, `deriv_annihIdx` (the mirrored recursion),
`flatMul_deriv_annihIdx_add`, `sum_annihDerivPair_window` (the `E⁺` fibre collapse, with the minus sign
and the shift `−K−2`) and `diagSum_annihDerivPiece(_regrouped)`; the generalized regrouping engine
`sum_sum_window_regroup_gen`.  **All three Leibniz pieces are now in one collapsed normal form.**

The residual `AnnihClosedLine` (both directions, and at FLM's datum
`negTwoExactResidualAligned_evenCocycle_iff_annihClosed`) is **not proved**, and the pieces do not
assemble: (i) the **block's second layer** is missing (the derivative block's fibre collapse is
operator-valued/per-state at the carrier); (ii) each exponential piece carries only one **ordering** of
its derivative, and the identification with `ZAligned E (creationExpVL a 1 (anchorVL E a b))`
((8.4.23)/(8.4.25)) is not landed.  The "mirror" is an **index reflection** `i ↦ −i−1` (same ordering).

### 85.3 The fronts after batch 188

1. `(∗)` — the two chambers of the `l = −1` face (a pure VOA identity);
2. the `−2` case: the block's second layer + the ordering identification;
3. the `l = 0` residuals (`≤ −3`, the Fock half) and the `l ≤ −2` faces;
4. the continuation to full Jacobi (§8.8 / §8.10) and the six boundary inputs.

## 86. Batch 189: `(∗)` and the `l = −1` slice are unconditional at FLM's datum; the ordering question settled

### 86.1 MILESTONE: the `l = −1` slice is closed at the even cocycle

`Definitions/MMFLM810NegOneChambers.lean` + `MMFLM810NegOneChambersClose.lean`
(`MM.FLM810NOC`/`MM.FLM810NOCC`):

* Both chambers landed (`honestDiag_eq_zero_of_one_le`, `honestDiag_eq_eps_smul_of_eq_zero`) and **`(∗)`
  itself unconditionally and window-independently** (`diagSum_honestDiag_eq`,
  `exists_honestDiag_window`) — only the form symmetry is needed.
* Route: the landed (8.4.25) expansion + **the landed (8.4.20) `MM.FLM86AR.assemblyDiagonal`** + a new
  `sum_range_ratioCoeff : Σ_{j≤N} ratioCoeff N j = (1−1)^N`.
* **`negOneFaceAligned_evenCocycle : NegOneFaceAligned (C.toCentralExtension h2)`** — batch 188-A's
  residual is a theorem; for an arbitrary extension the transport is
  `negOneFaceAligned_of_cocycleCompatible`.
* **Correction**: batch 188-A's "the cross side is the single-order diagonal of `(∗)`" is false in
  general — `crossTermSwap` is the opposite order and the two differ by `1 − c(b,a)(−1)^{⟨a,b⟩}`; the
  single-order form holds exactly under `CocycleCompatible` (true at the even cocycle).
* Trap recorded: `rwa` in the big cross-bracket context exceeded 1.6M heartbeats (`rw … at h; exact h`
  is instant).

### 86.2 The ordering question, settled; the `−2` residual is now the (8.4.23) dictionary

`Definitions/MMFLM86BlockSecondLayer.lean` + `MMFLM86BlockDerivRegrouped.lean` +
`MMFLM86NegTwoAssembly.lean` (`MM.FLM86BSL`/`MM.FLM86BDR`/`MM.FLM86NTA`):

* **The three-piece split is NOT buggy**: `firstDeriv = d/dz_1` differentiates only the first slot, so the
  "other orderings" are the `d/dz_2` halves — a different operator — and must not be added.  Landed:
  `flatMul_deriv_creationExpVL_half`, `flatMul_deriv_annihIdx_half`,
  `deriv_creationExpVL_eq_halves`; the pieces carry the `a(z)^-`, `a(0)`, `a(z)^+` terms of
  `:a(z)Y(ab,z):`.  **The batch-187-B header sentence "the other half is what the mirror piece has to
  produce" is false and has been corrected in place (dispatcher edit, file rebuilt).**
* **The block's second layer is landed**: `sum_firstDeriv_midBlock2_fiber` (fibre degree `K'` collapses
  at grading `K'+1`), with `exists_midGradDeriv_antidiagonal`/`exists_midGradDerivVL_antidiagonal` and
  `diagSum_blockDerivPiece_regrouped`.
* **Exact residual `NegTwoNormalFormLine`** (all three pieces collapsed; both directions).  **The
  remaining gap is the (8.4.23) dictionary `Y(a(−1)u,z) = 8a(z)Y(u,z)8` at the aligned boundary field**,
  not an ordering.  Also: `a(0)` must be `hZeroVL (ofLattice a)` (`modeVL a 0 = 0` in this pin).

### 86.3 The fronts after batch 189

1. the (8.4.23) dictionary (closes the `−2` case if it lands);
2. the `≤ −3` case, the Fock half, the `l ≤ −2` faces;
3. the continuation to full Jacobi (§8.8 / §8.10) and the six boundary inputs.

## 87. Batch 190: the `l = −2` face lands; the `z_0^1` line is now the single shared blocker

### 87.1 The `l = −2` face

`Definitions/MMFLM810NegTwoFace.lean` + `MMFLM810NegTwoChambers.lean`
(`MM.FLM810NTF`/`MM.FLM810NTC`):

* **`negTwoFaceAlignedOneLe_evenCocycle`** — the `1 ≤ ⟨a,b⟩` chamber of (8.8.41) at `l = −2`,
  **per element**, every past-vanishing window `N ≥ 2`, unconditional at FLM's datum.  Both sides are
  evaluated (`ε(a,b)·YFam (a+b) (m+n)` at `⟨a,b⟩ = 1`; `0` for `⟨a,b⟩ ≥ 2`).  Supporting: the exact cross
  side, the two-term iterate collapse for a general `E`, and the first-moment identity
  `Σ_j j·ratioCoeff N j = −1` (`N = 1`) / `0` (`N ≥ 2`).
* The `⟨a,b⟩ = 0` chamber is equivalent to `WeightedZOneLineZeroPairing` — the `z_0^1` line at
  pairing-zero pairs, the *same* identity as `ZOneLineNegTwo`/`NegTwoDiagonalWeight` (pairing `−2`);
  the iff itself was not landed (budget).
* **General `l ≤ −2`**: the cross side is a **weighted** antidiagonal, weight `ratioCoeff l (m+l−p)`,
  degree `L − 1 = −l − 1`; `L = 1` needs no moment, `L = 2` the first (killed by
  `Σ_j ratioCoeff = 0` — why `l = −2` lands), `L ≥ 3` the **moment hierarchy**
  `Σ_r r^m · normOrdered2 a b r (K−r) = 0` for `m + 1 ≤ ⟨a,b⟩` (= the `m`-th derivative of (8.4.40)),
  not landed; the iterate side needs the Fock-descendant evaluations.

### 87.2 The (8.4.23) dictionary, and the relocation of the `−2` gap

`Definitions/MMFLM86DerivDictionary.lean` (`MM.FLM86DD`): the dictionary `Y(a(−1)u,z) = 8a(z)Y(u,z)8`
was **already landed at an arbitrary vector and base** (`Yzero_modeVL_eq_actionFamily(_nat)`,
`ZAligned_creationStep`, `coherentField_one`), as was its `L(−1)` companion `BaseResidual (baseAligned E)`
(batch 172).  New here: the aligned-field and factor-level forms
(`splitMinus_factorFactorZero_one_zero = a(−1)`,
`splitPlus_factorFactorZero_one_neg_one = hZeroVL (ofLattice a) = a(0)`,
`headOp_factorFactorZero_one_ne_flatMul`), the anchor form
`ZAligned_creationExpVL_one_anchor` (which removes `anchorVL`/`ZAligned`/`Yzero` from the residual's
right-hand side), and the residual `DerivDictionaryLine` — **both directions** to
`NegTwoFirstDerivZero`/`NegTwoNormalFormLine`/`NegTwoExactResidualAligned`.

**The `−2` gap is the FLAT REASSEMBLY** — matching the three collapsed flat sums with
`headOp (heisFamZero a) + tailOp` of `Y(a+b,z)` ((8.4.36)/(8.4.40) at `z_0^1`): the creation half is
already in `flatMul (splitMinus (heisFam a)) (creationExpVL (a+b))` shape, the `a(0)` summand belongs to
the tail, and the negative `mid`-degrees must be carried by the free `(J,K')` windows.

### 87.3 The state after batch 190

Unconditional at FLM's datum: `l = 0` (`0 ≤ ⟨a,b⟩`, `⟨a,b⟩ = −1`), `l ≥ 0` (`0 ≤ ⟨a,b⟩`), `l = −1`,
and `l = −2`'s `1 ≤ ⟨a,b⟩` chamber.  **The single shared open object is the `z_0^1` line**
(`DerivDictionaryLine` = `ZOneLineNegTwo` = `WeightedZOneLineZeroPairing`).  Then: the moment hierarchy
(`l ≤ −3`), the Fock half, the continuation to full Jacobi, and the six boundary inputs.

## 88. Batch 191: the `z_0^1` obligation is unified as `ZOneLineAllPairings`; the moment picture corrected

### 88.1 The single shared obligation

`Definitions/MMFLM86ZOneReassembly.lean` (`MM.FLM86ZOR`):

* The reassembly is **not** landed; its missing half is diagnosed: carrying `a(k)` (`k ≥ 0`) past
  `E^+_{a+b}` through the **(8.4.19) contraction** inside the free `(J,K')` windows.  Step-1 grep was
  measured **negative**.
* Landed: `negTwoFaceAligned_iff_weightedZOneLine` (both directions, under `CocycleCompatible`), via
  `weightedHonestDiag_zero_eq_diagSumWeighted` and `negTwoZeroWindow_weighted_eq_zero`.
* **Correction**: `DerivDictionaryLine` (pairing `−2`) does not imply `WeightedZOneLineZeroPairing`
  (pairing `0`).  The unified obligation is **`ZOneLineAllPairings`** (the `z_0^1` line for **all**
  pairs), from which `zOneLineNegTwo_of_allPairings`, `weightedZOneLine_of_allPairings` and
  `derivDictionaryLine_of_allPairings` are landed.  **The tail contraction making
  `ZOneLineAllPairings` a theorem closes both the `l = 0`, `⟨a,b⟩ = −2` case and the `l = −2`,
  `⟨a,b⟩ = 0` chamber.**

### 88.2 The moment picture, corrected and landed

`Definitions/MMFLM86MomentHierarchy.lean` (`MM.FLM86MH`):

* **The batch-190-B picture was wrong**: the moments do **not** vanish for `m+1 ≤ ⟨a,b⟩`; `m = 0` is the
  assembly and `m = 1` is the `z_0^1` line (the landed residual).  Correct: the `j`-sum becomes a finite
  difference, so by `Σ_j ratioCoeff N j j^s = 0` (`s < N`) only the **low** moments `m ≤ c−1−N` survive.
* Master identity `weightedHonestDiag_eq_sum_ratioCoeff`, with specialisations:
  `…_eq_binomMoment` (`N ≤ c−1`: the single binomial moment `Σ_r C(r+m, c−1−N)·normOrdered2`, i.e. the
  `z_0^{c−1−N}` line of (8.4.36)/(8.4.40)); **`…_eq_zero_of_le` (`N ≥ c`: 0 — no moment, no new
  residual)**; `…_eq_assembly` (`N = c−1`, the landed `assemblyDiagonal`); `…_eq_firstMoment`
  (`N = c−2`, the `z_0^1` line).  Scalar core: `ratioCoeffSum_eq_binomCoeffFinDiff` (consuming the
  already-landed `MM.FLM86Y.binomCoeffFinDiff`), the **new vanishing case `binomCoeffFinDiff_eq_zero_of_lt`**
  (`s < n`), `binomCoeffFinDiff_eq_int`, and `deltaExpCoeff_neg_eq_binomCoeff`.
* **`negThree_weightedChambers`**: for `l = −3` and `2 ≤ ⟨a,b⟩` the weighted antidiagonal is
  `ε(a,b)·YFam (a+b) (m+n)` at `⟨a,b⟩ = 2` and `0` for `⟨a,b⟩ ≥ 3` — **the whole `2 ≤ ⟨a,b⟩` half of the
  `l = −3` face is determined by the landed assembly alone**.
* The `l = −3` residual: (a) the general-`c` cross-side reindexing (mechanical);
  (b) the `l = −c` analogue of `honestDiag_eq_zero_of_crossWindowOn`; (c) the iterate side at `l = −3`.
  The `⟨a,b⟩ = 1` chamber is **not** reachable today (it needs the `z_0^1` line at pairing 1).

### 88.3 The state after batch 191

Unconditional at FLM's datum: `l = 0` (`0 ≤ ⟨a,b⟩`, `= −1`), `l ≥ 0` (`0 ≤ ⟨a,b⟩`), `l = −1`,
`l = −2`'s `1 ≤ ⟨a,b⟩`, and `l = −3`'s `2 ≤ ⟨a,b⟩`.  The single shared obligation is
`ZOneLineAllPairings` (the (8.4.19) tail contraction).

## 89. Batch 192: the `l = −3` face lands; the `(8.4.19)` premise corrected

### 89.1 The `l = −3` face at `2 ≤ ⟨a,b⟩` is a theorem

`Definitions/MMFLM810NegThreeFace.lean` (`MM.FLM810NTH`): `negThreeFaceAlignedTwoLe_evenCocycle (C) (h2)
(hs)` — per element, per monomial, every window `N ≥ 3`, unconditional at `C.toCentralExtension h2`.
Supporting (general `c ≥ 1` where possible):

* **(a)** `crossBracket_neg_nat_eq_sum` (under `CocycleCompatible`): the cross side is
  `Σ_p binomCoeff (m−p−1) (c−1) • honestDiag E a b p (m+n−c−p) w` over the two half-lines; the reflection
  `binomCoeff_pos_eq_neg_pow` and `disjoint_negCWindows`.
* **(b)** `weightedHonestDiag_eq_zero_of_crossWindowOn`: the face's `CrossWindowOn` gives the **weighted**
  vanishing (the honest diag is *not* zero in the gap `m−c < p < m`), plus the window-independence bridge
  `weightedHonestDiag_neg_three_eq`.
* **(c)** `crossIterate_ZAligned_lattice_neg_three` (general `E`): `i = 0,1,2` survive; chamber forms give
  `ε(a,b)·YFam (a+b) (m+n)` at pairing `2` and `0` above.

### 89.2 The `(8.4.19)` premise refuted; the annihilation/zero-mode laws landed

`Definitions/MMFLM86TailContraction.lean` (`MM.FLM86TC2`):

* (8.4.19) off printed p. 192: `8α(z)Y(a,z)8 = 8Y(a,z)α(z)8 = α(z)⁻Y(a,z) + Y(a,z)α(z)⁺`.
* **No contraction past `E⁺`** for any `k ≥ 0` (`k ≥ 1` landed; `k = 0` proved here); the contraction is
  against `E⁻` and was landed (repackaged as `splitPlus_heisFamZero_contraction_creation`).  What was
  missing at the assembled field was the **annihilation/zero-mode** law, now landed:
  `modeVL_YFam_add_pos`, `hZeroVL_YFam_add`, and **`splitPlus_heisFamZero_YFam_add : a(k)(Y(a,z)_j v) =
  Y(a,z)_j (a(k)v) + ⟨b,a⟩ Y(a,z)_{j+k} v`** for all `k ≥ 0`.
* `ZAligned_anchor_head_tail` (the corrected head/tail spelling) and
  `zOneLineAllPairings_iff_headTail` (both directions).
* **`ZOneLineAllPairings` is still the residual**; what remains is the flat reassembly.  Conditional on it,
  both faces close: `negTwoFirstDerivZero_of_allPairings`, `negTwoExactResidualAligned_of_allPairings`,
  `negTwoFaceAlignedZeroPairing_of_allPairings`.
* Traps: `headOp` is `FLM85TA.headOp`; `factorFactorZero` in `FLM810ZM`;
  `sub_eq_iff_eq_add'`; the `Module.End` `Sub`/`Add` diamond (work at the vector level); repeated `rw`
  of one lemma errors on the second pass.

### 89.3 The state after batch 192

Unconditional at FLM's datum: `l = 0` (`0 ≤ ⟨a,b⟩`, `= −1`), `l ≥ 0` (`0 ≤ ⟨a,b⟩`), `l = −1`,
`l = −2`'s `1 ≤ ⟨a,b⟩`, `l = −3`'s `2 ≤ ⟨a,b⟩`.  The single shared obligation is the flat reassembly
(`ZOneLineAllPairings`), which closes the `l = 0`, `⟨a,b⟩ = −2` case and the `l = −2`, `⟨a,b⟩ = 0`
chamber.  Then: general `l ≤ −4`, the Fock half, the continuation to full Jacobi, the six boundary inputs.

## 90. Batch 193: general `l = −c` chambers; the `z_0^1` residual on the generators and its linearity

### 90.1 General `l = −c`: the `ν ≥ c−1` chamber is unconditional

`Definitions/MMFLM810NegCFace.lean` (`MM.FLM810NCF`): `negCFaceAlignedGe_evenCocycle (C) (h2) (hs) {c}
(hc : 1 ≤ c)` — the general face at `ν := ⟨a,b⟩ ≥ c−1`, unconditional at FLM's datum.  Supporting:
`negC_weightedChambers`, `crossBracket_ZAligned_lattice_neg_nat_eq_ite`, the general-`E` iterate side
`crossIterate_ZAligned_lattice_neg_nat` (+ the `ν ≤ c−2` decomposition with `k = c−1−ν` Fock
descendants), `crossWindowOn_ZAligned_lattice_neg_nat`.

**Exact residual `NegCBinomMomentAligned E c`** for `0 ≤ ν ≤ c−2`
(`negCFaceAligned_iff_binomMoment_evenCocycle`, both directions).  Chambers: `ν ≥ c−1` unconditional;
`ν = c−2` the first moment (`z_0^1`); `1 ≤ ν ≤ c−3` the `z_0^{c−1−ν}` lines; `ν = 0` the
`z_0^{c−1}` line.  **`c = 1` unconditional; `c = 2` leaves only `ν = 0` (the landed
`WeightedZOneLineZeroPairing`); `c = 3` leaves `ν ∈ {0,1}`.**

### 90.2 The `z_0^1` residual: generators landed, linearity landed

`Definitions/MMFLM86FlatReassembly.lean` (`MM.FLM86FRA`):

* **`zOneLineAllPairingsOnGenerators (hs) (E)`** — the residual holds at `v = ι(c)`, for **all** pairings,
  with the index bridges `sum_Icc_smul_eq_flatMul_deriv` (the weight `p` IS the (8.4.12) derivative),
  `sum_Icc_eq_flatMul`, `sum_range_toNat_succ_eq_flatMul`, plus `genFam_iotaVL` and
  `modeVL_iotaVL_eq_zero_of_pos`.
* **`F`-linearity in the state**: `ZOneLineAt`, `zOneLineAllPairings_iff_forall_ZOneLineAt`,
  `zOneLineAt_add/_smul/_zero/_of_mem_span`.  **The residual is determined by its values on any spanning
  set**; with the generator half, the only remaining input is the residual on the creation monomials — the
  Fock half.
* **Corrections**: `splitPlus_heisFamZero_YFam_add` was not the missing tool (the `a(k)` summands already
  are the tail); the reassembly is not a `(J,K')`-window reindexing (those windows belong to the
  `z_0^0`/firstDeriv line) — at an arbitrary state the flat pieces reach the action through the
  annihilation-pair contractions, i.e. the Fock half; and the `⟨a,b⟩ = −2` instance does not imply the
  general-state identity.

### 90.3 The state after batch 193

Unconditional at FLM's datum: `l = 0` (`0 ≤ ⟨a,b⟩`, `= −1`), `l ≥ 0` (`0 ≤ ⟨a,b⟩`), `l = −1`, and for
every `c ≥ 1` the `ν ≥ c−1` chamber of `l = −c`.  **The single shared obligation is the `z_0^1` line
`ZOneLineAllPairings`, now reduced to its Fock half.**  Then: the higher `z_0^m` lines, the continuation
to full Jacobi, and the six boundary inputs.

## 91. Batch 194: the `z_0^1` line at the first Fock level; the derivative ladder

### 91.1 The first Fock level of the shared blocker

`Definitions/MMFLM86ZOneFockOne.lean` (`MM.FLM86ZOF`): **`zOneLineAt_modeVL_iotaVL`** — the `z_0^1`
residual `ZOneLineAt` at `v = α_{c'}(−R)ι(c)`, every pairing, every `R ≥ 1`, unconditional apart from the
form symmetry.  Engine landed alongside:

* **the contraction** `normOrdered2_modeVL_sub`: `normOrdered2 a b p q (α_c(−r)w) = α_c(−r)(normOrdered2 p q w)
  − ⟨c,a⟩·normOrdered2 (p+r) q w − ⟨c,b⟩·normOrdered2 p (q+r) w` — shift `+r` in **both** indices (forced by
  consistency of the two laws);
* its weighted-diagonal corollary `diagSumWeighted_modeVL`;
* **the right-hand-side mode law `ZAligned_modeVL`**: `Z_j(α_c(−r)w) = α_c(−r)(Z_j w) − ⟨c,a+b⟩·Z_{j−r}w +
  ε(a,b)·r·⟨a,c⟩·Y(a+b,z)_{r−j}w` (the brief's engine covered only the LHS; the RHS needs this);
* the window laws `headWindow_modeVL_shift`/`tailWindow_modeVL_shift` (the landed
  `headWindow_modeVL_sub`/`tailWindow_modeVL_sub` force the field's lattice label to equal the factor's,
  so they could not be used as stated) and the generator collapse `diagSum_normOrdered2_iotaVL`.

**The general creation monomial is NOT reached**: at the next mode the contraction produces the unweighted
diagonal sum at the **level-one descendant** `α_{c''}(−R₂)ι(c)` — the **`z_0^0` line at a Fock
descendant**, genuine new input.  Traps: `-r • x` parses as `(-r)•x`; `rw` instantiates a lemma once per
pass (repeating a name silently rewrites only the first instantiation); `-γ•H` vs `-(γ•H)` needs
`calc`/`show`.

### 91.2 The derivative ladder: no higher line is easier

`Definitions/MMFLM86ZMoments.lean` (`MM.FLM86ZM`): **`zLineScheme_succ_firstDeriv`** (with
`momentSum_firstDeriv`, `zLineAt_firstDeriv`) is an **equivalence**: the `(j+1)`-st line of `X` at degree
`K+1` ⟺ the `j`-th line of `d/dz₁X` at degree `K`.  Hence order `k` **is** order 0 of
`firstDeriv^k(normOrdered2 a b)` — the derivative tower of the shared blocker.  Plus the Vandermonde
expansion `binomCoeff_add_eq_sum`/`binomCoeff_add_two` and the flat reassembly
`sum_binomCoeff_smul_eq_sum`.

**The exact residual `ZLine E j`**: `j = 0` is a theorem (the landed assembly), `j = 1` is verbatim the
shared blocker (`zLine_one_iff_zOneLineAllPairings`), `j ≥ 2` is new.  **The chamber decomposition**:
`NegCMomentLine E c k` = `ZLine E k` at pairings `N = c−1−k`; forward each chamber consumes exactly its own
line; backward `negCBinomMomentAligned_of_zLine`.  **Ledger for `l = −c`**: `N ≥ c` zero; `N = c−1` the
landed assembly; `N ≤ c−2` the residual chambers, **all `z_0^k` lines with `k = c−1−N`**; `c = 1`
residual-free.  Correction: the landed `z_0^2` statements are one-variable
`openBoxField`/`shiftFamily` ones, not the honest three-factor `normOrdered2`.

### 91.3 The state after batch 194

The shared obligation `ZOneLineAllPairings` is now: proved on the generators (193-A), `F`-linear in the
state (193-A), proved at the first Fock level (194-A), and the easiest of all the `z_0^k` lines (194-B).
**The next input is the descended `z_0^0` line** (`α_{c''}(−R₂)ι(c)`), then the creation-monomial induction.
Then: the continuation to full Jacobi (§8.8/§8.10) and the six boundary inputs.

## 92. 🎉 Batch 195: `ZOneLineAllPairings` IS A THEOREM

### 92.1 The breakthrough

`Definitions/MMFLM86FockInduction.lean` (`MM.FLM86FI`):
**`zOneLineAllPairings_of_symmetric_form (hs) (E) : MM.FLM86ZOR.ZOneLineAllPairings bL form E`** — the
`z_0^1` line of (8.4.36)/(8.4.40) at every symmetric pairing, from landed ingredients only.  This was the
campaign's single shared obligation since batch 186.

The chain: `zOneLineAtLevel_zero` (the generator case, batch 193-A) → `zOneLineAt_modeVL` (weigh the
level-`n` hypotheses at `(m,n)` and `(m−r,n)` against the landed assembly at `w` at degree `−m−n+r`; the
window `U = (s₁∪s₂∪s₃) ∪ (s₁∪s₂∪s₃)−r`; then `diagSumWeighted_modeVL` + `ZAligned_modeVL`) →
`zOneLineAtLevel_succ` → `zOneLineAtLevel_all` → `zOneLineAllPairings_of_level`
(`zOneLineAt_of_mem_span` + `spanningStatement`).  Caveat: only the symmetric-pairing instance is proved.

**Correction of record**: the "descended `z_0^0` line" (batch 194-A's measured next input) **does not
exist** — the landed `MM.FLM86AR.assemblyDiagonal`/`assemblyDiagonal_antidiagonal` already gives the
unweighted diagonal sum at every state and pairing; `diagSum_normOrdered2_iotaVL` is that law at `ι(c)`.
The level-`n` hypothesis therefore carries the `z_0^1` half only, and the induction closes.  Batch 195-A
(dispatched on the refuted premise) was steered mid-flight and stopped; its kept file
`MMFLM86DescendedAssembly.lean` adds only the window-level decomposition and an explicit witness window.

### 92.2 What this unlocks

The landed one-directional reductions compose: the `l = 0`, `⟨a,b⟩ = −2` case
(`NegTwoFirstDerivZero`, `NegTwoExactResidualAligned`, and the equivalent names); the `l = −2` face's
`⟨a,b⟩ = 0` chamber (`WeightedZOneLineZeroPairing`), hence the whole `l = −2` face; and for every `c`
the `ν = c−2` chamber of `l = −c` (`NegCMomentLine E c 1` from `ZLine E 1`).  Combined with batch 193-B's
`ν ≥ c−1` chamber: **every `l = −c` face is unconditional for `ν ≥ c−2`**, and the remaining chambers are
`0 ≤ ν ≤ c−3`, i.e. the lines `ZLine E j` for `j ≥ 2`.

### 92.3 The state after batch 195

Unconditional at FLM's datum: `l = 0` (`0 ≤ ⟨a,b⟩`, `= −1`, and — pending the batch-196 harvest — `= −2`);
`l ≥ 0` (`0 ≤ ⟨a,b⟩`); `l = −1`; `l = −2` (both chambers); and the `ν ≥ c−2` part of every `l = −c`.
Remaining: the lines `ZLine E j` (`j ≥ 2`), the Fock half of the `l = 0` residual, the continuation to
full Jacobi, and the six boundary inputs.
## §93 Batch 196 — the `ZLine` tower is one `c`-independent base from closed

### 93.1 The harvest (A)

Batch 195 made `ZOneLineAllPairings` a theorem.  Every landed one-directional reduction that had it as a
hypothesis therefore fires unconditionally, and batch 196-A collected them into two files.  The two
headline consequences:

* `negTwoFaceAligned_evenCocycle` — the **whole `l = −2` face** at FLM's datum.
* `negCFaceAlignedFrom_subTwo_evenCocycle` — the `ν ≥ c−2` chamber of the `l = −c` face, for **every** `c`.

and the sharp accounting statement

* `residueNegativeAligned_evenCocycle_iff_negThreeAndBelow` —
  `ResidueNegativeAligned (evenCocycle …) ↔ NegThreeAndBelowResidualAligned`.

The last one is the useful shape: the negative-pairing residue no longer carries any `l = 0` debt for
`⟨a,b⟩ ∈ {0,−1,−2}`, and carries no `l ≠ 0` debt for those pairings either.  What remains of
`ResidueNegativeAligned` is **exactly** the chamber `⟨a,b⟩ ≤ −3`.

### 93.2 The induction (B): one base, two halves

`Definitions/MMFLM86ZLineInduction.lean` proves the level induction and reduces the whole tower to a
single `c`-independent hypothesis `ZLineGeneratorBase E`:

```
zLine_all_of_generatorBase (hs) (E) (h : ZLineGeneratorBase …) : ∀ i ≥ 1, ZLine E i
zLineGeneratorBase_iff (hs) (E) : ZLineGeneratorBase … ↔ ∀ i ≥ 1, ZLine E i
negCBinomMomentAligned_of_generatorBase (hs) (E) (h) (hc : 1 ≤ c) : NegCBinomMomentAligned E c
```

The base is not one statement but two:

1. **generator line**: `ZLineAt (normOrdered2 a b) i K (iotaVL c₀) (zLineVal E a b i K (iotaVL c₀))`
   for all orders `i` — the order-`i` line at the lattice generators;
2. **mode law**: `ZLineModeAt E a b c i r K u` for `1 ≤ r` — the field of the coherent state
   `E⁻_a(z)_i ι(ab)` through one creation mode.

Both are landed at `i ≤ 1` and both are new at `i ≥ 2`.  The split is forced by the proof: the step
`zLineAt_modeVL_of_modeLaw` moves the line from a monomial to its `YFam`-descendant and needs the *value*
law there, while the *generator* law is the input at the bottom; neither is derivable from the other.
The converse of `zLineGeneratorBase_iff` is obtained by linearising the contraction over the line windows
(`zLineAtVal_of_mem_span`), which is what makes the base a faithful accounting of the residual and not an
artefact of the proof.

Supporting identities newly landed in the same file: the `j`-independent contraction
`momentSum_modeVL_normOrdered2` at weight `C(r,j)`; the Chu–Vandermonde identity
`binomCoeff_sub_eq_sum_moment` (`C(p−r,j) = Σ_l C(−r,l)C(p,j−l)`); the level induction
`ZLineAtAllLevel`/`_succ`/`_all`; the spanning assembly `zLineScheme_of_level`/`zLine_of_level`; and
`zLine_one_unconditional`, which re-derives the batch-195-B theorem without the base.

### 93.3 Accounting after batch 196

At FLM's datum (`E = C.toCentralExtension h2`, `C` an even cocycle, `form` symmetric):

| object | status |
| --- | --- |
| `l = 0`, `0 ≤ ⟨a,b⟩` and `⟨a,b⟩ = −1` | closed (earlier batches) |
| `l = 0`, `⟨a,b⟩ = −2` | closed (harvest) |
| `l ≥ 0` (`0 ≤ ⟨a,b⟩`) | closed (earlier) |
| `l = −1` | closed (batch 189) |
| `l = −2`, both chambers | **closed (harvest)** |
| `l = −c`, `ν ≥ c−2` | **closed (harvest)** |
| `l = −c`, `0 ≤ ν ≤ c−3` | `ZLine E j`, `j ≥ 2` — reduces to `ZLineGeneratorBase` |
| `l = 0`, `⟨a,b⟩ ≤ −3` | `NegThreeAndBelowResidualAligned` |
| Fock half / `CoherentCreatedStep` | open |
| continuation to full Jacobi (§8.8 / Props 8.10.3–8.10.7) | open |
| six boundary inputs `hnd/hs/S/hpd/hW/hfin` | open |

### 93.4 Brief errors (three, all consequential)

(a) The brief proposed to get the generator case from `firstDeriv^j`; but `zLineAt_firstDeriv` is an
**equivalence**, so it transfers the obligation rather than discharging it, and order 0 of
`firstDeriv^j(normOrdered2 a b)` is not a `normOrdered2`, so `assemblyDiagonal_antidiagonal` does not
apply.
(b) The step additionally needs the **lower-order** lines at degree `K+r` (not only order `j` at every
monomial).
(c) The step additionally needs the value law at the descendant — the second half of the base; a
one-half base would have been unsound bookkeeping.
(d) Index trap carried from batch 195: `zLineVal 0 K u = ε·genFam (a+b) K u` because
`genFam u m = YFam u (−m−1)`; an off-by-one there makes the mode law false.

## §94 Batch 197 — the order-2 line is two statements, and the Fock half is a display plus two carrier inputs

### 94.1 The truncated base (A)

Batch 196 reduced the whole `z_0^j` tower to one `c`-independent `ZLineGeneratorBase`.  Batch 197-A made
that reduction **partial and sharp**: `ZLineGeneratorBaseUpTo E J` restricts both halves to `i ≤ J`, and

```
zLineGeneratorBaseUpTo_iff (hs) (E) (J) : ZLineGeneratorBaseUpTo E J ↔ ∀ i, i ≤ J → ZLine E i
zLineGeneratorBase_iff_forall_upTo (hs) (E) : ZLineGeneratorBase E ↔ ∀ J, ZLineGeneratorBaseUpTo E J
```

hold with both directions at the same `J` — no direction secretly needs an order above the bound (the
brief feared one would; it does not).  The consumption is now chamberwise: the chamber `ν` of the
`l = -c` residual needs only the lines `1 ≤ j ≤ c-1-ν`
(`negCBinomMomentAlignedAt_of_lines`, with `hc : 1 ≤ c`), so `ZLine E 2` alone covers every chamber
`c - 1 - ν ≤ 2` (`negCBinomMomentAlignedAt_of_zLine_two`), i.e. the new chamber `ν = c-3`.

`zLine_two_iff` is the sharp statement of what is left at order two:

```
ZLine E 2 ↔ (the order-2 line at the lattice generators, GEN2) ∧ (the order-2 mode law, MODE2)
```

with the `i = 0, 1` components already discharged.  Everything else in the two A files is the
(8.4.16)/(8.4.12) window engine for the **derived factor** `a'(z) = (1/1!)(d/dz)a(z)` that MODE2
consumes; its tail correction is `-r(r+1)⟨c,a⟩ Y_{m+r+2}` at window `M ≥ r+1`.

MODE2 is not landed.  Its remaining step is pinned to three explicit items in the
`MMFLM86ZLineTwo.lean` header (the (8.5.5) recursion at degree two; the two *applied* `actionFamily`
laws; the three index/coefficient identifications), and the final coefficient arithmetic was checked
symbolically to close exactly against `ZLineModeAt`'s right-hand side.  GEN2 is untouched: it needs the
evaluation of the degree-2 coherent-state field at a lattice generator, which the landed derivative
ladder `zLineAt_firstDeriv` cannot supply (it is an equivalence, and `firstDeriv²(normOrdered2 a b)` is
not a `normOrdered2`, so the landed assembly does not apply).

### 94.2 The Fock half is two-layered (B)

Batch 197-B landed, at a general `E` with no cocycle hypothesis,

```
FockCreatedStep E ↔ IterateProductStepOnCreated (ZAligned E) convOneSided vacuumVL
FockCreatedStep E ↔ Display8610List (ZAligned E) vacuumVL convOneSided
FockCreatedStep E ↔ Display8610TwoOneSided E                -- given FockPairDatum + FockCreatedSpan
Display8610TwoOneSided E → CoherentCreatedStep E            -- given FockPairDatum + FockCreatedSpan
```

so the campaign's opaque Fock residual is *equivalent* to the concrete two-factor display (8.6.10) once
two named carrier inputs are granted: `FockPairDatum E` (every shifted field pairs finitely (8.10.5)
with the field of every created state) and `FockCreatedSpan E` (the created states span `V_L`).

The genuinely new mathematics here is **carrier linearity for the `dite` carrier**: unconditional
additivity of `convOneSided` in its second argument is FALSE (a compiled counterexample over `ℚ`,
`not_convOneSided_add_right_unconditional`), and the honest law is conditional on `PairFinite`
(`convOneSided_add_right_of_pairFinite`), which then transports along the span
(`pairFinite_shiftedField_of_mem_span`).  This is why the Fock residual is two-layered and not one: the
created-state evaluation alone does not give the general state without the carrier datum.

Non-vacuity of the datum is recorded at the vacuum-created state and at the single-factor
lattice-generator states with `0 ≤ ⟨a,b⟩`; the general case (lists of length ≥ 2, negative pairing) is
the open carrier statement, and it is *strictly stronger* than batch 182's `ShiftedPairFiniteGenerators`.

### 94.3 The next Fock step is probably cheap

`MM.FLM85CA.createdStateSpan_eq_top` (`MMFLM85ConvAdditive.lean:502`) already proves
`Submodule.span F (Set.range (iteratedCreation Y vac)) = ⊤` from a creation property `hcreate` and the
(8.5.2) mode identification `hmode` at an explicit family `umode`, by transporting the landed (8.5.4)
spanning.  So `FockCreatedSpan E` should be a *corollary* at `Y = ZAligned E`, `vac = vacuumVL` (the
landed (8.5.23) `creationPropertyAligned` gives `hcreate`), leaving only the (8.5.2) identification to
locate or to name.  That is the cheapest available reduction on the Fock front.

### 94.4 Corrections of record

1. `negCBinomMomentAlignedAt_of_lines` without `1 ≤ c` is **false** (`c = 0` forces
   `YFam(a+b)(m+n+1) = YFam(a+b)(m+n)`); the landed form carries `hc : 1 ≤ c`.
2. The order-2 mode law is **not** a homogeneous `actionFamily` statement: its first summand acts on the
   degree-one coherent field, whose commutator with `α_c(-r)` carries the (8.4.19) `⁺`-tail
   `-r⟨a,c⟩Y(a+b,z)`, so a two-component window law is required (the landed `actionFamily_modeVL` is
   homogeneous and does not apply as it stands).
3. The ledger's "the Fock half is implied by `IterateProductStep`" is now "equivalent to the `k = 2`
   display modulo `FockPairDatum` and `FockCreatedSpan`".
4. Dispatcher: the `MMFLM810TheoremEven.lean` ledger (the `⟨a,b⟩ = -2` bullet marked **open**, and the
   "three named residuals" paragraph) was corrected in place; the first conjunct of
   `EvenCocycleResiduals` is a theorem since batch 196.

### 94.5 Accounting after batch 197

| object | status |
| --- | --- |
| `ZLine E j`, `j ≤ 1` | theorem (`zLine_zero`, `zLine_one_unconditional`) |
| `ZLine E 2` | ⟺ GEN2 ∧ MODE2 (both open; MODE2 pinned to 3 explicit sub-steps) |
| `l = -c` chambers | `ν ≥ c-2` closed; `ν = c-3` closed once `ZLine E 2` lands |
| Fock | ⟺ `Display8610TwoOneSided` + `FockPairDatum` + `FockCreatedSpan` (span likely a corollary of landed material) |
| `NegThreeExpandedResidualAligned` | open (needs the degree-`k` coherent field for `k ≥ 2`) |
| `EvenCocycleJacobiStep` | open (assembly + whole `l ≠ 0` content + passage to (8.10.8)) |

## §95 Batch 198 — `ZLine E 2` is a theorem: the order-two base is closed on both halves

### 95.1 What closed

Batch 197 left the order-two line as exactly two statements.  Batch 198 proved both, each unconditionally at
a general `E` with only the symmetry `hs` of the form:

* **MODE2** = `MM.FLM86MLT.zLineModeAt_two` (`Definitions/MMFLM86ModeLawTwo.lean`, 618 lines);
* **GEN2** = `MM.FLM86GLT.zLineGeneratorTwo` (`MMFLM86GeneratorLineTwo{Aux,Eval,Comp,}.lean`, 1214 lines).

Hence (dispatcher capstone, `Definitions/MMFLM86ZLineTwoClosed.lean`)

```
zLine_two (hs) (E) : ZLine (F := F) bL form E 2
zLineGeneratorBaseUpTo_two (hs) (E) : ZLineGeneratorBaseUpTo (F := F) bL form E 2
negCBinomMomentAlignedAt_of_two (hs) (E) {c nu} (hc : 1 <= c) (hnu : nu <= c - 2) (hcJ : c - 1 - nu <= 2) :
    NegCBinomMomentAlignedAt (F := F) bL form E c nu
```

so the ``ν = c-3`` chamber of every `l = -c` face is unconditional, and this **supersedes NOTES 94.5's row
"`ZLine E 2` ⟺ GEN2 ∧ MODE2 (both open)"**.  The face-level bridge from
`NegCBinomMomentAlignedAt` to `NegCFaceAlignedFrom E c (c-3)` is still not landed (the recipe is: replace
`negCBinomMomentAlignedAt_sub_two` by `negCBinomMomentAlignedAt_of_zLine_two` and `(c-2)` by `(c-3)` in
`negCFaceAlignedFrom_subTwo_evenCocycle`).

### 95.2 The mathematics that was actually new

MODE2's proof needed the **two-component window law for the factor `a(z)`** (only the derived factor
`(1/1!)(d/dz)a(z)` had one, from batch 197-A), and it confirmed the (8.4.19) mechanism exactly: the
`δ`-window term and the `⁺`-tail correction are the SAME family, so they add to `+2r⟨a,c⟩B_{m+r+1}`
rather than cancelling.  GEN2's proof needed the **square of the creation half** (`flatMul_assoc`) for the
composite `:a(z)a(z)Y(ab,z):` head, and the window→`flatMul` bridge for a *shifted* field: at a lattice
generator the field is a creation exponential over `iota(a+b+c)`, so a bridge must relate the source vector
`w` and the target vector `w'` separately (`headWindow_eq_flatMul_of_shift`/`_of_shift`).

### 95.3 The `sorryAx`-from-elaboration-error trap (campaign-level)

The dispatcher's capstone first reported `[propext, sorryAx, Classical.choice, Quot.sound]` for all three of
its theorems.  Cause: its statements used `CentralExtension` without `open FLMLattice`, so the declarations
failed to elaborate and Lean replaced them by `sorryAx` terms — with the `#guard_msgs` mismatch as the ONLY
symptom (the driver still printed a `--- FAILED` line, but a `| tail` pipeline reported `exit 0`, masking
it for one round).  Rules adopted: scan the whole log for `error` lines; never use `… | tail` when the exit
code matters (use `set -o pipefail`); and after a green build, `#print axioms` every public declaration
from a scratch probe that has no guard docstring (a guard whose docstring was written from the actual output
can never catch this).

### 95.4 Corrections and traps of record

1. `import Definitions.MMFLM86ZLineTwo` does NOT give `zLine_two_iff` (that is in `MM.FLM86ZLineBaseUpTo`).
2. `M >= r+1` is required for the derived factor only; the generic applied law carries `r+1 <= M`.
3. The order-two assembly needs the three ring index identities in a specific order; `simp` normalises them
   the wrong way and leaves `K-2+r+2-2`.
4. `rw`/`simp [neg_smul]` does not fire on `(-A) • x` for `x : VL F L` (module instance diamond); use
   `module` or `(neg_smul A x).symm`.  `rw [← smul_add]` can rewrite the outer `(1/2) • (…)`; use
   `(smul_add _ _ _).symm` in a `calc`.
5. The derivative-ladder route to GEN2 does not exist as a shortcut: `zLineAt_firstDeriv` is an iff, but the
   order-one generator line is landed only for `normOrdered2` itself, not for its derivative.

### 95.5 Accounting after batch 198

| object | status |
| --- | --- |
| `ZLine E j`, `j <= 2` | theorem (`zLine_zero`, `zLine_one_unconditional`, `zLine_two`) |
| `ZLineGeneratorBaseUpTo E J`, `J <= 2` | theorem |
| `l = -c` chambers | `ν >= c-3` unconditional at `hs`; `0 <= ν <= c-4` = `ZLine E j`, `j >= 3` |
| `ZLineGeneratorBase` (all orders) | open: MODE-ALL + GEN-ALL (batch 199, in flight) |
| Fock | ⟺ `Display8610TwoOneSided` + `FockPairDatum` + `FockCreatedSpan` (`FockCreatedSpan` likely a corollary of the landed `createdStateSpan_eq_top`) |
| `NegThreeExpandedResidualAligned` | open |
| `EvenCocycleJacobiStep` | open (assembly + `l != 0` content + passage to (8.10.8)) |

## §96 Batch 199 — both halves of the general-`j` base are one named residual away

### 96.1 The two residuals of record

Batch 199 did for the general order `j` what batch 197 did for `j = 2`: it reduced each half of
`MM.FLM86ZLI.ZLineGeneratorBase` to ONE named statement, with the analytic inputs landed.

| half | status | the named residual |
| --- | --- | --- |
| mode law, all `j` | `j <= 2` landed; the rest is one induction step | `MM.FLM86MLA.AnchorModeCommStep E` |
| generator line, all `j` | LHS evaluated at every `j`; target ⟺ flat form | `MM.FLM86GLA.ZAlignedGeneratorFlat E` |

The consumers are landed: `MM.FLM86MLA.zLineModeAt_all_of_step` (the step gives the mode law at every `j`)
and `MM.FLM86GLA.zLineGeneratorAll_of_flat` (the flat form gives the generator line).  So once the two
residuals are theorems, `ZLineGeneratorBase` is a theorem, hence `zLine_all_of_generatorBase` and
`negCBinomMomentAligned_of_generatorBase`: EVERY chamber of EVERY `l = -c` face becomes unconditional.

### 96.2 The new mathematics of batch 199

* **The general-`n` derived-factor window law** (`MM.FLM86MLA`): the (8.4.16)/(8.4.19) head/tail behaviour of
  `(1/(n-1)!)(d/dz)^{n-1}a(z)` for every `n >= 1`, with the `^+`-commutator firing at `k = r+n-1` and the
  zero-mode repair `-n<c,a>C(-r,n)Y_{m+r+n}`.  Its applied form `actionFamily_modeVL_of_window` carries the
  window bound `r+n-1 <= M` — **the landed `actionFamily_two_modeVL_of` hardwires `r+1 <= M`, which is a
  genuine gap for `n >= 3`** (a brief-level correction of record).
* **The anchor-field layer** (`A_m = YzeroField (baseAligned E) (E^-_a(z_0)_m iota(ab))`, the (8.5.5)
  recursion for it, `zLineVal_eq_anchorField`) — this is also the natural language for the `l = 0`,
  `<a,b> <= -3` residual, and batch 201-B is using it there.
* **The order-`j` weight bridge** (`MM.FLM86GLA`): `sum_{i in Icc 0 N} C(i,j) X_i (Y_{N-i} w) =
  (j!)^{-1} flatMul (iterDeriv j X) Y (N-j) w`, which evaluates the whole left-hand side of the generator
  line at every `j`.

### 96.3 Accounting after batch 199

| object | status |
| --- | --- |
| `ZLine E j`, `j <= 2` | theorem |
| mode law, all `j` | ⟺ `AnchorModeCommStep` (`j <= 2` proved) |
| generator line, all `j` | ⟺ `ZAlignedGeneratorFlat` (`j <= 2` proved) |
| `l = -c` chambers | `ν >= c-3` unconditional; the rest is the two residuals above |
| `l = 0`, `<a,b> <= -3` | `NegThreeExpandedResidualAligned`; batch 201-B is reducing it to the anchor values |
| Fock | `Display8610TwoOneSided` + `FockPairDatum` + `FockCreatedSpan` |
| `EvenCocycleJacobiStep` | open (assembly + `l != 0` content + passage to (8.10.8)) |

### 96.4 Corrections and traps of record (batch 199)

1. The general-`i` window law needs no Leibniz induction (closed forms + `iterDeriv_apply_smul`).
2. `actionFamily_two_modeVL_of`'s window bound `r+1 <= M` is insufficient for `n >= 3`;
   `actionFamily_modeVL_of_window` is the honest template.
3. The order-`j` weight expansion is `MM.FLM86ZM.binomCoeff_add_eq_sum`;
   `MM.FLM86ZLI.binomCoeff_sub_eq_sum_moment` is the moment-level (mode-law) expansion.
4. `normOrdered2_iotaVL` is in `MMFLM86LimitStep.lean:482` (there is no `MMFLM86LS.lean`).
5. GEN2 generalises verbatim only on the left half; the right half for `j >= 3` acts on the field of a lower
   coherent state, and the general-`r` action evaluations at `iota(c)` are not landed.
6. The mode law's final identification needs the (8.5.5) recursion at order `j-1-l` plus the triangle
   transpose; the tail coefficient `-n<c,a>C(-r,n)` is forced by the count.

## §97 Batch 200 — the Fock span is discharged; the all-order generator line is complete up to one finite-sum assembly

### 97.1 Fock: one carrier input left, and it is `PairFiniteAll`

```
fockCreatedSpan (E) : FockCreatedSpan E                                    -- UNCONDITIONAL, no hs
fockPairDatum_iff_pairFiniteAll (E) : FockPairDatum E <-> PairFiniteAll E
PairFiniteAll E := forall a x, PairFinite (ZAligned E a) (ZAligned E x)
coherentCreatedStep_of_twoOneSided_of_pairDatum : FockPairDatum E -> Display8610TwoOneSided E -> CoherentCreatedStep E
fockPairDatum_imp_negPairing : FockPairDatum E -> PairFiniteNegPairing E
```

So the Fock front is now: **`Display8610TwoOneSided`** (the concrete two-factor (8.6.10) display) **plus**
`PairFiniteAll` (equivalently `FockPairDatum`, and implied by the weaker-named
`PairFiniteNegPairing` together with batch 182's positive part).  NOTES 94.5's Fock row is superseded: drop
`FockCreatedSpan`, replace `FockPairDatum` by `PairFiniteAll`, and drop the "lists of length >= 2" case
(it collapses by `pairFinite_shiftedField_iff` + the spanning).

### 97.2 GEN-ALL: everything but one finite-sum identity

Batch 200-A landed the whole computation around the residual: the algebra (triangle reindexings,
`sum_range_alternating_binomCoeff`, `prod_range_sub_eq_neg_pow_mul_factorial`, `binomCoeff_mul_pred`),
the creation half of the next derived factor (`splitMinus_factorFamilyZero_succ`, through `heisFamZero`),
the tail at `iota(c)` (`splitPlus_factorFamilyZero_succ_apply_iotaVL`,
`killsAbove_factorFamilyZero_succ_iotaVL`, `tailWindow_factorFamilyZero_succ_iotaVL`), the (8.4.16) head
against the flat value at all orders (`sum_head_flatGeneratorValueZ`), the tail collapse
(`tailOp_factorFamilyZero_flatGeneratorValueZ`), the (8.5.5) recursion at a generator in component form
(`ZAligned_creationExpVL_eq_sum_actionFamily`), and the CORRECTED factorial identity
`sum_factorial_flatMul_iterDeriv`.  What is left is the bookkeeping identity ASSEMBLY
(`(sum head_r) + (sum tail_r) = j.eps.sum_l C(s,l)((j-l)!)^{-1} D_{j-l}(N_l)`), with the proof route and the
coefficient count hand-verified; `ZAlignedGeneratorFlat` itself is NOT yet a theorem.

**Correction of record**: the "item (iv)" identity recorded in batch 199-B's report
(`D_j = sum_r C(j-1,r) flatMul (iterDeriv r a^-) D_{j-1-r}`) is **FALSE** — at `j = 2` it gives
`2 flatMul a^- E^-_{a+b}` instead of `flatMul (deriv a^-) E^-_{a+b} + flatMul (a^- a^-) E^-_{a+b}`.  The
landed correct form is `sum_factorial_flatMul_iterDeriv`.

### 97.3 Traps of record (batch 200)

1. The window replacement in the tail cannot use the factor's own bound `r+1 <= factor.bound`: the `k = r`
   value `(-1)^r<a,c>` may vanish, so the honest comparison is `max bound (r+1)`.
2. No `c`-independent operator-valued flat family can equal `ZAligned` at the coherent state — the (8.4.17)
   shift lives in the value at `iota(c)`; state the head against the flat value at components `n+i`.
3. `{iota(c)}` spans only `vacuum (x) F{L}`, so "reduce an arbitrary single-factor state by the landed
   spanning" does not work as stated; the correct reduction is via `PairFiniteAll`.
4. The `vertexOpOfField (Yaligned E)` spelling of the (8.5.23) creation property is DEFINITIONALLY
   `toVertexOp (ZAligned E)` — a bridge lemma is neither needed nor desirable.

### 97.4 Accounting after batch 200

| object | status |
| --- | --- |
| generator line, all `j` | ⟺ `ZAlignedGeneratorFlat`; ALL inputs landed, one finite-sum ASSEMBLY left |
| mode law, all `j` | ⟺ `AnchorModeCommStep` (batch 201-A, to be resumed) |
| Fock | `Display8610TwoOneSided` + `PairFiniteAll` (`FockCreatedSpan` DISCHARGED) |
| `l = 0`, `<a,b> <= -3` | `NegThreeExpandedResidualAligned` (batch 201-B, to be resumed) |
| `EvenCocycleJacobiStep` | open (assembly + `l != 0` content + passage to (8.10.8)) |

## §98 Batch 201 — the mode-law half is unconditional; `ZLineGeneratorBase` now rests on the generator half alone

### 98.1 `zLineModeAt_all` (unconditional)

```
anchorModeCommStep (hs) (E) : AnchorModeCommStep E            -- MM.FLM86MLA, batch 201-A
zLineModeAt_all (hs) (E) : forall j a b c r, 1 <= r -> forall K u, ZLineModeAt ... j r K u
```

So the second half of `MM.FLM86ZLI.ZLineGeneratorBase` is a theorem at a general `E` with only `hs`, and
NOTES 97.4's row "mode law, all `j` ⟺ `AnchorModeCommStep`" is superseded.  `ZLineGeneratorBase` now rests
on the FIRST half alone: `MM.FLM86GLA.ZAlignedGeneratorFlat E`, whose whole computation batch 200 landed
(one finite-sum ASSEMBLY left).

The one genuinely new input was the (8.4.16)/(8.4.19) shift against a **finite family** of correction fields:
the landed `actionFamily_modeVL_of_sumWindow` keeps a single `-gamma.headWindow` term OUTSIDE the `sum_l`,
so summing the landed single-field shifts counts it `N` times.  `headWindow_factorFamilyZero_modeVL_shift_sum`
and `tailWindow_factorFamilyZero_modeVL_shift_sum` fix that, and `modeCommFam_step` is the abstract step
(consuming the (8.5.5) recursion as a hypothesis) that closes the induction.

### 98.2 The `l = 0`, `<a,b> <= -3` residual, reduced to `normOrdered2` alone

```
negThreeExpandedResidualAligned_iff_anchorForm (E) : NegThreeExpandedResidualAligned E <-> NegThreeAnchorForm E
anchorGeneratorValue_iff_zAlignedGeneratorFlat (E) : AnchorGeneratorValue E <-> ZAlignedGeneratorFlat E
negThreeExpandedResidualAligned_iff_chamberMomentForm (hs) (E) (hZ : ZLineAll E) :
    NegThreeExpandedResidualAligned E <-> NegThreeChamberMomentForm E
negThreeAtMinusThree_iff_chamberMomentFormAtMinusThree (hs) (E) : ...   -- the -3 slice, unconditional
```

Three structural facts worth remembering: (i) the anchor-field spelling costs NOTHING (an IFF with no
hypothesis); (ii) the "anchor values at generators" statement is not a new residual — it IS
`ZAlignedGeneratorFlat`; (iii) the residue's summand is an OPERATOR component, not a value at `iota(c)`,
because `{iota(c)}` spans only the lattice factor and the Fock half must not be lost.

### 98.3 Corrections of record

1. There is NO iff between the residue and the anchor VALUES: the residue's left-hand side is the honest
   commutator `twoVarField - swap2`.
2. The `<a,b> = -3` slice does NOT follow from the landed `k <= 2` tower: the anchor fields cancel in the
   residue and the `N = 3` chamber collapse remains (`NegThreeChamberMomentFormAtMinusThree`).
3. Batch 200 did not close `ZAlignedGeneratorFlat` (it landed the recursion at a generator plus the head/tail
   evaluations).
4. `MM.FLM86HAPF`/`MM.FLM86CF2` are namespaces, not file names.
5. Lean: `-(C) • Z` negates the SCALAR, `a * b • c` parses `a * (b • c)` (`•` infixl:73 > `*` infixl:70),
   and the printer renders `(-C)•Z` and `-(C•Z)` identically — the `delta` family must be
   `((-1:F) * (theta * C l))`.  Unapplied `rw [neg_smul]`/`[smul_sub]`/`[smul_smul]`/`[Finset.smul_sum]`
   fail on syntactically identical occurrences in this pin, and `abel` mangles additive indices inside atom
   arguments; use explicitly applied local `have`s.
6. The `1/j` is never introduced: multiply by `j`, use `(j-1-l) + (l+1) = j`, cancel by
   `smul_right_injective`; the reindex `t = i+1` is unnecessary.

### 98.4 Accounting after batch 201

| object | status |
| --- | --- |
| mode law, all `j` | **THEOREM** (`zLineModeAt_all`) |
| generator line, all `j` | ⟺ `ZAlignedGeneratorFlat`; all inputs landed, one finite-sum ASSEMBLY left |
| `ZLineGeneratorBase` | ⟺ `ZAlignedGeneratorFlat` ALONE |
| `l = -c` chambers | once `ZAlignedGeneratorFlat` lands: every chamber, by `zLine_all_of_generatorBase` |
| `l = 0`, `<a,b> <= -3` | ⟺ (given `ZLineAll`) `NegThreeChamberMomentForm`; the `-3` slice is an unconditional IFF |
| Fock | `Display8610TwoOneSided` + `PairFiniteAll` |
| `EvenCocycleJacobiStep` | open (assembly + `l != 0` content + passage to (8.10.8)) |

## §99 Batch 202 — the tower is closed; every `l = -c` face is unconditional

### 99.1 The three-step composition

```
batch 201 : zLineModeAt_all                                   -- the mode-law half, unconditional
batch 202A: zAlignedGeneratorFlat -> zLineGeneratorAll -> zLineGeneratorBase
            zLine_all_of_generatorBase, negCBinomMomentAligned_of_generatorBase
batch 202B: negCFaceAlignedFrom_of_lines (+ the generator-base consumers)
dispatcher: negCFaceAligned_evenCocycle                        -- the whole l = -c face at FLM's datum
```

So Corollary 8.8.17 (8.8.41)'s `l != 0` content is settled: for every `c >= 1` and every pairing
`0 <= <a,b>` the cross-bracket equals the cross-iterate at the even-lattice extension, and the underlying
chamber identity `NegCBinomMomentAligned E c` even holds at a GENERAL `E` with only the symmetry `hs`.

### 99.2 Why the face consumer was cheap

Batch 202-B's key observation: the numerical identity `c-1-(c-2) = 1` is used only inside
`negCBinomMomentAlignedAt_sub_two`'s proof of the CHAMBER, never in the face consumer.  Hence the consumer
generalises verbatim to `NegCFaceAlignedFrom E c (c-1-J)` with no `C(r+m,k)` weight split, and the only new
arithmetic is `c-1-J <= nu -> c-1-nu <= J`.  This is why the whole face became unconditional essentially for
free once the tower closed.

### 99.3 Corrections and traps of record (batch 202)

1. `MM.FLM86GAI.sum_factorial_flatMul_iterDeriv` is stated over ℚ-scalars (`[Algebra QQ A]`); at
   `Module.End F (VL F L)` the resulting `HSMul` terms do not unify with F-scalars.  Landed the F-scalar form
   `sum_factorial_flatMul_iterDeriv_F` (cf. the ℚ-vs-`HahnSeries` traps already in AGENTS.md).
2. The head window replacement is off by one: kills-bound `M0+1`, `M0 = (q - <a,b+c> - n - 1).toNat`.
3. Family-level lemmas applied to a component and then to `iotaVL c` need an explicit
   `sum_apply`/`smul_apply` distribution step.
4. The tail reindexing needs `Finset.sum_congr` (the Nat subtraction does not reduce), the `L = 0` split before
   `sum_range_alternating_binomCoeff`, and a final scalar reorder.
5. The template of a consumer must bind `E = C.toCentralExtension h2` explicitly; `negCFaceAlignedGe_evenCocycle`
   covers the whole range `nu >= c-1`, not one chamber.

### 99.4 Accounting after batch 202

| object | status |
| --- | --- |
| `ZLine E i`, every `i >= 1` | **THEOREM** (general `E`, only `hs`) |
| `ZLineGeneratorBase` | **THEOREM** |
| `NegCBinomMomentAligned E c`, every `c >= 1` | **THEOREM** (general `E`) |
| `NegCFaceAligned (C.toCentralExtension h2) c`, every `c >= 1` | **THEOREM** (whole face, all chambers) |
| `l = 0`, `<a,b> <= -3` | `NegThreeChamberMomentForm` (equivalently `NegThreeExpandedResidualAligned`) |
| Fock | `Display8610TwoOneSided` + `PairFiniteAll` |
| `EvenCocycleJacobiStep` | open: the `l = 0` assembly at (8.6.2) states + the passage to (8.10.8) |

## §100 Batch 203 — the Fock ledger corrected; the `l = 0` face assembled at all states; the `<= -3` residual's exact status

### 100.1 The Fock front is ONE statement

```
display8610TwoOneSided_iff_fockCreatedStep (E) : Display8610TwoOneSided E <-> FockCreatedStep E   -- no hypotheses
coherentCreatedStep_of_twoOneSided (hnd) (hs) (E) : Display8610TwoOneSided E -> CoherentCreatedStep E
```

The mechanism is worth remembering, because it retired a whole layer: the display's `l = 0` slice uses the
unconditional (8.5.23) creation property `(Y v)_{-1} iota(1) = v`, so that slice is `IterateProductStepAt` at an
ARBITRARY state, and `iterateProductStep_iff_forall_at` makes it the full one-step (8.4.25).  The carrier inputs
(`FockPairDatum`, `PairFiniteAll`, `FockCreatedSpan`) were an artefact of the created-state route (batch
197-B/200-B), not of the mathematics.

### 100.2 The `<a,b> <= -3` residual cannot be reformulated into something easier

```
negThreeAndBelowResidualAligned_iff_chamberMomentForm (hs) (E) :
    NegThreeAndBelowResidualAligned E <-> NegThreeChamberMomentForm E          -- both directions, only hs
residueAtN_iff_chamberMomentAtN (E) (N) : ResidueAtN E N <-> ChamberMomentAtN E N
allChamberMoment_iff_slices : AllChamberMoment E <-> C1 /\ C2 /\ NegThreeChamberMomentForm E
not_allChamberMoment_rankOne : not (AllChamberMoment (F:=Q) (L:=Z) basisUnitInt formR extR)
```

So: the `<= -3` residual IS the `N >= 3` chamber collapse; the `N = 1, 2` slices are theorems at FLM's datum
(and FAIL without evenness --- the rank-one refutation above); and no pointwise slice is cheaper.  Do not spend
budget re-spelling this residual.

### 100.3 The all-states assembly, and its one named residual

`corollary851_allStates_of_lattice_and_step` assembles the (8.5.4) states by an explicit `List.induction` from
the lattice corner plus a STEP; the step is named `Corollary851ModeStep` (the two one-creation-mode steps
`C u v -> C (alpha_c(-r) u) v` and `C u v -> C u (alpha_c(-r) v)` at the SAME window `K`).  The window side
condition `hwin : forall a b, (-<a,b>).toNat <= K` is explicit because `ResidueNegativeAligned` is per-pair
canonical-window.  Composed consumers: `corollary851_allStates_of_residuals`,
`corollary851_allStates_of_fockCreatedStep`.

### 100.4 Traps of record (batch 203)

1. A literal `List.foldr` in the goal makes the (8.5.4) induction blow the `whnf` budget; state through
   `stateOfVL` and rewrite with `rfl` unfolding lemmas via `simpa only` (do NOT raise `maxHeartbeats`).
2. The positive-pairing half of the lattice corner exists only at the even cocycle (cocycle compatibility), so a
   composition that needs both halves lives at `C.toCentralExtension h2`; use the arbitrary-`Y` theorem
   `corollary851_allStates_of_lattice_and_step` if a general-`E` producer of the corner becomes available.
3. `hnd` is spent only by the Fock conjunct of the residual package.

### 100.5 Accounting after batch 203

| object | status |
| --- | --- |
| `l = -c` faces, all `c >= 1` | THEOREM (batch 202) |
| `NegTwoFirstDerivZero` | THEOREM |
| `NegThreeExpandedResidualAligned` = `NegThreeChamberMomentForm` | open (== the residual; `N=1,2` slices done, `N>=3` open) |
| `CoherentCreatedStep` | open, implied by `FockCreatedStep` = `Display8610TwoOneSided` (ONE statement now) |
| `l = 0` face at all states | `Corollary851ModeStep` + the lattice corner (named) |
| `EvenCocycleJacobiStep` | (ii) done; (i) as above; (iii) untouched |

## §101 Batch 204 — the `<= -3` residual is proved; the Fock front is the shift-zero corner

### 101.1 The residual that was called hard

Batch 203-A recommended not attacking `NegThreeChamberMomentForm`, calling it identical to the residual.  Batch
204-A showed the CHAMBER spelling is where it is easy: everything happens on ONE antidiagonal family
`M p = normOrdered2 E a b p (K-p) v`, the two chamber half-lines `p >= N-m-1` and `p <= -m-1` against the full
moment line with weight `C(p+m,N-1)`, with the (8.4.21) transpose supplying `c(b,a)`, the (8.5.37) coefficient
identities on the first chamber, the cocycle sign `c(b,a) = (-1)^N` on the second, and the falling-factorial
zero on the gap.  The only general-`E` input is that sign (`CocycleAtPairing`), a theorem at the even cocycle;
the underlying scalar identity holds BOTH ways (`neg_mul_ratioCoeff_eq_iff`).

Consequences: `ResidueNegativeAligned (C.toCentralExtension h2)` is now a THEOREM (the whole negative-pairing
`Res_{z_0}` face), and `EvenCocycleResiduals`'s second conjunct is discharged.  "Evenness" was the wrong word:
only `c(b,a) = (-1)^N` is used; at `N = 1` this is necessary (rank-one refutation), at `N >= 3` the general-`E`
form is undecided.

### 101.2 The Fock front, sharpest form

```
FockShiftZeroStep E := forall x v, ZAligned E ((ZAligned E x) (-1) v) = convOneSided (ZAligned E x) (ZAligned E v)
fockCreatedStep_iff_level_zero / fockCreatedStep_iff_shiftZero (hnd) (hs) (E)
```

The `L(-1)` ladder identifies the `j`-th level of (8.4.25) at `(x,v)` with the level-zero statement at
`(1/j!)L(-1)^j x` (iterated (8.10.13)); the abstract lemma carries no hypothesis on the product, so it applies
to the `dite` carrier.  `hnd`/`hs` turned out to be redundant on every consumer
(`coherentCreatedStep_of_twoOneSided_noHyp`, `fockCreatedStep_iff_createdStep`,
`fockCreatedStep_imp_coherentCreatedStep`).

### 101.3 A warning worth keeping

The Fock-level step through the mode laws does NOT work: the landed action laws
(`MM.FLM86MLA.actionFamily_factorFactorZero_modeVL`, `actionFamily_modeVL_of_window`) take the two-component
commutator as a HYPOTHESIS on the accumulated field, and the missing input would be the commutator of two
arbitrary honest modes --- exactly the open Jacobi content.  The `L(-1)` ladder avoids it entirely, which is why
the front collapsed from "display + two carrier inputs" to one shift-zero corner in three batches.

### 101.4 Accounting after batch 204

| object | status |
| --- | --- |
| `ResidueNegativeAligned` at FLM's datum | **THEOREM** |
| `NegThreeExpandedResidualAligned` (either spelling) | **THEOREM** at FLM's datum; general `E` needs `CocycleAtPairing` |
| `l = -c` faces | THEOREM (batch 202) |
| `CoherentCreatedStep` | open; ⟸ `FockShiftZeroStep` (= `FockCreatedStep` = the display), no `hnd`/`hs` needed |
| `EvenCocycleJacobiStep` (i) | `Corollary851ModeStep` + the lattice corner |
| `EvenCocycleJacobiStep` (iii) | untouched (Theorem 8.8.9 / Prop 8.10.7 route) |

## §102 Batch 205 — the Fock corner is refuted; the `l = 0` face is one mode step

### 102.1 A refuted target, and FLM warned us

`FockShiftZeroStep E` --- equivalently `FockCreatedStep E` and `Display8610TwoOneSided E` (batch 204-B's and
203-B's equivalences) --- is FALSE at honest data:
`not_fockShiftZeroStep_of_gram (E) (i) (hgram : form (bL i) (bL i) != 0)`, with an unconditional rank-one
instance, spending neither `hnd` nor `hs`.  The failing configuration is one oscillator on the vacuum:
`x = alpha_a(-1) iota(0)`, where the convolution has a summand `((-j)<a,a>)iota(0) != 0` for every `j <= -1`,
so `PairFinite` fails and `convOneSided` is identically `0` there while the two sides of (8.4.25) are not.

FLM flags exactly this: Remark 8.5.2 (p. 200) on (8.5.14) "not rigorous in the present setting", and Remark
8.6.4 (p. 211) on (8.6.28) "formal but suggestive".  The honest identity at a created state is the
NORMAL-ORDERED `Y(u_{-1}v) = :Y(u)Y(v):`; the plain product differs by the contraction.  The practical lesson for
this campaign: when a residual is "the book's display", check whether the book itself calls it formal.

### 102.2 What survives, and the honest Fock front

`CoherentCreatedStep` (the third conjunct of `EvenCocycleResiduals`, and the only Fock object the boundary
theorem consumes) is NOT refuted: its factors are honest GENERATOR fields (the second shifted), where the
carrier is batch 182's `pairFinite_shiftedField_ZAligned_iotaVL` for `0 <= <a,b>`, and the oscillator state
above does not occur.  So the honest front is the GENERATOR SLICE of (8.6.10)
(`Display8610TwoGenerators` / `CoherentCreatedForm`, batch 185-A's
`display8610TwoGenerators_iff_coherentForm`), with `PairFiniteNegPairing` the only open carrier case.
`fockCreatedStep_imp_coherentCreatedStep` and `coherentCreatedStep_of_twoOneSided_noHyp` are now VACUOUS.

### 102.3 The `l = 0` all-states face, precisely

```
allStates_iff_corner_and_modeStep (Y) (K) : (forall u v, C u v K) <-> corner /\ Corollary851ModeStep Y K
corollary851_latticeFactor : the corner extends to span{iota(a)} x span{iota(a)}   -- the exact largest slice
corollary851_iff_faceOf : C u v K <-> FaceOf Y (Y u) v K                          -- the face is a linear condition on the field
modeStepLeft_iff_faceOf_closure : the mode step = preservation of the face submodule by the (8.4.16) action
```

Given the corner (a theorem since batch 204-A), the mode step is the whole face content; its expansion terminates
in the mode--field commutators `[alpha_c(e), ZAligned E v n]` at arbitrary `v`, which the landed action laws
take as `hcomm` and return only up to a third term `kappa . Yt.fam (m+r+n)`.  `MM.FLM810CFC.currentFieldComm` is
(7.1.5) at the repaired BASE field only, so it is not the missing input.

### 102.4 Accounting after batch 205

| object | status |
| --- | --- |
| `l = -c` faces; `ResidueNegativeAligned`; `NegThree*` | THEOREM (batches 202, 204-A) |
| `NegTwoFirstDerivZero` | THEOREM |
| `CoherentCreatedStep` | open; honest producer = the GENERATOR slice of (8.6.10) |
| `FockCreatedStep` / `Display8610TwoOneSided` / `PairFiniteAll` | **REFUTED** |
| `l = 0` face at all states | = `Corollary851ModeStep` (= the mode--field commutators), open |
| `EvenCocycleJacobiStep` (iii) | untouched |

## §103 Batch 206 — the generator slice's `(0,0)` corner proved; the two exact residuals named

### 103.1 The Fock front, now precise

```
createdStepAt_zero_zero (hs) (0 <= <a,b>) : the (j,l) = (0,0) instance at generators   -- THEOREM, no hnd
coherentCreatedStep_iff_twoGenerators / <-> CoherentCreatedForm                       -- both ways
weightedAssemblyDiagonalZero_iff_assemblyDiagonal : the r = 0 slice IS (8.4.20)        -- both ways
```

The residual is **(WAD) = `WeightedAssemblyDiagonal E` at `r >= 1`**:
`sum_{p+q=K} C(K-p,r) normOrdered2 a b p (K-p) v = eps(a,b) ZAligned E (E^-_b(z_0)_r iota(a+b)) (r-K-1) v` on a
finite window, with the dictionary `CreatedStepAt E a b 0 l <-> (WAD)` at `r = l-<a,b>`,
`K = l-m-1-<a,b>` (and `j >= 1` the `L(-1)` ladder; `<a,b> < 0` additionally `PairFiniteNegPairing`).

Two more vacuous-theorem findings: `MM.FLM86CCS.createdStep_of_iterateProductStep` is vacuous (its
`IterateProductStep` at `(x,0)` with base `v := x` IS the refuted `FockShiftZeroStep`); and NOTES §102.2's
"the oscillator-carrying state does not occur" holds only for the FACTORS, since `creationExpVL b l (iota b)` is
oscillator-carrying for `l >= 1`.  What saves the generator slice is the carrier (pairs of shifted generator
fields, finite for `0 <= <a,b>`) plus (WAD).

### 103.2 The §8.6 engine: what it now has, and the one carrier it lacks

Landed at the honest field: the (8.6.5) series and its laws; `powerFam = YFam(-m-1)` with the exact pairing
shift `Y(a,w)_m iota(c) = E^-_a(w)_{m-<a,c>} iota(ac)`; `splitFold` (iterated (8.4.16), with `k = 1`
`Y(a,w)` and `k = 2` the landed `normalPair`); (8.6.10) at `k = 1`; and (8.6.6)/(8.6.8) at `k = 2` matching
the landed (8.4.20) assembly.

**Gap: (8.6.6) for `k >= 3`** --- a `k`-variable nested Cauchy product with local finiteness.  The carrier has
only the two-variable `convWith2`, which (8.4.20) uses twice.  The passage (iii) needs this carrier first.

### 103.3 Corrections (B206-B)

1. (8.6.5) and `kFoldNormalOrder` were already landed in batch 119 (`MMFLM86MultiState`, `MMFLM86KFold`);
   ROADMAP:5013-5015 / NOTES:1055-1056 were right and ROADMAP:4679 is stale.
2. `kFoldNormalOrder` is not (8.6.6)'s middle family for `k >= 2` on honest fields (its mode splitting includes
   `E^+`); only `normOrdered2` is.
3. Remark 8.6.4 shows the PLAIN product and calls it formal --- the normal-ordered repair is ours.
4. The `iota`-shifts are (8.5.11), not (8.6.5).
5. No associativity for the `k`-fold normal-ordered product exists in §8.6.

### 103.4 Accounting after batch 206

| object | status |
| --- | --- |
| `ZLine` tower / `l = -c` faces / `ResidueNegativeAligned` / `NegTwoFirstDerivZero` / `NegThree*` | THEOREM |
| `CoherentCreatedStep` | `(0,0)` at generators THEOREM; open from `(j,l) != (0,0)`; residual (WAD) at `r >= 1` |
| (8.6.6)`_{k>=3}` | the `k`-variable nested Cauchy carrier --- needed for (iii) |
| item (i) | `Corollary851ModeStep` = the mode--field commutators |
| (iii) | not reached |

## §104 Batch 207 — the nested Cauchy carrier is built; the Fock residual is (WAD) at `r >= 1`

### 104.1 The dictionary (both ways)

```
createdStepAt_zero_iff_weightedAt (hs) (E) (a b) (hN : 0 <= <a,b>) (hl : <a,b>.toNat <= l) :
    CreatedStepAt E a b 0 l <-> WeightedAssemblyAt E a b (l - <a,b>.toNat)
weightedAssemblyAt_iff_createdStepAt_zero : WeightedAssemblyAt E a b r <-> CreatedStepAt E a b 0 (r + <a,b>.toNat)
weightedAssemblyAt_zero : the r = 0 slice IS the landed (8.4.20)
createdStepAt_zero_of_lt : the gap l < <a,b>.toNat is a theorem (both sides 0)
```

So at `0 <= <a,b>` the Fock residual's entire `j = 0` face is (WAD) at `r >= 1`.  The negative-pairing face is NOT
covered (the (8.4.25) expansion and batch 182's carrier exist only for `0 <= <a,b>`; that face needs
`PairFiniteNegPairing` and an expansion of its own), and `j >= 1` is NOT covered because the `L(-1)` ladder
reduces level `j` to level 0 at the TRANSLATED factor `(1/j!)D^j a` --- a descendant of `iota(a)`, not a lattice
generator.  That is the measured reason the consumer cannot be composed yet.

### 104.2 The nested Cauchy carrier, and (8.6.6)/(8.6.8) at general k

```
normOrderedK_vacuum (E) (k) (as : Fin k -> L) (r : Fin k -> Nat) :
    (normOrderedK bL form E k as (fun i => (r i : Z))) vacuumVL
      = blockScalarK E k as . series865 bL form k as (sum i, as i) r
normOrderedK_one = MM.FLM86E86.powerFam ;  normOrderedK_two = MM.FLM86TN.normOrdered2
```

The finiteness of the nested product is a THEOREM, not an input: `locallyFiniteK_famFold` handles any ordered
product of one-variable locally finite families, so only `creationPairK` fails to be locally finite (the landed
`creationPair2_not_locallyFinite2`), which is (8.4.20)'s nesting kind.  Remaining in this route: (8.6.6)'s SECOND
equality (the pairing-factor family `prod_{i<j}(w_i-w_j)^{-<abar_i,abar_j>}`; the landed batch-119
`Display866Family3` plus the OPE (8.4.22)/(8.4.36)).  No general-`k` symmetry or associativity was invented ---
FLM states (8.4.21) for two factors only, and only `k = 2` is landed.

### 104.3 Traps of record

1. The shifted-weight collapse is orientation-sensitive: the needed identity is the created-state orientation
   `sum_ratioCoeff_mul_binomCoeff_shift` plus its GAP case `..._of_lt` (new in this batch), not the
   batch-203/204 moment machinery.
2. The `j >= 1` ladder does not feed the dictionary (descendant vs generator) --- do not assume it does.
3. The Fock residual's global spelling lives on the POSITIVE-pairing face; stating it globally is false.

### 104.4 Accounting after batch 207

| object | status |
| --- | --- |
| (8.6.6)/(8.6.8) at general `k` | **THEOREM** (nested Cauchy carrier built; finiteness discharged) |
| Fock residual | (WAD) at `r >= 1` = `CreatedStepAt(0,l)` at generators (dictionary both ways); `j >= 1` and the negative-pairing dictionary untouched |
| (8.6.6) second equality | the pairing-factor family + OPE (8.4.22)/(8.4.36) --- the next step of route (iii) |
| item (i) | `Corollary851ModeStep` (mode--field commutators) |
| (iii) | not reached |

## §105 Batch 208 — (WAD) is a theorem; (8.6.6)'s second equality is a named Prop at `k >= 3`

### 105.1 Reading the tower backwards

`WeightedAssemblyAt E a b r` holds at EVERY weight and EVERY pair (`weightedAssemblyAt_all`), with no positivity,
no evenness and no carrier input.  The proof is `zLine_all` at the TRANSPOSED pair `(b,a)` with order `r` and
scheme parameter `n = r-K-1` (diagonal degree `K` --- no index renormalisation), then the reindex `p |-> K-p`,
the (8.4.21) transpose (which moves the weight to the second index and produces `c(b,a)^-1`), the anchor expansion
`creationExpVL_anchorVL`, and finally `eps_mul_comm` (7.1.26).  **The real content is the weight ORIENTATION**:
`momentSum` weights the first index, (WAD) the second.  Consequence: `CreatedStepAt E a b 0 l` for ALL `l` at
`0 <= <a,b>` (`createdStepAt_zero_of_nonneg`), so the Fock residual's `j = 0` positive face is CLOSED.

The exact residual of `CoherentCreatedStep` is now, both ways
(`coherentCreatedStep_iff_of_pos_zero_face`):

1. `CreatedStepAtZeroNegPairing E` --- the negative-pairing orientation of the dictionary (needs
   `PairFiniteNegPairing` AND its own expansion; the (8.4.25) expansion is refuted at a negative pairing);
   note (WAD) itself is a theorem there too, so only the `(WAD) => CreatedStepAt` direction is missing;
2. `CoherentCreatedStepPos E` --- the `j >= 1` face, open everywhere including `(0,0)`, with NO producer in the
   tree (the `L(-1)` ladder reduces to a DESCENDANT of `iota(a)`).

### 105.2 (8.6.6)'s second equality

`Display866SecondEqK` / `Display866BoxK` (equivalent both ways) are now stated at every `k`, with `hs` and
`0 <= <abar_i,abar_j>` as explicit binders and the `k = 1, 2` slices proved (`k = 2` via the landed
`MM.FLM86YP.YFam_mul_apply_eq_sum_ratioCoeff`).  The composition `display866Display_of_second` turns the second
equality plus the landed first equality into (8.6.6) as FLM states it.  The remaining piece is the general-`k`
OPE/insertion step (one honest field against a `k`-fold normal-ordered product) --- the `k >= 3` case of
(8.4.22)/(8.4.36) --- with `Contraction8612Ratio` open even at `k = l = 1`.

Correction: batch 119's `Display866Family3` (families `Fin k -> Nat -> VL`, scalar shape) CANNOT carry the second
equality; the honest carrier is batch 207's `normOrderedK`.

### 105.3 Accounting after batch 208

| object | status |
| --- | --- |
| (WAD) / `WeightedAssemblyDiagonal` | **THEOREM**, every weight, every pair |
| `CreatedStepAt E a b 0 l` (`0 <= <a,b>`) | **THEOREM** |
| Fock residual | `CreatedStepAtZeroNegPairing` /\ `CoherentCreatedStepPos` |
| (8.6.6) second equality | `k <= 2` THEOREM; `k >= 3` the named Prop `Display866SecondEqK` |
| item (i) | `Corollary851ModeStep` |
| (iii) | needs `Display866SecondEqK` at `k >= 3` |

## §106 Batch 209 — the Fock residual is refuted as spelled; the honest slice is `0 <= <a,b>`

### 106.1 The refutation, two independent routes

```
yFam_creationExpVL_iotaVL : YFam E a (-<a,b>+q-1) (creationExpVL b q (iotaVL b))
                              = ratioCoeff <a,b> q . (eps(a,b) . iotaVL (a+b))          -- batch 209-B
zAligned_createdStep_left_zero : the l = 0 left-hand side, evaluated by ZAligned_mode_iotaVL -- batch 209-A
not_pairFinite_generators_of_neg / not_pairFinite_rankOne
not_createdStepAtZeroNegPairing_of_exists_neg / not_createdStepAt_rankOne
not_coherentCreatedStep_of_exists_neg / not_coherentCreatedStepPos_rankOne
```

At `<a,b> = -N < 0` the convolution summand is `C(N+q-1,q).eps.iota(a+b) != 0` for EVERY `q`, so
`PairFinite (ZAligned (iota a)) (ZAligned (iota b))` fails, `convOneSided` returns 0, and the residual asserts
that a nonzero field vanishes.  The dropped ingredient is (8.6.25)'s pairing factor
`prod (z_0+w_i-x_j)^{<a_i,b_j>}`, invisible on the diagonal iff `0 <= <a,b>`; FLM's Remarks 8.5.2 (p. 200) and
8.6.4 (p. 211) say exactly this.

### 106.2 What this costs, and what it does not

* `CoherentCreatedStep` (third conjunct of `EvenCocycleResiduals`) is FALSE at FLM's Leech datum, so
  `theorem8102_of_residuals` is VACUOUS and must be re-stated with the honest residual.
* NOT affected: the `ZLine` tower, the `l = -c` faces, `ResidueNegativeAligned`, `NegTwo*`, `NegThree*` --- all
  of those use `normOrdered2`, never `convOneSided`.
* Batch 200-B's "the summand cancels" note is REFUTED (it cancels in Fock degree, not in `j`).

### 106.3 The corrected accounting

```
CoherentCreatedStepPosNonneg E := forall a b, 0 <= form a b -> forall j, 1 <= j -> forall l, CreatedStepAt E a b j l
CoherentCreatedStepNonneg E    := forall a b, 0 <= form a b -> forall j l, CreatedStepAt E a b j l
coherentCreatedStepNonneg_iff_posNonneg (hs) : Nonneg <-> PosNonneg   -- the j = 0 face is batch 208-A
coherentCreatedStep_iff_slices (hs) : CoherentCreatedStep <->
    PosNonneg /\ CreatedStepAtZeroNegPairing /\ PosNegPairing        -- the last two are FALSE
```

`CoherentCreatedStepPosPairingFactor` names the honest negative-pairing replacement (threshold form of
(8.4.22)/(8.4.25), `MM.FLM86RX.threshold_holds`, matching `MM.FLM86MXP.Display8625One` at `k = l = 1`); it is
STATED, not proved, and the coupling of the outer window to the threshold `T` is flagged unverified.

### 106.4 The lesson (recorded for the whole campaign)

For three batches (197-B/203-B/204-B) the Fock front was progressively "reduced" to targets that were FALSE,
because the campaign's own `convOneSided` spelling dropped FLM's pairing factor.  The remedy that ended it was
the batch-208 discipline: **falsification check on a small instance before investing**, plus the axiom-guard probe
that catches silent `sorryAx`.  Every future "prove X" on this front must start with the check, and every target
must be quoted from FLM WITH its Remarks.

### 106.5 Accounting after batch 209

| object | status |
| --- | --- |
| `ZLine` tower / `l = -c` faces / `ResidueNegativeAligned` / `NegTwo*` / `NegThree*` | THEOREM (unaffected) |
| `CoherentCreatedStep` | **FALSE** (refuted); `EvenCocycleResiduals` false; `theorem8102_of_residuals` VACUOUS |
| `CoherentCreatedStepPosNonneg` (`0 <= <a,b>`) | open --- the honest Fock residual |
| `CoherentCreatedStepPosPairingFactor` | named, not proved (the honest negative-pairing replacement) |
| (8.6.6) second equality `k >= 3` | named Prop (route (iii)) |
| item (i) | `Corollary851ModeStep` |

## §107 Batch 210 — the honest boundary is landed; the Fock residual is one two-shift statement

### 107.1 The Fock residual, final shape

```
createdStepAt_shiftZero (hs) (0 <= <a,b>) : CreatedStepAt E a b j 0        -- EVERY j, the l = 0 face, THEOREM
CoherentCreatedStepShifted E := forall a b, 0 <= form a b -> forall j, 1 <= j -> forall l, 1 <= l,
    CreatedStepAt E a b j l                                               -- THE residual
coherentCreatedStepPosNonneg_iff_shifted : CoherentCreatedStepPosNonneg E <-> CoherentCreatedStepShifted E
coherentCreatedStep_iff_shifted_slices : CoherentCreatedStep E <->
    CoherentCreatedStepShifted E /\ CreatedStepAtZeroNegPairing E /\ CoherentCreatedStepPosNegPairing E
```

The `l = 0` face closes at every `j` by the reflected (8.5.37) finite difference collapsing the double-binomial
weight to `C(P, j-N)`, then the landed tower `ZLine E (j-N)`.  At `l >= 1` the weight carries the extra
`C(q+i,l)` and no single finite difference collapses it (hand-checked at `(N,j,l) = (2,1,1)`).

### 107.2 The honest boundary, and why it is not vacuous

```
FockResidualHonest E := CoherentCreatedStepPosNonneg E /\ CoherentCreatedStepNegPairingFactor E
                          /\ CreatedStepAtZeroNegPairingHonest E
EvenCocycleResidualsHonest C h2 := NegTwoFirstDerivZero /\ NegThreeExpandedResidualAligned
                                     /\ FockResidualHonest (C.toCentralExtension h2)
theorem8102_of_residuals_honest : Theorem8102
evenCocycleResidualsHonest_iff : (forall a b, 0 <= form a b) ->
    (EvenCocycleResidualsHonest C h2 <-> EvenCocycleResiduals C h2)          -- non-vacuity on that slice
```

The audit also lands the vacuity of the whole old Fock chain as theorems (see ROADMAP batch 210).

### 107.3 The one object still missing

`CreatedStepAtZeroNegPairingHonest` names the normal-ordered ONE-VARIABLE product at the shifted coherent state,
with the (8.6.25) threshold clause (without it the def is trivially provable --- the agent checked).  The tree has
no such object (`MMFLM86YP` §6(ii): `convWith (YFam E a) (YFam E b)` does not exist; `YFam` is not a `CField`
for `a != 0`).

### 107.4 Accounting after batch 210

| object | status |
| --- | --- |
| old `EvenCocycleResiduals` / `theorem8102_of_residuals` | **FALSE / VACUOUS** (audited as theorems) |
| honest package + `theorem8102_of_residuals_honest` | landed, non-vacuous on the `0 <= <a,b>` slice |
| `CoherentCreatedStepShifted` | open --- the positive-pairing Fock residual |
| `CreatedStepAtZeroNegPairingHonest` | open --- needs the missing normal-ordered object |
| `CoherentCreatedStepNegPairingFactor` | open |
| (i) `Corollary851ModeStep` / (iii) `Display866SecondEqK` | open |

## §108 Batch 211 — the two-shift face proved from a derivation identity; the shifted normal-ordered object built

### 108.1 `CoherentCreatedStepShifted` reduced to `ShiftedCreationDerivation`

```
ShiftedCreationDerivation E := forall n >= 1, forall w, L(-1)(alpha_a(-n) w) = alpha_a(-n)(L(-1) w) + n.alpha_a(-n-1) w
coherentCreatedStepShifted_of_derivation (hnd) (hs) (E) (hder) : CoherentCreatedStepShifted E
coherentCreatedStepPosNonneg_of_derivation (hnd) (hs) (E) (hder) : CoherentCreatedStepPosNonneg E
```

This is the (8.4.14)/(7.1.41) derivation identity --- the tree's open `MM.FLM810TG.LMinusOneCreationMode`, whose
generator case is landed.  The proof needs NO new collapse identity: it uses
`E^-_b(l) iota(b) = (1/l!)L(-1)^l iota(b)`, the new Leibniz rule `coefDeriv_convOneSided`, (8.6.9), and the
cancellation of `(j+1)(Y a)_{-j-2}B_l` against the level-`j+1` shift-zero statement.  The double-binomial weight
of batch 210-A is bypassed.  `hnd` IS spent (the `L(-1)` route goes through the conformal vector).

Next step: creation-list induction from `MM.FLM810TG.lMinusOneCreationMode_iota`, template
`MMFLM810DFA.translationResidual_of_baseResidual`.

### 108.2 `pairBlock`: the (8.6.25) object, built

`pairBlock E a b j l m T` is the block sum at the shifted coherent state with the pairing factor carried as
`ratioCoeff`; `convOneSided_shifted_eq_ratioSum` shows the carrier's summands ARE the two shift binomials
against `twoVarField`, **which is where the second slot index `l` comes from**.  The two negative-pairing faces
are now equivalent (both ways) to `HonestNegPairingZero` / `HonestNegPairingPos`.

### 108.3 Two defects of record (batch 210-B's spelling)

1. **Machine-checked slot error**: the second shift binomial was written with index `0` instead of `l`
   (`pairBlock_slot_discrepancy`), so `CreatedStepAtZeroNegPairingHonest` is not the `j = 0` slice of slice 2.
2. **Single threshold too small**: the honest spelling needs a threshold PER SHIFT INDEX (outer and inner).
   NOTES §106.3's "flagged unverified" is upgraded to "wrong as spelled".

The def was recorded with a defect note (docstring), NOT weakened; the corrected package
`MM.FLM86NOS.FockResidualHonestCorrected` agrees with the batch-210 package on the `0 <= <a,b>` slice.

### 108.4 What still blocks the negative-pairing faces

The **h-weight (Fock bidegree) grading of M(1)**: without it one cannot separate the
`E^-_a(P) E^-_b(Q) iota(a+b)` blocks with different `Q`, which is what the per-shift-index threshold needs.
That grading is not landed.

### 108.5 Accounting after batch 211

| object | status |
| --- | --- |
| `CoherentCreatedStepShifted` / `CoherentCreatedStepPosNonneg` | PROVED from `ShiftedCreationDerivation` (+ `hnd`) |
| `ShiftedCreationDerivation` (= `LMinusOneCreationMode`) | open; generator case landed |
| `HonestNegPairingZero` / `HonestNegPairingPos` | open; object built; blocked on the M(1) bidegree grading |
| (i) `Corollary851ModeStep` / (iii) `Display866SecondEqK` | open |

## §109 Batch 212 — the bidegree and its h-weight refinement; the residual pinned to the `YFam` modes

### 109.1 The residual, corrected and pinned

```
lMinusOne_eq_sugawaraModeZero : lMinusOne hnd E = sugawaraModeZero hnd (-1)        -- the currency bridge
shiftedCreationDerivation_iff_YFamShiftedDerivation : ShiftedCreationDerivation <-> YFamShiftedDerivation
```

**Batch 211-A's identification was WRONG** (machine-checked): the residual's modes are the (8.4.17) field of the
lattice generator (`YFam`), not the Heisenberg modes `modeVL` of `LMinusOneCreationMode`/`SugawaraDerivation`
--- at `a = 0, m = -1` they differ on the vacuum.  The tree's state-half object `MM.FLM87SR.sugawaraDerivation`
is a THEOREM (batch 165) and does not imply the residual.  What remains is `YFamModeDerivation` (= the tree
spelling) and its generator base case `YFamDerivationBase`; the creation-list step is hand-verified and recorded
in the docstring but its Lean proof was withdrawn at the scalar-normalisation step (`Module.End` smul trap).

### 109.2 The grading, and why the coarse one is not enough

`bidegPiece`/`bidegProj`/`bideg_separation` and the h-weight `hwWt`/`hwPiece` are landed.  The falsification
`pairBlock_block_deg` shows the `(N,a)` bidegree of every `pairBlock` summand is constant in `(q,k)` at a
lattice generator, so the SEPARATING grading is `hwWt` (the summand carries `(M+1-Q)a + (Q-2)b`).  This is
batch 211-B's per-shift-index threshold obstruction, now an identity.

### 109.3 Accounting after batch 212

| object | status |
| --- | --- |
| `CoherentCreatedStepShifted` / `PosNonneg` | ⟸ `YFamModeDerivation` + `YFamDerivationBase` (step hand-verified) |
| Fock bidegree + h-weight refinement | LANDED |
| `FockAnnihilationDegreeLaw` | named (exact-degree annihilation) |
| `HonestNegPairingZero`/`HonestNegPairingPos` | open; need the h-weight mode law + block separation |
| (i) `Corollary851ModeStep` / (iii) `Display866SecondEqK` | open |

## §110 Batch 213 — the positive-pairing Fock faces are theorems; the h-weight separation is landed

### 110.1 The residual is closed

```
yFamDerivationBase / yFamModeDerivation / shiftedCreationDerivation (hnd) (hs) (E) : ...
coherentCreatedStepShifted / coherentCreatedStepPosNonneg (hnd) (hs) (E) : ...
```

NO named residual remains for `CoherentCreatedStepPosNonneg`.  The base case is the creation half of
(8.10.13)/(8.10.14), `[L(-1),E^-(a,z)] = (d/dz)E^-(a,z) - a(-1)E^-(a,z)`, proved abstractly once
(`sub_mul_of_deriv_expField`).  The step is pure vector-level algebra.

### 110.2 The h-weight separation, and what it corrects

The mode law is homogeneous only at BASIS labels; for general `c` the mode is inhomogeneous
(`naiveHwModeLawRankTwo_false`), and the block separation `pairBlock_block_weight_eq_iff` holds at basis labels
--- so batch 212-B's general-label claim is corrected.  The two faces are now per-h-weight statements
(`HonestNegPairingZeroHw`/`HonestNegPairingPosHw`), with the remaining obstruction being the assembled
per-shift-index threshold, blocked on a missing fiberwise-sum lemma for `(q,k) |-> q+k` in this Mathlib pin.

### 110.3 Milestone: the honest residual package is two Fock faces

| conjunct of `EvenCocycleResidualsHonest` | status |
| --- | --- |
| `NegTwoFirstDerivZero` | THEOREM (batch 196) |
| `NegThreeExpandedResidualAligned` | THEOREM (batch 204-A) |
| `CoherentCreatedStepPosNonneg` | **THEOREM (batch 213-A)**, modulo `hnd`/`hs` |
| `CoherentCreatedStepNegPairingFactor` | open ⟺ `HonestNegPairingPos` ⟺ `HonestNegPairingPosHw` |
| `CreatedStepAtZeroNegPairingHonest` | open ⟺ `HonestNegPairingZero` ⟺ `HonestNegPairingZeroHw` |

Plus `EvenCocycleJacobiStepHonest` (the assembly), whose content is (i) `Corollary851ModeStep` and
(iii) `Display866SecondEqK` at `k >= 3`.

### 110.4 Traps of record (batch 213)

1. The mode `-(k+1)` index trap: the contraction shifts the `YFam` index by `k+1` (`m-k-1`, not `m-k`),
   because `module` treats `YFam a (m-1-k)` and `YFam a (m-k-1)` as different atoms.
2. `modeVL_YFam_add` yields `-↑n` / `j - ↑n`, only definitionally equal to `-1` / `m-1`; `rw`'s keyed matching
   fails across the difference (`simpa using h` fails where `exact h` succeeds).  Worth an AGENTS.md bullet.
3. The "scalar-normalisation blocker" was an artefact of an operator-level formulation; the vector-level
   formulation avoids the `Module.End` scalar API entirely.

## §111 Batch 214 — the boundary reduced to two Fock faces + the Jacobi step; the negative-pairing faces at per-`Q` thresholds

### 111.1 The reduced boundary (the campaign's current frontier)

```
EvenCocycleResidualsHonestReduced C h2 := CoherentCreatedStepNegPairingFactor E /\ CreatedStepAtZeroNegPairingHonest E
evenCocycleResidualsHonest_iff_reduced : EvenCocycleResidualsHonest C h2 <-> Reduced C h2
theorem8102_of_negPairingFock (hnd hs C h2 S hpd hW hfin) (hneg) (hzero) (hstep) : Theorem8102
EvenCocycleJacobiStepReduced C h2 : Prop   -- content (i) Corollary851ModeStep, (iii) Display866SecondEqK at k >= 3
```

Three of the five conjuncts of the honest package are THEOREMS at FLM's datum, so the residual is exactly: the two
negative-pairing Fock conjuncts + the Jacobi step.  At `hpd` the `0 <= <a,b>` non-vacuity slice is unavailable
(positive definite forms have `(x,-x)`), so the reduced hypothesis' satisfiability rests on the negative-pairing
faces themselves --- which is where the remaining work is.

### 111.2 The negative-pairing faces, corrected and assembled

```
pairBlock_eq_pairBlockIdxMax : pairBlock ... T = pairBlockIdx ... (l-T) (l+T) (fun Q => T - max 0 (Q-l))
HonestNegPairingZeroIdx / PosIdx     -- arbitrary windows and per-Q thresholds
honestNegPairing*_iff_diag           -- their diagonal slices are exactly batch 213-B's faces (both ways)
honestNegPairing*Idx_iff_hw          -- both ways to the per-h-weight inputs
```

The landed single-`T` forms are FALSE (falsification on batch 211-B's instance; coefficient core machine-checked
as `diagCoeff_pair_ne_one_one`), so the corrected (`Idx`) spelling is the honest one --- a genuine weakening.  The
operator-level refutation of the single-`T` forms still needs the linear independence of the distinct blocks.

### 111.3 Corrections of record

1. The "Mathlib's missing fiberwise-sum lemma" premise (batch 213-B / NOTES §110.2) is FALSE --- the lemmas exist
   and are used; what was missing was the explicit fiber/image of the window.
2. `AGENTS.md`'s "tools/build.sh is not usable on this machine" is stale.

### 111.4 Accounting after batch 214

| object | status |
| --- | --- |
| `theorem8102_of_negPairingFock` | landed --- Theorem 8.10.2 from the two negative-pairing Fock faces + the step |
| `HonestNegPairing*IdxHw` | open --- ONE named input per face |
| block linear independence | open (needed only for the refutation of the defective spelling) |
| (i) `Corollary851ModeStep` | open --- the Jacobi step's content |
| (iii) `Display866SecondEqK` at `k >= 3` | open --- the Jacobi step's content |
| six boundary inputs | as before |

## §112 Batch 215 — the general insertion step landed; the negative-pairing faces off-vacuum

### 112.1 The last two mathematical residuals of the campaign

    Fock  : HonestNegPairingZeroIdxHwNonvac E /\ HonestNegPairingPosIdxHwNonvac E   -- off-vacuum, <a,b> < 0
    Jacobi: (i) MM.FLM86C851.Corollary851ModeStep
            (iii) MM.FLM86D866T.Display866SeriesStep k                          -- k -> k+1 finite regrouping

Everything else in EvenCocycleResidualsHonestReduced and EvenCocycleJacobiStepReduced is either a theorem or
reduced to these.

### 112.2 What landed this batch

* the GENERAL OPE/insertion step powerFam_nestedExp (all lengths, only hs and 0 <= <a,b_j>) --- the k >= 3 case
  of (8.4.22)/(8.4.36) --- plus the l-fold (8.4.19) contraction and the series spelling with its both-way
  equivalence to Display866SecondEqK;
* the vacuum slice of the negative-pairing faces as a THEOREM, the both-way reduction to the off-vacuum residuals,
  the block-independence converse normOrdered2_blocks_no_cancel, and the OPERATOR-LEVEL refutation of the
  single-T ancestor spellings at the rank-one datum.

### 112.3 Traps and corrections of record

1. The operator-level refutation did not need the block independence (at the refutation datum C = 0 only the Q = 0
   block survives).
2. 0 <= <abar_i,abar_j> is load-bearing in (8.6.6): a negative pairing breaks the identity (falsification check),
   because pairSetK truncates.
3. Two attempted smaller negative-pairing reductions are non-reductions: basis-state restriction (witnesses not
   uniform in w) and single-shift collapse (separation needs i != j).
4. The coercion mismatch of zero (up-arrow 0 vs 0) in rw patterns, kin to the -n-vs-1 trap of batch 213-A.

### 112.4 Accounting after batch 215

| object | status |
| --- | --- |
| theorem8102_of_negPairingFock | landed |
| HonestNegPairing*IdxHwNonvac | open --- the off-vacuum (8.6.25)/(8.6.27) faces |
| Display866SeriesStep | open --- finite-index bookkeeping; OPE half proved; k = 3 follows from k = 2 |
| (i) Corollary851ModeStep | open |
| six boundary inputs | as before |

## §113 Batch 216 — (iii) closed; (i) refuted as spelled

### 113.1 Item (iii) is CLOSED

    display866SeriesStep : Display866SeriesStep bL form E k        -- every k
    display866SecondEqK_all : Display866SecondEqK at every k >= 1

The finite-index assembly PairIdx (k+1) = PairIdx k + Fin k is landed with all its bookkeeping, and the OPE half
(batch 215's powerFam_nestedExp) closes the step.  Item (iii) of the Jacobi ledger is therefore DONE.

### 113.2 Item (i) is false as spelled

    not_corollary851ModeStep_zero / _one : not (Corollary851ModeStep (ZAligned E) K)   -- K = 0, 1
    iterateOf_eq_zero_of_corollary851_succ : (C u v K -> C w v K) forces the K-th iterate of (w,v) to vanish

The window of Corollary851 is a TRUNCATION: the same-window step is strictly stronger than FLM (8.5.13).  The
corrected currency is Corollary851ModeStepExists (window-free), with the window-threaded (8.5.4) induction and the
composition with the batch-204-A corner landed --- ONE named input remains.

### 113.3 What the remaining (i) residual contains

1. the mode--field commutators [alpha_c(e), ZAligned E v n] at arbitrary v --- the ANNIHILATION modes
   alpha_b(n), n >= 0, are evaluated NOWHERE in the tree;
2. the (8.6.25)/(8.6.27) residue matching (powerFam_nestedExp is already a piece of it).

### 113.4 Accounting after batch 216

| object | status |
| --- | --- |
| (iii) Display866SecondEqK, every k >= 1 | **THEOREM** |
| (i) Corollary851ModeStepExists (window-free) | open --- the two pieces above |
| off-vacuum negative-pairing Fock faces | open |
| six boundary inputs | as before |

## §114 Batch 217 — (i) to three residuals; the negative-pairing faces in block form

### 114.1 Item (i), final shape

    Corollary851ModeStepExists Y <-> Left Y /\ Right Y                     -- Iff.rfl, per-half slices both ways
    corollary851ModeStepExists_iff_allStates : (i) <-> Corollary851AllStatesExists   -- both ways, modulo the lift
    ModeFieldCommInput : [alpha_c(e), Y(v)_n] = sum_j binom(e,j) Y(alpha_c(j)v)_{n+e-j}   -- PROVED at generators
                                                                                          and on their span

Residuals: ModeFieldCommInput off the generator span; ResidueInsertion8625; Corollary851SpanningToAllStates (a
genuine statement --- the landed (8.10.5) truncation is VECTORWISE).

### 114.2 The negative-pairing faces in block form

    HonestNegPairing*IdxHwNonvacBlock E   -- a FINITE set of shift indices, one truncation per index
    honestNegPairing*IdxHwNonvac_iff_block                                -- both ways (window scaffolding removed)
    lhsIdx_anchor_apply_of_neg : at l = 0 the LHS is eps(a,b).coherentFieldNat at iota(a+b), EVERY pairing

### 114.3 Corrections and traps of record

1. The 'annihilation modes are evaluated nowhere' claim is STALE (batch 192-A landed them at the assembled field).
2. E^-_2(r) is NOT 2^r h_r --- a first-draft refutation built on that was an arithmetic error.
3. rw with j := 0 yields the key -(up-arrow 0)-1, which does not match -1.
4. Re-verify an agent's files after its LAST write (two of this batch's files were still being written when the
   dispatcher's first rebuild ran, which failed; the final state builds clean).

### 114.4 Accounting after batch 217

| object | status |
| --- | --- |
| (iii) Display866SecondEqK, every k | THEOREM (batch 216) |
| (i) Corollary851ModeStepExists | open -> ModeFieldCommInput off-generator / ResidueInsertion8625 / SpanningToAllStates |
| Fock faces | open -> the four named block/anchor inputs |
| six boundary inputs | as before |

## §115 Batch 218 — (i) to one annihilation input; the Fock j = 0 face refuted

### 115.1 Item (i)

    modeFieldCommZeroHalf : the ZERO-MODE half of (8.6.9)/(8.6.10) at EVERY state   -- THEOREM
    modeFieldCommInput_iff_annStep : ModeFieldCommInput E <-> ModeFieldCommAnnStep E  -- BOTH WAYS

So (i)'s first residual is the ONE one-oscillator ANNIHILATION clause, with the (7.1.5) scalar defects, the ^+ half
vanishing, the two window laws and sum_scalar_term all landed.

### 115.2 The Fock j = 0 face is false in every spelling

At the rank-one negative datum, off the vacuum slice, the honest left side is `-(eps.eps).alpha_1(-1)iota(3)` while
the block form's right side is `(K.(eps.eps)).alpha_1(-1)iota(3)` with `K >= 0` a window cardinality.  The block,
per-Q and Idx spellings are all refuted (machine-checked, via the landed both-way reductions).  The corrected
residual is the FREE-coefficient form.

The methodological lesson (recorded): the check that missed it tested only the vacuum slice with `m <= -1`, where
the sign accident hid the defect.  Falsification scripts must probe the non-vacuum, non-generator regime too.

### 115.3 Accounting after batch 218

| object | status |
| --- | --- |
| (i) | ModeFieldCommAnnStep + ResidueInsertion8625 + Corollary851SpanningToAllStates |
| Fock j = 0 | the free form (refuted spellings replaced) |
| Fock j >= 1 | open (not refuted) |
| six boundary inputs | as before |

## §116 Batch 219 — the honest (8.6.25) coefficient; ModeFieldCommInput proved; the honest Fock package refuted

### 116.1 The honest coefficient (the answer to the Fock question)

    ZAligned E (YFam E a (-1) iota(b)) m w = sum_Q binomCoeff (C-Q) N . :Y(a,b):(C-Q,Q) w
    C = -m - <a,b> - 1,  N = -<a,b> > 0,   coefficient attached to the a-index P = C-Q

It is a BINOMIAL integer family, not the (8.5.37) fiber sum / cardinality that the campaign had used since batch
211-B.  At N = 1 it is C-Q, whose symmetric average over equal ordered pairs is C/2 = -m/2 --- exactly the
batch-218-B measurement.  Machine-checked for every mode m at w = iota(c).

### 116.2 Refuted spellings (do not consume)

    CreatedStepAtZeroNegPairingHonest / ...Corrected / FockResidualHonest / FockResidualHonestCorrected
    HonestNegPairingZero / HonestNegPairingZeroIdxHw / ...Nonvac / ...Block        (all cardinality-based)
    EvenCocycleResidualsHonest   -- and hence theorem8102_of_residuals_honest / theorem8102_of_negPairingFock
                                    are VACUOUS at the rank-one datum

### 116.3 The corrected residual

    HonestNegPairingZeroCoeff E   -- free support, DETERMINED coefficient binomCoeff (C-Q) N; attained at the datum
    FockResidualHonestCoeff := CoherentCreatedStepPosNonneg /\ HonestNegPairingPos /\ HonestNegPairingZeroCoeff

Slices 1 and 2 survive; slice 2 remains under suspicion (same pairBlock object).

### 116.4 Item (i): the mode-field commutator is PROVED

    modeFieldCommInput (hs) (E) : ModeFieldCommInput E     -- all states, (8.6.9)/(8.6.10)

Item (i) = ResidueInsertion8625 + Corollary851SpanningToAllStates (+ the bridge from the mode-field commutator to
the (8.5.13) mode step, which is the (8.6.4)--(8.6.27) residue matching itself).

### 116.5 Accounting after batch 219

| object | status |
| --- | --- |
| ModeFieldCommInput (all states) | THEOREM |
| HonestNegPairingZeroCoeff | open (the corrected Fock j=0 residual) |
| HonestNegPairingPos (j>=1) | open, under suspicion |
| general-N coefficient / l>=1 | open (needs the (8.6.27) dictionary) |
| ResidueInsertion8625 / Corollary851SpanningToAllStates | open |
| six boundary inputs | as before |

## §117 Batch 220 — slice 2 refuted; the residual is a reindexing identity

### 117.1 Fock: the corrected face and its single gap

    HonestNegPairingPos                              -- REFUTED (rank-one, (j,l,m,w) = (1,0,3,iota(1)))
    FockResidualHonestCoeff                          -- REFUTED (its 2nd conjunct)
    honestBlockCoeffJ a b j m Q = binomCoeff (blockFirstIdx j 0 m <a,b> - Q) (j + (-<a,b>).toNat)
    HonestNegPairingCoeff                            -- the corrected face (attained at the datum)
    FlatBinomialExpansion                            -- the ONE remaining identity (vertex-algebra-free)

### 117.2 Item (i): the matching is unnamed

ResidueInsertion8625 is the FINITENESS half only (proved); the (8.6.25)/(8.6.27) matching remains open and must be
named.  Corollary851SpanningToAllStates reduces to Corollary851SpanningEventualWindows (window synchronization).

### 117.3 Accounting after batch 220

| object | status |
| --- | --- |
| ModeFieldCommInput | THEOREM (batch 219) |
| HonestNegPairingCoeff (both slices) | open <-- FlatBinomialExpansion |
| (8.6.25)/(8.6.27) matching | open, unnamed |
| Corollary851SpanningEventualWindows | open |
| six boundary inputs | as before |

## §118 Batch 221 — the flat identity proved; the generator slice of the Fock residual proved; the matching named and half-proved

### 118.1 The honest identity (corrected window)

    flatBinomialExpansion : sum_{l<=n} C(s,l)((n-l)!)^-1 . flatMul (iterDeriv (n-l) X) Y (l+TOT-n)
                             = sum_{p in Icc 0 TOT} C(p+s,n) . (X p * Y (TOT-p))

The batch-220 `Finset.range (TOT.toNat+1)` spelling is FALSE at `TOT < 0` (machine-checked).

### 118.2 The Fock residual's current shape

    honestNegPairingCoeff_at_generators : the l = 0 slice at w = iotaVL c   -- THEOREM
    HonestNegPairingCoeff                                                  -- open at arbitrary w
    ResidueMatching8625NegSecondSlot                                       -- open (the l >= 1 slot)
    residueMatching8625Nonneg                                              -- THEOREM (half the matching)
    modeStepExists_of_insertion                                            -- the bridge, PROVED

### 118.3 Ledger after batch 221

| object | status |
| --- | --- |
| FlatBinomialExpansion | THEOREM (Icc 0 TOT form) |
| HonestNegPairingCoeff, l = 0 at generators | THEOREM |
| HonestNegPairingCoeff, arbitrary w | open |
| ResidueMatching8625NegSecondSlot | open |
| (8.6.25)/(8.6.27) matching | named; nonneg half THEOREM; bridge to the mode step PROVED |
| ModeFieldCommInsertionStep8625 / Corollary851SpanningEventualWindows | open |

## §119 Batch 222 — the boundary re-hung (non-vacuous); the Fock half named; the lattice factor proved

### 119.1 The corrected package (the new delivery frontier)

    EvenCocycleResidualsCorrected C h2 := ResidueMatching8625 E /\ Corollary851SpanningEventualWindows
        /\ exists Ins, IterateInsertion8625 E Ins /\ ModeFieldCommInsertionStep8625 E Ins
    theorem8102_of_correctedResiduals / theorem8102_of_correctedNormal : Theorem8102
    corollary851AllStatesExists_of_corrected : the package -> all-states (8.5.13)
    evenCocycleResidualsCorrected_iff_normal                                   -- BOTH WAYS

The four proved conjuncts are discharged by landed theorems; theorem8102_of_residuals is formally DEAD (its
package contains the refuted CoherentCreatedStep and is unsatisfiable at hpd).

### 119.2 The Fock side

    honestNegPairingCoeff_on_latticeSpan        -- THEOREM (the lattice factor F{L})
    honestNegPairingCoeff_iff_atStates          -- BOTH WAYS; the Fock half is the residual
    honestNegPairingCoeff_iff_finiteDimUniform  -- the uniformity is FORCED, not assumed

### 119.3 Accounting after batch 222

| object | status |
| --- | --- |
| boundary theorem (corrected package) | LANDED, non-vacuous |
| HonestNegPairingCoeff on the lattice factor | THEOREM |
| HonestNegPairingCoeffAtStates (Fock half) | open, the exact residual |
| ResidueMatching8625NegSecondSlot | open |
| Corollary851SpanningEventualWindows | open |
| ModeFieldCommInsertionStep8625 | open |
| EvenCocycleJacobiStepCorrected (assembly) | open |
| six boundary inputs | as before |

## §120 Batch 223 — the assembly built; the ledger halves again

### 120.1 The assembly's residual

    stepCorrected_of_spanningEventual : Corollary851SpanningEventualWindows (ZAligned E)
        -> NegativeResidual E -> EvenCocycleJacobiStepCorrected C h2
    crossBracket_eq_crossIterate_of_nonneg_of_grounded : every l >= 0 face is a translate of the grounded l = 0 face
    faceWindows_zAligned : (8.10.8)'s finiteness = the landed (8.10.5)

So `l > 0` is NOT residual, and `NegativeResidual E` (the `l < 0` faces at non-generator pairs) is the new named
obligation --- batch 202's faces were only the generator `0 <= <a,b>` chamber (a correction of record).

### 120.2 The insertion conjunct is redundant

    evenCocycleResidualsCorrected C h2 <-> ResidueMatching8625 E /\ Corollary851SpanningEventualWindows (ZAligned E)
    ModeFieldCommInsertionStep8625 E (honestIns8625 E) <-> Corollary851SpanningEventualWindows (ZAligned E)

### 120.3 Accounting after batch 223

| object | status |
| --- | --- |
| assembly step | reduced to the windows conjunct + NegativeResidual |
| l >= 0 faces, every state/pairing | THEOREM (the translate engine) |
| l = -c faces, generator 0 <= <a,b> chamber | THEOREM (batch 202) |
| NegativeResidual (l < 0 at non-generator pairs) | open --- the normal-ordering engine there |
| Corollary851SpanningEventualWindows | open |
| HonestNegPairingCoeffAtStates / ResidueMatching8625NegSecondSlot | open (Fock) |
| six boundary inputs | as before |


**HANDOVER**: the state of the campaign as of batch 223 (delivered reductions, the remaining book formulas, the refuted-spelling blacklist, the module map and the verification discipline) is summarised in `HANDOVER.md` at the repository root.

## §121 Batch 224 — residual #1 sharpened: the window synchronization is the grounded one-mode step

### 121.1 The sharpened residual and the theorem corner

    GroundedPairWindow Y u v : exists K, Corollary851 Y u v K and iterateOf Y u v i = 0 for all i >= K
    GroundedModeStepAtStates Y : grounded at (D, D') -> grounded at (alpha_c(-r) u_D, u_D') and (u_D, alpha_c(-r) u_D')
    groundedLatticeCorner_evenCocycle : GroundedLatticeCorner (ZAligned E)        -- THEOREM
    spanningEventual_zAligned_iff_groundedStep :
        Corollary851SpanningEventualWindows (ZAligned E) <-> GroundedModeStepAtStates (ZAligned E)

The corner is unconditional at the even cocycle (batch 204-A's lattice identity with the PROVED negative
pairing MM.FLM86NTP.residueNegativeAligned_evenCocycle, plus (8.5.11) through the iterate); the equivalence
is both ways: forward because a one-mode successor of a (8.5.4) pair is again a (8.5.4) pair, backward by
the (8.5.4) list induction in the grounded currency.  So residual #1 carries exactly ONE piece of content:
the grounded one-mode step, i.e. the (8.6.23)/(8.6.24) cross contraction at the descendant pair.

### 121.2 The delivery re-hung

    groundedZeroFace_of_groundedStep / stepCorrected_of_groundedStep / theorem8102_of_matching_and_groundedStep

### 121.3 Accounting after batch 224

| object | status |
| --- | --- |
| residual #1 | = GroundedModeStepAtStates (ZAligned E) (both ways; the window-free form is strictly weaker) |
| (8.5.4) lattice corner | THEOREM (unconditional at the even cocycle) |
| NegativeResidual | open --- the normal-ordering engine at non-generator pairs |
| HonestNegPairingCoeffAtStates / ResidueMatching8625NegSecondSlot | open (Fock) |
| six boundary inputs | as before |

## §122 Batch 225 — the window synchronization is absorbed: residual #1 IS the display

### 122.1 The bridge between the grounded and the threshold currencies

    groundedPairWindow_iff_aboveThreshold : (forall i >= N, iterateOf Y u v i = 0)
        -> (GroundedPairWindow Y u v <-> forall K >= N, Corollary851 Y u v K)
    pairWindowAboveThreshold_mono

### 122.2 The display gives the descendant windows outright

    groundedPairWindow_modeVL_left/right_of_commutatorInsertion :
        CommutatorInsertion8625 E (honestIns8625 E) -> the (8.10.5) threshold of the descendant pair is a grounded window
    groundedModeStep_of_commutatorInsertion :
        CommutatorInsertion8625 E (honestIns8625 E) -> GroundedModeStepAtStates (ZAligned E)     -- NO hypotheses
    DescendantsGroundedWindows / descendantsGrounded_of_commutatorInsertion

The threshold window is never raised, so the 223-A WindowSyncAtStates obstruction is bypassed rather
than solved: the display's own vanishing hypothesis is the honest window.

### 122.3 The accounting, both ways

    groundedModeStep_iff_commutatorInsertion_of_evenCocycle
    spanningEventual_of_commutatorInsertion_of_evenCocycle

### 122.4 Accounting after batch 225

| object | status |
| --- | --- |
| residual #1 | = CommutatorInsertion8625 E (honestIns8625 E) (both ways at an even cocycle) |
| window synchronization (223-A WindowSyncAtStates) | ABSORBED by (8.10.5) + the display |
| (8.5.4) lattice corner | THEOREM (unconditional at the even cocycle) |
| NegativeResidual | open — the normal-ordering engine at non-generator pairs |
| HonestNegPairingCoeffAtStates / ResidueMatching8625NegSecondSlot | open (Fock) |
| six boundary inputs | as before |

## §123 Batch 226 — residual #1 in the per-pair display currency

### 123.1 The display at a pair, and the per-pair bridge

    DisplayAtPair Y u v : forall K, (forall i >= K, iterateOf Y u v i = 0) -> Corollary851 Y u v K
    DisplayAllStates Y := forall u v, DisplayAtPair Y u v
    displayAllStates_iff_commutatorInsertion8625 :
        DisplayAllStates (ZAligned E) <-> CommutatorInsertion8625 E (honestIns8625 E)
    displayAtPair_iff_groundedPairWindow_of_threshold :
        (threshold N) -> (DisplayAtPair Y u v <-> GroundedPairWindow Y u v)
    displayAtPair_lattice_evenCocycle : the display at the lattice pairs is a THEOREM at the even cocycle

The pair alone selects the display: the inert (8.6.4) labels `c, r` are dropped, and the per-pair bridge
identifies the display with the grounded window (batch 224's currency) on the nose.

### 123.2 The step, and the residual

    DisplayModeStep Y     -- the display is inherited by the two one-creation-mode descendants
    displayModeStep_iff_groundedModeStep_of_evenCocycle
    honestDisplay_iff_displayModeStep_of_evenCocycle :
        DisplayAllStates (ZAligned E) <-> DisplayModeStep (ZAligned E)
    displayAllStates_iff_spanningEventual_of_evenCocycle

### 123.3 Accounting after batch 226

| object | status |
| --- | --- |
| residual #1 | = DisplayModeStep (ZAligned E) (the (8.6.23)/(8.6.24) cross contraction; label-free display currency) |
| window synchronization | ABSORBED (batch 225) |
| (8.5.4) lattice corner / display at lattice pairs | THEOREM (unconditional at the even cocycle) |
| NegativeResidual | open |
| HonestNegPairingCoeffAtStates / ResidueMatching8625NegSecondSlot | open (Fock) |
| six boundary inputs | as before |

## §124 Batch 227 — residual #1 IS the source's (8.6.3)

### 124.1 The carriers coincide at one window

    corollary851_iff_sourceUnshifted / corollary851_iff_sourceStatement
    corollary851_iff_theorem861SourceStatement

The spine's factor-free carrier IS the landed corollary851Residue (rfl), and the source's operator-valued
grading factor is inert (its sector sum is the identity).

### 124.2 Residual #1 at a labelled pair, and at all pairs

    displayAtPair_iff_forall_theorem861SourceStatement
    displayAllStates_iff_sourceStatements_of_evenCocycle :
        DisplayAllStates (ZAligned E) <-> (the source's (8.6.3) at every labelled (8.6.2) pair, at every
        window above the vanishing bound)

### 124.3 Accounting after batch 227

| object | status |
| --- | --- |
| residual #1 | = FLM (8.6.3) in the source's carrier (both ways; `MMFLM86SourceBridge`) |
| the spine's named next step (8.6.3) | THE SAME statement (machine-checked) |
| window synchronization / labels | absorbed (batches 225/226) |
| (8.5.4) lattice corner / display at lattice pairs | THEOREM (unconditional at the even cocycle) |
| NegativeResidual | open |
| HonestNegPairingCoeffAtStates / ResidueMatching8625NegSecondSlot | open (Fock) |
| six boundary inputs | as before |

## §125 Batch 228 — the Fock half is ONE one-mode step; its lattice base is a theorem

### 125.1 The face at a family, and the step

    FaceAtFamily E a b j m n D              -- the (8.6.25) face at one finite family of (8.5.4) states
    honestNegPairingCoeffAtStates_iff_familyFaces
    FockStep E                              -- the face at a family is inherited when a LIST of creation
                                            -- modes is appended to each state (one-mode: fockStep_imp_oneMode)
    faceAtFamily_lattice                    -- THEOREM (the union of the canonical windows)
    honestNegPairingCoeffAtStates_iff_fockStep : HonestNegPairingCoeffAtStates E <-> FockStep E

The step's proof is the mode action on the normal-ordered blocks `blockOfShift` (the recorded gap), the
left side being the PROVED (8.6.9)/(8.6.10) mode--field commutator at the inserted state and the
coefficients being compared by the landed flat binomial expansion.

### 125.2 Accounting after batch 228

| object | status |
| --- | --- |
| residual #1 | = the source's (8.6.3) (batches 225--227) |
| Fock half (residual #3) | = FockStep E (one-mode step; lattice base a THEOREM) |
| l >= 1 second slot | open (ResidueMatching8625NegSecondSlot) |
| NegativeResidual | open |
| six boundary inputs | as before |

## §126 Batch 229 --- the two Chapter-8 theorems delivered with one registered `sorry` each

Owner's directive ("未证明部分使用sorry") turned the residuals #1/#2 into named holes of named
theorems rather than descriptions:

* `Definitions/MMFLM810Theorem861Stated.lean` (`MM.FLM810T861S`): `displayAllStates_evenCocycle` is
  the registered `sorry` (residual #1); `theorem861_source`/`theorem861_all_pairs`/
  `theorem861_residual` are FLM Theorem 8.6.1 at the boundary field, composed from landed theorems.
* `Definitions/MMFLM88Theorem889Stated.lean` (`MM.FLM88T889S`): `theorem889_jacobi` is the
  registered `sorry` (residual #2 at its `l < 0` part); `theorem889_delta`,
  `remark8811_res_z0`/`_res_z1`, `remark8812_res_z2` are Remark 8.8.11's faces; and
  `theorem861_of_theorem889` (the engine link) is PROVED with the three standard axioms.
* Guards: the sorry-consuming declarations print `[propext, sorryAx, Classical.choice, Quot.sound]`;
  `README.md`'s `sorry` map gained a two-row table for them; `Probe/forbidden_tokens.py` reads
  `sorry=1` for exactly these two files.  Acceptance: `FinalCheck.lean` GREEN with the two imports.

## §127 Policy: per-batch `sorry` is the sanctioned marker of unfinished work (2026-09-22)

Owner's decision: **each batch may leave `sorry`s for the parts that are not yet proved** --- it is
the sanctioned way to deliver a statement whose proof is still open --- provided every `sorry` is
registered in `README.md`'s `sorry` map **and** tied to the open task/residual it belongs to in
`ROADMAP.md` / `HANDOVER.md`.  The declaration that consumes it carries a `#guard_msgs` footprint
printing `[propext, sorryAx, Classical.choice, Quot.sound]`, so the hole is visible in the build.
**"No `sorry` anywhere" is the completion criterion of the whole project** (the formalization of
monstrous moonshine), not a per-batch invariant.  `axiom`, `admit` and `native_decide` remain
forbidden.  The policy text now lives in `AGENTS.md` (ground rules + "Before any change is
considered done"), `README.md` (top + `sorry` map), `ROADMAP.md` ("Working agreement") and
`HANDOVER.md` (§0 and §5).  The first holes under it are batch 229-A's two statement-only
deliveries (`MM.FLM810T861S.displayAllStates_evenCocycle`, `MM.FLM88T889S.theorem889_jacobi`), tied
to residual #1 and residual #2.
