/-
Copyright (c) 2026 The MM project. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: MM project (FLM Chapter 8 transcription, batch 152 file 1)

Frenkel--Lepowsky--Meurman, *Vertex Operator Algebras and the Monster*, Academic Press 1988:
**the uniform-in-`(m,n)` vanishing of the summands of Corollary 8.5.4 (8.5.26)** -- the source's
finiteness parenthetical of printed p. 201, "we note that `ι(a)_i·ι(b) = 0` for `i` sufficiently
large" -- as a statement about `MM.FLM85Br.bracketTerm` and, in the `ℤ`-indexed form the source
writes it in, about the state `ι(a)_i·ι(b)` and the iterate `Y(Y(a,z_0)ι(b),z_2)`.

## What is proved here

`bracketTerm Y a b m n i = C(m,i)·(ι(a)_i·ι(b))_{m+n-i}` (the landed `MM.FLM85Br.bracketTerm`).  The
content of the parenthetical is that the *state* `ι(a)_i·ι(b)` vanishes for `i` large, and it is
uniform in `(m,n)` because the outer component `(·)_{m+n-i}` is applied to that state linearly: once
the state is `0`, the summand is `0` for **every** `(m,n)`.  This file lands that in four shapes.

* **(1) `bracketTerm_vanishing_of_grading_uniform`** -- the brief's interface, verbatim (hypotheses
  `hOm`, `hgrad`, `hb`, `hW`).  **It is VACUOUS as stated**, and the vacuity is a theorem here
  (`not_forall_isHomogeneousOp`, §0): the hypothesis `hOm` is *refutable*, because the landed
  `WeightGrading.IsHomogeneousOp` demands `S.wt (T a) = S.wt a + p` also when `T a = 0`, and
  `component Y n 0 = 0` with `0` homogeneous.  See §0 for the two-line refutation.
* **(1-honest) `bracketTerm_vanishing_of_gradingOn` and `..._uniform`, and the engine
  `exists_component_vanishing_uniform`** -- the same mathematics with the *zero-image case removed*
  from the hypothesis: `IsHomogeneousOpOn S T p` requires the weight identity only when `T a ≠ 0`.
  The repaired hypothesis is satisfiable (it is FLM (8.5.22) with the `T a = 0` case, where `wt` of `0`
  is unconstrained by `WeightGrading.wt_eq_of_mem`, dropped), and it is *weaker* than the landed one
  (`IsHomogeneousOp.isHomogeneousOpOn`).  These are the non-vacuous statements of the parenthetical
  from the grading.
* **(1a) `exists_uniform_bracketTerm_vanishing`** -- the axiom-level form: for a landed
  `MM.FLM810.VertexOperatorAlgebra A`, the vanishing is a **one-line consequence of the axiom
  (8.10.5)** (`A.componentTruncation`), with **no** `hOm`, `hgrad`, `hb`, `hW` and no grading at all.
  The source's parenthetical *is* (8.10.5) at the pair `(a,b)`; see §3.  This is the statement the
  consumer file can actually instantiate.
* **(2) `exists_iterate_uniform_vanishing`** -- the `ℤ`-indexed form `∃K, ∀ i ≥ K, iterateOf Y a b i = 0`
  (the whole family `(ι(a)_i·ι(b))_j` vanishes, `j ∈ ℤ`), from (8.10.5), with the implication
  (2) ⇒ (1) landed as `bracketTerm_vanishing_of_iterate_uniform` (§4).

## The window, and the case split that makes it uniform in `(m,n)`

For the state vanishing at the finite-window shapes the window is `N := (S.wt a + S.wt b).toNat`
(`bracketTerm_vanishing_of_gradingOn`), exactly the landed
`MM.FLM85Br.bracketTerm_vanishing_of_grading` window, under the repaired hypothesis.  For a vector `a`
that is *not* homogeneous the window is the maximum of `j + S.wt b` over the weights `j` of a graded
decomposition `a = Σ_{j∈s} c_j` of the landed `WeightGrading.exists_sum_graded`
(`exists_component_vanishing_uniform`, `bracketTerm_vanishing_of_gradingOn_uniform`, `N := ((Σ_{j∈s}
max j 0) + Σ_{l∈t} max l 0).toNat`); the brief's `(S.wt a + S.wt b).toNat` is **not** a valid window
there, because `S.wt` carries no information on a non-homogeneous vector (`wt_eq_of_mem` constrains
`wt` only on nonzero elements of a graded piece).  No case split on the sign of `m` or on the binomial
is needed: the state window is uniform in `(m,n)` on its own, and the binomial `binomCoeff m i` -- which
for `m ≥ 0` vanishes for `i > m` but for `m < 0` does not vanish at all -- never enters.

