The Lean 4 theorem `le_of_rpow_two_le` in the `?` chapter of the timepiece formalization

import Definitions.Def_ChapterQuantumGravityFock
import Definitions.Def_ChapterBrstReducedTransfer
import Mathlib
import Theorems.Thm_BookProof_BrstReducedTransfer_exactStates_le_physicalStates
import Theorems.Thm_BookProof_BrstReducedTransfer_transfer_zero
import Theorems.Thm_BookProof_BrstReducedTransfer_transfer_comp
import Theorems.Thm_BookProof_BrstReducedTransfer_transfer_bijective


/-!
# The bounded BRST charge on the *completed* graded Hilbert space, and its reduced transfer

`CONSOLIDATED_PLAN.md` §10.6.2 item 4 is closed except for one join: the BRST charge of
`ChapterQuantumGravityBrstCharge` is built on the *algebraic* graded space
`ℂ[x₀,…,x₈₃] ⊗ Λ(ℂ¹⁹)`, whereas the reduced-transfer theorems of
`ChapterBrstReducedTransfer` need a **bounded** nilpotent charge on a *complete* space.
This module supplies exactly that missing object and performs the join.

## What is proved

* **A bounded weighted shift calculus on `ℓ²`** (`wshift`).  For a weight `w` with
  `‖w i‖ ≤ 1` and a reindexing `e` that is injective on the support of `w`, the map
  `f ↦ (i ↦ w i * f (e i))` is a bounded operator of norm `≤ 1` on `ℓ²(ι)`
  (`memlp_weighted`, `wshiftL_norm_le`).  This is the analytic content: the pullback of a
  square-summable family along a partially injective reindexing stays square-summable.
* **The ghost creation operators on the completed graded space.**  On
  `QGH = ℓ²(GradedIdx)` — the completion of the graded Fock space of
  `ChapterQuantumGravityFock`, `GradedIdx = BoseConf × FermConf` — the operator
  `brstTerm sym a` is `Ψ†_a` dressed with a bounded boson-sector constraint symbol
  `sym a : BoseConf → ℂ`.  It is bounded by `1` and satisfies the Jordan–Wigner
  anticommutation relations `brstTerm_comp_self` (`(Ψ†_a)² = 0`) and `brstTerm_anticomm`
  (`؆_a؆_b + ؆_b؆_a = 0`).
* **The bounded nilpotent BRST charge** `qgBrstCharge sym = ∑_{a<19} sym_a Ψ†_a` over the
  book's `19` diffeomorphism ghosts: `qgBrstCharge_nilpotent` (`Ω² = 0`) and
  `qgBrstCharge_ne_zero` (it is not the zero operator, so the statement is not vacuous).
* **An explicit unitary group commuting with it**: `qgPhase omega t`, multiplication by
  `e^{-it·(boson energy)}`, with `qgPhase_zero`, `qgPhase_group`, `qgPhase_isometry` and
  `qgPhase_comm_brst`.  `qgPhase_single` identifies it on the occupation basis as the
  evolution generated by the graded Fock symbol `qgGradedSymbol omega 0` of
  `ChapterQuantumGravityFock` — the ghost-energy-free case, which is precisely the case in
  which the evolution commutes with the ghost ladder.
* **The join** (§10.6.2 item 4): `qgBrstTransfer` is the induced one-parameter group on the
  BRST cohomology `Cohomology (qgBrstCharge sym)` of the completed space, with
  `qgBrstTransfer_zero`, `qgBrstTransfer_comp`, `qgBrstTransfer_bijective`,
  `qgPhase_mem_physicalStates` (the §10.3 caveat: the evolution preserves the physical
  subspace) and `qgBrstTransfer_infDist` (the BRST quotient norm is preserved).

## Honest boundary

The charge is `Ω = ∑_a C_a Ψ†_a` with the constraint symbols `C_a` *diagonal* in the boson
occupation basis and bounded by one; the full gauge-fixed constraint algebra (whose
generators are unbounded) is not represented, and no claim is made that this `Ω` is the
BRST charge of the `R + αR²` theory.  What is claimed, and proved, is that the reduced
transfer of §10.6.2 item 4 now has a concrete bounded nilpotent charge on a complete
Hilbert space, together with a nontrivial commuting unitary group.  The Hamiltonian whose
group is used here has no ghost energy: a nonzero ghost energy does *not* commute with the
ghost ladder, so its evolution does not descend — that obstruction is recorded, not hidden.
-/

namespace BookProof.QgBrstCompleted

open scoped ENNReal
open BookProof BookProof.QuantumGravityFock BookProof.BrstReducedTransfer

noncomputable section

/-- A one-ghost state carries exactly the energy of its ghost mode.

