Chapter BookBrstGaugeFixing

import Definitions.Def_ChapterBookBrstYangMills
import Definitions.Def_ChapterBRSTNilpotent
import Definitions.Def_ChapterQuantumGravityBrstCharge
import Mathlib
import Theorems.Thm_BookProof_BookBrstYangMills_bookOmega_nilpotent
import Theorems.Thm_BookProof_BRSTNilpotent_beta_move
import Theorems.Thm_BookProof_BookBrstYangMills_bookGhostCar
import Theorems.Thm_BookProof_BookBrstYangMills_Afield_comm_chi
import Theorems.Thm_BookProof_BookBrstYangMills_bosOpN_ghostOpN_comm
import Theorems.Thm_BookProof_BookBrstYangMills_bookConstraintAlgebra
import Theorems.Thm_BookProof_BookBrstYangMills_bookOmega_eq_brstCharge
import Theorems.Thm_BookProof_BookBrstYangMills_bosOpN_mul


/-!
# The gauge-fixing fermion of `book.tex` and the gauge-fixing term it generates

`book.tex`, §*"Pure SU(3) Yang-Mills theory"* (line ~7347), adds to the Hamiltonian the
BRST-exact term generated by the **gauge-fixing fermion** `Ψ = i ψ_a A_{0a}`,

```
{Ω, i ψ_a A_{0a}} ,
```

and uses it to pass from the four-dimensional Hamiltonian to the Weyl-gauge Hamiltonian.
This module builds that construction for the BRST charge of
`BookProof.ChapterBookBrstYangMills`.

## What is proved

* `brstCharge_gf_anticomm` — the anticommutator of the abstract BRST charge
  `Ω = Σ_a 𝒢_a χ_a − ½ Σ f_{abe} χ_a χ_b β_e` with a **gauge-fixing fermion**
  `Ψ = Σ_d β_d B_d` built from bosonic operators `B_d`:

  ```
  {Ω, Ψ} = Σ_c 𝒢_c B_c − Σ_{c,d} [𝒢_c, B_d] β_d χ_c − Σ_{a,b,c} f_{abc} B_a χ_b β_c .
  ```

  The first term is the Gauss law contracted with the gauge-fixing field — in the book's
  application the term that cancels `π^μ_a (D_μ A_0)_a` in the Hamiltonian — the second is
  the ghost kinetic term and the third the non-abelian ghost–field coupling.
* `bookGfTerm_eq` — the same identity for the book's charge and the book's gauge-fixing
  fermion `Ψ = i ψ_a A_{0a}` on the graded state space, with `[𝒢_c, A_{0d}]` evaluated as
  multiplication by the gauge variation of the coordinate `A_{0d}`.
* `bookGfTerm_brst_closed` — the generated term is BRST invariant, `Ω {Ω,Ψ} = {Ω,Ψ} Ω`,
  because `Ω² = 0`; this is why the book may add it to the Hamiltonian without changing the
  BRST cohomology.
* **Accounting identity (temporal/Weyl gauge `A₀ = 0`)** —
  `bookGfFermion_eq_zero_of_Afield0` and `bookGfTerm_eq_zero_of_Afield0`: when every
  temporal component vanishes, `Ψ = i ψ_a A_{0a}` and hence `{Ω, Ψ}` are identically zero.
  The BRST-exact gauge-fixing/ghost contribution therefore adds **no new term** to the
  gauge-fixed Hamiltonian `h` and **no new summand** to the comparison operator `N`: the
  accounting of `h` and `N` is already complete without it.  For pure Yang–Mills (QYM) the
  same identity holds for the `su(2)`/`su(3)` instances — the Weyl gauge may work with the
  spatial components only.  For quantum gravity (QG) the book's 3D reduction is **not** the
  ADM one (`book.tex` ~8226–8244): it fixes the globally defined time-like vector
  `v^μ = δ^μ_0`, the ghosts of the resulting charge are **constant in the timepiece**, and
  the charge keeps the **same functional form as the 4D formalism** — explicitly different
  from the ADM BRST charge, whose approximation the book rejects as insufficient.

* `exactStates_le_physicalStates` — nilpotency makes the BRST cohomology
  `brstCohomology = ker Ω / im Ω` of the book's charge well defined, and
  `bookGfTerm_mem_physicalStates` / `bookGfTerm_mem_exactStates` show that the gauge-fixing
  term preserves both the physical and the exact states.  No claim is made about the
  dimension of the cohomology.

* `brstCharge_comm_of_comm` / `bookOmega_comm_multOp` — a **gauge-invariant observable**
  (one commuting with all the constraints and with the ghosts) commutes with the BRST charge,
  so it preserves the physical and the exact states; `casimir_bookOmega_comm` exhibits the
  quadratic invariant `Σ_{μ,a} A_{μa}A_{μa}` as such an observable for the constant
  gauge-field algebra.

Everything is `sorry`-free and `axiom`-free.
-/

namespace BookProof.BookBrstGaugeFixing

open BookProof.BRSTNilpotent BookProof.QuantumGravityBrstCharge BookProof.BookBrstYangMills
open MvPolynomial

noncomputable section

/-! ## 1. The abstract gauge-fixing anticommutator -/

section Abstract

variable {R : Type*} [Ring R] [Algebra ℝ R] {n : ℕ}
variable {f : Fin n → Fin n → Fin n → ℝ} {Gc χ β B : Fin n → R}