## What is NOT proved here

* **(1) is not derived from the `VertexOperatorAlgebra` axioms, and it cannot be**: its hypothesis is
  refutable.  The axiom-level theorem is (1a), which does not go through the weight statement.
* The landed **Remark 8.10.1** (`v_n` raises the weight by `wt v − n − 1`) is **not** derived from
  `A.L0_grading`/`A.translation`/`A.jacobi` here; §0 records only that its landed formalisation
  `IsHomogeneousOp` is refutable for the `∀u` form, and `IsHomogeneousOpOn` is the satisfiable
  replacement.  Deriving `IsHomogeneousOpOn` from the axioms would need the *uniqueness* half of the
  direct sum `V = ∐_n V_(n)` (an `L(0)`-eigenvector of eigenvalue `k` lies in `W k`), which the landed
  `WeightGrading` interface deliberately does not carry (`MMFLM810Axioms.lean:147--152`).
* No `sorry`, no `axiom`, no `native_decide`, no `maxHeartbeats`.
-/

import Definitions.MMFLM810Axioms
import Definitions.MMFLM85Iterate
import Definitions.MMFLM85Extraction
import Mathlib.Tactic

set_option autoImplicit false

-- Two hypotheses below (`hb` of `bracketTerm_vanishing_of_gradingOn_uniform`, `hgrad` of
-- `bracketTerm_vanishing_of_grading_uniform`) are deliberately kept for interface fidelity although
-- the proof does not consume them; they are documented in the docstrings.  The linter's warning is
-- therefore expected and is switched off for this file only.
set_option linter.unusedVariables false

noncomputable section

namespace MM

namespace FLM86UV

open FLM85 FLM85Br FLM810 FLM85It FLM85Ext

variable {F : Type*} [Field F]
variable {V : Type*} [AddCommGroup V] [Module F V]

/-! ## §0. The zero-image defect of `IsHomogeneousOp`, and the repair `IsHomogeneousOpOn`

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

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

The second conjunct is demanded also when `T a = 0`, where it reads `S.wt 0 = S.wt a + p`; and
`S.wt 0` is a *single* integer while `S.wt a` ranges over the weights of the homogeneous vectors killed
by `T`.  Two such vectors of different weights therefore refute the predicate, and the `∀ u` form used
by the source's (8.5.22) is refuted outright by `u = 0`, because `component Y n 0 = 0`.  The repair
below keeps the weight identity exactly where it has content (`T a ≠ 0`, which is where
`WeightGrading.wt_eq_of_mem` is used) and is satisfiable. -/

/-- **FLM (8.5.22)** with the zero-image case removed: `T` raises the weight by `p` on the homogeneous
vectors that it does *not* kill.  This is the landed `WeightGrading.IsHomogeneousOp` with the case
`T a = 0` dropped; it is the satisfiable reading of `deg v_n = n − wt v + 1`, and it is all the
vanishing arguments below consume. -/
def IsHomogeneousOpOn (S : WeightGrading F V) (T : V →ₗ[F] V) (p : ℤ) : Prop :=
  ∀ a : V, S.IsHomogeneous a → T a ≠ 0 → S.IsHomogeneous (T a) ∧ S.wt (T a) = S.wt a + p

/-- The landed `IsHomogeneousOp` implies the repaired `IsHomogeneousOpOn` -- so every theorem below
stated for `IsHomogeneousOpOn` generalises its `IsHomogeneousOp` counterpart. -/
theorem IsHomogeneousOp.isHomogeneousOpOn {S : WeightGrading F V} {T : V →ₗ[F] V} {p : ℤ}
    (h : S.IsHomogeneousOp T p) : IsHomogeneousOpOn S T p :=
  fun a ha _ => h a ha