Grafted here: the published Def_ChapterQuantumGravityFock carries
`qgGradedSymbol_vacuum` but not this sibling theorem (upstream
ChapterQuantumGravityFock.lean:762), so the proof at the use site could not
elaborate -- def gate FAIL `Unknown identifier qgGradedSymbol_oneGhost`.
Single consumer of the lemma; declared in this bundle's namespace so the
unqualified `rw` keeps resolving. -/
theorem qgGradedSymbol_oneGhost (omega g : ℕ → ℝ) (a : ℕ) :
    qgGradedSymbol omega g (0, ({a} : FermConf)) = g a := by
  simp [qgGradedSymbol, BookProof.NavierStokesFlow.FockOfFock.confEnergy_zero, ghostEnergy]

/-! ## A bounded weighted-shift calculus on `ℓ²` -/

section WeightedShift

variable {ι : Type*}

/-- `ℓ²` over an arbitrary index type. -/
abbrev L2 (ι : Type*) := lp (fun _ : ι => ℂ) 2

theorem le_of_rpow_two_le {a b : ℝ} (hb : 0 ≤ b) (h : a ^ (2 : ℝ) ≤ b ^ (2 : ℝ)) : a ≤ b := by
  rw [show (2 : ℝ) = ((2 : ℕ) : ℝ) by norm_num, Real.rpow_natCast, Real.rpow_natCast] at h
  nlinarith

theorem summable_sq_lp (f : L2 ι) : Summable fun j => ‖f j‖ ^ (2 : ℝ) := by
  have hp : (0 : ℝ) < ((2 : ℝ≥0∞)).toReal := by norm_num
  have h := lp.memℓp f
  rw [memℓp_gen_iff hp] at h
  simpa using h

/-- **The analytic heart.**  Pulling a square-summable family back along a reindexing that
is injective on the support of a weight bounded by one keeps it square-summable, and does
not increase the sum. -/
theorem tsum_sq_weighted_le (w : ι → ℂ) (e : ι → ι) (hw : ∀ i, ‖w i‖ ≤ 1)
    (hinj : Set.InjOn e {i | w i ≠ 0}) (f : ι → ℂ) (hf : Summable fun j => ‖f j‖ ^ (2 : ℝ)) :
    Summable (fun i => ‖w i * f (e i)‖ ^ (2 : ℝ)) ∧
      ∑' i, ‖w i * f (e i)‖ ^ (2 : ℝ) ≤ ∑' j, ‖f j‖ ^ (2 : ℝ) := by
  classical
  set S : Set ι := {i | w i ≠ 0} with hS
  have hinj' : Function.Injective (fun x : S => e (x : ι)) := fun x y hxy =>
    Subtype.ext (hinj x.2 y.2 hxy)
  have hsub : Summable (fun x : S => ‖f (e (x : ι))‖ ^ (2 : ℝ)) := hf.comp_injective hinj'
  have hind : Summable (S.indicator (fun i => ‖f (e i)‖ ^ (2 : ℝ))) :=
    summable_subtype_iff_indicator.mp hsub
  have hle : ∀ i, ‖w i * f (e i)‖ ^ (2 : ℝ) ≤ S.indicator (fun i => ‖f (e i)‖ ^ (2 : ℝ)) i := by
    intro i
    by_cases hi : i ∈ S
    · rw [Set.indicator_of_mem hi]
      have h1 : ‖w i * f (e i)‖ ≤ ‖f (e i)‖ := by
        rw [norm_mul]
        calc ‖w i‖ * ‖f (e i)‖ ≤ 1 * ‖f (e i)‖ :=
              mul_le_mul_of_nonneg_right (hw i) (norm_nonneg _)
          _ = ‖f (e i)‖ := one_mul _
      exact Real.rpow_le_rpow (norm_nonneg _) h1 (by norm_num)
    · have hw0 : w i = 0 := by simpa [hS] using hi
      simp [hw0, Set.indicator_of_notMem hi]
  have hsum : Summable (fun i => ‖w i * f (e i)‖ ^ (2 : ℝ)) :=
    hind.of_nonneg_of_le (fun i => by positivity) hle
  refine ⟨hsum, ?_⟩
  calc ∑' i, ‖w i * f (e i)‖ ^ (2 : ℝ) ≤ ∑' i, S.indicator (fun i => ‖f (e i)‖ ^ (2 : ℝ)) i :=
        hsum.tsum_le_tsum hle hind
    _ = ∑' x : S, ‖f (e (x : ι))‖ ^ (2 : ℝ) := (tsum_subtype S _).symm
    _ ≤ ∑' j, ‖f j‖ ^ (2 : ℝ) :=
        hsub.tsum_le_tsum_of_inj (fun x : S => e (x : ι)) hinj' (fun c _ => by positivity)
          (fun _ => le_refl _) hf

theorem memlp_weighted (w : ι → ℂ) (e : ι → ι) (hw : ∀ i, ‖w i‖ ≤ 1)
    (hinj : Set.InjOn e {i | w i ≠ 0}) (f : L2 ι) :
    Memℓp (fun i => w i * f (e i)) 2 := by
  have hp : (0 : ℝ) < ((2 : ℝ≥0∞)).toReal := by norm_num
  rw [memℓp_gen_iff hp]
  simpa using (tsum_sq_weighted_le w e hw hinj (fun i => f i) (summable_sq_lp f)).1

