/-
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 Theorem 8.6.1, described from the book --- definitions + the theorem (with `sorry`), Mathlib only

Frenkel--Lepowsky--Meurman, *Vertex Operator Algebras and the Monster*, Academic Press 1988:
(7.1.1)--(7.1.5) (printed pp. 143--145), (7.1.6)--(7.1.9) (p. 145), (7.1.20)--(7.1.32)
(pp. 146--147), (7.1.34)--(7.1.41) (pp. 147--148), (8.4.7)--(8.4.25) (pp. 189--193),
(8.5.1)--(8.5.24) (pp. 198--201) and **Theorem 8.6.1, (8.6.1)--(8.6.3)** (printed p. 205).

This file is a clean-room STATEMENT of FLM Theorem 8.6.1: every definition below is the book's own
definition, written with Mathlib only (no `Definitions/` layer), and the only `sorry` is the theorem
itself.  Where the book writes an infinite sum that is finite on every vector (the exponentials of
(8.4.17), the normal ordered product (8.4.16)), the definition is given as the book's *relation* with
the finiteness window existentially quantified, exactly as the book uses it.

## What the theorem says

(8.6.1) `(a,b) ∈ ℤ` and `c(a,b) = (-1)^(a,b)`; (8.6.2) `u = u' ⊗ ι(a)`, `v = v' ⊗ ι(b)`; then
(8.6.3) `[Y(u,z₁),Y(v,z₂)] = Res_{z₀} z₂⁻¹ Y(Y(u,z₀)v,z₂) e^{-z₀∂/∂z₁}((z₁/z₂)^a δ(z₁/z₂))`,
stated componentwise in the book's (8.5.15) indexing (equivalently, Corollary 8.5.4/(8.5.26)):
`[u_m, v_n] = Σ_{i≥0} binom(m,i) (u_i·v)_{m+n-i}`, the sum being finite.
## REPAIR (batch 344-A): the drafted (8.4.16)/(8.4.17)/(8.5.5) definitions corrected

The first draft of this file rendered four of the book's definitions with index errors; all four are
refuted by compiled witnesses in `Refuted/MMFLM861BookFieldRefute.lean` (namespace `MM.B344A`):

* `IsNormalOrder` evaluated both halves of (8.4.16) at indices of the wrong sign, so the predicate
  held only for `Z = 0` (`MM.B344A.isNormalOrder_apply_eq_zero`); the fold then forced
  `Y (stateOf D) = 0` at every state with a nonempty oscillator list
  (`MM.B344A.isVertexOperator_stateOf_eq_zero`), while the honest (8.4.16) is nonzero there
  (`MM.B344A.honestAction_neg_one_ne_zero`);
* `IsBaseField`'s right-hand side did not mention `m` at all --- the antidiagonal constraint
  `r = p + m + q` of the (8.4.17) product of the two exponential factors with `a z^∂` was missing;
* `IsEplus`'s recurrence carried the coefficient `E (j - n)` where the component indexing of `E^+`
  (the coefficient of `z^{-r-1}`) requires `E (j - n - 1)`;
* `derivedFactor` read the file's `mode`, which is `0` at the mode `0`, so the (8.4.14) zero mode
  `a(0)` that the source's normal ordering keeps was missing (`MM.B344A.derivedFactor_zero_eq_zero`
  against `MM.B344A.honestFactor_zeroMode_ne`).

The repaired definitions below are the source's (8.4.16)/(8.4.17)/(8.5.5) in the (8.5.15) component
indexing (`heisVL` is the (8.4.7) field with the (8.4.14) zero mode, `hZeroVLF` its `F`-valued
companion).  The three book-facing theorem STATEMENTS are untouched; the field bridge is in its
ROUTE-A shape `exists_evenCocycle_eq_zAligned` (batch 359-A: the definitions read the book's OWN
section, so the bridge is FLM (8.5.1) uniqueness of the prescription --- the batch-346-A gauge/ray
shape and the batch-348-A/349-A (P1)/(beta) reduction are RETIRED) and is discussed in its own
docstring.

**Batch 352-A split; batch 359-A state.**  This file keeps only the CONSUMERS of the definitions: the
frozen book-facing statements (the entry and FLM Theorem 8.6.1) with their axiom-footprint guards.  The
definitions moved to `Definitions/FLM861BookDefs.lean` (which since 359-A also carries the book's own
section and the `azPowD` that reads it), the battlefield to
`Definitions/FLM861BookTransport.lean` (which since 359-A carries the (8.6.1) parity inputs, the
existence statement and the ONE registered piece `rigidity_of_hY`); both are imported below, so every
name in scope is unchanged.
-/

import Definitions.FLM861BookDefs
import Definitions.FLM861BookTree
import Definitions.FLM861BookTransport
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
import Definitions.MMFLM810Theorem861Stated
import Definitions.MMFLM85Conjugation

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 κ]