/-- The landed `IsHomogeneousOp` is refuted by the zero operator unless `p = 0`: at `a = 0`, which is
homogeneous (`WeightGrading.isHomogeneous_zero`), the weight clause reads `S.wt 0 = S.wt 0 + p`. -/
theorem not_isHomogeneousOp_zero {S : WeightGrading F V} {p : ℤ} (hp : p ≠ 0) :
    ¬ S.IsHomogeneousOp (0 : V →ₗ[F] V) p := by
  intro h
  have h0 := (h 0 S.isHomogeneous_zero).2
  simp only [LinearMap.zero_apply] at h0
  omega

/-- A component operator that kills two homogeneous vectors of *different* weights satisfies
`IsHomogeneousOp` at no `p`. -/
theorem not_isHomogeneousOp_of_kills {S : WeightGrading F V} (T : V →ₗ[F] V) (p : ℤ)
    {w1 w2 : V} (h1 : S.IsHomogeneous w1) (h2 : S.IsHomogeneous w2)
    (hz1 : T w1 = 0) (hz2 : T w2 = 0) (hw : S.wt w1 ≠ S.wt w2) :
    ¬ S.IsHomogeneousOp T p := by
  intro h
  have e1 := (h w1 h1).2
  have e2 := (h w2 h2).2
  rw [hz1] at e1
  rw [hz2] at e2
  omega

/-- **The hypothesis `hOm` of `bracketTerm_vanishing_of_grading_uniform` is REFUTABLE**, with no
hypothesis on `S` or `Y` at all: `0` is homogeneous and `component Y n 0 = 0`, so the weight clause at
`u = 0` reads `S.wt 0 = S.wt 0 + (S.wt 0 - n - 1)`, i.e. `S.wt 0 = n + 1`, for *every* `n ∈ ℤ`.  So the
main theorem of this file that takes `hOm` is vacuous, and the usable statements are the
`IsHomogeneousOpOn` ones and the axiom-level (1a) in §3. -/
theorem not_forall_isHomogeneousOp (S : WeightGrading F V) (Y : VertexOp F V) :
    ¬ (∀ u : V, S.IsHomogeneous u →
      ∀ n : ℤ, S.IsHomogeneousOp (VertexOp.component Y n u) (S.wt u - n - 1)) := by
  intro h
  have h0 : ∀ n : ℤ, S.wt (0 : V) - n - 1 = 0 := by
    intro n
    have h1 := h 0 S.isHomogeneous_zero n
    rw [show VertexOp.component Y n (0 : V) = 0 from (VertexOp.component Y n).map_zero] at h1
    have h2 := (h1 0 S.isHomogeneous_zero).2
    simp only [LinearMap.zero_apply] at h2
    omega
  have h2 := h0 0
  have h3 := h0 1
  omega

/-! ## §1. The engine, with the repaired hypothesis -/

/-- **FLM (8.5.22) with §7.1**, the repaired form of the landed
`MM.FLM85Br.component_apply_eq_zero_of_weight_lt`: the same conclusion from the weaker hypothesis
`IsHomogeneousOpOn`. -/
theorem component_eq_zero_of_weight_lt_on (S : WeightGrading F V) (Y : VertexOp F V) {u w : V}
    (n : ℤ) (hOp : IsHomogeneousOpOn S (VertexOp.component Y n u) (S.wt u - n - 1))
    (hw : S.IsHomogeneous w) (hW : ∀ k : ℤ, k < 0 → S.W k = ⊥)
    (hneg : S.wt u + S.wt w < n + 1) : VertexOp.component Y n u w = 0 := by
  by_contra hne
  obtain ⟨hh, hwt⟩ := hOp w hw hne
  obtain ⟨k, hk⟩ := hh
  have hk_eq : k = S.wt w + (S.wt u - n - 1) := by
    rw [← S.wt_eq_of_mem hk hne, hwt]
  have hkneg : k < 0 := by omega
  rw [hW k hkneg, Submodule.mem_bot] at hk
  exact hne hk