variable (w : ι → ℂ) (e : ι → ι) (hw : ∀ i, ‖w i‖ ≤ 1) (hinj : Set.InjOn e {i | w i ≠ 0})

include hw hinj in
/-- The weighted shift as a linear map on `ℓ²`. -/
def wshiftL : L2 ι →ₗ[ℂ] L2 ι where
  toFun f := ⟨fun i => w i * f (e i), memlp_weighted w e hw hinj f⟩
  map_add' f g := by ext i; simp only [lp.coeFn_add, Pi.add_apply, mul_add]
  map_smul' c f := by ext i; simp [mul_left_comm]

@[simp] theorem wshiftL_apply (f : L2 ι) (i : ι) : (wshiftL w e hw hinj f) i = w i * f (e i) := rfl

theorem wshiftL_norm_le (f : L2 ι) : ‖wshiftL w e hw hinj f‖ ≤ ‖f‖ := by
  have hp : (0 : ℝ) < ((2 : ℝ≥0∞)).toReal := by norm_num
  have h1 := lp.norm_rpow_eq_tsum hp (wshiftL w e hw hinj f)
  have h2 := lp.norm_rpow_eq_tsum hp f
  have hle := (tsum_sq_weighted_le w e hw hinj (fun i => f i) (summable_sq_lp f)).2
  rw [show ((2 : ℝ≥0∞)).toReal = 2 by norm_num] at h1 h2
  refine le_of_rpow_two_le (norm_nonneg f) ?_
  rw [h1, h2]
  simpa using hle

/-- **The bounded weighted shift** `f ↦ (i ↦ w i · f (e i))` on `ℓ²`, of norm at most one. -/
def wshift : L2 ι →L[ℂ] L2 ι :=
  LinearMap.mkContinuous (wshiftL w e hw hinj) 1 fun f => by
    simpa using wshiftL_norm_le w e hw hinj f

@[simp] theorem wshift_apply (f : L2 ι) (i : ι) : (wshift w e hw hinj f) i = w i * f (e i) := rfl

theorem wshift_norm_le (f : L2 ι) : ‖wshift w e hw hinj f‖ ≤ ‖f‖ := wshiftL_norm_le w e hw hinj f

/-- If the weight has modulus one everywhere and the reindexing is the identity, the
weighted shift is an isometry. -/
theorem wshift_norm_eq (hw1 : ∀ i, ‖w i‖ = 1) (hid : e = id) (f : L2 ι) :
    ‖wshift w e hw hinj f‖ = ‖f‖ := by
  have hp : (0 : ℝ) < ((2 : ℝ≥0∞)).toReal := by norm_num
  have h1 := lp.norm_rpow_eq_tsum hp (wshift w e hw hinj f)
  have h2 := lp.norm_rpow_eq_tsum hp f
  rw [show ((2 : ℝ≥0∞)).toReal = 2 by norm_num] at h1 h2
  have hpt : ∀ i, ‖(wshift w e hw hinj f) i‖ ^ (2 : ℝ) = ‖f i‖ ^ (2 : ℝ) := by
    intro i
    rw [wshift_apply, norm_mul, hw1, one_mul, hid, id_eq]
  refine le_antisymm (le_of_rpow_two_le (norm_nonneg f) ?_)
    (le_of_rpow_two_le (norm_nonneg _) ?_)
  · rw [h1, h2]; exact le_of_eq (tsum_congr hpt)
  · rw [h1, h2]; exact le_of_eq (tsum_congr fun i => (hpt i).symm)

end WeightedShift

/-! ## The completed graded Hilbert space and the ghost creation operators -/

/-- The **completed** graded state space: the `ℓ²` completion of the graded Fock space of
`ChapterQuantumGravityFock`, indexed by joint boson/ghost occupations. -/
abbrev QGH := L2 GradedIdx

/-- The weight of the `a`-th dressed ghost creation operator: the Jordan–Wigner sign times a
bounded boson-sector constraint symbol, supported on the configurations occupying `a`. -/
def ghostWeight (sym : ℕ → BoseConf → ℂ) (a : ℕ) : GradedIdx → ℂ :=
  fun p => if a ∈ p.2 then sym a p.1 * jwSign a p.2 else 0

/-- The reindexing of the `a`-th ghost creation operator: remove the ghost `a`. -/
def ghostShift (a : ℕ) : GradedIdx → GradedIdx := fun p => (p.1, p.2.erase a)

theorem norm_jwSign (a : ℕ) (α : FermConf) : ‖jwSign a α‖ = 1 := by
  rw [jwSign, norm_pow, norm_neg, norm_one, one_pow]

theorem ghostWeight_norm_le {sym : ℕ → BoseConf → ℂ} (hsym : ∀ a n, ‖sym a n‖ ≤ 1) (a : ℕ)
    (p : GradedIdx) : ‖ghostWeight sym a p‖ ≤ 1 := by
  rw [ghostWeight]
  split
  · rw [norm_mul, norm_jwSign, mul_one]; exact hsym a p.1
  · simp