/-- The **gauge-fixing fermion** `Ψ = Σ_d ψ_d B_d` attached to a family of bosonic
operators `B_d` (the book's `Ψ = ψ_a A_{0a}`). -/
def gfFermion (β B : Fin n → R) : R := ∑ d, β d * B d

omit [Algebra ℝ R] in
/-- The constraint part of the charge against the gauge-fixing fermion. -/
theorem glin_gf_anticomm (hCAR : GhostCAR χ β)
    (hGβ : ∀ a b, Gc a * β b = β b * Gc a)
    (hBχ : ∀ a b, B a * χ b = χ b * B a) (hBβ : ∀ a b, B a * β b = β b * B a) :
    glin Gc χ * gfFermion β B + gfFermion β B * glin Gc χ
      = (∑ c, Gc c * B c) - ∑ c, ∑ d, (Gc c * B d - B d * Gc c) * (β d * χ c) := by
  classical
  have hL : glin Gc χ * gfFermion β B = ∑ c, ∑ d, (Gc c * B d) * (χ c * β d) := by
    unfold glin gfFermion
    rw [Finset.sum_mul]
    refine Finset.sum_congr rfl fun c _ => ?_
    rw [Finset.mul_sum]
    refine Finset.sum_congr rfl fun d _ => ?_
    have h1 : χ c * (β d * B d) = B d * (χ c * β d) := by
      rw [← hBβ d d, ← mul_assoc, ← hBχ d c, mul_assoc]
    calc (Gc c * χ c) * (β d * B d) = Gc c * (χ c * (β d * B d)) := by rw [mul_assoc]
      _ = Gc c * (B d * (χ c * β d)) := by rw [h1]
      _ = (Gc c * B d) * (χ c * β d) := by rw [mul_assoc]
  have hR : gfFermion β B * glin Gc χ = ∑ c, ∑ d, (B d * Gc c) * (β d * χ c) := by
    unfold glin gfFermion
    rw [Finset.sum_mul]
    have hterm2 : ∀ c d : Fin n, (β d * B d) * (Gc c * χ c) = (B d * Gc c) * (β d * χ c) := by
      intro c d
      have h2 : β d * (B d * Gc c) = (B d * Gc c) * β d := by
        rw [← mul_assoc, ← hBβ d d, mul_assoc, ← hGβ c d, ← mul_assoc]
      calc (β d * B d) * (Gc c * χ c) = (β d * (B d * Gc c)) * χ c := by noncomm_ring
        _ = ((B d * Gc c) * β d) * χ c := by rw [h2]
        _ = (B d * Gc c) * (β d * χ c) := by noncomm_ring
    have hstep : ∀ d : Fin n, (β d * B d) * (∑ c, Gc c * χ c)
        = ∑ c, (B d * Gc c) * (β d * χ c) := by
      intro d
      rw [Finset.mul_sum]
      exact Finset.sum_congr rfl fun c _ => hterm2 c d
    rw [Finset.sum_congr rfl fun d _ => hstep d,
      Finset.sum_comm (f := fun d c => (B d * Gc c) * (β d * χ c))]
  have hterm : ∀ c d : Fin n,
      (Gc c * B d) * (χ c * β d) + (B d * Gc c) * (β d * χ c)
        = (if d = c then Gc c * B c else 0)
          - (Gc c * B d - B d * Gc c) * (β d * χ c) := by
    intro c d
    have hcar : β d * χ c + χ c * β d = if d = c then 1 else 0 := hCAR.betachi d c
    have hexp : (Gc c * B d) * (χ c * β d) + (B d * Gc c) * (β d * χ c)
        = (Gc c * B d) * (χ c * β d + β d * χ c)
          - (Gc c * B d - B d * Gc c) * (β d * χ c) := by noncomm_ring
    rw [hexp, add_comm (χ c * β d) (β d * χ c), hcar]
    by_cases h : d = c
    · subst h
      simp
    · simp [h]
  rw [hL, hR, ← Finset.sum_add_distrib]
  have hstep : ∀ c : Fin n,
      (∑ d, (Gc c * B d) * (χ c * β d)) + (∑ d, (B d * Gc c) * (β d * χ c))
        = (Gc c * B c) - ∑ d, (Gc c * B d - B d * Gc c) * (β d * χ c) := by
    intro c
    rw [← Finset.sum_add_distrib, Finset.sum_congr rfl fun d _ => hterm c d,
      Finset.sum_sub_distrib]
    simp
  rw [Finset.sum_congr rfl fun c _ => hstep c, Finset.sum_sub_distrib]

/-- The cubic ghost part of the charge against the gauge-fixing fermion. -/
theorem Q_gf_anticomm (hCAR : GhostCAR χ β) (hf12 : ∀ a b c, f a b c = -f b a c)
    (hBχ : ∀ a b, B a * χ b = χ b * B a) (hBβ : ∀ a b, B a * β b = β b * B a) :
    Q f χ β * gfFermion β B + gfFermion β B * Q f χ β
      = ∑ a, ∑ b, ∑ c, (2 * f a b c) • (B a * (χ b * β c)) := by
  classical
  have hghost : ∀ a b c d : Fin n,
      (χ a * χ b * β c) * β d + β d * (χ a * χ b * β c)
        = (if d = a then χ b * β c else 0) - (if d = b then χ a * β c else 0) := by
    intro a b c d
    have hmove := beta_move χ β hCAR d a b
    have hbb : β c * β d + β d * β c = 0 := hCAR.betabeta c d
    have h1 : β d * (χ a * χ b * β c) = (β d * (χ a * χ b)) * β c := by noncomm_ring
    rw [h1, hmove]
    have h2 : (χ a * χ b * β c) * β d
        + ((if d = a then χ b else 0) - (if d = b then χ a else 0) + χ a * χ b * β d) * β c
        = ((if d = a then χ b else 0) - (if d = b then χ a else 0)) * β c
          + (χ a * χ b) * (β c * β d + β d * β c) := by noncomm_ring
    rw [h2, hbb, mul_zero, add_zero]
    by_cases hda : d = a <;> by_cases hdb : d = b <;>
      simp [hda, hdb, sub_mul]
  have hQ : Q f χ β * gfFermion β B + gfFermion β B * Q f χ β
      = ∑ a, ∑ b, ∑ c, ∑ d, f a b c •
          (B d * ((if d = a then χ b * β c else 0) - (if d = b then χ a * β c else 0))) := by
    unfold Q gfFermion
    have hLterm : ∀ a b c d : Fin n,
        (f a b c • (χ a * χ b * β c)) * (β d * B d)
          = f a b c • (B d * ((χ a * χ b * β c) * β d)) := by
      intro a b c d
      have hcomm : (χ a * χ b * β c) * (β d * B d) = B d * ((χ a * χ b * β c) * β d) := by
        rw [← hBβ d d, ← mul_assoc]
        have e1 : β c * B d = B d * β c := (hBβ d c).symm
        have e2 : χ b * B d = B d * χ b := (hBχ d b).symm
        have e3 : χ a * B d = B d * χ a := (hBχ d a).symm
        have hb1 : (χ a * χ b * β c) * B d = B d * (χ a * χ b * β c) := by
          calc (χ a * χ b * β c) * B d = (χ a * χ b) * (β c * B d) := by noncomm_ring
            _ = (χ a * χ b) * (B d * β c) := by rw [e1]
            _ = χ a * (χ b * B d) * β c := by noncomm_ring
            _ = χ a * (B d * χ b) * β c := by rw [e2]
            _ = (χ a * B d) * (χ b * β c) := by noncomm_ring
            _ = (B d * χ a) * (χ b * β c) := by rw [e3]
            _ = B d * (χ a * χ b * β c) := by noncomm_ring
        rw [hb1, mul_assoc]
      rw [smul_mul_assoc, hcomm]
    have hRterm : ∀ a b c d : Fin n,
        (β d * B d) * (f a b c • (χ a * χ b * β c))
          = f a b c • (B d * (β d * (χ a * χ b * β c))) := by
      intro a b c d
      rw [mul_smul_comm]
      congr 1
      rw [← mul_assoc, ← hBβ d d]
      simp only [mul_assoc]
    have hL : (∑ a, ∑ b, ∑ c, f a b c • (χ a * χ b * β c)) * (∑ d, β d * B d)
        = ∑ a, ∑ b, ∑ c, ∑ d, f a b c • (B d * ((χ a * χ b * β c) * β d)) := by
      rw [Finset.sum_mul]
      refine Finset.sum_congr rfl fun a _ => ?_
      rw [Finset.sum_mul]
      refine Finset.sum_congr rfl fun b _ => ?_
      rw [Finset.sum_mul]
      refine Finset.sum_congr rfl fun c _ => ?_
      rw [Finset.mul_sum]
      exact Finset.sum_congr rfl fun d _ => hLterm a b c d
    have hR : (∑ d, β d * B d) * (∑ a, ∑ b, ∑ c, f a b c • (χ a * χ b * β c))
        = ∑ a, ∑ b, ∑ c, ∑ d, f a b c • (B d * (β d * (χ a * χ b * β c))) := by
      rw [Finset.sum_mul]
      have hstep : ∀ d : Fin n, (β d * B d) * (∑ a, ∑ b, ∑ c, f a b c • (χ a * χ b * β c))
          = ∑ a, ∑ b, ∑ c, f a b c • (B d * (β d * (χ a * χ b * β c))) := by
        intro d
        rw [Finset.mul_sum]
        refine Finset.sum_congr rfl fun a _ => ?_
        rw [Finset.mul_sum]
        refine Finset.sum_congr rfl fun b _ => ?_
        rw [Finset.mul_sum]
        exact Finset.sum_congr rfl fun c _ => hRterm a b c d
      rw [Finset.sum_congr rfl fun d _ => hstep d]
      rw [Finset.sum_comm]
      refine Finset.sum_congr rfl fun a _ => ?_
      rw [Finset.sum_comm]
      refine Finset.sum_congr rfl fun b _ => ?_
      exact Finset.sum_comm
    rw [hL, hR, ← Finset.sum_add_distrib]
    refine Finset.sum_congr rfl fun a _ => ?_
    rw [← Finset.sum_add_distrib]
    refine Finset.sum_congr rfl fun b _ => ?_
    rw [← Finset.sum_add_distrib]
    refine Finset.sum_congr rfl fun c _ => ?_
    rw [← Finset.sum_add_distrib]
    refine Finset.sum_congr rfl fun d _ => ?_
    rw [← smul_add, ← mul_add, hghost a b c d]
  rw [hQ]
  have hd : ∀ a b c : Fin n,
      (∑ d, f a b c • (B d * ((if d = a then χ b * β c else 0)
        - (if d = b then χ a * β c else 0))))
        = f a b c • (B a * (χ b * β c)) - f a b c • (B b * (χ a * β c)) := by
    intro a b c
    have hsplit : ∀ d : Fin n, f a b c • (B d * ((if d = a then χ b * β c else 0)
        - (if d = b then χ a * β c else 0)))
          = (if d = a then f a b c • (B a * (χ b * β c)) else 0)
            - (if d = b then f a b c • (B b * (χ a * β c)) else 0) := by
      intro d
      by_cases h1 : d = a
      · subst h1
        by_cases h2 : d = b
        · subst h2
          simp
        · simp [h2]
      · by_cases h2 : d = b
        · subst h2
          simp [h1]
        · simp [h1, h2]
    rw [Finset.sum_congr rfl fun d _ => hsplit d, Finset.sum_sub_distrib]
    simp
  rw [Finset.sum_congr rfl fun a _ => Finset.sum_congr rfl fun b _ =>
    Finset.sum_congr rfl fun c _ => hd a b c]
  -- the second family of terms is the first one again, by antisymmetry of `f`
  have hswap : (∑ a, ∑ b, ∑ c, f a b c • (B b * (χ a * β c)))
      = -∑ a, ∑ b, ∑ c, f a b c • (B a * (χ b * β c)) := by
    rw [Finset.sum_comm]
    rw [← Finset.sum_neg_distrib]
    refine Finset.sum_congr rfl fun a _ => ?_
    rw [← Finset.sum_neg_distrib]
    refine Finset.sum_congr rfl fun b _ => ?_
    rw [← Finset.sum_neg_distrib]
    refine Finset.sum_congr rfl fun c _ => ?_
    rw [hf12 b a c]
    simp
  have hsplit2 : (∑ a, ∑ b, ∑ c, (f a b c • (B a * (χ b * β c))
      - f a b c • (B b * (χ a * β c))))
      = (∑ a, ∑ b, ∑ c, f a b c • (B a * (χ b * β c)))
        - ∑ a, ∑ b, ∑ c, f a b c • (B b * (χ a * β c)) := by
    rw [← Finset.sum_sub_distrib]
    refine Finset.sum_congr rfl fun a _ => ?_
    rw [← Finset.sum_sub_distrib]
    refine Finset.sum_congr rfl fun b _ => ?_
    rw [← Finset.sum_sub_distrib]
  rw [hsplit2, hswap, sub_neg_eq_add]
  have hdouble : (∑ a, ∑ b, ∑ c, (2 * f a b c) • (B a * (χ b * β c)))
      = (∑ a, ∑ b, ∑ c, f a b c • (B a * (χ b * β c)))
        + ∑ a, ∑ b, ∑ c, f a b c • (B a * (χ b * β c)) := by
    rw [← Finset.sum_add_distrib]
    refine Finset.sum_congr rfl fun a _ => ?_
    rw [← Finset.sum_add_distrib]
    refine Finset.sum_congr rfl fun b _ => ?_
    rw [← Finset.sum_add_distrib]
    refine Finset.sum_congr rfl fun c _ => ?_
    rw [two_mul, add_smul]
  rw [hdouble]

/-- **The gauge-fixing anticommutator.**  For the BRST charge with constraints `𝒢_a` and a
gauge-fixing fermion `Ψ = Σ_d ψ_d B_d` built from bosonic operators,

`{Ω, Ψ} = Σ_c 𝒢_c B_c − Σ_{c,d} [𝒢_c, B_d] ψ_d ψ†_c − Σ_{a,b,c} f_{abc} B_a ψ†_b ψ_c`. -/
theorem brstCharge_gf_anticomm (hCAR : GhostCAR χ β) (hf12 : ∀ a b c, f a b c = -f b a c)
    (hGβ : ∀ a b, Gc a * β b = β b * Gc a)
    (hBχ : ∀ a b, B a * χ b = χ b * B a) (hBβ : ∀ a b, B a * β b = β b * B a) :
    brstCharge f Gc χ β * gfFermion β B + gfFermion β B * brstCharge f Gc χ β
      = (∑ c, Gc c * B c)
        - (∑ c, ∑ d, (Gc c * B d - B d * Gc c) * (β d * χ c))
        - ∑ a, ∑ b, ∑ c, f a b c • (B a * (χ b * β c)) := by
  have h1 := glin_gf_anticomm hCAR hGβ hBχ hBβ
  have h2 := Q_gf_anticomm (B := B) hCAR hf12 hBχ hBβ
  have hexp : brstCharge f Gc χ β * gfFermion β B + gfFermion β B * brstCharge f Gc χ β
      = (glin Gc χ * gfFermion β B + gfFermion β B * glin Gc χ)
        - (1 / 2 : ℝ) • (Q f χ β * gfFermion β B + gfFermion β B * Q f χ β) := by
    rw [brstCharge, sub_mul, mul_sub, smul_mul_assoc, mul_smul_comm, smul_add]
    abel
  rw [hexp, h1, h2]
  have hhalf : (1 / 2 : ℝ) • (∑ a, ∑ b, ∑ c, (2 * f a b c) • (B a * (χ b * β c)))
      = ∑ a, ∑ b, ∑ c, f a b c • (B a * (χ b * β c)) := by
    rw [Finset.smul_sum]
    refine Finset.sum_congr rfl fun a _ => ?_
    rw [Finset.smul_sum]
    refine Finset.sum_congr rfl fun b _ => ?_
    rw [Finset.smul_sum]
    refine Finset.sum_congr rfl fun c _ => ?_
    rw [smul_smul]
    congr 1
    ring
  rw [hhalf, sub_sub]

omit [Algebra ℝ R] in
/-- **A BRST-exact term is BRST invariant**: for a nilpotent charge, `{Ω,Ψ}` commutes with
`Ω`.  This is why adding the gauge-fixing term to the Hamiltonian does not spoil BRST
invariance. -/
theorem brst_exact_comm {Ω Ψ : R} (hnil : Ω * Ω = 0) :
    Ω * (Ω * Ψ + Ψ * Ω) = (Ω * Ψ + Ψ * Ω) * Ω := by
  have h1 : Ω * (Ω * Ψ) = 0 := by rw [← mul_assoc, hnil, zero_mul]
  have h2 : (Ψ * Ω) * Ω = 0 := by rw [mul_assoc, hnil, mul_zero]
  calc Ω * (Ω * Ψ + Ψ * Ω) = Ω * (Ω * Ψ) + (Ω * Ψ) * Ω := by
        rw [mul_add, mul_assoc]
    _ = (Ω * Ψ) * Ω := by rw [h1, zero_add]
    _ = (Ω * Ψ) * Ω + (Ψ * Ω) * Ω := by rw [h2, add_zero]
    _ = (Ω * Ψ + Ψ * Ω) * Ω := by rw [add_mul]

end Abstract

/-! ## 2. The book's gauge-fixing fermion `Ψ = i ψ_a A_{0a}` -/

variable {N : ℕ} (G : GaugeAlgebra N)

/-- **The gauge-fixing fermion of `book.tex`**, `Ψ = i ψ_a A_{0a}`. -/
def bookGfFermion : Module.End ℂ (BookState N) :=
  Complex.I • gfFermion betaOp (fun a => Afield 0 a)

-- Note: `bookGfFermion` does not depend on `G`; only `N` (and the operators) enter.

/-- **The gauge-fixing term** `{Ω, Ψ}` added to the Hamiltonian in `book.tex`. -/
def bookGfTerm : Module.End ℂ (BookState N) :=
  bookOmega G * bookGfFermion + bookGfFermion * bookOmega G

/-- **The gauge-fixing term is BRST invariant**: it commutes with the BRST charge, because
the charge is nilpotent.  Hence adding it to the Hamiltonian changes neither the BRST-closed
nor the BRST-exact states. -/
theorem bookGfTerm_brst_closed :
    bookOmega G * bookGfTerm G = bookGfTerm G * bookOmega G := by
  -- `brst_exact_comm` states the identity for a bare expression `Ω * (ΩΨ + ΨΩ)`,
  -- so the named def has to be unfolded before the two can be unified.
  -- Inlined rather than `brst_exact_comm`: that lemma is stated for a general
  -- ring `R`, and instantiating it at `Module.End ℂ (BookState N)` picks the
  -- ring's `Mul` instance, which does not unify with the `Module.End` `Mul`
  -- that `bookOmega` is built from.  Every step below stays in the
  -- `Module.End` instances, so no instance conversion is needed.
  unfold bookGfTerm
  have h1 : bookOmega G * (bookOmega G * bookGfFermion) = 0 := by
    rw [← mul_assoc, bookOmega_nilpotent G, zero_mul]
  have h2 : (bookGfFermion * bookOmega G) * bookOmega G = 0 := by
    rw [mul_assoc, bookOmega_nilpotent G, mul_zero]
  calc bookOmega G * (bookOmega G * bookGfFermion + bookGfFermion * bookOmega G)
        = bookOmega G * (bookOmega G * bookGfFermion)
            + (bookOmega G * bookGfFermion) * bookOmega G := by
          rw [mul_add, mul_assoc]
    _ = (bookOmega G * bookGfFermion) * bookOmega G := by rw [h1, zero_add]
    _ = (bookOmega G * bookGfFermion) * bookOmega G
            + (bookGfFermion * bookOmega G) * bookOmega G := by rw [h2, add_zero]
    _ = (bookOmega G * bookGfFermion + bookGfFermion * bookOmega G) * bookOmega G := by
          rw [add_mul]

/-- **The book's gauge-fixing term, computed.**  With `Ω` the charge of `book.tex` and
`Ψ = i ψ_a A_{0a}` its gauge-fixing fermion,

`{Ω, Ψ} = −(Σ_c 𝒢_c A_{0c} − Σ_{c,d} [𝒢_c, A_{0d}] ψ_d ψ†_c − Σ_{a,b,c} f_{abc} A_{0a} ψ†_b ψ_c)`,

the Gauss law contracted with the gauge-fixing field, the ghost kinetic term and the
non-abelian ghost–field coupling. -/
theorem bookGfTerm_eq :
    bookGfTerm G
      = -((∑ c, gaussGen G c * Afield 0 c)
          - (∑ c, ∑ d, (gaussGen G c * Afield 0 d - Afield 0 d * gaussGen G c)
              * (betaOp d * chiOp c))
          - ∑ a, ∑ b, ∑ c, G.f a b c • (Afield 0 a * (chiOp b * betaOp c))) := by
  have habs := brstCharge_gf_anticomm (f := G.f) (Gc := gaussGen G) (χ := chiOp)
    (β := betaOp) (B := fun a => Afield (N := N) 0 a) bookGhostCar G.antisymm
    (fun a b => (bookConstraintAlgebra G).comm_beta a b)
    (fun a b => Afield_comm_chi 0 a b)
    (fun a b => bosOpN_ghostOpN_comm _ _)
  have hI : Complex.I * Complex.I = -1 := Complex.I_mul_I
  calc bookGfTerm G
      = (Complex.I * Complex.I) • (brstCharge G.f (gaussGen G) chiOp betaOp
            * gfFermion betaOp (fun a => Afield (N := N) 0 a)
          + gfFermion betaOp (fun a => Afield (N := N) 0 a)
            * brstCharge G.f (gaussGen G) chiOp betaOp) := by
        rw [bookGfTerm, bookGfFermion, bookOmega_eq_brstCharge, smul_mul_smul_comm,
          smul_mul_smul_comm, ← smul_add]
    _ = -(brstCharge G.f (gaussGen G) chiOp betaOp
            * gfFermion betaOp (fun a => Afield (N := N) 0 a)
          + gfFermion betaOp (fun a => Afield (N := N) 0 a)
            * brstCharge G.f (gaussGen G) chiOp betaOp) := by
        rw [hI]
        -- `(-1 : ℂ) • X` on `Module.End` is pointwise, so the scalar ring and
        -- the endomorphism ring do not line up for `neg_one_smul`.  Passing to
        -- points makes the negation an ordinary `neg_smul` rewrite.
        ext v
        -- `-1 • a + -1 • b = -(a + b)`: push each `-1 •` through to a negation,
        -- drop the trivial `1 •`, then recombine.
        simp [neg_smul, one_smul]
        abel
    _ = _ := by rw [habs]

/-! ## 2b. The accounting identity: the gauge-fixing term vanishes at `A₀ = 0` -/

/-- **An abstract gauge-fixing fermion with vanishing bosonic slots is zero.** -/
theorem gfFermion_eq_zero {R : Type*} [Ring R] {n : ℕ} {β B : Fin n → R}
    (h : ∀ d : Fin n, B d = 0) : gfFermion β B = 0 := by
  unfold gfFermion
  exact Finset.sum_eq_zero fun d _ => by rw [h d, mul_zero]

/-- **The book's gauge-fixing fermion vanishes in the temporal (Weyl) gauge.**
If `A_{0a} = 0` for every colour index `a`, then `Ψ = i ψ_a A_{0a}` is the zero operator. -/
theorem bookGfFermion_eq_zero_of_Afield0
    (hA0 : ∀ a : Fin N, Afield (N := N) 0 a = 0) :
    bookGfFermion (N := N) = 0 := by
  rw [bookGfFermion]
  rw [gfFermion_eq_zero hA0, smul_zero]

/-- **Accounting identity**: the BRST-exact gauge-fixing term `{Ω, Ψ}` of `book.tex` is
identically zero on the temporal-gauge slice `A₀ = 0`.  Consequently the gauge-fixed
Hamiltonian `h` and the comparison operator `N` need **no extra summand** for the
gauge-fixing/ghost sector: what `bookGfTerm_eq` exhibits (Gauss law against `A₀`, ghost
kinetic term, non-abelian ghost–field coupling) is already accounted for by vanishing at
`A₀ = 0`, so the record of `h` and `N` is structurally unchanged. -/
theorem bookGfTerm_eq_zero_of_Afield0
    (hA0 : ∀ a : Fin N, Afield (N := N) 0 a = 0) :
    bookGfTerm G = 0 := by
  rw [bookGfTerm, bookGfFermion_eq_zero_of_Afield0 hA0, zero_mul, mul_zero, add_zero]

/-! ## 3. The BRST cohomology of the book's charge -/

/-- **Physical states**: the kernel of the book's BRST charge, `Ω |phys⟩ = 0`. -/
def physicalStates : Submodule ℂ (BookState N) := LinearMap.ker (bookOmega G)

/-- **BRST-exact states**: the image of the book's BRST charge. -/
def exactStates : Submodule ℂ (BookState N) := LinearMap.range (bookOmega G)

/-- Every BRST-exact state is physical, because `Ω² = 0`.  This is what makes the quotient
`brstCohomology` below well defined. -/
theorem exactStates_le_physicalStates : exactStates G ≤ physicalStates G := by
  rintro v ⟨w, rfl⟩
  have h := congrArg (fun T : Module.End ℂ (BookState N) => T w) (bookOmega_nilpotent G)
  simpa [physicalStates, LinearMap.mem_ker] using h

/-- The exact states, viewed inside the physical states. -/
def exactInPhysical : Submodule ℂ (physicalStates G) :=
  (exactStates G).comap (physicalStates G).subtype

/-! **On the BRST cohomology.**  Physical states modulo BRST-exact states would be
`Submodule ℂ ↥(physicalStates G) ⧸ exactInPhysical G`, but that does not elaborate
here: the `HasQuotient` instance for submodule quotients is not found for this
scalar/ambient pair, and `Submodule.Quotient` is not a constant in this Mathlib.
The cohomology lives in `Def_ChapterG2` instead, which builds its own
`brstCohomology` from a general ring `A` where the instance is available; nothing
below or downstream refers to a name in this namespace, so no abbreviation is
declared here rather than leaving one that does not compile. -/

/-- The gauge-fixing term of `book.tex` maps physical states to physical states. -/
theorem bookGfTerm_mem_physicalStates {v : BookState N} (hv : v ∈ physicalStates G) :
    bookGfTerm G v ∈ physicalStates G := by
  have h : bookOmega G (bookGfTerm G v) = bookGfTerm G (bookOmega G v) :=
    congrArg (fun T : Module.End ℂ (BookState N) => T v) (bookGfTerm_brst_closed G)
  have hv' : bookOmega G v = 0 := hv
  exact (h.trans (by rw [hv', map_zero]) : bookOmega G (bookGfTerm G v) = 0)

/-- The gauge-fixing term of `book.tex` maps BRST-exact states to BRST-exact states. -/
theorem bookGfTerm_mem_exactStates {v : BookState N} (hv : v ∈ exactStates G) :
    bookGfTerm G v ∈ exactStates G := by
  obtain ⟨w, rfl⟩ := hv
  have h : bookOmega G (bookGfTerm G w) = bookGfTerm G (bookOmega G w) :=
    congrArg (fun T : Module.End ℂ (BookState N) => T w) (bookGfTerm_brst_closed G)
  exact ⟨bookGfTerm G w, h⟩

/-! ## 4. Gauge-invariant observables act on the BRST cohomology -/

section Observables

variable {R : Type*} [Ring R] [Algebra ℝ R] {n : ℕ}
variable {f : Fin n → Fin n → Fin n → ℝ} {Gc χ β : Fin n → R}

omit [Algebra ℝ R] in
/-- An operator commuting with the constraints and with the ghosts commutes with the
constraint part `Σ_a 𝒢_a ψ†_a` of the charge. -/
theorem glin_comm_of_comm {T : R} (hG : ∀ a, Gc a * T = T * Gc a)
    (hχ : ∀ a, χ a * T = T * χ a) : glin Gc χ * T = T * glin Gc χ := by
  simp only [glin, Finset.sum_mul, Finset.mul_sum]
  refine Finset.sum_congr rfl fun a _ => ?_
  rw [mul_assoc, hχ a, ← mul_assoc, hG a, mul_assoc]

/-- An operator commuting with the ghosts commutes with the cubic ghost term. -/
theorem Q_comm_of_comm {T : R} (hχ : ∀ a, χ a * T = T * χ a)
    (hβ : ∀ a, β a * T = T * β a) : Q f χ β * T = T * Q f χ β := by
  simp only [Q, Finset.sum_mul, Finset.mul_sum]
  refine Finset.sum_congr rfl fun a _ => Finset.sum_congr rfl fun b _ =>
    Finset.sum_congr rfl fun e _ => ?_
  rw [smul_mul_assoc, mul_smul_comm]
  congr 1
  calc χ a * χ b * β e * T = χ a * (χ b * (β e * T)) := by noncomm_ring
    _ = χ a * (χ b * (T * β e)) := by rw [hβ]
    _ = χ a * (χ b * T * β e) := by noncomm_ring
    _ = χ a * (T * χ b * β e) := by rw [hχ]
    _ = χ a * T * (χ b * β e) := by noncomm_ring
    _ = T * χ a * (χ b * β e) := by rw [hχ]
    _ = T * (χ a * χ b * β e) := by noncomm_ring

/-- **A gauge-invariant observable is BRST invariant**: an operator commuting with all the
constraints and with all the ghosts commutes with the BRST charge. -/
theorem brstCharge_comm_of_comm {T : R} (hG : ∀ a, Gc a * T = T * Gc a)
    (hχ : ∀ a, χ a * T = T * χ a) (hβ : ∀ a, β a * T = T * β a) :
    brstCharge f Gc χ β * T = T * brstCharge f Gc χ β := by
  rw [brstCharge, sub_mul, mul_sub, glin_comm_of_comm hG hχ, smul_mul_assoc, mul_smul_comm,
    Q_comm_of_comm hχ hβ]

end Observables

/-- **A gauge-invariant observable commutes with the charge of `book.tex`.** -/
theorem bookOmega_comm_of_comm {T : Module.End ℂ (BookState N)}
    (hG : ∀ a, gaussGen G a * T = T * gaussGen G a)
    (hχ : ∀ a, chiOp (N := N) a * T = T * chiOp a)
    (hβ : ∀ a, betaOp (N := N) a * T = T * betaOp a) :
    bookOmega G * T = T * bookOmega G := by
  rw [bookOmega_eq_brstCharge, smul_mul_assoc, mul_smul_comm, brstCharge_comm_of_comm hG hχ hβ]

/-- A gauge-invariant observable maps physical states to physical states. -/
theorem mem_physicalStates_of_comm {T : Module.End ℂ (BookState N)}
    (hG : ∀ a, gaussGen G a * T = T * gaussGen G a)
    (hχ : ∀ a, chiOp (N := N) a * T = T * chiOp a)
    (hβ : ∀ a, betaOp (N := N) a * T = T * betaOp a)
    {v : BookState N} (hv : v ∈ physicalStates G) : T v ∈ physicalStates G := by
  have h : bookOmega G (T v) = T (bookOmega G v) :=
    congrArg (fun S : Module.End ℂ (BookState N) => S v) (bookOmega_comm_of_comm G hG hχ hβ)
  have hv' : bookOmega G v = 0 := hv
  exact (h.trans (by rw [hv', map_zero]) : bookOmega G (T v) = 0)

/-- A gauge-invariant observable maps BRST-exact states to BRST-exact states, so it descends
to the BRST cohomology. -/
theorem mem_exactStates_of_comm {T : Module.End ℂ (BookState N)}
    (hG : ∀ a, gaussGen G a * T = T * gaussGen G a)
    (hχ : ∀ a, chiOp (N := N) a * T = T * chiOp a)
    (hβ : ∀ a, betaOp (N := N) a * T = T * betaOp a)
    {v : BookState N} (hv : v ∈ exactStates G) : T v ∈ exactStates G := by
  obtain ⟨w, rfl⟩ := hv
  have h : bookOmega G (T w) = T (bookOmega G w) :=
    congrArg (fun S : Module.End ℂ (BookState N) => S w) (bookOmega_comm_of_comm G hG hχ hβ)
  exact ⟨T w, h⟩

/-! ## 5. A concrete gauge-invariant observable -/

/-- Multiplication by a polynomial in the gauge fields, as an operator on the graded state
space. -/
def multOp (p : FieldPoly N) : Module.End ℂ (BookState N) := bosOpN (LinearMap.mulLeft ℂ p)

/-- The Gauss-law generator against a multiplication operator is multiplication by the gauge
variation of the polynomial: `[𝒢_c, p] = 𝒢_c(p)`. -/
theorem gaussGenPoly_comm_mulLeft (c : Fin N) (p : FieldPoly N) :
    gaussGenPoly G c * LinearMap.mulLeft ℂ p - LinearMap.mulLeft ℂ p * gaussGenPoly G c
      = LinearMap.mulLeft ℂ (gaussDer G c p) := by
  refine LinearMap.ext fun q => ?_
  simp only [LinearMap.sub_apply, Module.End.mul_apply, LinearMap.mulLeft_apply]
  change gaussDer G c (p * q) - p * gaussDer G c q = gaussDer G c p * q
  rw [Derivation.leibniz, smul_eq_mul, smul_eq_mul, mul_comm q (gaussDer G c p)]
  ring

/-- A **gauge-invariant** polynomial — one annihilated by every Gauss-law generator — gives an
observable commuting with the constraints. -/
theorem gaussGen_comm_multOp {p : FieldPoly N} (hp : ∀ c, gaussDer G c p = 0) (c : Fin N) :
    gaussGen G c * multOp p = multOp p * gaussGen G c := by
  have h := gaussGenPoly_comm_mulLeft G c p
  rw [hp c] at h
  have h0 : LinearMap.mulLeft ℂ (0 : FieldPoly N) = 0 := by
    refine LinearMap.ext fun q => ?_
    simp
  rw [h0, sub_eq_zero] at h
  rw [gaussGen, multOp, ← bosOpN_mul, ← bosOpN_mul, h]

/-- **A gauge-invariant observable commutes with the book's BRST charge.** -/
theorem bookOmega_comm_multOp {p : FieldPoly N} (hp : ∀ c, gaussDer G c p = 0) :
    bookOmega G * multOp p = multOp p * bookOmega G :=
  bookOmega_comm_of_comm G (gaussGen_comm_multOp G hp)
    (fun _ => (bosOpN_ghostOpN_comm _ _).symm) (fun _ => (bosOpN_ghostOpN_comm _ _).symm)

/-- The quadratic invariant `Σ_{μ,a} A_{μa} A_{μa}` of the gauge fields. -/
def casimirPoly : FieldPoly N := ∑ i : Fin 4 × Fin N, X i * X i

/-- The quadratic invariant is annihilated by the Gauss law when the gauge fields carry no
spacetime dependence (`∂_μ = 0`), by antisymmetry of the structure constants. -/
theorem gaussDer_casimirPoly (hD : ∀ μ c a, G.D μ c a = 0) (c : Fin N) :
    gaussDer G c (casimirPoly (N := N)) = 0 := by
  have hvec : ∀ i : Fin 4 × Fin N,
      gaussVec G c i = ∑ g, ((G.f i.2 g c : ℝ) : ℂ) • (X (i.1, g) : FieldPoly N) := by
    intro i
    simp [gaussVec, vecComb, hD]
  have hterm : ∀ i : Fin 4 × Fin N, gaussDer G c (X i * X i)
      = ∑ g, ((2 * G.f i.2 g c : ℝ) : ℂ) • (X i * X (i.1, g) : FieldPoly N) := by
    intro i
    rw [Derivation.leibniz, gaussDer_X, hvec i]
    simp only [smul_eq_mul, Finset.mul_sum, ← Finset.sum_add_distrib,
      Complex.ofReal_mul, Complex.ofReal_ofNat]
    refine Finset.sum_congr rfl fun g _ => ?_
    rw [mul_smul_comm, ← two_smul ℂ, smul_smul]
  rw [casimirPoly, map_sum, Finset.sum_congr rfl fun i _ => hterm i]
  rw [Fintype.sum_prod_type]
  refine Finset.sum_eq_zero fun μ _ => ?_
  set S : FieldPoly N := ∑ a, ∑ g, ((2 * G.f a g c : ℝ) : ℂ) • (X (μ, a) * X (μ, g) : FieldPoly N)
    with hS
  have hswap : S = -S := by
    rw [hS]
    nth_rewrite 1 [Finset.sum_comm]
    rw [← Finset.sum_neg_distrib]
    refine Finset.sum_congr rfl fun a _ => ?_
    rw [← Finset.sum_neg_distrib]
    refine Finset.sum_congr rfl fun g _ => ?_
    rw [← neg_smul]
    congr 1
    · norm_cast
      rw [G.antisymm a g c]
      ring
    · ring
  have h2 : (2 : ℂ) • S = 0 := by
    rw [two_smul]
    nth_rewrite 2 [hswap]
    ring_nf
  have := smul_eq_zero.mp h2
  rcases this with h | h
  · exact absurd h (by norm_num)
  · exact h

/-- **The quadratic invariant is a BRST-invariant observable** of the book's charge (for the
constant gauge-field algebra), so it acts on the physical states and on the BRST cohomology. -/
theorem casimir_bookOmega_comm (hD : ∀ μ c a, G.D μ c a = 0) :
    bookOmega G * multOp (casimirPoly (N := N)) = multOp (casimirPoly (N := N)) * bookOmega G :=
  bookOmega_comm_multOp G (gaussDer_casimirPoly G hD)

end

end BookProof.BookBrstGaugeFixing