/- **THE FIELD BRIDGE OF THIS FILE (route A, batch 359-A: THE SECTION CONVENTION REPAIRED AT THE
DEFINITIONS).**  The honest field reads the SECTION, not only the commutator map (compiled below as
`zAligned_iotaVL_apply_eq_eps`), so the bridge is a statement about ONE section.  FLM fix ONE central
extension --- the one of (7.2.22)/(7.2.23) --- and write `Y(a,z)` of (8.4.17) at ITS section (7.1.24);
the definitions of `Definitions/FLM861BookDefs.lean` therefore read the book's OWN section
(`bookEvenCocycle`, and `azPowD` hence `IsBaseField`/`IsVertexOperator` --- the extension parameter
is not read there), and at that section the hypothesis (8.6.1) is the THEOREM
`hypothesis861_evenSect` (batch 359-A, step A-1b).

**The statement below** is then FLM (8.5.1)'s content: the prescription (8.4.17)+(8.5.5) DETERMINES the
field, and its value is the honest field of the book's own even cocycle.  It is PROVED here (one line)
from the battlefield's single registered piece `rigidity_of_hY`, instantiated at the canonical
`bookEvenCocycle bL form hs heven` whose evenness datum is `even_of_hypothesis861 form E hE`.

**What this RETIRES (batch 359-A), and what stands.**  The previous gauge/ray spelling
`∃ C Λ, Y = conjFam (conjGauge Λ) (ZAligned (C.toCentralExtension h2))` is retired together with its
(P1) input `epsExists_of_hE` and the classical (beta) lemma `symmCocycle_isCoboundary`: they existed
only because the file let `E.eps` be an ARBITRARY section, and FLM never compare two sections.  The
refutation `MM.B345A.bridge_conclusion_false` (batch 345-A) STANDS and is untouched: the honest field
of the trivial section `extR` is NOT the honest field of any even cocycle.  What that refutation
forbids is the equality for a field at a NON-book section; the present statement's hypothesis is the
book's own prescription, which the honest field of `extR` does not satisfy (`azPowD` no longer reads
`E.eps`).  See NOTES.md section 276 and HANDOVER.md section 3.

**The front line.**  `FLM_8_6_1` below consumes the bridge together with the landed
`MM.FLM810T861S.theorem861_all_pairs`, with no gauge transport at all.  Its parameters `(E, hE)` are
kept because the book-facing statements are FROZEN and their `(E, hE)` parameterization is FLM's own
(7.1.6)/(8.6.1) setting; the definitions read the book's own section. -/

theorem exists_evenCocycle_eq_zAligned (bL : Module.Basis κ ℤ L)
    (form : L →ₗ[ℤ] L →ₗ[ℤ] ℤ)
    (hs : ∀ a b : L, form a b = form b a) (E : CentralExtension F L)
    (hE : ∀ a b : L, Hypothesis861 form E a b) (Y : VL F L →ₗ[F] CompFam F L)
    (hY : IsVertexOperator bL form E Y) :
    ∃ C : MM.FLMLattice.EvenCocycle L form,
      Y = MM.FLM810JZF.ZAligned bL form
        (C.toCentralExtension (F := F) (two_ne_zero (α := F))) :=
  ⟨bookEvenCocycle bL form hs fun a => even_of_hypothesis861 form E hE a,
    rigidity_of_hY bL form hs (fun a => even_of_hypothesis861 form E hE a) E Y hY⟩

/-! ## FLM Theorem 8.6.1 -/

/-- **FLM Theorem 8.6.1, (8.6.1)--(8.6.3)**, in the component form of the display: for
u = u' ⊗ ι(a), v = v' ⊗ ι(b) and (a,b) satisfying (8.6.1), the (m,n)-coefficient of the commutator is
the residue of the iterate, the sum being finite (the window K is past the iterate's vanishing, which
the grading (8.5.22) supplies in the book).  The form is symmetric, as in (7.1.1).