theorem ghostShift_injOn (sym : ℕ → BoseConf → ℂ) (a : ℕ) :
    Set.InjOn (ghostShift a) {p : GradedIdx | ghostWeight sym a p ≠ 0} := by
  intro p hp q hq hpq
  have hpa : a ∈ p.2 := by
    by_contra h
    exact hp (by simp [ghostWeight, h])
  have hqa : a ∈ q.2 := by
    by_contra h
    exact hq (by simp [ghostWeight, h])
  obtain ⟨h1, h2⟩ : p.1 = q.1 ∧ p.2.erase a = q.2.erase a := by
    simpa [ghostShift, Prod.ext_iff] using hpq
  have h3 : p.2 = q.2 := by
    rw [← Finset.insert_erase hpa, ← Finset.insert_erase hqa, h2]
  exact Prod.ext h1 h3

/-- **The dressed ghost creation operator** `C_a Ψ†_a` on the completed graded space: a
bounded operator of norm at most one. -/
def brstTerm (sym : ℕ → BoseConf → ℂ) (hsym : ∀ a n, ‖sym a n‖ ≤ 1) (a : ℕ) : QGH →L[ℂ] QGH :=
  wshift (ghostWeight sym a) (ghostShift a) (ghostWeight_norm_le hsym a) (ghostShift_injOn sym a)

@[simp] theorem brstTerm_apply {sym : ℕ → BoseConf → ℂ} (hsym : ∀ a n, ‖sym a n‖ ≤ 1) (a : ℕ)
    (f : QGH) (p : GradedIdx) :
    (brstTerm sym hsym a f) p =
      (if a ∈ p.2 then sym a p.1 * jwSign a p.2 else 0) * f (p.1, p.2.erase a) := rfl

theorem brstTerm_norm_le {sym : ℕ → BoseConf → ℂ} (hsym : ∀ a n, ‖sym a n‖ ≤ 1) (a : ℕ)
    (f : QGH) : ‖brstTerm sym hsym a f‖ ≤ ‖f‖ :=
  wshift_norm_le _ _ _ _ f

/-- **The Pauli principle on the completed space**: `(C_aΨ†_a)² = 0`. -/
theorem brstTerm_comp_self {sym : ℕ → BoseConf → ℂ} (hsym : ∀ a n, ‖sym a n‖ ≤ 1) (a : ℕ)
    (f : QGH) : brstTerm sym hsym a (brstTerm sym hsym a f) = 0 := by
  ext p
  rw [brstTerm_apply]
  by_cases ha : a ∈ p.2
  · rw [if_pos ha, brstTerm_apply, if_neg (Finset.notMem_erase a p.2)]
    simp
  · rw [if_neg ha]
    simp

/-- **The anticommutation relation on the completed space**: distinct dressed ghost
creations anticommute. -/
theorem brstTerm_anticomm {sym : ℕ → BoseConf → ℂ} (hsym : ∀ a n, ‖sym a n‖ ≤ 1) {a b : ℕ}
    (hab : a ≠ b) (f : QGH) :
    brstTerm sym hsym a (brstTerm sym hsym b f) + brstTerm sym hsym b (brstTerm sym hsym a f)
      = 0 := by
  ext p
  obtain ⟨n, α⟩ := p
  simp only [lp.coeFn_add, lp.coeFn_zero, Pi.add_apply, Pi.zero_apply, brstTerm_apply]
  by_cases ha : a ∈ α
  · by_cases hb : b ∈ α
    · have hbe : b ∈ α.erase a := Finset.mem_erase.mpr ⟨(Ne.symm hab), hb⟩
      have hae : a ∈ α.erase b := Finset.mem_erase.mpr ⟨hab, ha⟩
      rw [if_pos ha, if_pos hb, if_pos hbe, if_pos hae]
      have hsw : jwSign a α * jwSign b (α.erase a) = -(jwSign b α * jwSign a (α.erase b)) :=
        jw_swap_erase hab ha hb
      have herase : (α.erase a).erase b = (α.erase b).erase a := Finset.erase_right_comm
      rw [herase]
      linear_combination (sym a n * sym b n * f (n, (α.erase b).erase a)) * hsw
    · have hbe : b ∉ α.erase a := fun h => hb (Finset.mem_of_mem_erase h)
      rw [if_pos ha, if_neg hb, if_neg hbe]
      simp
  · by_cases hb : b ∈ α
    · have hae : a ∉ α.erase b := fun h => ha (Finset.mem_of_mem_erase h)
      rw [if_neg ha, if_pos hb, if_neg hae]
      simp
    · rw [if_neg ha, if_neg hb]
      simp

/-! ## The bounded nilpotent BRST charge -/

/-- **The bounded BRST charge** on the completed graded space: the sum of the dressed ghost
creations over the book's `19` diffeomorphism ghosts. -/
def qgBrstCharge (sym : ℕ → BoseConf → ℂ) (hsym : ∀ a n, ‖sym a n‖ ≤ 1) : QGH →L[ℂ] QGH :=
  ∑ a ∈ Finset.range qgGhostModes, brstTerm sym hsym a