/-- **FLM (8.5.22) with §7.1**, the threshold made explicit, repaired form of the landed
`MM.FLM85Br.component_eq_zero_of_toNat_le`. -/
theorem component_eq_zero_of_toNat_le_on (S : WeightGrading F V) (Y : VertexOp F V) {u w : V}
    (hw : S.IsHomogeneous w)
    (hOp : ∀ n : ℤ, IsHomogeneousOpOn S (VertexOp.component Y n u) (S.wt u - n - 1))
    (hW : ∀ k : ℤ, k < 0 → S.W k = ⊥) :
    ∀ i : ℕ, (S.wt u + S.wt w).toNat ≤ i → VertexOp.component Y (i : ℤ) u w = 0 := by
  intro i hi
  refine component_eq_zero_of_weight_lt_on S Y (i : ℤ) (hOp _) hw hW ?_
  rcases lt_trichotomy (S.wt u + S.wt w) 0 with h | h | h
  · omega
  · omega
  · have ht : (((S.wt u + S.wt w).toNat : ℕ) : ℤ) = S.wt u + S.wt w :=
      Int.toNat_of_nonneg (le_of_lt h)
    have hi' : (((S.wt u + S.wt w).toNat : ℕ) : ℤ) ≤ (i : ℤ) := by exact_mod_cast hi
    omega

/-! ## §2. The uniform-in-`(m,n)` vanishing from the repaired weight hypothesis -/

/-- **FLM Corollary 8.5.4, the finiteness parenthetical, at the small window**: with the repaired
hypothesis at the single state `a` (and `b` homogeneous), the summands of (8.5.26) vanish from
`(S.wt a + S.wt b).toNat` on -- the landed `MM.FLM85Br.bracketTerm_vanishing_of_grading`, with its
hypothesis `IsHomogeneousOp` weakened to `IsHomogeneousOpOn`. -/
theorem bracketTerm_vanishing_of_gradingOn (S : WeightGrading F V) (Y : VertexOp F V) {a b : V}
    (hb : S.IsHomogeneous b)
    (hOp : ∀ n : ℤ, IsHomogeneousOpOn S (VertexOp.component Y n a) (S.wt a - n - 1))
    (hW : ∀ k : ℤ, k < 0 → S.W k = ⊥) :
    ∃ N : ℕ, ∀ (m n : ℤ) (i : ℕ), N ≤ i → bracketTerm Y a b m n i = 0 := by
  refine ⟨(S.wt a + S.wt b).toNat, fun m n i hi => ?_⟩
  have hz : VertexOp.component Y (i : ℤ) a b = 0 :=
    component_eq_zero_of_toNat_le_on S Y hb hOp hW i hi
  rw [bracketTerm, hz, map_zero, smul_zero]

