/-
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, task B152-W2)

FLM Theorem 8.6.1, display (8.6.3) (printed p. 205), from the Section 8.10 Jacobi axiom.

**Proved.**  `MM.FLM86TDA.Display863 form E Y u' v' a b K` — the landed display, i.e. the identity of
the two-variable operator families `displayLeft863 = displayRight863` at the states of (8.6.2), under
(8.6.1), at the window `K` — follows from exactly two inputs:

* `hJ : MM.FLM810JF.FaithfulJacobi Y u v`, the faithful (8.10.8): the `jacobi` field of a landed
  `MM.FLM810.VertexOperatorAlgebra` at its own `Y` (`display863_of_voa_self`), transported to a named
  `Y` against `A.Y.coeff = Y` (`display863_of_voa`);
* `hvan : UniformBracketWindow Y u v`, the source's parenthetical "`ι(a)_i·ι(b) = 0` for `i`
  sufficiently large" (p. 201), **uniform in `(m,n)`**: one `N ≥ 1` with
  `bracketTerm (toVertexOp Y) u v m n i = 0` for `N ≤ i` and all `m, n`.

The route is the landed reduction, not a re-derivation: `display863_iff_residue863` (at `1 ≤ K`) turns
the display into the `Res_{z₀}` face `Residue863`, which is the `l = 0` face of (8.8.41);
`residue863_of_faithfulJacobi` proves that face from `FaithfulJacobi` + `hvan`, using `hvan` only to
*pin* the axiom's per-monomial, per-element window (at `l = 0` the cross side is the window-independent
commutator family, and the iterate side has stopped at `N`).

**Not proved, and not claimed.**  (i) `UniformBracketWindow` is not derived here from the abstract
carrier: `uniformBracketWindow_of_weight`/`_of_grading` record the landed implication from (8.5.22)
(`IsHomogeneousOp`, a statement about the concrete Fock space) and §7.1 nonnegativity.  The lattice
weight of `stateOf u' a` for `u' ≠ 1` is the unproved `MM.FLMLatSt.StateWeightStatement`, assumed
nowhere here.  (ii) The uniform `MM.FLM88.JacobiIdentity Y u v N` — one window for *all* monomials,
operator-valued — is **not** obtained from `A.jacobi`, and is not needed: the display is the `l = 0`
face only.  (iii) `A.jacobi` transports to a named `Y` only against agreement on *all* states, because
both `FaithfulJacobi` and the display's right-hand side mention the operator at the iterate states
`u_s · v` (`MM.FLM88.iterateComponent`); agreement at the two states `u`, `v` alone does **not**
suffice, and no theorem here claims it — hence `hY : A.Y.coeff = Y` in `display863_of_voa`.
(iv) The display holds at `hvan`'s window `N` and at every `K ≥ N`; at `K < N` it is a different,
smaller sum and is not derived.