theorem qgBrstCharge_apply_eq_sum {sym : ℕ → BoseConf → ℂ} (hsym : ∀ a n, ‖sym a n‖ ≤ 1)
    (f : QGH) :
    qgBrstCharge sym hsym f = ∑ a ∈ Finset.range qgGhostModes, brstTerm sym hsym a f := by
  rw [qgBrstCharge, ContinuousLinearMap.sum_apply]

/-- In a complex vector space an element equal to its own negative vanishes. -/
theorem eq_zero_of_eq_neg_self {E : Type*} [NormedAddCommGroup E] [NormedSpace ℂ E] {x : E}
    (h : x = -x) : x = 0 := by
  have h2 : (2 : ℂ) • x = 0 := by
    rw [two_smul]
    nth_rewrite 2 [h]
    simp
  simpa using h2

/-- **Nilpotency of the BRST charge**, `Ω² = 0`, on the *completed* Hilbert space. -/
theorem qgBrstCharge_nilpotent {sym : ℕ → BoseConf → ℂ} (hsym : ∀ a n, ‖sym a n‖ ≤ 1)
    (f : QGH) : qgBrstCharge sym hsym (qgBrstCharge sym hsym f) = 0 := by
  classical
  have hanti : ∀ a b : ℕ, brstTerm sym hsym a (brstTerm sym hsym b f)
      + brstTerm sym hsym b (brstTerm sym hsym a f) = 0 := by
    intro a b
    by_cases hab : a = b
    · subst hab
      simp [brstTerm_comp_self hsym a f]
    · exact brstTerm_anticomm hsym hab f
  have hS : qgBrstCharge sym hsym (qgBrstCharge sym hsym f)
      = ∑ a ∈ Finset.range qgGhostModes, ∑ b ∈ Finset.range qgGhostModes,
          brstTerm sym hsym a (brstTerm sym hsym b f) := by
    rw [qgBrstCharge_apply_eq_sum, qgBrstCharge_apply_eq_sum]
    exact Finset.sum_congr rfl fun a _ => map_sum _ _ _
  rw [hS]
  refine eq_zero_of_eq_neg_self ?_
  calc ∑ a ∈ Finset.range qgGhostModes, ∑ b ∈ Finset.range qgGhostModes,
          brstTerm sym hsym a (brstTerm sym hsym b f)
      = ∑ a ∈ Finset.range qgGhostModes, ∑ b ∈ Finset.range qgGhostModes,
          -brstTerm sym hsym a (brstTerm sym hsym b f) := by
        rw [Finset.sum_comm]
        exact Finset.sum_congr rfl fun a _ => Finset.sum_congr rfl fun b _ =>
          eq_neg_of_add_eq_zero_left (hanti b a)
    _ = -∑ a ∈ Finset.range qgGhostModes, ∑ b ∈ Finset.range qgGhostModes,
          brstTerm sym hsym a (brstTerm sym hsym b f) := by
        simp

/-- The undressed (unit-symbol) BRST charge. -/
def oneSym : ℕ → BoseConf → ℂ := fun _ _ => 1

theorem oneSym_norm_le (a : ℕ) (n : BoseConf) : ‖oneSym a n‖ ≤ 1 := by simp [oneSym]

/-- The charge sends the ghost vacuum component to the one-ghost component of mode `0`. -/
theorem qgBrstCharge_one_ghost_zero (f : QGH) (n : BoseConf) :
    (qgBrstCharge oneSym oneSym_norm_le f) (n, ({0} : FermConf)) = f (n, (∅ : FermConf)) := by
  classical
  rw [qgBrstCharge_apply_eq_sum, lp.coeFn_sum, Finset.sum_apply, Finset.sum_eq_single 0]
  · rw [brstTerm_apply]
    have herase : ({0} : FermConf).erase 0 = ∅ := by simp
    rw [if_pos (by simp : (0 : ℕ) ∈ ({0} : FermConf))]
    simp only [herase, oneSym, jwSign, jwCount]
    norm_num
  · intro a _ hane
    rw [brstTerm_apply]
    have ha0 : a ∉ ({0} : FermConf) := by simpa using hane
    simp [ha0]
  · intro h
    exact absurd (Finset.mem_range.mpr (by norm_num [qgGhostModes])) h

/-- The BRST charge is **not** the zero operator: it moves the ghost vacuum over a boson
configuration into the one-ghost sector. -/
theorem qgBrstCharge_ne_zero : qgBrstCharge oneSym oneSym_norm_le ≠ 0 := by
  classical
  intro hzero
  have hval := qgBrstCharge_one_ghost_zero (lp.single 2 ((0 : BoseConf), (∅ : FermConf)) 1) 0
  rw [hzero] at hval
  simp at hval

/-! ## An explicit unitary group commuting with the charge -/