/-- **FLM Corollary 8.5.4, the finiteness parenthetical, `ℤ`-indexed and uniform in `(m,n)`**: under
the repaired (8.5.22) for every homogeneous state, the state `ι(a)_i·ι(b)` vanishes for all `i` past a
window that depends only on `(a,b)`.  Both `a` and `b` are decomposed into finitely many graded parts
(`WeightGrading.exists_sum_graded`), so neither needs to be homogeneous; the window is the maximum of
`j + l` over the weights `j` of `a`'s decomposition and `l` of `b`'s. -/
theorem exists_component_vanishing_uniform (S : WeightGrading F V) (Y : VertexOp F V) {a b : V}
    (hOm : ∀ u : V, S.IsHomogeneous u →
      ∀ n : ℤ, IsHomogeneousOpOn S (VertexOp.component Y n u) (S.wt u - n - 1))
    (hW : ∀ k : ℤ, k < 0 → S.W k = ⊥) :
    ∃ N : ℕ, ∀ i : ℤ, (N : ℤ) ≤ i → VertexOp.component Y i a b = 0 := by
  classical
  obtain ⟨s, c, hc, hsum⟩ := S.exists_sum_graded a
  obtain ⟨t, d, hd, hsumd⟩ := S.exists_sum_graded b
  refine ⟨(((∑ j ∈ s, max j 0) + ∑ l ∈ t, max l 0)).toNat, fun i hi => ?_⟩
  have hK : (∑ j ∈ s, max j 0) + ∑ l ∈ t, max l 0 ≤ i := by
    have h1 : (∑ j ∈ s, max j 0) + ∑ l ∈ t, max l 0
        ≤ ((((∑ j ∈ s, max j 0) + ∑ l ∈ t, max l 0).toNat : ℕ) : ℤ) := Int.self_le_toNat _
    omega
  have hsplit : VertexOp.component Y i a = ∑ j ∈ s, VertexOp.component Y i (c j) := by
    rw [hsum, map_sum]
  rw [hsplit, LinearMap.sum_apply]
  refine Finset.sum_eq_zero fun j hj => ?_
  have hsplitb : VertexOp.component Y i (c j) b
      = ∑ l ∈ t, VertexOp.component Y i (c j) (d l) := by
    rw [hsumd, map_sum]
  rw [hsplitb]
  refine Finset.sum_eq_zero fun l hl => ?_
  by_cases hzj : c j = 0
  · simp [hzj]
  by_cases hzl : d l = 0
  · simp [hzl]
  by_contra hne
  obtain ⟨hh, hwt⟩ := hOm (c j) ⟨j, hc j hj⟩ i (d l) ⟨l, hd l hl⟩ hne
  obtain ⟨k, hk⟩ := hh
  have hwt' : S.wt (VertexOp.component Y i (c j) (d l)) = j + l - i - 1 := by
    rw [hwt, S.wt_eq_of_mem (hc j hj) hzj, S.wt_eq_of_mem (hd l hl) hzl]
    ring
  have hk_eq : k = j + l - i - 1 := by
    rw [← S.wt_eq_of_mem hk hne, hwt']
  have hjle : j ≤ ∑ j' ∈ s, max j' 0 :=
    le_trans (le_max_left j 0) (Finset.single_le_sum (fun k _ => le_max_right k 0) hj)
  have hlle : l ≤ ∑ l' ∈ t, max l' 0 :=
    le_trans (le_max_left l 0) (Finset.single_le_sum (fun k _ => le_max_right k 0) hl)
  have hkneg : k < 0 := by omega
  rw [hW k hkneg, Submodule.mem_bot] at hk
  exact hne hk

/-- **FLM Corollary 8.5.4, the finiteness parenthetical** from the repaired (8.5.22) for every
homogeneous state: the summands of (8.5.26) vanish from one window on, uniformly in `(m,n)`.  The
hypothesis `hb` is *not* consumed (the engine decomposes `b` as well); it is retained so that this is
the exact `IsHomogeneousOpOn`-analogue of the brief's statement. -/
theorem bracketTerm_vanishing_of_gradingOn_uniform (S : WeightGrading F V) (Y : VertexOp F V) {a b : V}
    (hOm : ∀ u : V, S.IsHomogeneous u →
      ∀ n : ℤ, IsHomogeneousOpOn S (VertexOp.component Y n u) (S.wt u - n - 1))
    (hb : S.IsHomogeneous b) (hW : ∀ k : ℤ, k < 0 → S.W k = ⊥) :
    ∃ N : ℕ, ∀ (m n : ℤ) (i : ℕ), N ≤ i → bracketTerm Y a b m n i = 0 := by
  obtain ⟨N, hN⟩ := exists_component_vanishing_uniform S Y hOm hW (a := a) (b := b)
  exact ⟨N, fun m n i hi => by
    have hz : VertexOp.component Y (i : ℤ) a b = 0 := hN (i : ℤ) (by exact_mod_cast hi)
    rw [bracketTerm, hz, map_zero, smul_zero]⟩

/-- **FLM (8.5.26): the summands of Corollary 8.5.4 vanish from a window that is uniform in `(m,n)`.**
This is the brief's interface statement, verbatim.  Its hypothesis `hOm` is refutable
(`not_forall_isHomogeneousOp`), so the theorem is vacuous; the non-vacuous statement is
`bracketTerm_vanishing_of_gradingOn_uniform` above, and the axiom-level theorem is
`exists_uniform_bracketTerm_vanishing` in §3.  `hgrad` is not needed: it is a consequence of `hOm` and
`hb` (`hgrad_of_hOm`). -/
theorem bracketTerm_vanishing_of_grading_uniform
    (S : WeightGrading F V) (Y : VertexOp F V) {a b : V}
    (hOm : ∀ u : V, S.IsHomogeneous u →
      ∀ n : ℤ, S.IsHomogeneousOp (VertexOp.component Y n u) (S.wt u - n - 1))
    (hgrad : ∀ u : V, S.IsHomogeneous u → ∀ n : ℤ, S.IsHomogeneous (VertexOp.component Y n u b))
    (hb : S.IsHomogeneous b)
    (hW : ∀ k : ℤ, k < 0 → S.W k = ⊥) :
    ∃ N : ℕ, ∀ (m n : ℤ) (i : ℕ), N ≤ i → bracketTerm Y a b m n i = 0 :=
  bracketTerm_vanishing_of_gradingOn_uniform S Y
    (fun u hu n => IsHomogeneousOp.isHomogeneousOpOn (hOm u hu n)) hb hW

/-- The hypothesis `hgrad` of `bracketTerm_vanishing_of_grading_uniform` is redundant: it is the first
conjunct of `hOm u hu n` applied to `b`. -/
theorem hgrad_of_hOm (S : WeightGrading F V) (Y : VertexOp F V) {b : V}
    (hOm : ∀ u : V, S.IsHomogeneous u →
      ∀ n : ℤ, S.IsHomogeneousOp (VertexOp.component Y n u) (S.wt u - n - 1))
    (hb : S.IsHomogeneous b) :
    ∀ u : V, S.IsHomogeneous u → ∀ n : ℤ, S.IsHomogeneous (VertexOp.component Y n u b) :=
  fun u hu n => (hOm u hu n b hb).1

/-! ## §3. The axiom-level vanishing (outcome (1a)): FLM (8.10.5) is the parenthetical

The source's parenthetical is `ι(a)_i·ι(b) = 0` for `i` large, i.e. `component Y i a b = 0` for `i`
large **as a vector**.  That is verbatim the axiom (8.10.5) `u_n v = 0 for n sufficiently large`
(`MM.FLM810.ComponentTruncation`) at the *pair* `(u,v) = (a,b)` -- no grading, no (8.5.22), no
homogeneity.  The passage from the *state* vanishing to the summands of (8.5.26) is linearity of the
outer component in the state, which is `MM.FLM85.VertexOp.component`'s linearity. -/

/-- **FLM (8.10.5) is the finiteness parenthetical of Corollary 8.5.4**: for a landed
`VertexOperatorAlgebra`, the summands of (8.5.26) vanish from one window on, uniformly in `(m,n)`.
The only input is the axiom (8.10.5) at the pair `(a,b)`; the threshold is its own witness. -/
theorem exists_uniform_bracketTerm_vanishing (A : VertexOperatorAlgebra F V) (a b : V) :
    ∃ N : ℕ, ∀ (m n : ℤ) (i : ℕ), N ≤ i →
      bracketTerm (FLM85Ext.toVertexOp A.Y.coeff) a b m n i = 0 := by
  obtain ⟨N, hN⟩ := A.componentTruncation a b
  refine ⟨N.toNat, fun m n i hi => ?_⟩
  have hiN : N ≤ (i : ℤ) := by
    have h1 : N ≤ (N.toNat : ℤ) := Int.self_le_toNat N
    have h2 : (N.toNat : ℤ) ≤ (i : ℤ) := by exact_mod_cast hi
    omega
  have hz : VertexOp.component (FLM85Ext.toVertexOp A.Y.coeff) (i : ℤ) a b = 0 := by
    rw [VertexOp.component_apply]
    exact hN (i : ℤ) hiN
  rw [bracketTerm, hz, map_zero, smul_zero]

/-- The same, for an arbitrary field `Y` satisfying the truncation axiom (8.10.5) -- the form in which
a concrete field on `V_L` is consumed. -/
theorem exists_uniform_bracketTerm_vanishing_of_truncation (Y : V →ₗ[F] CoefFamily F V)
    (hT : ComponentTruncation (FLM85Ext.toVertexOp Y)) (a b : V) :
    ∃ N : ℕ, ∀ (m n : ℤ) (i : ℕ), N ≤ i →
      bracketTerm (FLM85Ext.toVertexOp Y) a b m n i = 0 := by
  obtain ⟨N, hN⟩ := hT a b
  refine ⟨N.toNat, fun m n i hi => ?_⟩
  have hiN : N ≤ (i : ℤ) := by
    have h1 : N ≤ (N.toNat : ℤ) := Int.self_le_toNat N
    have h2 : (N.toNat : ℤ) ≤ (i : ℤ) := by exact_mod_cast hi
    omega
  have hz : VertexOp.component (FLM85Ext.toVertexOp Y) (i : ℤ) a b = 0 := by
    rw [VertexOp.component_apply]
    exact hN (i : ℤ) hiN
  rw [bracketTerm, hz, map_zero, smul_zero]

/-- The same with the normalization `1 ≤ N` that `MM.FLM88.corollary851_of_jacobiIdentity` needs of
its window (it is weakened there anyway by enlarging the window). -/
theorem exists_uniform_bracketTerm_vanishing_one_le (Y : V →ₗ[F] CoefFamily F V)
    (hT : ComponentTruncation (FLM85Ext.toVertexOp Y)) (a b : V) :
    ∃ N : ℕ, 1 ≤ N ∧ ∀ (m n : ℤ) (i : ℕ), N ≤ i →
      bracketTerm (FLM85Ext.toVertexOp Y) a b m n i = 0 := by
  obtain ⟨N, hN⟩ := exists_uniform_bracketTerm_vanishing_of_truncation Y hT a b
  exact ⟨max N 1, le_max_right N 1,
    fun m n i hi => hN m n i (le_trans (le_max_left N 1) hi)⟩

/-! ## §4. The `ℤ`-indexed iterate form (outcome (2)) and its implication to (1) -/

/-- **FLM Corollary 8.5.4, the finiteness parenthetical read on the iterate**: from (8.10.5), the whole
family `(ι(a)_i·ι(b))_j` (`j ∈ ℤ`) vanishes for `i` past a window, i.e. `iterateOf Y a b i = 0` as a
function of `j`.  This is the source's `ι(a)_i·ι(b) = 0` for `i` sufficiently large. -/
theorem exists_iterate_uniform_vanishing (Y : V →ₗ[F] CoefFamily F V)
    (hT : ComponentTruncation (FLM85Ext.toVertexOp Y)) (a b : V) :
    ∃ K : ℕ, ∀ i : ℤ, (K : ℤ) ≤ i → iterateOf Y a b i = 0 := by
  obtain ⟨N, hN⟩ := hT a b
  refine ⟨N.toNat, fun i hi => ?_⟩
  have hiN : N ≤ i := by
    have h1 : N ≤ (N.toNat : ℤ) := Int.self_le_toNat N
    have h2 : (N.toNat : ℤ) ≤ i := by exact_mod_cast hi
    omega
  have hz : (Y a) i b = 0 := hN i hiN
  funext j
  show Y ((Y a) i b) j = 0
  rw [hz, map_zero]
  rfl

/-- **FLM (8.5.26)**: `bracketTerm` is the binomial times the `(m+n−i)`-th iterate component -- the
landed `MM.FLM85Ex.iterateSummand_eq_bracketTerm` read at the definitional unfolding (the numbering of
the summand is the same on both sides). -/
theorem bracketTerm_eq_binomCoeff_smul_iterateOf (Y : VertexOp F V) (a b : V) (m n : ℤ) (i : ℕ) :
    bracketTerm Y a b m n i =
      binomCoeff (F := F) m i • iterateOf Y.coeff a b (i : ℤ) (m + n - (i : ℤ)) := rfl

/-- **(2) implies (1)**: a uniform window for the iterate family is a uniform window for the summands
of (8.5.26), in the exact form `MM.FLM88.corollary851_of_jacobiIdentity` consumes. -/
theorem bracketTerm_vanishing_of_iterate_uniform (Y : VertexOp F V) {a b : V} {K : ℕ}
    (h : ∀ i : ℤ, (K : ℤ) ≤ i → iterateOf Y.coeff a b i = 0) :
    ∀ (m n : ℤ) (i : ℕ), K ≤ i → bracketTerm Y a b m n i = 0 := by
  intro m n i hi
  have hi' : (K : ℤ) ≤ (i : ℤ) := by exact_mod_cast hi
  have h0 : iterateOf Y.coeff a b (i : ℤ) (m + n - (i : ℤ)) = 0 :=
    (congrFun (h (i : ℤ) hi') (m + n - (i : ℤ))).trans (Pi.zero_apply _)
  rw [bracketTerm_eq_binomCoeff_smul_iterateOf, h0, smul_zero]

end FLM86UV

end MM