**The object `L` (batch 363-A, owner's directive).**  The SETTING is ONE input, `D : FLM861Datum` ---
the (7.1.1) lattice with its form and basis, the chosen (7.1.6) section `D.E` of `L̂` and the
(8.4.17)/(8.5.5) field `D.Y` on `V_L` --- while THIS THEOREM's hypotheses are stated here, on the
theorem's side: (8.6.1) `hE` and the book's prescription `hY` for `D.Y`.  The (8.6.2)/(8.6.3) data
(the two Fock parts `u'`, `v'`, the two lattice elements `a`, `b` and the window `K`) stay
arguments too.  The content is unchanged: the same hypotheses on the same objects, same conclusion.

**Route A reading (batch 359-A).**  The definitions read the book's OWN section (7.1.24) at the
(7.2.22)/(7.2.23) extension, so `Y` here is FLM's `Y` of `V_L` and the (8.6.1) hypothesis `hE` ---
which the frozen statement retains, FLM's own (7.1.6) parameterization --- holds automatically at that
section (`hypothesis861_evenSect`); the proof below does not consume it.

The proof is the repository's landed Theorem 8.6.1, MM.FLM810T861S.theorem861_all_pairs (B229-A; its
chain runs through the two registered pieces MM.FLM86S5H.spanningStepLeftGen8625 and
MM.FLM86S5H.spanningStepRight8625), reached through the field bridge `exists_evenCocycle_eq_zAligned`
above --- FLM (8.5.1) uniqueness of the prescription, the file's single registered piece
(`rigidity_of_hY`), with NO gauge transport (the (P1)/(beta) route was retired in batch 359-A). -/
theorem FLM_8_6_1 (D : FLM861Datum (F := F))
    (hE : ∀ a b : D.R.L, Hypothesis861 D.form D.E a b)
    (hY : IsVertexOperator D.bL D.form D.E D.Y)
    (u' v' : M1 F D.R.L) (a b : D.R.L) (K : ℕ)
    (hK : ∀ i : ℤ, (K : ℤ) ≤ i →
      iterateOf D.Y (stateOfFock u' a) (stateOfFock v' b) i = 0) :
    ∀ m n : ℤ,
      commutatorFamily D.Y (stateOfFock u' a) (stateOfFock v' b) m n
        = corollary851Residue D.Y (stateOfFock u' a) (stateOfFock v' b) K m n := by
  obtain ⟨C, hYg⟩ := exists_evenCocycle_eq_zAligned D.bL D.form D.form_symm D.E hE D.Y hY
  rw [hYg] at hK ⊢
  intro m n
  have hwin : ∀ i : ℤ, (K : ℤ) ≤ i →
      MM.FLM85It.iterateOf
        (MM.FLM810JZF.ZAligned D.bL D.form
          (C.toCentralExtension (F := F) (two_ne_zero (α := F))))
        (stateOfFock u' a) (stateOfFock v' b) i = 0 := by
    intro i hi
    rw [← iterateOf_fam_eq_tree]
    exact hK i hi
  have hZ := MM.FLM810T861S.theorem861_all_pairs (F := F) D.bL D.form C (two_ne_zero (α := F))
    D.form_symm (stateOfFock u' a) (stateOfFock v' b) K hwin
  rw [commutatorFamily_eq_tree, corollary851Residue_eq_tree]
  exact hZ m n

/-- **Theorem 8.6.1 at the book's own states, with the WINDOW DERIVED**: `u = u' ⊗ ι(a)`,
`v = v'' ⊗ ι(b)` presented by WORDS (8.5.4)/(8.6.2), so that the homogeneity of Corollary 8.6.7 and the
finiteness of (8.6.3) come from the grading (8.5.21)/(8.5.22) through `iterateOf_window_zero` instead of
being the hypothesis `hK` of `FLM_8_6_1`.  The conclusion is (8.6.3) in the component form (8.5.15): the
`(m,n)`-coefficient of `[Y(u,z₁),Y(v,z₂)]` equals that of
`Res_{z₀} z₂^{-1}Y(Y(u,z₀)v,z₂)e^{-z₀(a,∂/∂z₁)}((z₁/z₂)^{(a,b)}δ(z₁/z₂))`. -/
theorem FLM_8_6_1_window (D : FLM861Datum (F := F))
    (hE : ∀ a b : D.R.L, Hypothesis861 D.form D.E a b)
    (hY : IsVertexOperator D.bL D.form D.E D.Y)
    (S T : BookState F D.R.L) (m n : ℤ) :
    commutatorFamily D.Y S.vl T.vl m n
      = corollary851Residue D.Y S.vl T.vl (window S T) m n :=
  FLM_8_6_1 D hE hY S.fock T.fock S.lattice T.lattice (window S T)
    (iterateOf_window_zero D.Y S T) m n

/-- **Theorem 8.6.1, SECOND PARAGRAPH** (the book, p. 205, verbatim): "If `L` is integral and (8.6.1)
holds for all `a, b ∈ L`" --- "in which case `L` is also even, `c(a,a)` being equal to `1`" --- "then
(8.6.3), with the factor `(z₁/z₂)^{(a,b)}` omitted, holds for all `u, v ∈ V_L`."  In the component form
of (8.5.15) used here: every pair `u, v ∈ V_L` comes with a window past which the iterate vanishes and
the display holds --- the lattice labels `a, b` are gone from the conclusion, which is (8.6.3) at the
trivial character. -/
theorem FLM_8_6_1_all (D : FLM861Datum (F := F))
    (hE : ∀ a b : D.R.L, Hypothesis861 D.form D.E a b)
    (hY : IsVertexOperator D.bL D.form D.E D.Y)
    (u v : VL F D.R.L) :
    ∃ K : ℕ, (∀ i : ℤ, (K : ℤ) ≤ i → iterateOf D.Y u v i = 0) ∧
      ∀ m n : ℤ, commutatorFamily D.Y u v m n = corollary851Residue D.Y u v K m n := by
  sorry


/-! ## Axiom footprints (measured by the build; the printed text is what guard_msgs compares) -/

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

end FLM861Book

end MM
