/-
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 Definitions.FLM61Lattices
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
  /-- **§6.1 (6.1.1)**: the (rational) lattice `L` of the book's §6.1 --- "a rank `n` free abelian group
  provided with a rational-valued symmetric `ℤ`-bilinear form `(·,·) : L × L → ℚ`" --- with that form.
  This is the DEFAULT of the book, and the chapter-8 form below is its INTEGRAL (6.1.9) specialisation.
  The lattice `L` itself is read off this datum (`FLM861Datum.L`). -/
  R : MM.FLM61.RationalLattice.{v}
  /-- 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 κ ℤ R.L
  /-- (7.1.1) the symmetric form `(·,·)` of the chapter --- the INTEGRAL (6.1.9) specialisation of the
  §6.1 form `R.form`. -/
  form : R.L →ₗ[ℤ] R.L →ₗ[ℤ] ℤ
  /-- (7.1.1) the form is symmetric. -/
  form_symm : ∀ a b : R.L, form a b = form b a
  /-- **§6.1 (6.1.1) with (6.1.9)**: the `ℤ`-valued form above IS the §6.1 form on `L`. -/
  form_eq : ∀ a b : R.L, R.form a b = (form a b : ℚ)
  /-- **§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 R.L
  /-- (8.4.17)/(8.5.5) the field `Y` on `V_L` --- DATA (the operator the display is about). -/
  Y : VL F R.L →ₗ[F] CompFam F R.L

attribute [instance] FLM861Datum.fintype FLM861Datum.decEq

namespace FLM861Datum

variable (D : FLM861Datum F)

/-- **§6.1 (6.1.9)**: the §6.1 form is INTEGRAL on `L` --- equivalently `D.form` takes values in `ℤ`
(`D.form_eq`); this is the `(a,b) ∈ ℤ` half of the hypothesis (8.6.1). -/
theorem form_int (a b : D.R.L) : ∃ m : ℤ, D.R.form a b = (m : ℚ) :=
  ⟨D.form a b, D.form_eq a b⟩

/-- **§6.1 (6.1.2) is the standing assumption of §7.1**: `L` is NONdegenerate, here as the
nonsingularity `D.hnd` of the form on `h = L ⊗_ℤ F`. -/
theorem nondegenerate_on_h : hFormNondegenerate F D.bL D.form := D.hnd

end FLM861Datum

/-! ## (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