/-- The phase weight `e^{-it·E(n)}` of the boson-diagonal evolution. -/
def phaseWeight (omega : ℕ → ℝ) (t : ℝ) : GradedIdx → ℂ :=
  fun p => Complex.exp (-(t * BookProof.NavierStokesFlow.FockOfFock.confEnergy omega p.1) *
    Complex.I)

theorem phaseWeight_norm (omega : ℕ → ℝ) (t : ℝ) (p : GradedIdx) :
    ‖phaseWeight omega t p‖ = 1 := by
  rw [phaseWeight, mul_comm]
  rw [Complex.norm_exp]
  simp

theorem phaseWeight_norm_le (omega : ℕ → ℝ) (t : ℝ) (p : GradedIdx) :
    ‖phaseWeight omega t p‖ ≤ 1 := le_of_eq (phaseWeight_norm omega t p)

theorem id_injOn (omega : ℕ → ℝ) (t : ℝ) :
    Set.InjOn (id : GradedIdx → GradedIdx) {p | phaseWeight omega t p ≠ 0} :=
  fun _ _ _ _ h => h

/-- **The evolution group** on the completed graded space: multiplication by the phase
`e^{-it·E(n)}` of the boson energy.  This is the unitary group generated by the graded Fock
Hamiltonian of `ChapterQuantumGravityFock` with vanishing ghost energy. -/
def qgPhase (omega : ℕ → ℝ) (t : ℝ) : QGH →L[ℂ] QGH :=
  wshift (phaseWeight omega t) id (phaseWeight_norm_le omega t) (id_injOn omega t)

@[simp] theorem qgPhase_apply (omega : ℕ → ℝ) (t : ℝ) (f : QGH) (p : GradedIdx) :
    (qgPhase omega t f) p = phaseWeight omega t p * f p := rfl

theorem qgPhase_zero (omega : ℕ → ℝ) (f : QGH) : qgPhase omega 0 f = f := by
  ext p
  simp [phaseWeight]

theorem qgPhase_group (omega : ℕ → ℝ) (s t : ℝ) (f : QGH) :
    qgPhase omega s (qgPhase omega t f) = qgPhase omega (s + t) f := by
  ext p
  simp only [qgPhase_apply, phaseWeight, ← mul_assoc, ← Complex.exp_add]
  congr 2
  push_cast
  ring

theorem qgPhase_isometry (omega : ℕ → ℝ) (t : ℝ) (f : QGH) : ‖qgPhase omega t f‖ = ‖f‖ :=
  wshift_norm_eq _ _ _ _ (phaseWeight_norm omega t) rfl f

/-- On an occupation basis vector the group acts by the phase of the graded Fock symbol with
vanishing ghost energy — it *is* the second-quantized evolution of
`ChapterQuantumGravityFock`. -/
theorem qgPhase_single (omega : ℕ → ℝ) (t : ℝ) (p : GradedIdx) (c : ℂ) :
    qgPhase omega t (lp.single 2 p c)
      = Complex.exp (-(t * qgGradedSymbol omega (fun _ => 0) p) * Complex.I) •
          lp.single 2 p c := by
  classical
  ext q
  rw [qgPhase_apply, lp.coeFn_smul, Pi.smul_apply, smul_eq_mul]
  by_cases hq : q = p
  · subst hq
    rw [phaseWeight]
    congr 3
    rw [qgGradedSymbol]
    simp [ghostEnergy]
  · simp [lp.single_apply, hq]

/-- The evolution commutes with the BRST charge: the phase depends only on the boson
occupation, which the ghost ladder does not change. -/
theorem qgPhase_comm_brst {sym : ℕ → BoseConf → ℂ} (hsym : ∀ a n, ‖sym a n‖ ≤ 1)
    (omega : ℕ → ℝ) (t : ℝ) (f : QGH) :
    qgPhase omega t (qgBrstCharge sym hsym f) = qgBrstCharge sym hsym (qgPhase omega t f) := by
  classical
  have hterm : ∀ a : ℕ, qgPhase omega t (brstTerm sym hsym a f)
      = brstTerm sym hsym a (qgPhase omega t f) := by
    intro a
    ext p
    rw [qgPhase_apply, brstTerm_apply, brstTerm_apply, qgPhase_apply]
    rw [phaseWeight, phaseWeight]
    ring
  rw [qgBrstCharge_apply_eq_sum, qgBrstCharge_apply_eq_sum, map_sum]
  exact Finset.sum_congr rfl fun a _ => hterm a

/-! ## The ghost-energy obstruction -/

/-- The phase weight of the **full** graded Fock symbol, boson energy *plus* ghost energy. -/
def fullPhaseWeight (omega g : ℕ → ℝ) (t : ℝ) : GradedIdx → ℂ :=
  fun p => Complex.exp (-(t * qgGradedSymbol omega g p) * Complex.I)

theorem fullPhaseWeight_norm (omega g : ℕ → ℝ) (t : ℝ) (p : GradedIdx) :
    ‖fullPhaseWeight omega g t p‖ = 1 := by
  rw [fullPhaseWeight, mul_comm, Complex.norm_exp]
  simp