**The assembly form.**  `display863_of_remainingFields` states the display at the boundary of
`MM.FLM810CA.theorem8102_of_remainingFields`; the display half consumes only the `JacobiAxiom` conjunct
of the four `MM.FLM810AFT.ActionRemainingFields` conjuncts (see that section's header).
-/

import Definitions.MMFLM86TheoremDisplay
import Definitions.MMFLM810JacobiFaithful
import Definitions.MMFLM810CorrectedAssembly

set_option autoImplicit false

noncomputable section

namespace MM

namespace FLM86DVS

variable {F : Type*} [Field F]
variable {L : Type*} [AddCommGroup L]

/-! ## (A) The finiteness interface: the uniform window -/

/-- The finiteness input of FLM Corollary 8.5.4 for the states of Theorem 8.6.1, in the exact form
`MM.FLM88.corollary851_of_jacobiIdentity` consumes: a window uniform in `(m,n)`. -/
def UniformBracketWindow (Y : FLM86SG.Op861 F L) (u v : FLM86SG.VL F L) : Prop :=
  ∃ N : ℕ, 1 ≤ N ∧ ∀ (m n : ℤ) (i : ℕ),
    N ≤ i → FLM85Br.bracketTerm (FLM85Ext.toVertexOp Y) u v m n i = 0

/-- **The uniform window from the grading**: the landed `MM.FLM85Br.bracketTerm_vanishing_of_grading`
is *already* uniform in `(m,n)` — its window is `(wt u + wt v).toNat` — and is enlarged here to
`max 1 _` so that the consumers, all of which need a nonempty window, can take it.  The hypotheses are
the source's own: (8.5.22) for the state `u` (`IsHomogeneousOp`, `deg u_n = n − wt u + 1`) and the
vanishing of the negative weight pieces (FLM §7.1, (8.10.3)). -/
theorem uniformBracketWindow_of_weight {V : Type*} [AddCommGroup V] [Module F V]
    (S : FLM85.WeightGrading F V) (Y : FLM85.VertexOp F V) {u v : V}
    (hv : S.IsHomogeneous v)
    (hOp : ∀ n : ℤ, S.IsHomogeneousOp (Y.component n u) (S.wt u - n - 1))
    (hW : ∀ k : ℤ, k < 0 → S.W k = ⊥) :
    ∃ N : ℕ, 1 ≤ N ∧ ∀ (m n : ℤ) (i : ℕ), N ≤ i → FLM85Br.bracketTerm Y u v m n i = 0 :=
  ⟨max 1 (S.wt u + S.wt v).toNat, le_max_left _ _,
    fun m n i hi => FLM85Br.bracketTerm_vanishing_of_grading S Y hv hOp hW m n i
      (le_trans (le_max_right _ _) hi)⟩

/-- The same on the display's own carrier: `UniformBracketWindow` *is* the conclusion of
`uniformBracketWindow_of_weight` at `Y := toVertexOp Y`, so a caller holding (8.5.22) for the states
`u = stateOf u' a`, `v = stateOf v' b` has this file's finiteness input outright. -/
theorem uniformBracketWindow_of_grading (S : FLM85.WeightGrading F (FLM86SG.VL F L))
    (Y : FLM86SG.Op861 F L) {u v : FLM86SG.VL F L}
    (hv : S.IsHomogeneous v)
    (hOp : ∀ n : ℤ, S.IsHomogeneousOp
      (FLM85.VertexOp.component (FLM85Ext.toVertexOp Y) n u) (S.wt u - n - 1))
    (hW : ∀ k : ℤ, k < 0 → S.W k = ⊥) :
    UniformBracketWindow Y u v :=
  uniformBracketWindow_of_weight S (FLM85Ext.toVertexOp Y) hv hOp hW

/-! ## (B) The display from the faithful (8.10.8) and the uniform window -/

/-- **The `Res_{z₀}` face of the Jacobi identity at the window of `hvan`.**  `FaithfulJacobi` is the
landed per-monomial, per-element reading of (8.10.8); at the monomial `(l,m,n) = (0,m,n)` and the
element `w` it gives a window `N₀` past which both sums have stopped and at which they agree.  Taking
the identity at `max N₀ N` and moving both sides to `N` is legitimate because of `hvan`: the cross side
at `l = 0` is the window-independent commutator family
(`MM.FLM88.crossBracket_zero_eq_commutatorFamily`, at any window `≥ 1`), and the iterate side has
stopped at `N` (`MM.FLM85Br.bracketSum_eq_of_forall_eq_zero` through
`MM.FLM88.crossIterate_zero_eq_bracketSum`).  The result is operator-valued (`LinearMap.ext` on `w`)
and is exactly the hypothesis `MM.FLM86TDA.Residue863` names. -/
theorem residue863_of_faithfulJacobi
    (Y : FLM86SG.Op861 F L) (u' v' : FLMFock.M1 F L) (a b : L)
    (hJ : FLM810JF.FaithfulJacobi Y (FLM86.stateOf (F := F) u' a)
      (FLM86.stateOf (F := F) v' b))
    {N : ℕ} (hN : 1 ≤ N)
    (hvan : ∀ (m n : ℤ) (i : ℕ), N ≤ i →
      FLM85Br.bracketTerm (FLM85Ext.toVertexOp Y) (FLM86.stateOf (F := F) u' a)
        (FLM86.stateOf (F := F) v' b) m n i = 0) :
    FLM86TDA.Residue863 Y u' v' a b N := by
  intro m n
  refine LinearMap.ext fun w => ?_
  obtain ⟨N₀, _hC, hid⟩ :=
    (FLM810JF.faithfulJacobi_iff_stable Y _ _).mp hJ (0 : ℤ) m n w
  have hle := hid (max N₀ N) (le_max_left _ _)
  rw [FLM88.crossBracket_zero_eq_commutatorFamily Y _ _ (show 1 ≤ max N₀ N by omega) m n,
    FLM88.crossIterate_zero_eq_bracketSum,
    FLM85Br.bracketSum_eq_of_forall_eq_zero (FLM85Ext.toVertexOp Y) _ _ (hvan m n)
      (max N₀ N) (le_max_right _ _),
    ← FLM88.crossIterate_zero_eq_bracketSum,
    ← FLM88.crossBracket_zero_eq_commutatorFamily Y _ _ hN m n] at hle
  exact hle

/-- **The display at a window past the finiteness window.**  With the uniform vanishing at `N`
(`hvanN`), the display holds at every `K ≥ N`: apply `MM.FLM86TDA.display863_iff_residue863` and
`residue863_of_faithfulJacobi` at `K`, the vanishing at `N` giving it at every larger window. -/
theorem display863_of_faithfulJacobi_at
    (form : L →ₗ[ℤ] L →ₗ[ℤ] ℤ) (E : FLMLattice.CentralExtension F L)
    (Y : FLM86SG.Op861 F L) (u' v' : FLMFock.M1 F L) (a b : L)
    (hJ : FLM810JF.FaithfulJacobi Y (FLM86.stateOf (F := F) u' a)
      (FLM86.stateOf (F := F) v' b))
    {N K : ℕ} (hN : 1 ≤ N)
    (hvanN : ∀ (m n : ℤ) (i : ℕ), N ≤ i →
      FLM85Br.bracketTerm (FLM85Ext.toVertexOp Y) (FLM86.stateOf (F := F) u' a)
        (FLM86.stateOf (F := F) v' b) m n i = 0)
    (hNK : N ≤ K) :
    FLM86TDA.Display863 form E Y u' v' a b K :=
  (FLM86TDA.display863_iff_residue863 form E Y u' v' a b (le_trans hN hNK)).mpr
    (fun _ => residue863_of_faithfulJacobi Y u' v' a b hJ (le_trans hN hNK)
      (fun m n i hi => hvanN m n i (le_trans hNK hi)))

/-- **FLM Theorem 8.6.1, display (8.6.3), from the faithful (8.10.8) plus the uniform finiteness
window** — the display with its two inputs explicit, at the window `hvan` supplies. -/
theorem display863_of_faithfulJacobi
    (form : L →ₗ[ℤ] L →ₗ[ℤ] ℤ) (E : FLMLattice.CentralExtension F L)
    (Y : FLM86SG.Op861 F L) (u' v' : FLMFock.M1 F L) (a b : L)
    (hJ : FLM810JF.FaithfulJacobi Y (FLM86.stateOf (F := F) u' a)
      (FLM86.stateOf (F := F) v' b))
    (hvan : UniformBracketWindow Y (FLM86.stateOf (F := F) u' a)
      (FLM86.stateOf (F := F) v' b)) :
    ∃ K : ℕ, 1 ≤ K ∧ FLM86TDA.Display863 form E Y u' v' a b K := by
  obtain ⟨N, hN, hvanN⟩ := hvan
  exact ⟨N, hN, display863_of_faithfulJacobi_at form E Y u' v' a b hJ hN hvanN (le_refl N)⟩

/-- **The display for the structure's own operator.**  No transport hypothesis occurs: the `jacobi`
field is the faithful (8.10.8) for `A.Y.coeff` itself, and the display's right-hand side is evaluated
at the iterate states of that same operator.  This is how the Section 8.10 assembly feeds the display,
since `MM.FLM810.Theorem8102Conclusion` existentially quantifies its witness and cannot name its
`Y`. -/
theorem display863_of_voa_self
    (form : L →ₗ[ℤ] L →ₗ[ℤ] ℤ) (E : FLMLattice.CentralExtension F L)
    (A : FLM810.VertexOperatorAlgebra F (FLM86SG.VL F L))
    (u' v' : FLMFock.M1 F L) (a b : L)
    (hvan : UniformBracketWindow A.Y.coeff (FLM86.stateOf (F := F) u' a)
      (FLM86.stateOf (F := F) v' b)) :
    ∃ K : ℕ, 1 ≤ K ∧ FLM86TDA.Display863 form E A.Y.coeff u' v' a b K :=
  display863_of_faithfulJacobi form E A.Y.coeff u' v' a b
    (A.jacobi (FLM86.stateOf (F := F) u' a) (FLM86.stateOf (F := F) v' b)) hvan

/-- **FLM Theorem 8.6.1, display (8.6.3), from a landed Section 8.10 structure `A`** whose field is a
*named* `Y` (`hY : A.Y.coeff = Y`), together with the uniform finiteness window.

The hypothesis `hY` is not decoration: `FaithfulJacobi A.Y.coeff u v` — the `jacobi` field — mentions
`A.Y.coeff` at the states `u`, `v` and at every iterate `u_s · v` (`MM.FLM88.iterateComponent`), and so
does the display's right-hand side.  Agreement of `A.Y.coeff` with `Y` at the two states `u`, `v` alone
does **not** transport the axiom, and no theorem in this file claims it; `display863_of_voa_self` is the
transport-free form.  `hvac` and `hW` are carried so that `A` is visibly the landed structure on `V_L`
with the landed vacuum and the landed grading (7.1.40); the display does not consume them. -/
theorem display863_of_voa
    (form : L →ₗ[ℤ] L →ₗ[ℤ] ℤ) (E : FLMLattice.CentralExtension F L)
    (A : FLM810.VertexOperatorAlgebra F (FLM86SG.VL F L))
    (hvac : A.vacuum = FLMLattice.vacuumVL)
    (hW : ∀ k : ℤ, A.grading.W k = FLMLattice.weightPiece (F := F) form (k : ℚ))
    (Y : FLM86SG.Op861 F L) (hY : A.Y.coeff = Y)
    (u' v' : FLMFock.M1 F L) (a b : L)
    (hvan : UniformBracketWindow Y (FLM86.stateOf (F := F) u' a)
      (FLM86.stateOf (F := F) v' b)) :
    ∃ K : ℕ, 1 ≤ K ∧ FLM86TDA.Display863 form E Y u' v' a b K := by
  have _hvac := hvac
  have _hW := hW
  exact display863_of_faithfulJacobi form E Y u' v' a b
    (hY ▸ A.jacobi (FLM86.stateOf (F := F) u' a) (FLM86.stateOf (F := F) v' b)) hvan

/-! ## (C) The Section 8.10 assembly form

`MM.FLM810CA.theorem8102_of_remainingFields` is the verified assembly boundary: the four remaining
conformal/Jacobi fields (`MM.FLM810AFT.ActionRemainingFields`) for the action prescription of (8.5.5)
produce `MM.FLM810.Theorem8102Conclusion form r` — the structure `A` on `V_L` with the landed vacuum,
the landed grading and the Virasoro axioms.  Two structural points, both measured:

* The assembly's witness `A` is **existentially quantified** (`theorem8102_of_fields` is applied inside
  `theorem8102_of_actionHrel` to a `Y` obtained from `existsUnique_actionPrescriptionTA_...`), so the
  `Y` it was built from cannot be named.  The display is therefore stated for the *named*
  action-prescription family `Yfield` and its re-indexed component operator
  `(FLM810F.vertexOpOfField Yfield).coeff` — the (8.5.15) dictionary `n ↦ −n−1` between the
  power-indexed field of (8.10.4) and the component-indexed operator the display uses.  The assembly
  conclusion is recorded as the first component of the conjunction.
* The display half consumes **only** the `JacobiAxiom` conjunct of `hrem Yfield hYid`, and **none** of
  `hpd`, `heven`, `hrank`, `hW`, `hfin`; those five are consumed by the assembly half.  The spanning
  input (Remark 8.3.9) and FLM's coefficient extraction (8.6.5)--(8.6.27) are consumed nowhere. -/

section Assembly

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

/-- **FLM Theorem 8.6.1, display (8.6.3), at the Section 8.10 assembly boundary.**  The hypotheses are
those of `MM.FLM810CA.theorem8102_of_remainingFields` (`bL`, `form`, `E`, `weight`, `S`, `om`, `r`,
`hpd`, `hrank`, `hW`, `hfin`, `hrem`), the evenness `heven` of FLM's "positive definite **even**
lattice" hypothesis of Theorem 8.10.2, the identification `hYid` of the named field `Yfield` with the
action prescription of (8.5.5), and the uniform window `hvan` for `Yfield`'s component operator.  The
conclusion is the assembly's `Theorem8102Conclusion` **and** the display at that named operator. -/
theorem display863_of_remainingFields (bL : Module.Basis κ ℤ L) (form : L →ₗ[ℤ] L →ₗ[ℤ] ℤ)
    (E : FLMLattice.CentralExtension F L) (weight : ℤ)
    (S : FLM85.WeightGrading F (FLM86SG.VL F L)) (om : FLM86SG.VL F L) (r : ℚ)
    (hpd : FLM810.PositiveDefinite form) (heven : ∀ a : L, 2 ∣ form a a)
    (hrank : FLM810.RankStatement (L := L) r)
    (hW : ∀ k : ℤ, S.W k = FLMLattice.weightPiece (F := F) form (k : ℚ))
    (hfin : FLMLattice.WeightPiecesFinite (F := F) (L := L) form)
    (hrem : ∀ Yfield : FLM86SG.VL F L →ₗ[F] FLM85.CoefFamily F (FLM86SG.VL F L),
      (∀ D : FLM85Un.StateDatum L,
        Yfield (FLM85Un.stateOfVL (F := F) bL form D) =
          (FLM85AP.actionPrescriptionTA (F := F) bL form
            (FLM85TAV.modelBaseField (F := F) bL form E weight) D).fam) →
      FLM810AFT.ActionRemainingFields (F := F) (L := L) S om r (FLM810F.vertexOpOfField Yfield))
    (Yfield : FLM86SG.VL F L →ₗ[F] FLM85.CoefFamily F (FLM86SG.VL F L))
    (hYid : ∀ D : FLM85Un.StateDatum L,
      Yfield (FLM85Un.stateOfVL (F := F) bL form D) =
        (FLM85AP.actionPrescriptionTA (F := F) bL form
          (FLM85TAV.modelBaseField (F := F) bL form E weight) D).fam)
    (u' v' : FLMFock.M1 F L) (a b : L)
    (hvan : UniformBracketWindow (FLM810F.vertexOpOfField Yfield).coeff
      (FLM86.stateOf (F := F) u' a) (FLM86.stateOf (F := F) v' b)) :
    FLM810.Theorem8102Conclusion (F := F) (L := L) form r ∧
      ∃ K : ℕ, 1 ≤ K ∧ FLM86TDA.Display863 form E (FLM810F.vertexOpOfField Yfield).coeff
        u' v' a b K := by
  refine ⟨?_, display863_of_faithfulJacobi form E (FLM810F.vertexOpOfField Yfield).coeff u' v' a b
    ((hrem Yfield hYid).1 (FLM86.stateOf (F := F) u' a) (FLM86.stateOf (F := F) v' b)) hvan⟩
  exact ((FLM810CA.theorem8102_of_remainingFields (F := F) bL form E weight S om r hpd hrank hW
    hfin hrem) ⟨hpd, heven⟩ two_ne_zero).2

end Assembly

/-! ## Axiom footprints

Every message below is the **measured** printed form from the build of this file; `#guard_msgs` fails
the build if a footprint changes.  All nine declarations come out with the full
`[propext, Classical.choice, Quot.sound]` (none warns, none mentions `sorryAx`), and each fits on one
printed line (< 120 characters). -/

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

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

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

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

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

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

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

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

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

end FLM86DVS

end MM
