/-
Copyright (c) 2026 The MM project. All rights reserved.
Released under Apache 2.0 license as described in the LICENSE file.
Authors: MM project (owner's directive, 2026-09-24)
-/

/-
# FLM (7.1)--(8.5) layer of the Theorem 8.6.1 clean-room statement: THE DEFINITIONS

Split out of `Definitions/FLM861Book.lean` (batch 352-A) so that the statement file keeps only the
book-facing statements.  This file carries every definition of the book's (7.1.1)--(7.1.41),
(8.4.16)--(8.4.25) and (8.5.13)--(8.5.24) layer, the book's OWN section --- the (6.1.27)--(6.1.29)
`ε₁` construction, `bookEvenCocycle` and the (7.1.24) value `bookEvenCocycle_eps` that `azPowD`
reads (route A, batch 359-A) --- the diagonal gauge `conjGauge` (batch 346-B; OFF the frozen
statements' chain since 359-A, kept as the compiled gauge diagnosis), the five identification lemmas
(`commutatorFamily_eq_tree`, `iterateOf_eq_tree`, `iterateOf_fam_eq_tree`, `deltaExpCoeff_eq_tree`,
`corollary851Residue_eq_tree`) and `zAligned_iotaVL_apply_eq_eps`, with their axiom-footprint guards.
`Definitions/FLM861Book.lean` (the statements) and `Definitions/FLM861BookTransport.lean` (the
battlefield) both import this file.
-/

import Mathlib.Data.ZMod.Basic
import Mathlib.LinearAlgebra.BilinearForm.Properties
import Mathlib.LinearAlgebra.FreeModule.Basic
import Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
import Mathlib.Algebra.TrivSqZeroExt.Basic
import Mathlib.LinearAlgebra.TensorProduct.Basic
import Mathlib.LinearAlgebra.TensorProduct.Basis
import Mathlib.Data.Int.Interval
import Mathlib.LinearAlgebra.Finsupp.Defs
import Mathlib.LinearAlgebra.Finsupp.LinearCombination
import Mathlib.Data.Nat.Choose.Basic
import Mathlib.Tactic.Abel
import Mathlib.Tactic.Ring

noncomputable section

set_option linter.unusedSectionVars false

open scoped TensorProduct

namespace MM

namespace FLM861Book

universe u v w

variable {F : Type u} [Field F] [CharZero F]
variable {L : Type v} [AddCommGroup L] [Module.Free ℤ L]
variable {κ : Type w} [Fintype κ] [DecidableEq κ]


/-! ## (7.1.1): `h = L ⊗_ℤ F`, with its symmetric form -/

/-- (7.1.1) `h = L_F = L ⊗_ℤ F` (Mathlib: `F ⊗[ℤ] L`, the form with the `F`-module structure). -/
abbrev h (F : Type u) (L : Type v) [Field F] [AddCommGroup L] : Type (max u v) := F ⊗[ℤ] L

/-- (7.1.1) a `ℤ`-basis of the lattice base-changes to an `F`-basis of `h`. -/
def hBasis (bL : Module.Basis κ ℤ L) : Module.Basis κ F (h F L) := bL.baseChange F

/-- (7.1.1) the symmetric form on `h`, read off the Gram matrix of the lattice form. -/
def hForm (bL : Module.Basis κ ℤ L) (form : L →ₗ[ℤ] L →ₗ[ℤ] ℤ) :
    h F L →ₗ[F] h F L →ₗ[F] F :=
  (hBasis bL).constr F fun i => ∑ j, (form (bL i) (bL j) : F) • (hBasis bL).coord j

/-- `a ∈ L` as the element `a ⊗ 1` of `h`. -/
def ofL (a : L) : h F L := 1 ⊗ₜ[ℤ] a

/-! ### (7.2.23)--(7.2.26): the sign character and the §7.1 nondegeneracy (Mathlib only)

The two notions the book's (7.2.22)--(7.2.26) and §7.1 need are defined HERE, in Mathlib terms, so that
this file carries no `Definitions/` layer: `signPow` is the character `x ↦ (−1)^{x.val}` of `ZMod 2`
(the repository's landed sign character is the same object), and `hFormNondegenerate` is the §7.1
assumption "we assume only that `L` is nondegenerate" (printed p. 144), stated as Mathlib's
`LinearMap.BilinForm.Nondegenerate` for the form `hForm` induced on `h = L_F`. -/

/-- (7.2.23)/(7.2.24): the sign `(−1)^n` as the character `signPow F x = (−1)^{x.val}` of `ZMod 2`. -/
def signPow (F : Type u) [Field F] (x : ZMod 2) : F := (-1 : F) ^ x.val

/-- **(7.2.23)/(7.2.24)**: the two spellings of the sign agree, `(−1)^{n mod 2} = (−1)^n` --- the parity
bridge of (8.6.1). -/
theorem signPow_zmod_two_eq_zpow (n : ℤ) : signPow F ((n : ℤ) : ZMod 2) = (-1 : F) ^ n := by
  have hval : (((n : ZMod 2).val : ℕ) : ℤ) = n % 2 := ZMod.val_intCast n
  have hmod : (-1 : F) ^ n = (-1 : F) ^ (n % 2) := by
    rcases Int.even_or_odd n with h | h
    · have h2 : n % 2 = 0 := by obtain ⟨k, rfl⟩ := h; omega
      rw [h.neg_one_zpow, h2, zpow_zero]
    · have h2 : n % 2 = 1 := by obtain ⟨k, rfl⟩ := h; omega
      rw [h.neg_one_zpow, h2]
      norm_num
  rw [signPow, ← zpow_natCast, hval, ← hmod]

/-- **§7.1 (printed p. 144)**: "we assume only that `L` is NONDEGENERATE" --- the form `hForm` induced
on `h = L_F = L ⊗_ℤ F` is nonsingular. -/
def hFormNondegenerate (F : Type u) [Field F] (bL : Module.Basis κ ℤ L)
    (form : L →ₗ[ℤ] L →ₗ[ℤ] ℤ) : Prop :=
  (hForm (F := F) bL form).Nondegenerate

/-! ## (7.1.3)--(7.1.5): the Fock space `M(1) = S(ĥ_Z^-)` and its modes -/

/-- (7.1.3) `ĥ_Z^- = ⊕_{n<0} h ⊗ t^n`, indexed by `ℕ+` so that `single n a` is `a ⊗ t^{-n}`.
(`ĥ_Z = ĥ_Z^- ⊕ F c ⊕ ĥ_Z^+`; `c` acts as `1` on `M(1)`, so only the negative part is carried.) -/
abbrev negHalf (F : Type u) (L : Type v) [Field F] [AddCommGroup L] : Type (max u v) :=
  ℕ+ →₀ h F L

/-- (7.1.4) `M(1) = S(ĥ_Z^-)`, the `ĥ_Z`-irreducible module on which `c` acts as `1`. -/
abbrev M1 (F : Type u) (L : Type v) [Field F] [AddCommGroup L] : Type (max u v) :=
  SymmetricAlgebra F (negHalf F L)

/-- (7.1.4) the vacuum `1 = |0⟩`. -/
def vacuum : M1 F L := 1

/-- (7.1.4)/(7.1.5) creation `a(-n)`, `n ≥ 1`: multiplication by the generator `a ⊗ t^{-n}`. -/
def creation (n : ℕ+) (a : h F L) : Module.End F (M1 F L) :=
  LinearMap.mulLeft F (SymmetricAlgebra.ι F (negHalf F L) (Finsupp.single n a))

/-- (7.1.5) the functional `a' ⊗ t^{-n} ↦ n⟨a,a'⟩` of the annihilation derivation `a(n)`. -/
def annihFun (bL : Module.Basis κ ℤ L) (form : L →ₗ[ℤ] L →ₗ[ℤ] ℤ) (n : ℕ+) (a : h F L) :
    negHalf F L →ₗ[F] F :=
  (n : F) • (hForm bL form a).comp (Finsupp.lapply n)

/-- (7.1.5) the derivation `D_φ` of `S(ĥ_Z^-)` with `D_φ(ι v) = φ v`, as the `ε`-component of
`ι v ↦ ι v + ε φ(v)`: the first-order exponential of a derivation (through `F[ε]/ε²`). -/
def dualNumberLift (φ : negHalf F L →ₗ[F] F) :
    M1 F L →ₐ[F] TrivSqZeroExt (M1 F L) (M1 F L) :=
  SymmetricAlgebra.lift
    { toFun := fun v =>
        TrivSqZeroExt.inl (SymmetricAlgebra.ι F (negHalf F L) v) + TrivSqZeroExt.inr (φ v • 1)
      map_add' := by
        intro v w
        refine TrivSqZeroExt.ext ?_ ?_
        · simp only [TrivSqZeroExt.fst_add, TrivSqZeroExt.fst_inl, TrivSqZeroExt.fst_inr, map_add]
          abel
        · simp only [TrivSqZeroExt.snd_add, TrivSqZeroExt.snd_inl, TrivSqZeroExt.snd_inr, map_add,
            add_smul]
          abel
      map_smul' := by
        intro c v
        refine TrivSqZeroExt.ext ?_ ?_
        · simp only [TrivSqZeroExt.fst_smul, TrivSqZeroExt.fst_add, TrivSqZeroExt.fst_inl,
            TrivSqZeroExt.fst_inr, map_smul]
          simp
        · simp only [TrivSqZeroExt.snd_smul, TrivSqZeroExt.snd_add, TrivSqZeroExt.snd_inl,
            TrivSqZeroExt.snd_inr, map_smul]
          simp [smul_smul] }

/-- (7.1.5) the derivation of `S(ĥ_Z^-)` determined by the functional `φ`. -/
def derivOf (φ : negHalf F L →ₗ[F] F) : M1 F L →ₗ[F] M1 F L :=
  ((TrivSqZeroExt.sndHom (M1 F L) (M1 F L)).restrictScalars F).comp (dualNumberLift φ).toLinearMap

/-- (7.1.5) the annihilation mode `a(n)`, `n ≥ 1`: the derivation contracting `a' ⊗ t^{-n}` to
`n⟨a,a'⟩`. -/
def annihilation (bL : Module.Basis κ ℤ L) (form : L →ₗ[ℤ] L →ₗ[ℤ] ℤ) (n : ℕ+) (a : h F L) :
    Module.End F (M1 F L) :=
  derivOf (annihFun bL form n a)

/-- (7.1.5) the modes `a(m)`, `m ∈ ℤ`: creation for `m < 0`, annihilation for `m > 0`, zero for
`m = 0` (the zero mode of `ĥ_Z` is not in the Heisenberg subalgebra; `h(0)` acts on `F{L}`). -/
def mode (bL : Module.Basis κ ℤ L) (form : L →ₗ[ℤ] L →ₗ[ℤ] ℤ) (m : ℤ) (a : h F L) :
    Module.End F (M1 F L) :=
  if hm : m < 0 then
    creation ⟨(-m).natAbs, Int.natAbs_pos.mpr (ne_of_gt (neg_pos.mpr hm))⟩ a
  else if hm0 : m = 0 then 0
  else
    annihilation bL form
      ⟨m.natAbs, Int.natAbs_pos.mpr (ne_of_gt (lt_of_le_of_ne (le_of_not_gt hm) (Ne.symm hm0)))⟩ a

/-! ## (7.1.6)--(7.1.9): the central extension `L̂` and its commutator map `c` -/

/-- (7.1.6)--(7.1.9): a central extension of `L` by a finite cyclic group, in the normalised
section form used from (7.1.20) on: `ε(a,b)` is the factor with `ι(a)ι(b) = ε(a,b)ι(a+b)`, subject
to the associativity (7.1.24) and the normalisations (7.1.27)/(7.1.28). -/
structure CentralExtension (F : Type u) (L : Type v) [Field F] [AddCommGroup L] where
  /-- (7.1.20): the commutator factor of the section. -/
  eps : L → L → Fˣ
  /-- (7.1.27): `ε(a,0) = 1`. -/
  eps_zero_left : ∀ a, eps 0 a = 1
  /-- (7.1.28): `ε(0,a) = 1`. -/
  eps_zero_right : ∀ a, eps a 0 = 1
  /-- (7.1.24): associativity of the twisted multiplication. -/
  cocycle : ∀ a b c, eps a b * eps (a + b) c = eps b c * eps a (b + c)

/-- (7.1.9): the commutator map `c(a,b) = ε(a,b)ε(b,a)^{-1}` (`aba^{-1}b^{-1} = κ^{c(a,b)}`). -/
def commutator {F : Type u} {L : Type v} [Field F] [AddCommGroup L]
    (E : CentralExtension F L) (a b : L) : Fˣ :=
  E.eps a b * (E.eps b a)⁻¹

/-- FLM (8.6.1): `(a,b) ∈ ℤ` and `c(a,b) = (-1)^{(a,b)}`.  In this model the form is `ℤ`-valued, so
the first half is free and the content is the commutator equation. -/
def Hypothesis861 (form : L →ₗ[ℤ] L →ₗ[ℤ] ℤ) (E : CentralExtension F L) (a b : L) : Prop :=
  (commutator E a b : F) = (-1 : F) ^ (form a b)

/-! ### (6.1.27)--(6.1.29): `ε₁`, THE BOOK'S OWN SECTION (definitional layer of this file since 359-A)

FLM build `V_L` from ONE central extension --- the one of (7.2.22)/(7.2.23) (`s = 2`, `ω = −1`,
`c₀(α,β) = ε₁(α,β) − ε₁(β,α)`, `ε₀ = ε₁`) --- and write `Y(a,z)` of (8.4.17) at ITS section
`ε(α,β) = ω^{ε₀(α,β)}` (7.1.24).  The `Z/2` form `ε₁` is the one of (6.1.27)--(6.1.29): `phi`,
`eps1Map` and the lemmas below realise it on the basis `bL`, `bookEvenCocycle` packages it as the
repository's `EvenCocycle`, and `bookEvenCocycle_eps` records the section value
`ε(α,β) = (−1)^{ε₁(α,β)}` that the (8.4.17) factor `azPowD` reads.  This is the section-convention
repair of route A (batch 359-A, step A-2); the block lived in `FLM861BookTransport.lean` (batches
354-A/355-A) until the re-pointing. -/
/-- The basis values of the `Z/2` form `(γ-eps1)`: the diagonal carries `(form e_i e_i / 2) mod 2`,
and one entry of each unordered off-diagonal pair carries `form e_i e_j mod 2` (the choice through the
well-ordering of `κ` induced by `Fintype.equivFin`). -/
def phi (bL : Module.Basis κ ℤ L) (form : L →ₗ[ℤ] L →ₗ[ℤ] ℤ) (i j : κ) : ZMod 2 :=
  if i = j then ((form (bL i) (bL i) / 2 : ℤ) : ZMod 2)
  else if (Fintype.equivFin κ i).val < (Fintype.equivFin κ j).val then 0
  else ((form (bL i) (bL j) : ℤ) : ZMod 2)

/-- The `ℤ`-bilinear extension of the basis values --- the candidate `eps1` of `(γ-eps1)`. -/
def eps1Map (bL : Module.Basis κ ℤ L) (form : L →ₗ[ℤ] L →ₗ[ℤ] ℤ) :
    L →ₗ[ℤ] L →ₗ[ℤ] ZMod 2 :=
  bL.constr ℤ fun i => bL.constr ℤ fun j => phi bL form i j

/-- `eps1Map` on the basis (batch 354-A, PROVED). -/
theorem eps1Map_basis (bL : Module.Basis κ ℤ L) (form : L →ₗ[ℤ] L →ₗ[ℤ] ℤ) (i j : κ) :
    eps1Map bL form (bL i) (bL j) = phi bL form i j := by
  rw [eps1Map, Module.Basis.constr_basis, Module.Basis.constr_basis]

/-- **The pairing property** of the basis values (batch 354-A, PROVED): `φ i j + φ j i = form e_i e_j`
mod 2, uniformly in `i, j`. -/
theorem phi_pair (bL : Module.Basis κ ℤ L) (form : L →ₗ[ℤ] L →ₗ[ℤ] ℤ)
    (hs : ∀ a b : L, form a b = form b a) (heven : ∀ a : L, 2 ∣ form a a) (i j : κ) :
    phi bL form i j + phi bL form j i = ((form (bL i) (bL j) : ℤ) : ZMod 2) := by
  by_cases hij : i = j
  · subst hij
    obtain ⟨k, hk'⟩ := heven (bL i)
    have hdiv : form (bL i) (bL i) / 2 = k := by
      rw [hk']
      exact Int.mul_ediv_cancel_left k (by norm_num)
    unfold phi
    rw [if_pos rfl, hdiv, hk']
    push_cast
    ring
  · have hne : ¬ (i = j) := hij
    have hne' : ¬ (j = i) := fun h => hij h.symm
    unfold phi
    rw [if_neg hne, if_neg hne']
    rcases lt_or_gt_of_ne (fun h : (Fintype.equivFin κ i).val = (Fintype.equivFin κ j).val =>
      hij ((Fintype.equivFin κ).injective (Fin.ext h))) with hlt | hgt
    · rw [if_pos hlt, if_neg (by omega), zero_add, hs]
    · rw [if_neg (by omega), if_pos hgt, add_zero]

/-- The swap `(a,b) ↦ T b a` of a bilinear form. -/
def flipB (T : L →ₗ[ℤ] L →ₗ[ℤ] ZMod 2) : L →ₗ[ℤ] L →ₗ[ℤ] ZMod 2 where
  toFun a :=
    { toFun := fun b => T b a
      map_add' := by intro b b'; simp
      map_smul' := by intro c b; simp }
  map_add' := by intro a a'; ext b; simp
  map_smul' := by intro c a; ext b; simp

/-- `(a,b) ↦ ((form a b : ℤ) : ZMod 2)` as a bilinear form over `ℤ`. -/
def castForm (form : L →ₗ[ℤ] L →ₗ[ℤ] ℤ) : L →ₗ[ℤ] L →ₗ[ℤ] ZMod 2 where
  toFun a :=
    { toFun := fun b => ((form a b : ℤ) : ZMod 2)
      map_add' := by intro b b'; simp [map_add]
      map_smul' := by intro c b; simp [map_smul, zsmul_eq_mul] }
  map_add' := by intro a a'; ext b; simp [map_add]
  map_smul' := by intro c a; ext b; simp [map_smul, zsmul_eq_mul]

/-- **(6.1.29) [PROVED in batch 354-A]**: `eps1Map`'s symmetric part is `form`.  Reduced to the basis
by the bilinear identity `flipB eps1 + eps1 = castForm` and two nested `Module.Basis.ext`. -/
theorem eps1Map_symm (bL : Module.Basis κ ℤ L) (form : L →ₗ[ℤ] L →ₗ[ℤ] ℤ)
    (hs : ∀ a b : L, form a b = form b a) (heven : ∀ a : L, 2 ∣ form a a) (a b : L) :
    eps1Map bL form a b + eps1Map bL form b a = ((form a b : ℤ) : ZMod 2) := by
  have hmap : flipB (eps1Map bL form) + eps1Map bL form = castForm form := by
    refine Module.Basis.ext bL fun i => Module.Basis.ext bL fun j => ?_
    show eps1Map bL form (bL j) (bL i) + eps1Map bL form (bL i) (bL j)
      = ((form (bL i) (bL j) : ℤ) : ZMod 2)
    rw [eps1Map_basis, eps1Map_basis, add_comm, phi_pair bL form hs heven]
  have h := congrArg (fun f : L →ₗ[ℤ] L →ₗ[ℤ] ZMod 2 => f a b) hmap
  have h2 : eps1Map bL form b a + eps1Map bL form a b = ((form a b : ℤ) : ZMod 2) := h
  rw [add_comm]
  exact h2

/-! ### (6.1.28), PROVED in batch 355-A by the plan recorded here: the diagonal of `eps1Map`.
`Q a := eps1Map bL form a a + ((form a a / 2 : ℤ) : ZMod 2)`; `Q` is additive because
`eps1 (a+b) (a+b) = eps1 a a + eps1 a b + eps1 b a + eps1 b b` and the polar identity
`q (a+b) = q a + q b + form a b` holds for `q a := ((form a a / 2 : ℤ) : ZMod 2)` (from
`form (a+b) (a+b) = form a a + 2 * form a b + form b b`, `heven a` and `heven b`), so that
(6.1.29) at `(a,b)` --- the landed `eps1Map_symm` --- gives `Q (a+b) = Q a + Q b`; and
`Q (bL i) = φ i i + ((form e_i e_i / 2 : ℤ) : ZMod 2) = 0` by `eps1Map_basis` and `phi`.  Then
`a = ∑ i, bL.repr a i • bL i` (`Module.Basis.sum_repr`) and `Q`'s additivity give
`Q a = ∑ i, bL.repr a i • Q (bL i) = 0`, i.e. `eps1Map bL form a a = ((form a a / 2 : ℤ) : ZMod 2)`. -/
/-- `ZMod 2` is of characteristic two. -/
theorem add_self_zmod2 (x : ZMod 2) : x + x = 0 := by
  have h2 : (2 : ZMod 2) = 0 := by decide
  calc x + x = 2 * x := by ring
    _ = 0 * x := by rw [h2]
    _ = 0 := by ring

/-- In `ZMod 2`, `x + y = 0` forces `x = y`. -/
theorem eq_of_add_eq_zero {x y : ZMod 2} (h : x + y = 0) : x = y := by
  calc x = x + 0 := (add_zero x).symm
    _ = x + (y + y) := by rw [add_self_zmod2 y, add_zero]
    _ = (x + y) + y := by abel
    _ = 0 + y := by rw [h]
    _ = y := zero_add y

/-- **The polar identity of `q a := ((form a a / 2 : ℤ) : ZMod 2)`** (batch 355-A, PROVED): it is the
quadratic form whose polar form is `(form a b) mod 2`. -/
theorem q_polar (form : L →ₗ[ℤ] L →ₗ[ℤ] ℤ) (hs : ∀ a b : L, form a b = form b a)
    (heven : ∀ a : L, 2 ∣ form a a) (a b : L) :
    ((form (a + b) (a + b) / 2 : ℤ) : ZMod 2)
      = ((form a a / 2 : ℤ) : ZMod 2) + ((form b b / 2 : ℤ) : ZMod 2)
        + ((form a b : ℤ) : ZMod 2) := by
  obtain ⟨x, hx⟩ := heven a
  obtain ⟨y, hy⟩ := heven b
  have hdivx : (2 * x) / 2 = x := Int.mul_ediv_cancel_left x (by norm_num)
  have hdivy : (2 * y) / 2 = y := Int.mul_ediv_cancel_left y (by norm_num)
  have hxy : 2 * x + 2 * (form a b) + 2 * y = 2 * (x + form a b + y) := by ring
  have hdiv : (2 * x + 2 * (form a b) + 2 * y) / 2 = x + form a b + y := by
    rw [hxy, Int.mul_ediv_cancel_left _ (by norm_num)]
  have hexp : form (a + b) (a + b) = 2 * x + 2 * (form a b) + 2 * y := by
    simp only [map_add, LinearMap.add_apply, hs b a, hx, hy]
    ring
  rw [hexp, hdiv, hx, hy, hdivx, hdivy]
  push_cast
  ring

/-- **`Q`'s additivity** (batch 355-A, PROVED): `Q a := eps1 a a + q a` is additive --- the polarization
step of (6.1.28), using the landed (6.1.29) `eps1Map_symm` and `q_polar`. -/
theorem Q_add (bL : Module.Basis κ ℤ L) (form : L →ₗ[ℤ] L →ₗ[ℤ] ℤ)
    (hs : ∀ a b : L, form a b = form b a) (heven : ∀ a : L, 2 ∣ form a a) (a b : L) :
    eps1Map bL form (a + b) (a + b) + ((form (a + b) (a + b) / 2 : ℤ) : ZMod 2)
      = (eps1Map bL form a a + ((form a a / 2 : ℤ) : ZMod 2))
        + (eps1Map bL form b b + ((form b b / 2 : ℤ) : ZMod 2)) := by
  refine eq_of_add_eq_zero ?_
  have h1 : eps1Map bL form (a + b) (a + b)
      = eps1Map bL form a a + eps1Map bL form a b + eps1Map bL form b a
        + eps1Map bL form b b := by
    simp only [map_add, LinearMap.add_apply]
    abel
  have hsym : eps1Map bL form a b + eps1Map bL form b a = ((form a b : ℤ) : ZMod 2) :=
    eps1Map_symm bL form hs heven a b
  rw [h1, q_polar form hs heven a b, ← hsym]
  ring_nf
  simp only [show (2 : ZMod 2) = 0 from by decide, mul_zero, add_zero, zero_add,
    add_self_zmod2, zero_add]

/-- `Q` vanishes on the basis. -/
theorem Q_basis (bL : Module.Basis κ ℤ L) (form : L →ₗ[ℤ] L →ₗ[ℤ] ℤ) (i : κ) :
    eps1Map bL form (bL i) (bL i) + ((form (bL i) (bL i) / 2 : ℤ) : ZMod 2) = 0 := by
  have hphi : phi bL form i i = ((form (bL i) (bL i) / 2 : ℤ) : ZMod 2) := by
    unfold phi
    rw [if_pos rfl]
  rw [eps1Map_basis, hphi, add_self_zmod2]

theorem eps1Map_self (bL : Module.Basis κ ℤ L) (form : L →ₗ[ℤ] L →ₗ[ℤ] ℤ)
    (hs : ∀ a b : L, form a b = form b a) (heven : ∀ a : L, 2 ∣ form a a) (a : L) :
    eps1Map bL form a a = ((form a a / 2 : ℤ) : ZMod 2) := by
  have hQadd := Q_add bL form hs heven
  let Qh : L →+ ZMod 2 :=
    { toFun := fun c => eps1Map bL form c c + ((form c c / 2 : ℤ) : ZMod 2)
      map_zero' := by simp
      map_add' := hQadd }
  have hQ0 : ∀ i : κ, Qh (bL i) = 0 := fun i => Q_basis bL form i
  have ha : Qh a = 0 := by
    conv_lhs => rw [← bL.sum_repr a]
    rw [map_sum]
    simp [map_zsmul, hQ0]
  exact eq_of_add_eq_zero ha

theorem exists_eps1 (bL : Module.Basis κ ℤ L) (form : L →ₗ[ℤ] L →ₗ[ℤ] ℤ)
    (hs : ∀ a b : L, form a b = form b a) (heven : ∀ a : L, 2 ∣ form a a) :
    ∃ eps1 : L →ₗ[ℤ] L →ₗ[ℤ] ZMod 2,
      (∀ a : L, eps1 a a = ((form a a / 2 : ℤ) : ZMod 2)) ∧
      (∀ a b : L, eps1 a b + eps1 b a = ((form a b : ℤ) : ZMod 2)) :=
  ⟨eps1Map bL form, eps1Map_self bL form hs heven, eps1Map_symm bL form hs heven⟩

/-! ## (7.1.20)--(7.1.41): `V_L = M(1) ⊗ F{L}`, the action of `L̂`, the degree shift `z^h` -/

/-- (7.1.20)/(7.1.28): the twisted multiplication by `a` on `F{L}`:
`ι(b) ↦ ε(a,b) ι(a+b)`, extended linearly. -/
def actL (E : CentralExtension F L) (a : L) : (L →₀ F) →ₗ[F] (L →₀ F) :=
  Finsupp.linearCombination F fun b => (E.eps a b : F) • Finsupp.single (a + b) (1 : F)

/-- (7.1.33): the zero mode `h(0)` on `F{L}`: `ι(b) ↦ ⟨h,b⟩ ι(b)`. -/
def hZeroL (φ : L →ₗ[ℤ] ℤ) : (L →₀ F) →ₗ[F] (L →₀ F) :=
  Finsupp.linearCombination F fun b => (φ b : F) • Finsupp.single b (1 : F)

/-- (7.1.34)/(7.1.35): the coefficient of `z^h` at `z^m` on `F{L}` -- the grading projector
`ι(b) ↦ ι(b)` if `⟨h,b⟩ = m`, else `0`. -/
def zPowL (φ : L →ₗ[ℤ] ℤ) (m : ℤ) : (L →₀ F) →ₗ[F] (L →₀ F) :=
  Finsupp.linearCombination F fun b => (if φ b = m then (1 : F) else 0) • Finsupp.single b (1 : F)

/-- (7.1.31) `V_L = M(1) ⊗ F{L}`. -/
abbrev VL (F : Type u) (L : Type v) [Field F] [AddCommGroup L] : Type (max u v) :=
  M1 F L ⊗[F] (L →₀ F)

/-- (7.1.32) `ι(a) = 1 ⊗ ι(a)`. -/
def iotaVL (a : L) : VL F L := vacuum (F := F) (L := L) ⊗ₜ[F] Finsupp.single a (1 : F)

/-- (7.1.32)/(7.1.41) the action of `a ∈ L̂` on `V_L` (the identity on `M(1)`). -/
def actVL (E : CentralExtension F L) (a : L) : VL F L →ₗ[F] VL F L :=
  TensorProduct.map LinearMap.id (actL E a)

/-- (7.1.33)/(7.1.41) the zero mode `h(0)` on `V_L`. -/
def hZeroVL (φ : L →ₗ[ℤ] ℤ) : VL F L →ₗ[F] VL F L :=
  TensorProduct.map LinearMap.id (hZeroL (F := F) (L := L) φ)

/-- (7.1.33) with (8.4.7): the zero mode a(0) of a general element a ∈ h, as the diagonal operator
on the lattice factor with the eigenvalues ⟨a, b̄⟩ ∈ F.  Because h = F ⊗_ℤ L these eigenvalues are
not integral in general, so this is the F-valued companion of hZeroVL.  The (8.4.14) normal
ordering of the (8.5.5) factors keeps a(0); the file's mode is 0 at the mode 0 (the ĥ_ℤ zero mode
is not in the Heisenberg subalgebra), so the fold's factors must carry this operator separately
(see derivedFactor). -/
def hZeroVLF (bL : Module.Basis κ ℤ L) (form : L →ₗ[ℤ] L →ₗ[ℤ] ℤ) (a : h F L) :
    VL F L →ₗ[F] VL F L :=
  TensorProduct.map LinearMap.id
    (Finsupp.linearCombination F fun b => (hForm bL form a (ofL b)) • Finsupp.single b (1 : F))


/-- (7.1.35)/(7.1.41) the grading shift `z^h` on `V_L`, componentwise in `z`. -/
def zPowVL (φ : L →ₗ[ℤ] ℤ) (m : ℤ) : VL F L →ₗ[F] VL F L :=
  TensorProduct.map LinearMap.id (zPowL (F := F) (L := L) φ m)

/-- (7.1.41) the Heisenberg modes on `V_L` (they act on the `M(1)` factor only). -/
def modeVL (bL : Module.Basis κ ℤ L) (form : L →ₗ[ℤ] L →ₗ[ℤ] ℤ) (a : h F L) (m : ℤ) :
    VL F L →ₗ[F] VL F L :=
  TensorProduct.map (mode bL form m a) LinearMap.id

/-- (7.1.41): the creation modes on `V_L`. -/
def creationVL (n : ℕ+) (a : h F L) : VL F L →ₗ[F] VL F L :=
  TensorProduct.map (creation (F := F) (L := L) n a) LinearMap.id

/-! ## (8.5.4)/(8.6.2): the states, and the component indexing (8.5.15) -/

/-- (8.5.4) a state `α₁(-n₁) ⋯ α_k(-n_k) ⊗ ι(a)` of `V_L`, as its list of oscillators and its
lattice label. -/
abbrev StateDatum (F : Type u) (L : Type v) [Field F] [AddCommGroup L] : Type (max u v) :=
  List (ℕ+ × h F L) × L

/-- (8.5.4) the Fock half `α₁(-n₁) ⋯ α_k(-n_k) · 1` of a state. -/
def fockWord (l : List (ℕ+ × h F L)) : M1 F L :=
  l.foldr (fun p acc => creation p.1 p.2 acc) 1

/-- (8.5.4) the state of a datum. -/
def stateOf (D : StateDatum F L) : VL F L :=
  fockWord D.1 ⊗ₜ[F] Finsupp.single D.2 (1 : F)

/-- (8.6.2) the state `u = u' ⊗ ι(a)` with a prescribed Fock part `u'`. -/
def stateOfFock (u' : M1 F L) (a : L) : VL F L :=
  u' ⊗ₜ[F] Finsupp.single a (1 : F)

/-! /-! ### (8.5.4) with (8.5.21)/(8.5.22): the WEIGHT of a Fock word

FLM present an element of `S(h^-)` in the form (8.5.4) `u = a1(-n1)...ak(-nk) (x) iota(a)`, and write its
weight as `wt u = n1 + ... + nk + (1/2)(a,a)` (8.5.21).  The word presentation is exactly what the
hypothesis "`u` is homogeneous" of Corollary 8.6.7 refers to, and the weight is what makes the sums finite
((8.5.22): `deg u_n = n - wt u + 1` and `wt (u_n . w) = wt u + wt w - n - 1`).  The weight is therefore
carried by the WORD, not by the type `M1 F L` itself: a symmetric algebra element does not determine a
canonical weight datum. -/

/-- **(8.5.4) with (8.5.21)/(8.5.22): the weight `n1 + ... + nk` of the Fock word
`a1(-n1)...ak(-nk)`** --- the Fock half of `wt u` in (8.5.21). -/
def wtWord (l : List (ℕ+ × h F L)) : ℕ := (l.map fun p => (p.1 : ℕ)).sum

@[simp] theorem wtWord_nil : wtWord ([] : List (ℕ+ × h F L)) = 0 := rfl

@[simp] theorem wtWord_cons (p : ℕ+ × h F L) (l : List (ℕ+ × h F L)) :
    wtWord (p :: l) = (p.1 : ℕ) + wtWord l := by
  simp [wtWord]

/-- The weight is additive on concatenation of words --- the word-level form of (8.5.22). -/
theorem wtWord_append (l₁ l₂ : List (ℕ+ × h F L)) :
    wtWord (l₁ ++ l₂) = wtWord l₁ + wtWord l₂ := by
  simp [wtWord, List.sum_append]

/-- **(8.5.21) with (8.6.1): the weight of a (8.5.4) word WITH its lattice label**, the Fock half plus
`(1/2)(a,a)`; stated doubled, `2 * wtWord l + form a a`, so that no half-integer is needed --- the doubled
weight is `2 * wt u`, and it is twice an integer exactly when `L` is integral ((8.6.1); then `2 | form a a`). -/
def wtWordOfLattice (form : L →ₗ[ℤ] L →ₗ[ℤ] ℤ) (l : List (ℕ+ × h F L)) (a : L) : ℤ :=
  2 * (wtWord l : ℤ) + form a a

## The diagonal lattice gauge `conjGauge` (batch 346-B) -/

/-- The base of `F{L}` at `b`. -/
theorem basisSingleOne_eq_single (b : L) :
    (Finsupp.basisSingleOne : Module.Basis L F (L →₀ F)) b = Finsupp.single b (1 : F) := by
  have h := Module.Basis.repr_self (Finsupp.basisSingleOne : Module.Basis L F (L →₀ F)) b
  simpa using h

/-- **THE DIAGONAL LATTICE GAUGE ON `F{L}`**: `single b 1 ↦ Λ b • single b 1`, the change of basis
from `Finsupp.basisSingleOne` to its `unitsSMul` scaling. -/
def conjGaugeFL (Λ : L → Fˣ) : (L →₀ F) ≃ₗ[F] (L →₀ F) :=
  (Finsupp.basisSingleOne.repr).trans ((Finsupp.basisSingleOne.unitsSMul Λ).repr.symm)

/-- The gauge on the base vectors. -/
theorem conjGaugeFL_single (Λ : L → Fˣ) (b : L) :
    conjGaugeFL (F := F) Λ (Finsupp.single b (1 : F)) = Λ b • Finsupp.single b (1 : F) := by
  rw [conjGaugeFL, LinearEquiv.trans_apply, ← basisSingleOne_eq_single (F := F) b,
    Module.Basis.repr_self, LinearEquiv.symm_apply_eq, ← basisSingleOne_eq_single (F := F) b,
    ← Module.Basis.unitsSMul_apply, Module.Basis.repr_self]
  exact basisSingleOne_eq_single (F := F) b

/-- **THE DIAGONAL LATTICE GAUGE ON `V_L`**: the identity on `M(1)` tensored with `conjGaugeFL`. -/
def conjGauge (Λ : L → Fˣ) : VL F L ≃ₗ[F] VL F L :=
  TensorProduct.congr (LinearEquiv.refl F (M1 F L)) (conjGaugeFL (F := F) Λ)

/-- **THE RAY LEMMA**: the gauge fixes the RAY of every state `stateOfFock u' a`, with eigenvalue
`Λ a` -- this is the ray datum that the bridge's statement used to carry as a hypothesis. -/
theorem conjGauge_stateOfFock (Λ : L → Fˣ) (u' : M1 F L) (a : L) :
    conjGauge (F := F) Λ (stateOfFock u' a) = (Λ a : F) • stateOfFock u' a := by
  rw [stateOfFock, conjGauge, TensorProduct.congr_tmul, LinearEquiv.refl_apply, conjGaugeFL_single,
    TensorProduct.tmul_smul]
  rfl

/-- The same at the lattice states. -/
theorem conjGauge_iotaVL (Λ : L → Fˣ) (a : L) :
    conjGauge (F := F) Λ (iotaVL (F := F) a) = (Λ a : F) • iotaVL (F := F) a := by
  rw [iotaVL, conjGauge, TensorProduct.congr_tmul, LinearEquiv.refl_apply, conjGaugeFL_single,
    TensorProduct.tmul_smul]
  rfl

/-- info: 'MM.FLM861Book.conjGaugeFL_single' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs in
#print axioms MM.FLM861Book.conjGaugeFL_single

/-- info: 'MM.FLM861Book.conjGauge_stateOfFock' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs in
#print axioms MM.FLM861Book.conjGauge_stateOfFock

/-- info: 'MM.FLM861Book.conjGauge_iotaVL' depends on axioms: [propext, Classical.choice, Quot.sound] -/
#guard_msgs in
#print axioms MM.FLM861Book.conjGauge_iotaVL

/-- (8.5.15) the component indexing: `Y(v,z) = Σ_n v_n z^{-n-1}`; a field on `V_L` is its family
of components `ℤ → End V_L`. -/
abbrev CompFam (F : Type u) (L : Type v) [Field F] [AddCommGroup L] : Type (max u v) :=
  ℤ → (VL F L →ₗ[F] VL F L)

/-- (8.4.10) the creation half `X^-(z)` of a component family: the components of index `< 0`. -/
def splitMinus (X : CompFam F L) : CompFam F L := fun m => if m < 0 then X m else 0

/-- (8.4.10) the annihilation half `X^+(z)`: the components of index `≥ 0`. -/
def splitPlus (X : CompFam F L) : CompFam F L := fun m => if 0 ≤ m then X m else 0

/-! ## (8.4.16)--(8.4.17): the normal ordered product and the base field `Y(a,z)` -/

/-- (8.4.16)/(8.4.19) the normal ordered product `:XY:`, as the book's sums -- finite on every
vector because `X^+` is locally nilpotent and `Y` is lower truncated. -/
def IsNormalOrder (X Y Z : CompFam F L) : Prop :=
  ∀ (m : ℤ) (w : VL F L), ∃ N : ℕ,
    Z m w = (∑ i ∈ Finset.range N, splitMinus X (-(i : ℤ) - 1) (Y (m + (i : ℤ)) w))
      + (∑ k ∈ Finset.range N, Y (m - 1 - (k : ℤ)) (splitPlus X (k : ℤ) w))

/-- (8.4.7) with (8.4.14): the Heisenberg field a(z) = Σ_{k∈ℤ}a(k)z^{-k-1} of a ∈ h in the component
indexing (8.5.15): the mode a(k) is the component k, with the (7.1.33) zero mode at k = 0 (the
(8.4.14) normal ordering keeps a(0)) -- the input of the (8.5.5) derived factors. -/
def heisVL (bL : Module.Basis κ ℤ L) (form : L →ₗ[ℤ] L →ₗ[ℤ] ℤ) (a : h F L) : CompFam F L :=
  fun m => if m = 0 then hZeroVLF bL form a else modeVL bL form a m

/-- (8.5.37): the binomial coefficient `binom(l,k) = l(l-1)⋯(l-k+1)/k!` for `l ∈ ℤ`, as the book
defines it for an element of an algebra (the falling factorial, NOT `Nat.choose`: at a negative
`l` the two differ, and the source's (8.5.5) reads the falling factorial). -/
def binomCoeff (l : ℤ) (k : ℕ) : F :=
  (∏ j ∈ Finset.range k, ((l - (j : ℤ) : ℤ) : F)) / (k.factorial : F)

/-- (8.5.5) with (8.5.16)--(8.5.21): the derived Heisenberg factor
`(1/(n-1)!)(d/dz)^{n-1} a(z)` attached to the creation mode `a(-n)`, in the (8.5.15) indexing:
its `m`-th component is `(-1)^{n-1} binom(m,n-1) a(m+1-n)`, with the (8.5.37) falling factorial.
(The batch-344-A spelling `Nat.choose m.toNat (n-1)` agrees with the falling factorial only for
`m ≥ 0`; on the creation half `m < 0` it is the constant `0`, which is not the source's factor --
see `MM.B345A.draftedDerivedFactor_eq_zero_of_neg` and `MM.B345A.drafted_coeff_ne_source_coeff`
+(`Refuted/MMFLM861BookBridgeRefute.lean`) and `toBook_factorFamilyZero` in
`Definitions/FLM861BookProducer.lean`.) -/
def derivedFactor (bL : Module.Basis κ ℤ L) (form : L →ₗ[ℤ] L →ₗ[ℤ] ℤ) (n : ℕ+) (a : h F L) :
    CompFam F L :=
  fun m =>
    (((-1 : F) ^ ((n : ℕ) - 1)) * binomCoeff (F := F) m ((n : ℕ) - 1)) •
      heisVL bL form a (m + 1 - (n : ℤ))

/-- (8.5.5): the fold of the derived factors of a list of oscillators against a base field
`Y(a,z)`, in the displayed order: `8 X₁(z) ⋯ X_k(z) Y(a,z) 8`.

**WINDOW DEFECT OF RECORD (batch 361-A, truth determination; NOTES.md section 278).**  `IsNormalOrder`'s
window `N` is EXISTENTIAL and the relation does NOT require the terms beyond it to vanish (the two
sums are cut at `N` but their tails are unconstrained): a SMALL window is therefore admissible, where
the partial sums are not yet constant, so the relation does not determine `Z`.  The book's content is
exactly that finiteness ("the sums are finite on every vector"), whose value is the LIMIT; the missing
conjuncts are "the `i`-tail and the `k`-tail at `N` vanish".  Repaired by the batch that re-points
the uniqueness (see `isVertexOperator_unique`'s docstring). -/
def IsFold (bL : Module.Basis κ ℤ L) (form : L →ₗ[ℤ] L →ₗ[ℤ] ℤ) :
    List (ℕ+ × h F L) → CompFam F L → CompFam F L → Prop
  | [], B, Z => Z = B
  | p :: l, B, Z => ∃ Z', IsFold bL form l B Z' ∧ IsNormalOrder (derivedFactor bL form p.1 p.2) Z' Z

/-- (8.4.17) the creation exponential `E^-(a,z) = exp(Σ_{n≥1} (a(-n)/n) z^n)`, as its exponential
series: `E^-(0) = 1` and `(m+1)E^-_{m+1} = Σ_{n=1}^{m+1} a(-n) E^-_{m+1-n}` (the derivative of the
exponential), supported in nonnegative powers. -/
def IsEminus (a : h F L) (E : CompFam F L) : Prop :=
  (∀ m : ℤ, m < 0 → E m = 0) ∧ E 0 = 1 ∧
    ∀ m : ℕ, (m + 1 : F) • E ((m : ℤ) + 1) =
      ∑ n ∈ Finset.range (m + 1),
        creationVL (F := F) (L := L) ⟨n + 1, Nat.succ_pos n⟩ a * E ((m : ℤ) - (n : ℤ))

/-- (8.4.17) the annihilation exponential `E^+(a,z) = exp(-Σ_{n≥1} (a(n)/n) z^{-n})`: the
exponential series in `w = z^{-1}`, `E^+ = Σ_j e_j w^j` with `e_j = E^+_{j-1}`, `e_0 = 1`, and
`(j+1)e_{j+1} = -Σ_{n=1}^{j+1} a(n) e_{j+1-n}` (finite on every vector: the `a(n)` are locally
nilpotent, which is why the relation is stated with an explicit truncation as a hypothesis of the
base field below). -/
def IsEplus (bL : Module.Basis κ ℤ L) (form : L →ₗ[ℤ] L →ₗ[ℤ] ℤ) (a : h F L)
    (E : CompFam F L) : Prop :=
  (∀ m : ℤ, m < -1 → E m = 0) ∧ E (-1) = 1 ∧
    ∀ j : ℕ, (j + 1 : F) • E (j : ℤ) =
      -∑ n ∈ Finset.range (j + 1),
        modeVL bL form a ((n : ℤ) + 1) * E ((j : ℤ) - (n : ℤ) - 1)

/-- (8.4.17) with (7.1.34)/(7.1.35): the operator `a z^∂`, componentwise in `z`: on `ι(b)` it is
`ε(a,b) ι(a+b)` when `⟨a,b⟩ = m` and `0` otherwise.  **THE SECTION IS THE BOOK'S OWN** (route A,
batch 359-A, step A-2): FLM fix ONE extension --- the one of (7.2.22)/(7.2.23) --- and write `Y(a,z)`
at ITS section `ε(α,β) = (−1)^{ε₁(α,β)}` (7.1.24 with `s = 2`, `ω = −1`), which is
`bookEvenCocycle_eps`; in particular the section is INDEPENDENT of the extension parameter `E`.
That parameter is retained (and unused here) because the frozen book-facing statements keep FLM's own
`(E, hE)` parameterization of (7.1.6)/(8.6.1) --- at the book's own section `hE` is the THEOREM
`hypothesis861_evenSect`, which is what retires the gauge route (P1)/(β). -/
def azPowD (bL : Module.Basis κ ℤ L) (form : L →ₗ[ℤ] L →ₗ[ℤ] ℤ) (_E : CentralExtension F L)
    (a : L) (m : ℤ) : VL F L →ₗ[F] VL F L :=
  TensorProduct.map LinearMap.id
    (Finsupp.linearCombination F fun b =>
      (if (form a) b = m then signPow F (eps1Map bL form a b) else 0)
        • Finsupp.single (a + b) (1 : F))

/-- (8.4.17): the base field `Y(a,z) = 8 E^-(a,z) · a z^∂ · E^+(a,z) 8` of a lattice generator, as
the book's product of the two exponentials and the lattice shift (finite on every vector).  The lattice
shift `azPowD` carries the book's OWN section (see its docstring), so the predicate does not read the
extension parameter `E`.

**WINDOW DEFECT OF RECORD (batch 361-A, truth identification; NOTES.md section 278).**  The rectangle
window `N` is EXISTENTIAL and the relation does NOT require the terms outside the rectangle to vanish
(the `p`-tail beyond `N`, and the `q`-tail beyond `Icc (-N) N`), so the value is not pinned to the
limit.  The missing conjuncts are exactly the book's finiteness, and they are PROVABLE in the honest
case: the `p`-tail by `annihFam_killsAbove` (already landed) and the `q`-tail by the lattice
confinement of `azPowD`. -/
def IsBaseField (bL : Module.Basis κ ℤ L) (form : L →ₗ[ℤ] L →ₗ[ℤ] ℤ)
    (E : CentralExtension F L) (Y : L → CompFam F L) : Prop :=
  ∀ a : L, ∃ Em Ep : CompFam F L,
    IsEminus (ofL (F := F) a) Em ∧ IsEplus bL form (ofL (F := F) a) Ep ∧
      ∀ (m : ℤ) (w : VL F L), ∃ N : ℕ,
        Y a m w = ∑ p ∈ Finset.range N,
          ∑ q ∈ Finset.Icc (-(N : ℤ)) (N : ℤ),
            Em p (azPowD bL form E a q (Ep (p + m + q) w))

/-- (8.5.5)--(8.5.6): a vertex operator on `V_L` in the sense of the book -- its value on every
(8.5.4) state is the normal ordered product (8.5.5) of the derived Heisenberg factors with the base
field (8.4.17) `Y(a,z)` at the state's lattice label, and the base field is (8.4.17). -/
def IsVertexOperator (bL : Module.Basis κ ℤ L) (form : L →ₗ[ℤ] L →ₗ[ℤ] ℤ)
    (E : CentralExtension F L) (Y : VL F L →ₗ[F] CompFam F L) : Prop :=
  (IsBaseField bL form E fun a => Y (iotaVL (F := F) (L := L) a)) ∧
    ∀ D : StateDatum F L,
      ∃ Z : CompFam F L, IsFold bL form D.1 (Y (iotaVL (F := F) (L := L) D.2)) Z ∧ Y (stateOf D) = Z

/-! ## THE OBJECT `L` OF THEOREM 8.6.1 (batch 363-A, owner's directive)

FLM Theorem 8.6.1 is a statement about ONE object: the lattice `L` of (7.1.1) with its form and a
chosen `ℤ`-basis, the central extension `L̂` of (7.1.6) in the normalised section form of
(7.1.20)--(7.1.28) carrying the hypothesis (8.6.1), and the field `Y` of (8.4.17)/(8.5.5) on `V_L`
carrying its prescription.  That object is the structure below, so that the theorem's signature names
it ONCE instead of eleven loose parameters.  The (8.6.2)/(8.6.3) data --- the two Fock parts, the two
lattice elements and the window --- stay arguments: they are the theorem's own data, not part of the
object `L`. -/

/-- **THE OBJECT `L` OF THEOREM 8.6.1**: THE (7.1.1) LATTICE IN THE BOOK'S OWN SENSE --- the standing
assumption of §7.1 (printed p. 144), verbatim: "We start with a lattice `L` with symmetric form
`(·,·)`, and we assume only that `L` is NONDEGENERATE --- not necessarily even or positive definite";
`h = L_F = L ⊗_ℤ F` (7.1.1) is a finite-dimensional `F`-vector space with NONSINGULAR symmetric form
(`hnd`) --- together with a chosen `ℤ`-basis, the (7.1.6) extension `L̂` as the normalised section of
(7.1.20)/(7.1.24) carrying the (8.6.1) hypothesis, and the (8.4.17)/(8.5.5) field `Y` on `V_L`
carrying its prescription.

So the lattice's properties are the book's, and they are FIELDS of this object rather than loose
parameters: `L` is a free `ℤ`-module of FINITE RANK (`[Module.Free ℤ L]` plus a basis over a FINITE
index type `κ`), `form` is a symmetric (`form_symm`, (7.1.1)) `ℤ`-bilinear form, and `hnd` is the
§7.1 nondegeneracy `hFormNondegenerate` (nonsingularity of the form on `h = L ⊗_ℤ F`).

**THE THEOREM'S HYPOTHESES ARE NOT HERE (owner's directive).**  This structure carries only the DATA
of the setting --- the lattice with its properties, the chosen section `E` of `L̂` and the field `Y`.
The hypotheses of Theorem 8.6.1 are stated at the THEOREM's side: (8.6.1)
`c(ā,b̄) = (−1)^{⟨ā,b̄⟩}` and the book's prescription (8.4.17)+(8.5.5) for `Y` are arguments of
`MM.FLM861Book.FLM_8_6_1` (and of every other statement that needs them).
**EVENNESS AND POSITIVE DEFINITENESS ARE NOT ASSUMED**: the book says so explicitly ("not necessarily
even or positive definite"); evenness is what (8.6.1) FORCES in the integral case ("in which case `L`
is also even, `c(a,a)` being equal to 1", p. 205) --- the landed `even_of_hypothesis861` --- and
positive definiteness belongs to Theorem 8.10.2's hypothesis ("For a positive definite even lattice
`L`", p. 245), not to (7.1.1). -/
structure FLM861Datum (F : Type u) [Field F] [CharZero F] where
  /-- (7.1.1) the lattice `L`: a free `ℤ`-module of finite rank. -/
  L : Type v
  /-- (7.1.1) `L` is an abelian group. -/
  [addCommGroup : AddCommGroup L]
  /-- (7.1.1) `L` is a free `ℤ`-module (of finite rank: the basis below is indexed by the finite
  `κ`). -/
  [moduleFree : Module.Free ℤ L]
  /-- an indexing type for a `ℤ`-basis of `L`. -/
  κ : Type w
  /-- the indexing type is finite. -/
  [fintype : Fintype κ]
  /-- the indexing type has decidable equality. -/
  [decEq : DecidableEq κ]
  /-- (7.1.1) a `ℤ`-basis of `L`, the one the chapter-8 constructions are read in. -/
  bL : Module.Basis κ ℤ L
  /-- (7.1.1) the symmetric form `(·,·)`. -/
  form : L →ₗ[ℤ] L →ₗ[ℤ] ℤ
  /-- (7.1.1) the form is symmetric. -/
  form_symm : ∀ a b : L, form a b = form b a
  /-- **§7.1 (printed p. 144): "we assume only that `L` is nondegenerate"** --- the form on
  `h = L ⊗_ℤ F` is nonsingular (`hFormNondegenerate`). -/
  hnd : hFormNondegenerate F bL form
  /-- (7.1.6)/(7.1.20) the extension `L̂`, in the normalised section form of (7.1.20)--(7.1.28) ---
  DATA, not a hypothesis: FLM fix ONE extension. -/
  E : CentralExtension F L
  /-- (8.4.17)/(8.5.5) the field `Y` on `V_L` --- DATA (the operator the display is about). -/
  Y : VL F L →ₗ[F] CompFam F L

attribute [instance] FLM861Datum.addCommGroup FLM861Datum.moduleFree FLM861Datum.fintype
  FLM861Datum.decEq

/-! ## (8.5.13)--(8.5.26): the commutator family, the iterate and the residue -/

/-- (8.5.15) the left hand side of (8.5.13): the coefficient of `z₁^{-m-1}z₂^{-n-1}` in
`[Y(u,z₁),Y(v,z₂)]`. -/
def commutatorFamily (Y : VL F L →ₗ[F] CompFam F L) (u v : VL F L) (m n : ℤ) :
    VL F L →ₗ[F] VL F L :=
  Y u m * Y v n - Y v n * Y u m

/-- (8.5.24) the iterate: `Y(Y(u,z₀)v,z₂) = Σ_{i,j} (u_i·v)_j z₀^{-i-1}z₂^{-j-1}`; in components,
`iterateOf Y u v i j = Y (u_i·v) j`. -/
def iterateOf (Y : VL F L →ₗ[F] CompFam F L) (u v : VL F L) (i j : ℤ) :
    VL F L →ₗ[F] VL F L :=
  Y ((Y u i) v) j

/-- (8.5.25): the coefficient family of `e^{-z₀∂/∂z₁}δ(z₁/z₂)`, `(-1)^k binom(l,k)`. -/
def deltaExpCoeff (k : ℕ) (l : ℤ) : F := (-1 : F) ^ k * binomCoeff (F := F) l k

/-- (8.5.13) with (8.5.24), (8.5.25) and (8.4.33): the coefficient of `z₁^{-m-1}z₂^{-n-1}` in
`Res_{z₀} z₂^{-1} Y(Y(u,z₀)v,z₂) e^{-z₀∂/∂z₁}δ(z₁/z₂)` -- the right hand side of the display. -/
def corollary851Residue (Y : VL F L →ₗ[F] CompFam F L) (u v : VL F L) (K : ℕ) (m n : ℤ) :
    VL F L →ₗ[F] VL F L :=
  ∑ i ∈ Finset.range K,
    deltaExpCoeff (F := F) i ((i : ℤ) - m - 1) •
      iterateOf Y u v (i : ℤ) (m + n - (i : ℤ))

end FLM861Book

end MM