theorem fullPhaseWeight_norm_le (omega g : ℕ → ℝ) (t : ℝ) (p : GradedIdx) :
    ‖fullPhaseWeight omega g t p‖ ≤ 1 := le_of_eq (fullPhaseWeight_norm omega g t p)

theorem id_injOn_full (omega g : ℕ → ℝ) (t : ℝ) :
    Set.InjOn (id : GradedIdx → GradedIdx) {p | fullPhaseWeight omega g t p ≠ 0} :=
  fun _ _ _ _ h => h

/-- The evolution generated by the **full** graded Fock symbol: boson energy plus ghost
energy.  It is again a unitary group on the completed graded space. -/
def qgPhaseFull (omega g : ℕ → ℝ) (t : ℝ) : QGH →L[ℂ] QGH :=
  wshift (fullPhaseWeight omega g t) id (fullPhaseWeight_norm_le omega g t)
    (id_injOn_full omega g t)

@[simp] theorem qgPhaseFull_apply (omega g : ℕ → ℝ) (t : ℝ) (f : QGH) (p : GradedIdx) :
    (qgPhaseFull omega g t f) p = fullPhaseWeight omega g t p * f p := rfl

theorem qgPhaseFull_isometry (omega g : ℕ → ℝ) (t : ℝ) (f : QGH) :
    ‖qgPhaseFull omega g t f‖ = ‖f‖ :=
  wshift_norm_eq _ _ _ _ (fullPhaseWeight_norm omega g t) rfl f

/-- **The ghost-energy obstruction is real, not a stylistic restriction.**  If some ghost
energy is nonzero, the evolution it generates does *not* commute with the BRST charge, so
it does not descend to the BRST cohomology.  This is why the group used above carries no
ghost energy. -/
theorem qgPhaseFull_not_comm_brst (omega g : ℕ → ℝ) (hg : g 0 ≠ 0) :
    ¬ ∀ (t : ℝ) (y : QGH), qgPhaseFull omega g t (qgBrstCharge oneSym oneSym_norm_le y)
      = qgBrstCharge oneSym oneSym_norm_le (qgPhaseFull omega g t y) := by
  classical
  intro hcomm
  set t : ℝ := Real.pi / g 0 with ht
  set f : QGH := lp.single 2 ((0 : BoseConf), (∅ : FermConf)) 1 with hf
  have hfv : f ((0 : BoseConf), (∅ : FermConf)) = 1 := by
    rw [hf]; simp
  have h := congrArg (fun z : QGH => z ((0 : BoseConf), ({0} : FermConf))) (hcomm t f)
  simp only [qgPhaseFull_apply, qgBrstCharge_one_ghost_zero] at h
  rw [hfv, mul_one] at h
  -- the vacuum has zero energy, the one-ghost state has energy `g 0`
  have hg0 : ((g 0 : ℝ) : ℂ) ≠ 0 := by exact_mod_cast hg
  have hpi : ((t : ℂ) * ((g 0 : ℝ) : ℂ)) = ((Real.pi : ℝ) : ℂ) := by
    rw [ht]
    push_cast
    field_simp
  rw [fullPhaseWeight, fullPhaseWeight, qgGradedSymbol_oneGhost, qgGradedSymbol_vacuum,
    hpi] at h
  rw [show (-((Real.pi : ℝ) : ℂ)) * Complex.I = -(((Real.pi : ℝ) : ℂ) * Complex.I) by ring,
    Complex.exp_neg, Complex.exp_pi_mul_I] at h
  norm_num at h

/-! ## The join: the BRST-reduced transfer on the completed graded space -/

variable {sym : ℕ → BoseConf → ℂ} (hsym : ∀ a n, ‖sym a n‖ ≤ 1) (omega : ℕ → ℝ)

include hsym in
/-- The commutation hypothesis in the exact shape the reduction theorems consume. -/
theorem qgPhase_commutes :
    ∀ (t : ℝ) (y : QGH), qgPhase omega t (qgBrstCharge sym hsym y)
      = qgBrstCharge sym hsym (qgPhase omega t y) :=
  fun t y => qgPhase_comm_brst hsym omega t y

include hsym in
/-- The exact states are physical: the cohomology of the completed space is defined. -/
theorem qgExact_le_physical :
    exactStates (qgBrstCharge sym hsym) ≤ physicalStates (qgBrstCharge sym hsym) :=
  exactStates_le_physicalStates _ (qgBrstCharge_nilpotent hsym)

include hsym in
/-- **The §10.3 caveat, on the completed space**: the evolution maps physical (BRST-closed)
states to physical states. -/
theorem qgPhase_mem_physicalStates (t : ℝ) {x : QGH}
    (hx : x ∈ physicalStates (qgBrstCharge sym hsym)) :
    qgPhase omega t x ∈ physicalStates (qgBrstCharge sym hsym) :=
  physicalStates_invariant (Om := qgBrstCharge sym hsym) (qgPhase_commutes hsym omega t) x hx

include hsym in
/-- The evolution maps BRST-exact states to BRST-exact states. -/
theorem qgPhase_mem_exactStates (t : ℝ) {x : QGH}
    (hx : x ∈ exactStates (qgBrstCharge sym hsym)) :
    qgPhase omega t x ∈ exactStates (qgBrstCharge sym hsym) :=
  exactStates_invariant (Om := qgBrstCharge sym hsym) (qgPhase_commutes hsym omega t) x hx

/-- **The BRST-reduced transfer of §10.6.2 item 4**, now on the completed graded Hilbert
space with a genuinely bounded nilpotent charge. -/
def qgBrstTransfer (t : ℝ) :
    Cohomology (qgBrstCharge sym hsym) →ₗ[ℂ] Cohomology (qgBrstCharge sym hsym) :=
  transfer (qgBrstCharge sym hsym) (qgPhase omega) (qgPhase_commutes hsym omega) t

theorem qgBrstTransfer_zero : qgBrstTransfer hsym omega 0 = LinearMap.id :=
  transfer_zero (qgBrstCharge sym hsym) (qgPhase omega) (qgPhase_commutes hsym omega)
    (qgPhase_zero omega)

theorem qgBrstTransfer_comp (s t : ℝ) :
    (qgBrstTransfer hsym omega s).comp (qgBrstTransfer hsym omega t)
      = qgBrstTransfer hsym omega (s + t) :=
  transfer_comp (qgBrstCharge sym hsym) (qgPhase omega) (qgPhase_commutes hsym omega)
    (qgPhase_group omega) s t

theorem qgBrstTransfer_bijective (t : ℝ) : Function.Bijective (qgBrstTransfer hsym omega t) :=
  transfer_bijective (qgBrstCharge sym hsym) (qgPhase omega) (qgPhase_commutes hsym omega)
    (qgPhase_zero omega) (qgPhase_group omega) t

/-- The BRST quotient norm is preserved by the reduced transfer
(upstream `ChapterBrstReducedTransfer.infDist_exactStates_eq`, grafted).

The published thm module dropped the `include hcomm` the proof needs, so its
statement is unprovable as published AND its Open status would block this
bundle's `imported theorems must be Proved` submission gate.  Local copy with
hcomm as an explicit binder; single consumer. -/
theorem infDist_exactStates_eq {H : Type*} [NormedAddCommGroup H] [NormedSpace ℂ H]
    (Om : H →L[ℂ] H) (U : ℝ → H →L[ℂ] H)
    (hcomm : ∀ (t : ℝ) (y : H), U t (Om y) = Om (U t y))
    (hzero : ∀ x : H, U 0 x = x)
    (hgroup : ∀ (s t : ℝ) (x : H), U s (U t x) = U (s + t) x)
    (hisom : ∀ (t : ℝ) (x : H), ‖U t x‖ = ‖x‖) (t : ℝ) (x : H) :
    Metric.infDist (U t x) (exactStates Om) = Metric.infDist x (exactStates Om) := by
  have hne : (exactStates Om : Set H).Nonempty := ⟨0, (exactStates Om).zero_mem⟩
  have key : ∀ (s : ℝ) (y : H),
      Metric.infDist (U s y) (exactStates Om) ≤ Metric.infDist y (exactStates Om) := by
    intro s y
    refine le_of_forall_pos_le_add fun ε hε => ?_
    obtain ⟨z, hz, hdz⟩ := (Metric.infDist_lt_iff hne).1
      (by linarith [Metric.infDist_nonneg (x := y) (s := (exactStates Om : Set H))] :
        Metric.infDist y (exactStates Om) < Metric.infDist y (exactStates Om) + ε)
    have hd : dist (U s y) (U s z) = dist y z := by
      simp [dist_eq_norm, ← map_sub, hisom]
    calc Metric.infDist (U s y) (exactStates Om)
        ≤ dist (U s y) (U s z) :=
          Metric.infDist_le_dist_of_mem (exactStates_invariant (hcomm s) z hz)
      _ = dist y z := hd
      _ ≤ Metric.infDist y (exactStates Om) + ε := le_of_lt hdz
  refine le_antisymm (key t x) ?_
  have hback := key (-t) (U t x)
  rwa [hgroup, neg_add_cancel, hzero] at hback

/-- **The BRST (quotient) norm is preserved** by the reduced transfer. -/
theorem qgBrstTransfer_infDist (t : ℝ) (x : QGH) :
    Metric.infDist (qgPhase omega t x) (exactStates (qgBrstCharge sym hsym))
      = Metric.infDist x (exactStates (qgBrstCharge sym hsym)) :=
  infDist_exactStates_eq (qgBrstCharge sym hsym) (qgPhase omega) (qgPhase_commutes hsym omega)
    (qgPhase_zero omega) (qgPhase_group omega) (qgPhase_isometry omega) t x

end

end BookProof.QgBrstCompleted