Physlib.QFT.PerturbationTheory.WickAlgebra.NormalOrder.Lemmas

Imports

/-
Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Joseph Tooby-Smith
-/
module

public import Physlib.QFT.PerturbationTheory.WickAlgebra.NormalOrder.Basic
public import Physlib.QFT.PerturbationTheory.WickAlgebra.SuperCommute

Basic properties of normal ordering

@[expose] public section

Properties of normal ordering.

              lemma normalOrder_eq_ι_normalOrderF (a : 𝓕.FieldOpFreeAlgebra) :
    𝓝(ι a) = ι 𝓝ᶠ(a) := rfl

lemma normalOrder_ofCrAnList (φs : List 𝓕.CrAnFieldOp) :
    𝓝(ofCrAnList φs) = normalOrderSign φs • ofCrAnList (normalOrderList φs) := by𝓕:FieldSpecificationφs:List 𝓕.CrAnFieldOp⊢ normalOrder (ofCrAnList φs) = normalOrderSign φs • ofCrAnList (normalOrderList φs)
  rw [ofCrAnList,𝓕:FieldSpecificationφs:List 𝓕.CrAnFieldOp⊢ normalOrder (ι (ofCrAnListF φs)) = normalOrderSign φs • ofCrAnList (normalOrderList φs)𝓕:FieldSpecificationφs:List 𝓕.CrAnFieldOp⊢ ι (normalOrderSign φs • ofCrAnListF (normalOrderList φs)) = normalOrderSign φs • ofCrAnList (normalOrderList φs) normalOrder_eq_ι_normalOrderF,𝓕:FieldSpecificationφs:List 𝓕.CrAnFieldOp⊢ ι (normalOrderF (ofCrAnListF φs)) = normalOrderSign φs • ofCrAnList (normalOrderList φs)𝓕:FieldSpecificationφs:List 𝓕.CrAnFieldOp⊢ ι (normalOrderSign φs • ofCrAnListF (normalOrderList φs)) = normalOrderSign φs • ofCrAnList (normalOrderList φs) normalOrderF_ofCrAnListF𝓕:FieldSpecificationφs:List 𝓕.CrAnFieldOp⊢ ι (normalOrderSign φs • ofCrAnListF (normalOrderList φs)) = normalOrderSign φs • ofCrAnList (normalOrderList φs)𝓕:FieldSpecificationφs:List 𝓕.CrAnFieldOp⊢ ι (normalOrderSign φs • ofCrAnListF (normalOrderList φs)) = normalOrderSign φs • ofCrAnList (normalOrderList φs)]𝓕:FieldSpecificationφs:List 𝓕.CrAnFieldOp⊢ ι (normalOrderSign φs • ofCrAnListF (normalOrderList φs)) = normalOrderSign φs • ofCrAnList (normalOrderList φs)
  rflAll goals completed! 🐙

@[simp]
lemma normalOrder_one_eq_one : normalOrder (𝓕 := 𝓕) 1 = 1 := by𝓕:FieldSpecification⊢ normalOrder 1 = 1
  have h1 : 1 = ofCrAnList (𝓕 := 𝓕) [] := by simp [ofCrAnList]𝓕:FieldSpecificationh1:1 = ofCrAnList []⊢ normalOrder 1 = 1𝓕:FieldSpecificationh1:1 = ofCrAnList []⊢ normalOrder 1 = 1
  rw [h1𝓕:FieldSpecificationh1:1 = ofCrAnList []⊢ normalOrder (ofCrAnList []) = ofCrAnList []𝓕:FieldSpecificationh1:1 = ofCrAnList []⊢ normalOrder (ofCrAnList []) = ofCrAnList []]𝓕:FieldSpecificationh1:1 = ofCrAnList []⊢ normalOrder (ofCrAnList []) = ofCrAnList []
  rw [normalOrder_ofCrAnList𝓕:FieldSpecificationh1:1 = ofCrAnList []⊢ normalOrderSign [] • ofCrAnList (normalOrderList []) = ofCrAnList []𝓕:FieldSpecificationh1:1 = ofCrAnList []⊢ normalOrderSign [] • ofCrAnList (normalOrderList []) = ofCrAnList []]𝓕:FieldSpecificationh1:1 = ofCrAnList []⊢ normalOrderSign [] • ofCrAnList (normalOrderList []) = ofCrAnList []
  simpAll goals completed! 🐙

@[simp]
lemma normalOrder_ofFieldOpList_nil : normalOrder (𝓕 := 𝓕) (ofFieldOpList []) = 1 := by𝓕:FieldSpecification⊢ normalOrder (ofFieldOpList []) = 1
  rw [ofFieldOpList𝓕:FieldSpecification⊢ normalOrder (ι (ofFieldOpListF [])) = 1𝓕:FieldSpecification⊢ normalOrder (ι (ofFieldOpListF [])) = 1]𝓕:FieldSpecification⊢ normalOrder (ι (ofFieldOpListF [])) = 1
  rw [normalOrder_eq_ι_normalOrderF𝓕:FieldSpecification⊢ ι (normalOrderF (ofFieldOpListF [])) = 1𝓕:FieldSpecification⊢ ι (normalOrderF (ofFieldOpListF [])) = 1]𝓕:FieldSpecification⊢ ι (normalOrderF (ofFieldOpListF [])) = 1
  simp only [ofFieldOpListF_nil]𝓕:FieldSpecification⊢ ι (normalOrderF 1) = 1
  change normalOrder (𝓕 := 𝓕) 1 = _𝓕:FieldSpecification⊢ normalOrder 1 = 1
  simpAll goals completed! 🐙

@[simp]
lemma normalOrder_ofCrAnList_nil : normalOrder (𝓕 := 𝓕) (ofCrAnList []) = 1 := by𝓕:FieldSpecification⊢ normalOrder (ofCrAnList []) = 1
  rw [normalOrder_ofCrAnList𝓕:FieldSpecification⊢ normalOrderSign [] • ofCrAnList (normalOrderList []) = 1𝓕:FieldSpecification⊢ normalOrderSign [] • ofCrAnList (normalOrderList []) = 1]𝓕:FieldSpecification⊢ normalOrderSign [] • ofCrAnList (normalOrderList []) = 1
  simp only [normalOrderSign_nil, normalOrderList_nil, ofCrAnList_nil]𝓕:FieldSpecification⊢ 1 • 1 = 1
  moduleAll goals completed! 🐙lemma ofCrAnList_eq_normalOrder (φs : List 𝓕.CrAnFieldOp) :
    ofCrAnList (normalOrderList φs) = normalOrderSign φs • 𝓝(ofCrAnList φs) := by𝓕:FieldSpecificationφs:List 𝓕.CrAnFieldOp⊢ ofCrAnList (normalOrderList φs) = normalOrderSign φs • normalOrder (ofCrAnList φs)
  erw [normalOrder_ofCrAnList,𝓕:FieldSpecificationφs:List 𝓕.CrAnFieldOp⊢ ofCrAnList (normalOrderList φs) = normalOrderSign φs • normalOrderSign φs • ofCrAnList (normalOrderList φs) smul_smul,𝓕:FieldSpecificationφs:List 𝓕.CrAnFieldOp⊢ ofCrAnList (normalOrderList φs) = (normalOrderSign φs * normalOrderSign φs) • ofCrAnList (normalOrderList φs) normalOrderSign,𝓕:FieldSpecificationφs:List 𝓕.CrAnFieldOp⊢ ofCrAnList (normalOrderList φs) =
  (Wick.koszulSign 𝓕.crAnStatistics normalOrderRel φs * Wick.koszulSign 𝓕.crAnStatistics normalOrderRel φs) •
    ofCrAnList (normalOrderList φs) Wick.koszulSign_mul_self,𝓕:FieldSpecificationφs:List 𝓕.CrAnFieldOp⊢ ofCrAnList (normalOrderList φs) = 1 • ofCrAnList (normalOrderList φs)
    one_smul𝓕:FieldSpecificationφs:List 𝓕.CrAnFieldOp⊢ ofCrAnList (normalOrderList φs) = ofCrAnList (normalOrderList φs)]All goals completed! 🐙

lemma normalOrder_normalOrder_mid (a b c : 𝓕.WickAlgebra) :
    𝓝(a * b * c) = 𝓝(a * 𝓝(b) * c) := by𝓕:FieldSpecificationa:𝓕.WickAlgebrab:𝓕.WickAlgebrac:𝓕.WickAlgebra⊢ normalOrder (a * b * c) = normalOrder (a * normalOrder b * c)
  obtain ⟨a, rfl⟩ := ι_surjective a𝓕:FieldSpecificationb:𝓕.WickAlgebrac:𝓕.WickAlgebraa:𝓕.FieldOpFreeAlgebra⊢ normalOrder (ι a * b * c) = normalOrder (ι a * normalOrder b * c)
  obtain ⟨b, rfl⟩ := ι_surjective b𝓕:FieldSpecificationc:𝓕.WickAlgebraa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebra⊢ normalOrder (ι a * ι b * c) = normalOrder (ι a * normalOrder (ι b) * c)
  obtain ⟨c, rfl⟩ := ι_surjective c𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebra⊢ normalOrder (ι a * ι b * ι c) = normalOrder (ι a * normalOrder (ι b) * ι c)
  rw [normalOrder_eq_ι_normalOrderF𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebra⊢ normalOrder (ι a * ι b * ι c) = normalOrder (ι a * ι (normalOrderF b) * ι c)𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebra⊢ normalOrder (ι a * ι b * ι c) = normalOrder (ι a * ι (normalOrderF b) * ι c)]𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebra⊢ normalOrder (ι a * ι b * ι c) = normalOrder (ι a * ι (normalOrderF b) * ι c)
  simp only [← map_mul]𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebra⊢ normalOrder (ι (a * b * c)) = normalOrder (ι (a * normalOrderF b * c))
  rw [normalOrder_eq_ι_normalOrderF𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebra⊢ ι (normalOrderF (a * b * c)) = normalOrder (ι (a * normalOrderF b * c))𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebra⊢ ι (normalOrderF (a * b * c)) = normalOrder (ι (a * normalOrderF b * c))]𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebra⊢ ι (normalOrderF (a * b * c)) = normalOrder (ι (a * normalOrderF b * c))
  rw [normalOrderF_normalOrderF_mid𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebra⊢ ι (normalOrderF (a * normalOrderF b * c)) = normalOrder (ι (a * normalOrderF b * c))𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebra⊢ ι (normalOrderF (a * normalOrderF b * c)) = normalOrder (ι (a * normalOrderF b * c))]𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebra⊢ ι (normalOrderF (a * normalOrderF b * c)) = normalOrder (ι (a * normalOrderF b * c))
  rflAll goals completed! 🐙

lemma normalOrder_normalOrder_left (a b : 𝓕.WickAlgebra) :
    𝓝(a * b) = 𝓝(𝓝(a) * b) := by𝓕:FieldSpecificationa:𝓕.WickAlgebrab:𝓕.WickAlgebra⊢ normalOrder (a * b) = normalOrder (normalOrder a * b)
  obtain ⟨a, rfl⟩ := ι_surjective a𝓕:FieldSpecificationb:𝓕.WickAlgebraa:𝓕.FieldOpFreeAlgebra⊢ normalOrder (ι a * b) = normalOrder (normalOrder (ι a) * b)
  obtain ⟨b, rfl⟩ := ι_surjective b𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebra⊢ normalOrder (ι a * ι b) = normalOrder (normalOrder (ι a) * ι b)
  rw [normalOrder_eq_ι_normalOrderF𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebra⊢ normalOrder (ι a * ι b) = normalOrder (ι (normalOrderF a) * ι b)𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebra⊢ normalOrder (ι a * ι b) = normalOrder (ι (normalOrderF a) * ι b)]𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebra⊢ normalOrder (ι a * ι b) = normalOrder (ι (normalOrderF a) * ι b)
  simp only [← map_mul]𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebra⊢ normalOrder (ι (a * b)) = normalOrder (ι (normalOrderF a * b))
  rw [normalOrder_eq_ι_normalOrderF𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebra⊢ ι (normalOrderF (a * b)) = normalOrder (ι (normalOrderF a * b))𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebra⊢ ι (normalOrderF (a * b)) = normalOrder (ι (normalOrderF a * b))]𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebra⊢ ι (normalOrderF (a * b)) = normalOrder (ι (normalOrderF a * b))
  rw [normalOrderF_normalOrderF_left𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebra⊢ ι (normalOrderF (normalOrderF a * b)) = normalOrder (ι (normalOrderF a * b))𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebra⊢ ι (normalOrderF (normalOrderF a * b)) = normalOrder (ι (normalOrderF a * b))]𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebra⊢ ι (normalOrderF (normalOrderF a * b)) = normalOrder (ι (normalOrderF a * b))
  rflAll goals completed! 🐙

lemma normalOrder_normalOrder_right (a b : 𝓕.WickAlgebra) :
    𝓝(a * b) = 𝓝(a * 𝓝(b)) := by𝓕:FieldSpecificationa:𝓕.WickAlgebrab:𝓕.WickAlgebra⊢ normalOrder (a * b) = normalOrder (a * normalOrder b)
  obtain ⟨a, rfl⟩ := ι_surjective a𝓕:FieldSpecificationb:𝓕.WickAlgebraa:𝓕.FieldOpFreeAlgebra⊢ normalOrder (ι a * b) = normalOrder (ι a * normalOrder b)
  obtain ⟨b, rfl⟩ := ι_surjective b𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebra⊢ normalOrder (ι a * ι b) = normalOrder (ι a * normalOrder (ι b))
  rw [normalOrder_eq_ι_normalOrderF𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebra⊢ normalOrder (ι a * ι b) = normalOrder (ι a * ι (normalOrderF b))𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebra⊢ normalOrder (ι a * ι b) = normalOrder (ι a * ι (normalOrderF b))]𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebra⊢ normalOrder (ι a * ι b) = normalOrder (ι a * ι (normalOrderF b))
  simp only [← map_mul]𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebra⊢ normalOrder (ι (a * b)) = normalOrder (ι (a * normalOrderF b))
  rw [normalOrder_eq_ι_normalOrderF𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebra⊢ ι (normalOrderF (a * b)) = normalOrder (ι (a * normalOrderF b))𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebra⊢ ι (normalOrderF (a * b)) = normalOrder (ι (a * normalOrderF b))]𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebra⊢ ι (normalOrderF (a * b)) = normalOrder (ι (a * normalOrderF b))
  rw [normalOrderF_normalOrderF_right𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebra⊢ ι (normalOrderF (a * normalOrderF b)) = normalOrder (ι (a * normalOrderF b))𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebra⊢ ι (normalOrderF (a * normalOrderF b)) = normalOrder (ι (a * normalOrderF b))]𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebra⊢ ι (normalOrderF (a * normalOrderF b)) = normalOrder (ι (a * normalOrderF b))
  rflAll goals completed! 🐙

lemma normalOrder_normalOrder (a : 𝓕.WickAlgebra) : 𝓝(𝓝(a)) = 𝓝(a) := by𝓕:FieldSpecificationa:𝓕.WickAlgebra⊢ normalOrder (normalOrder a) = normalOrder a
  trans 𝓝(𝓝(a) * 1)𝓕:FieldSpecificationa:𝓕.WickAlgebra⊢ normalOrder (normalOrder a) = normalOrder (normalOrder a * 1)𝓕:FieldSpecificationa:𝓕.WickAlgebra⊢ normalOrder (normalOrder a * 1) = normalOrder a
  ·𝓕:FieldSpecificationa:𝓕.WickAlgebra⊢ normalOrder (normalOrder a) = normalOrder (normalOrder a * 1) simpAll goals completed! 🐙
  ·𝓕:FieldSpecificationa:𝓕.WickAlgebra⊢ normalOrder (normalOrder a * 1) = normalOrder a rw [← normalOrder_normalOrder_left𝓕:FieldSpecificationa:𝓕.WickAlgebra⊢ normalOrder (a * 1) = normalOrder a𝓕:FieldSpecificationa:𝓕.WickAlgebra⊢ normalOrder (a * 1) = normalOrder a]𝓕:FieldSpecificationa:𝓕.WickAlgebra⊢ normalOrder (a * 1) = normalOrder a
    simpAll goals completed! 🐙

mul anpart and crpart



lemma normalOrder_mul_anPart (φ : 𝓕.FieldOp) (a : 𝓕.WickAlgebra) :
    𝓝(a * anPart φ) = 𝓝(a) * anPart φ := by𝓕:FieldSpecificationφ:𝓕.FieldOpa:𝓕.WickAlgebra⊢ normalOrder (a * anPart φ) = normalOrder a * anPart φ
  obtain ⟨a, rfl⟩ := ι_surjective a𝓕:FieldSpecificationφ:𝓕.FieldOpa:𝓕.FieldOpFreeAlgebra⊢ normalOrder (ι a * anPart φ) = normalOrder (ι a) * anPart φ
  rw [anPart,𝓕:FieldSpecificationφ:𝓕.FieldOpa:𝓕.FieldOpFreeAlgebra⊢ normalOrder (ι a * ι (anPartF φ)) = normalOrder (ι a) * ι (anPartF φ)𝓕:FieldSpecificationφ:𝓕.FieldOpa:𝓕.FieldOpFreeAlgebra⊢ ι (normalOrderF a * anPartF φ) = normalOrder (ι a) * ι (anPartF φ) ← map_mul,𝓕:FieldSpecificationφ:𝓕.FieldOpa:𝓕.FieldOpFreeAlgebra⊢ normalOrder (ι (a * anPartF φ)) = normalOrder (ι a) * ι (anPartF φ)𝓕:FieldSpecificationφ:𝓕.FieldOpa:𝓕.FieldOpFreeAlgebra⊢ ι (normalOrderF a * anPartF φ) = normalOrder (ι a) * ι (anPartF φ) normalOrder_eq_ι_normalOrderF,𝓕:FieldSpecificationφ:𝓕.FieldOpa:𝓕.FieldOpFreeAlgebra⊢ ι (normalOrderF (a * anPartF φ)) = normalOrder (ι a) * ι (anPartF φ)𝓕:FieldSpecificationφ:𝓕.FieldOpa:𝓕.FieldOpFreeAlgebra⊢ ι (normalOrderF a * anPartF φ) = normalOrder (ι a) * ι (anPartF φ) normalOrderF_mul_anPartF𝓕:FieldSpecificationφ:𝓕.FieldOpa:𝓕.FieldOpFreeAlgebra⊢ ι (normalOrderF a * anPartF φ) = normalOrder (ι a) * ι (anPartF φ)𝓕:FieldSpecificationφ:𝓕.FieldOpa:𝓕.FieldOpFreeAlgebra⊢ ι (normalOrderF a * anPartF φ) = normalOrder (ι a) * ι (anPartF φ)]𝓕:FieldSpecificationφ:𝓕.FieldOpa:𝓕.FieldOpFreeAlgebra⊢ ι (normalOrderF a * anPartF φ) = normalOrder (ι a) * ι (anPartF φ)
  rflAll goals completed! 🐙



lemma crPart_mul_normalOrder (φ : 𝓕.FieldOp) (a : 𝓕.WickAlgebra) :
    𝓝(crPart φ * a) = crPart φ * 𝓝(a) := by𝓕:FieldSpecificationφ:𝓕.FieldOpa:𝓕.WickAlgebra⊢ normalOrder (crPart φ * a) = crPart φ * normalOrder a
  obtain ⟨a, rfl⟩ := ι_surjective a𝓕:FieldSpecificationφ:𝓕.FieldOpa:𝓕.FieldOpFreeAlgebra⊢ normalOrder (crPart φ * ι a) = crPart φ * normalOrder (ι a)
  rw [crPart,𝓕:FieldSpecificationφ:𝓕.FieldOpa:𝓕.FieldOpFreeAlgebra⊢ normalOrder (ι (crPartF φ) * ι a) = ι (crPartF φ) * normalOrder (ι a)𝓕:FieldSpecificationφ:𝓕.FieldOpa:𝓕.FieldOpFreeAlgebra⊢ ι (crPartF φ * normalOrderF a) = ι (crPartF φ) * normalOrder (ι a) ← map_mul,𝓕:FieldSpecificationφ:𝓕.FieldOpa:𝓕.FieldOpFreeAlgebra⊢ normalOrder (ι (crPartF φ * a)) = ι (crPartF φ) * normalOrder (ι a)𝓕:FieldSpecificationφ:𝓕.FieldOpa:𝓕.FieldOpFreeAlgebra⊢ ι (crPartF φ * normalOrderF a) = ι (crPartF φ) * normalOrder (ι a) normalOrder_eq_ι_normalOrderF,𝓕:FieldSpecificationφ:𝓕.FieldOpa:𝓕.FieldOpFreeAlgebra⊢ ι (normalOrderF (crPartF φ * a)) = ι (crPartF φ) * normalOrder (ι a)𝓕:FieldSpecificationφ:𝓕.FieldOpa:𝓕.FieldOpFreeAlgebra⊢ ι (crPartF φ * normalOrderF a) = ι (crPartF φ) * normalOrder (ι a) normalOrderF_crPartF_mul𝓕:FieldSpecificationφ:𝓕.FieldOpa:𝓕.FieldOpFreeAlgebra⊢ ι (crPartF φ * normalOrderF a) = ι (crPartF φ) * normalOrder (ι a)𝓕:FieldSpecificationφ:𝓕.FieldOpa:𝓕.FieldOpFreeAlgebra⊢ ι (crPartF φ * normalOrderF a) = ι (crPartF φ) * normalOrder (ι a)]𝓕:FieldSpecificationφ:𝓕.FieldOpa:𝓕.FieldOpFreeAlgebra⊢ ι (crPartF φ * normalOrderF a) = ι (crPartF φ) * normalOrder (ι a)
  rflAll goals completed! 🐙

Normal order and super commutes

For a field specification 𝓕, and a and b in 𝓕.WickAlgebra the normal ordering of the super commutator of a and b vanishes, i.e. 𝓝([a,b]ₛ) = 0.


@[simp]
lemma normalOrder_superCommute_eq_zero (a b : 𝓕.WickAlgebra) :
    𝓝([a, b]ₛ) = 0 := by𝓕:FieldSpecificationa:𝓕.WickAlgebrab:𝓕.WickAlgebra⊢ normalOrder ((superCommute a) b) = 0
  obtain ⟨a, rfl⟩ := ι_surjective a𝓕:FieldSpecificationb:𝓕.WickAlgebraa:𝓕.FieldOpFreeAlgebra⊢ normalOrder ((superCommute (ι a)) b) = 0
  obtain ⟨b, rfl⟩ := ι_surjective b𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebra⊢ normalOrder ((superCommute (ι a)) (ι b)) = 0
  rw [superCommute_eq_ι_superCommuteF,𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebra⊢ normalOrder (ι ((superCommuteF a) b)) = 0𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebra⊢ ι (normalOrderF ((superCommuteF a) b)) = 0 normalOrder_eq_ι_normalOrderF𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebra⊢ ι (normalOrderF ((superCommuteF a) b)) = 0𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebra⊢ ι (normalOrderF ((superCommuteF a) b)) = 0]𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebra⊢ ι (normalOrderF ((superCommuteF a) b)) = 0
  simpAll goals completed! 🐙

              

@[simp]
lemma normalOrder_superCommute_left_eq_zero (a b c: 𝓕.WickAlgebra) :
    𝓝([a, b]ₛ * c) = 0 := by𝓕:FieldSpecificationa:𝓕.WickAlgebrab:𝓕.WickAlgebrac:𝓕.WickAlgebra⊢ normalOrder ((superCommute a) b * c) = 0
  obtain ⟨a, rfl⟩ := ι_surjective a𝓕:FieldSpecificationb:𝓕.WickAlgebrac:𝓕.WickAlgebraa:𝓕.FieldOpFreeAlgebra⊢ normalOrder ((superCommute (ι a)) b * c) = 0
  obtain ⟨b, rfl⟩ := ι_surjective b𝓕:FieldSpecificationc:𝓕.WickAlgebraa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebra⊢ normalOrder ((superCommute (ι a)) (ι b) * c) = 0
  obtain ⟨c, rfl⟩ := ι_surjective c𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebra⊢ normalOrder ((superCommute (ι a)) (ι b) * ι c) = 0
  rw [superCommute_eq_ι_superCommuteF,𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebra⊢ normalOrder (ι ((superCommuteF a) b) * ι c) = 0𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebra⊢ ι (normalOrderF ((superCommuteF a) b * c)) = 0 ← map_mul,𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebra⊢ normalOrder (ι ((superCommuteF a) b * c)) = 0𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebra⊢ ι (normalOrderF ((superCommuteF a) b * c)) = 0 normalOrder_eq_ι_normalOrderF𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebra⊢ ι (normalOrderF ((superCommuteF a) b * c)) = 0𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebra⊢ ι (normalOrderF ((superCommuteF a) b * c)) = 0]𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebra⊢ ι (normalOrderF ((superCommuteF a) b * c)) = 0
  simpAll goals completed! 🐙

@[simp]
lemma normalOrder_superCommute_right_eq_zero (a b c: 𝓕.WickAlgebra) :
    𝓝(c * [a, b]ₛ) = 0 := by𝓕:FieldSpecificationa:𝓕.WickAlgebrab:𝓕.WickAlgebrac:𝓕.WickAlgebra⊢ normalOrder (c * (superCommute a) b) = 0
  obtain ⟨a, rfl⟩ := ι_surjective a𝓕:FieldSpecificationb:𝓕.WickAlgebrac:𝓕.WickAlgebraa:𝓕.FieldOpFreeAlgebra⊢ normalOrder (c * (superCommute (ι a)) b) = 0
  obtain ⟨b, rfl⟩ := ι_surjective b𝓕:FieldSpecificationc:𝓕.WickAlgebraa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebra⊢ normalOrder (c * (superCommute (ι a)) (ι b)) = 0
  obtain ⟨c, rfl⟩ := ι_surjective c𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebra⊢ normalOrder (ι c * (superCommute (ι a)) (ι b)) = 0
  rw [superCommute_eq_ι_superCommuteF,𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebra⊢ normalOrder (ι c * ι ((superCommuteF a) b)) = 0𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebra⊢ ι (normalOrderF (c * (superCommuteF a) b)) = 0 ← map_mul,𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebra⊢ normalOrder (ι (c * (superCommuteF a) b)) = 0𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebra⊢ ι (normalOrderF (c * (superCommuteF a) b)) = 0 normalOrder_eq_ι_normalOrderF𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebra⊢ ι (normalOrderF (c * (superCommuteF a) b)) = 0𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebra⊢ ι (normalOrderF (c * (superCommuteF a) b)) = 0]𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebra⊢ ι (normalOrderF (c * (superCommuteF a) b)) = 0
  simpAll goals completed! 🐙

@[simp]
lemma normalOrder_superCommute_mid_eq_zero (a b c d : 𝓕.WickAlgebra) :
    𝓝(a * [c, d]ₛ * b) = 0 := by𝓕:FieldSpecificationa:𝓕.WickAlgebrab:𝓕.WickAlgebrac:𝓕.WickAlgebrad:𝓕.WickAlgebra⊢ normalOrder (a * (superCommute c) d * b) = 0
  obtain ⟨a, rfl⟩ := ι_surjective a𝓕:FieldSpecificationb:𝓕.WickAlgebrac:𝓕.WickAlgebrad:𝓕.WickAlgebraa:𝓕.FieldOpFreeAlgebra⊢ normalOrder (ι a * (superCommute c) d * b) = 0
  obtain ⟨b, rfl⟩ := ι_surjective b𝓕:FieldSpecificationc:𝓕.WickAlgebrad:𝓕.WickAlgebraa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebra⊢ normalOrder (ι a * (superCommute c) d * ι b) = 0
  obtain ⟨c, rfl⟩ := ι_surjective c𝓕:FieldSpecificationd:𝓕.WickAlgebraa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebra⊢ normalOrder (ι a * (superCommute (ι c)) d * ι b) = 0
  obtain ⟨d, rfl⟩ := ι_surjective d𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebrad:𝓕.FieldOpFreeAlgebra⊢ normalOrder (ι a * (superCommute (ι c)) (ι d) * ι b) = 0
  rw [superCommute_eq_ι_superCommuteF,𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebrad:𝓕.FieldOpFreeAlgebra⊢ normalOrder (ι a * ι ((superCommuteF c) d) * ι b) = 0𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebrad:𝓕.FieldOpFreeAlgebra⊢ ι (normalOrderF (a * (superCommuteF c) d * b)) = 0 ← map_mul,𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebrad:𝓕.FieldOpFreeAlgebra⊢ normalOrder (ι (a * (superCommuteF c) d) * ι b) = 0𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebrad:𝓕.FieldOpFreeAlgebra⊢ ι (normalOrderF (a * (superCommuteF c) d * b)) = 0 ← map_mul,𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebrad:𝓕.FieldOpFreeAlgebra⊢ normalOrder (ι (a * (superCommuteF c) d * b)) = 0𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebrad:𝓕.FieldOpFreeAlgebra⊢ ι (normalOrderF (a * (superCommuteF c) d * b)) = 0 normalOrder_eq_ι_normalOrderF𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebrad:𝓕.FieldOpFreeAlgebra⊢ ι (normalOrderF (a * (superCommuteF c) d * b)) = 0𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebrad:𝓕.FieldOpFreeAlgebra⊢ ι (normalOrderF (a * (superCommuteF c) d * b)) = 0]𝓕:FieldSpecificationa:𝓕.FieldOpFreeAlgebrab:𝓕.FieldOpFreeAlgebrac:𝓕.FieldOpFreeAlgebrad:𝓕.FieldOpFreeAlgebra⊢ ι (normalOrderF (a * (superCommuteF c) d * b)) = 0
  simpAll goals completed! 🐙

Swapping terms in a normal order.

              

lemma normalOrder_ofFieldOp_ofFieldOp_swap (φ φ' : 𝓕.FieldOp) :
    𝓝(ofFieldOp φ * ofFieldOp φ') = 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') • 𝓝(ofFieldOp φ' * ofFieldOp φ) := by𝓕:FieldSpecificationφ:𝓕.FieldOpφ':𝓕.FieldOp⊢ normalOrder (ofFieldOp φ * ofFieldOp φ') = (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛφ') • normalOrder (ofFieldOp φ' * ofFieldOp φ)
  rw [ofFieldOp_mul_ofFieldOp_eq_superCommute𝓕:FieldSpecificationφ:𝓕.FieldOpφ':𝓕.FieldOp⊢ normalOrder
    ((exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛφ') • ofFieldOp φ' * ofFieldOp φ + (superCommute (ofFieldOp φ)) (ofFieldOp φ')) =
  (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛφ') • normalOrder (ofFieldOp φ' * ofFieldOp φ)𝓕:FieldSpecificationφ:𝓕.FieldOpφ':𝓕.FieldOp⊢ normalOrder
    ((exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛφ') • ofFieldOp φ' * ofFieldOp φ + (superCommute (ofFieldOp φ)) (ofFieldOp φ')) =
  (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛφ') • normalOrder (ofFieldOp φ' * ofFieldOp φ)]𝓕:FieldSpecificationφ:𝓕.FieldOpφ':𝓕.FieldOp⊢ normalOrder
    ((exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛφ') • ofFieldOp φ' * ofFieldOp φ + (superCommute (ofFieldOp φ)) (ofFieldOp φ')) =
  (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛφ') • normalOrder (ofFieldOp φ' * ofFieldOp φ)
  simpAll goals completed! 🐙

lemma normalOrder_ofCrAnOp_ofCrAnList (φ : 𝓕.CrAnFieldOp)
    (φs : List 𝓕.CrAnFieldOp) : 𝓝(ofCrAnOp φ * ofCrAnList φs) =
    𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φs) • 𝓝(ofCrAnList φs * ofCrAnOp φ) := by𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpφs:List 𝓕.CrAnFieldOp⊢ normalOrder (ofCrAnOp φ * ofCrAnList φs) =
  (exchangeSign (𝓕.crAnStatistics φ)) (ofList 𝓕.crAnStatistics φs) • normalOrder (ofCrAnList φs * ofCrAnOp φ)
  rw [← ofCrAnList_singleton,𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpφs:List 𝓕.CrAnFieldOp⊢ normalOrder (ofCrAnList [φ] * ofCrAnList φs) =
  (exchangeSign (𝓕.crAnStatistics φ)) (ofList 𝓕.crAnStatistics φs) • normalOrder (ofCrAnList φs * ofCrAnList [φ])𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpφs:List 𝓕.CrAnFieldOp⊢ normalOrder
    ((exchangeSign (ofList 𝓕.crAnStatistics [φ])) (ofList 𝓕.crAnStatistics φs) • ofCrAnList φs * ofCrAnList [φ] +
      (superCommute (ofCrAnList [φ])) (ofCrAnList φs)) =
  (exchangeSign (𝓕.crAnStatistics φ)) (ofList 𝓕.crAnStatistics φs) • normalOrder (ofCrAnList φs * ofCrAnList [φ]) ofCrAnList_mul_ofCrAnList_eq_superCommute𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpφs:List 𝓕.CrAnFieldOp⊢ normalOrder
    ((exchangeSign (ofList 𝓕.crAnStatistics [φ])) (ofList 𝓕.crAnStatistics φs) • ofCrAnList φs * ofCrAnList [φ] +
      (superCommute (ofCrAnList [φ])) (ofCrAnList φs)) =
  (exchangeSign (𝓕.crAnStatistics φ)) (ofList 𝓕.crAnStatistics φs) • normalOrder (ofCrAnList φs * ofCrAnList [φ])𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpφs:List 𝓕.CrAnFieldOp⊢ normalOrder
    ((exchangeSign (ofList 𝓕.crAnStatistics [φ])) (ofList 𝓕.crAnStatistics φs) • ofCrAnList φs * ofCrAnList [φ] +
      (superCommute (ofCrAnList [φ])) (ofCrAnList φs)) =
  (exchangeSign (𝓕.crAnStatistics φ)) (ofList 𝓕.crAnStatistics φs) • normalOrder (ofCrAnList φs * ofCrAnList [φ])]𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpφs:List 𝓕.CrAnFieldOp⊢ normalOrder
    ((exchangeSign (ofList 𝓕.crAnStatistics [φ])) (ofList 𝓕.crAnStatistics φs) • ofCrAnList φs * ofCrAnList [φ] +
      (superCommute (ofCrAnList [φ])) (ofCrAnList φs)) =
  (exchangeSign (𝓕.crAnStatistics φ)) (ofList 𝓕.crAnStatistics φs) • normalOrder (ofCrAnList φs * ofCrAnList [φ])
  simpAll goals completed! 🐙

lemma normalOrder_ofCrAnOp_ofFieldOpList_swap (φ : 𝓕.CrAnFieldOp) (φ' : List 𝓕.FieldOp) :
    𝓝(ofCrAnOp φ * ofFieldOpList φ') = 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') •
    𝓝(ofFieldOpList φ' * ofCrAnOp φ) := by𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpφ':List 𝓕.FieldOp⊢ normalOrder (ofCrAnOp φ * ofFieldOpList φ') =
  (exchangeSign (𝓕.crAnStatistics φ)) (ofList 𝓕.fieldOpStatistic φ') • normalOrder (ofFieldOpList φ' * ofCrAnOp φ)
  rw [← ofCrAnList_singleton,𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpφ':List 𝓕.FieldOp⊢ normalOrder (ofCrAnList [φ] * ofFieldOpList φ') =
  (exchangeSign (𝓕.crAnStatistics φ)) (ofList 𝓕.fieldOpStatistic φ') • normalOrder (ofFieldOpList φ' * ofCrAnList [φ])𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpφ':List 𝓕.FieldOp⊢ normalOrder
    ((exchangeSign (ofList 𝓕.crAnStatistics [φ])) (ofList 𝓕.fieldOpStatistic φ') • ofFieldOpList φ' * ofCrAnList [φ] +
      (superCommute (ofCrAnList [φ])) (ofFieldOpList φ')) =
  (exchangeSign (𝓕.crAnStatistics φ)) (ofList 𝓕.fieldOpStatistic φ') • normalOrder (ofFieldOpList φ' * ofCrAnList [φ]) ofCrAnList_mul_ofFieldOpList_eq_superCommute𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpφ':List 𝓕.FieldOp⊢ normalOrder
    ((exchangeSign (ofList 𝓕.crAnStatistics [φ])) (ofList 𝓕.fieldOpStatistic φ') • ofFieldOpList φ' * ofCrAnList [φ] +
      (superCommute (ofCrAnList [φ])) (ofFieldOpList φ')) =
  (exchangeSign (𝓕.crAnStatistics φ)) (ofList 𝓕.fieldOpStatistic φ') • normalOrder (ofFieldOpList φ' * ofCrAnList [φ])𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpφ':List 𝓕.FieldOp⊢ normalOrder
    ((exchangeSign (ofList 𝓕.crAnStatistics [φ])) (ofList 𝓕.fieldOpStatistic φ') • ofFieldOpList φ' * ofCrAnList [φ] +
      (superCommute (ofCrAnList [φ])) (ofFieldOpList φ')) =
  (exchangeSign (𝓕.crAnStatistics φ)) (ofList 𝓕.fieldOpStatistic φ') • normalOrder (ofFieldOpList φ' * ofCrAnList [φ])]𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpφ':List 𝓕.FieldOp⊢ normalOrder
    ((exchangeSign (ofList 𝓕.crAnStatistics [φ])) (ofList 𝓕.fieldOpStatistic φ') • ofFieldOpList φ' * ofCrAnList [φ] +
      (superCommute (ofCrAnList [φ])) (ofFieldOpList φ')) =
  (exchangeSign (𝓕.crAnStatistics φ)) (ofList 𝓕.fieldOpStatistic φ') • normalOrder (ofFieldOpList φ' * ofCrAnList [φ])
  simpAll goals completed! 🐙

lemma normalOrder_anPart_ofFieldOpList_swap (φ : 𝓕.FieldOp) (φ' : List 𝓕.FieldOp) :
    𝓝(anPart φ * ofFieldOpList φ') = 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') • 𝓝(ofFieldOpList φ' * anPart φ) := by𝓕:FieldSpecificationφ:𝓕.FieldOpφ':List 𝓕.FieldOp⊢ normalOrder (anPart φ * ofFieldOpList φ') =
  (exchangeSign (𝓕|>ₛφ)) (ofList 𝓕.fieldOpStatistic φ') • normalOrder (ofFieldOpList φ' * anPart φ)
  match φ with
  | .inAsymp φ =>𝓕:FieldSpecificationφ✝:𝓕.FieldOpφ':List 𝓕.FieldOpφ:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ normalOrder (anPart (FieldOp.inAsymp φ) * ofFieldOpList φ') =
  (exchangeSign (𝓕|>ₛFieldOp.inAsymp φ)) (ofList 𝓕.fieldOpStatistic φ') •
    normalOrder (ofFieldOpList φ' * anPart (FieldOp.inAsymp φ))
    simp only [anPart_inAsymp, zero_mul, map_zero, mul_zero]𝓕:FieldSpecificationφ✝:𝓕.FieldOpφ':List 𝓕.FieldOpφ:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ 0 = (exchangeSign (𝓕|>ₛFieldOp.inAsymp φ)) (ofList 𝓕.fieldOpStatistic φ') • 0
    moduleAll goals completed! 🐙
  | .position φ =>𝓕:FieldSpecificationφ✝:𝓕.FieldOpφ':List 𝓕.FieldOpφ:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTime⊢ normalOrder (anPart (FieldOp.position φ) * ofFieldOpList φ') =
  (exchangeSign (𝓕|>ₛFieldOp.position φ)) (ofList 𝓕.fieldOpStatistic φ') •
    normalOrder (ofFieldOpList φ' * anPart (FieldOp.position φ))
    simp only [anPart_position]𝓕:FieldSpecificationφ✝:𝓕.FieldOpφ':List 𝓕.FieldOpφ:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTime⊢ normalOrder (ofCrAnOp ⟨FieldOp.position φ, CreateAnnihilate.annihilate⟩ * ofFieldOpList φ') =
  (exchangeSign (𝓕|>ₛFieldOp.position φ)) (ofList 𝓕.fieldOpStatistic φ') •
    normalOrder (ofFieldOpList φ' * ofCrAnOp ⟨FieldOp.position φ, CreateAnnihilate.annihilate⟩)
    rw [normalOrder_ofCrAnOp_ofFieldOpList_swap𝓕:FieldSpecificationφ✝:𝓕.FieldOpφ':List 𝓕.FieldOpφ:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTime⊢ (exchangeSign (𝓕.crAnStatistics ⟨FieldOp.position φ, CreateAnnihilate.annihilate⟩)) (ofList 𝓕.fieldOpStatistic φ') •
    normalOrder (ofFieldOpList φ' * ofCrAnOp ⟨FieldOp.position φ, CreateAnnihilate.annihilate⟩) =
  (exchangeSign (𝓕|>ₛFieldOp.position φ)) (ofList 𝓕.fieldOpStatistic φ') •
    normalOrder (ofFieldOpList φ' * ofCrAnOp ⟨FieldOp.position φ, CreateAnnihilate.annihilate⟩)𝓕:FieldSpecificationφ✝:𝓕.FieldOpφ':List 𝓕.FieldOpφ:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTime⊢ (exchangeSign (𝓕.crAnStatistics ⟨FieldOp.position φ, CreateAnnihilate.annihilate⟩)) (ofList 𝓕.fieldOpStatistic φ') •
    normalOrder (ofFieldOpList φ' * ofCrAnOp ⟨FieldOp.position φ, CreateAnnihilate.annihilate⟩) =
  (exchangeSign (𝓕|>ₛFieldOp.position φ)) (ofList 𝓕.fieldOpStatistic φ') •
    normalOrder (ofFieldOpList φ' * ofCrAnOp ⟨FieldOp.position φ, CreateAnnihilate.annihilate⟩)]𝓕:FieldSpecificationφ✝:𝓕.FieldOpφ':List 𝓕.FieldOpφ:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTime⊢ (exchangeSign (𝓕.crAnStatistics ⟨FieldOp.position φ, CreateAnnihilate.annihilate⟩)) (ofList 𝓕.fieldOpStatistic φ') •
    normalOrder (ofFieldOpList φ' * ofCrAnOp ⟨FieldOp.position φ, CreateAnnihilate.annihilate⟩) =
  (exchangeSign (𝓕|>ₛFieldOp.position φ)) (ofList 𝓕.fieldOpStatistic φ') •
    normalOrder (ofFieldOpList φ' * ofCrAnOp ⟨FieldOp.position φ, CreateAnnihilate.annihilate⟩)
    rflAll goals completed! 🐙
  | .outAsymp φ =>𝓕:FieldSpecificationφ✝:𝓕.FieldOpφ':List 𝓕.FieldOpφ:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ normalOrder (anPart (FieldOp.outAsymp φ) * ofFieldOpList φ') =
  (exchangeSign (𝓕|>ₛFieldOp.outAsymp φ)) (ofList 𝓕.fieldOpStatistic φ') •
    normalOrder (ofFieldOpList φ' * anPart (FieldOp.outAsymp φ))
    simp only [anPart_outAsymp]𝓕:FieldSpecificationφ✝:𝓕.FieldOpφ':List 𝓕.FieldOpφ:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ normalOrder (ofCrAnOp ⟨FieldOp.outAsymp φ, ()⟩ * ofFieldOpList φ') =
  (exchangeSign (𝓕|>ₛFieldOp.outAsymp φ)) (ofList 𝓕.fieldOpStatistic φ') •
    normalOrder (ofFieldOpList φ' * ofCrAnOp ⟨FieldOp.outAsymp φ, ()⟩)
    rw [normalOrder_ofCrAnOp_ofFieldOpList_swap𝓕:FieldSpecificationφ✝:𝓕.FieldOpφ':List 𝓕.FieldOpφ:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ (exchangeSign (𝓕.crAnStatistics ⟨FieldOp.outAsymp φ, ()⟩)) (ofList 𝓕.fieldOpStatistic φ') •
    normalOrder (ofFieldOpList φ' * ofCrAnOp ⟨FieldOp.outAsymp φ, ()⟩) =
  (exchangeSign (𝓕|>ₛFieldOp.outAsymp φ)) (ofList 𝓕.fieldOpStatistic φ') •
    normalOrder (ofFieldOpList φ' * ofCrAnOp ⟨FieldOp.outAsymp φ, ()⟩)𝓕:FieldSpecificationφ✝:𝓕.FieldOpφ':List 𝓕.FieldOpφ:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ (exchangeSign (𝓕.crAnStatistics ⟨FieldOp.outAsymp φ, ()⟩)) (ofList 𝓕.fieldOpStatistic φ') •
    normalOrder (ofFieldOpList φ' * ofCrAnOp ⟨FieldOp.outAsymp φ, ()⟩) =
  (exchangeSign (𝓕|>ₛFieldOp.outAsymp φ)) (ofList 𝓕.fieldOpStatistic φ') •
    normalOrder (ofFieldOpList φ' * ofCrAnOp ⟨FieldOp.outAsymp φ, ()⟩)]𝓕:FieldSpecificationφ✝:𝓕.FieldOpφ':List 𝓕.FieldOpφ:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ (exchangeSign (𝓕.crAnStatistics ⟨FieldOp.outAsymp φ, ()⟩)) (ofList 𝓕.fieldOpStatistic φ') •
    normalOrder (ofFieldOpList φ' * ofCrAnOp ⟨FieldOp.outAsymp φ, ()⟩) =
  (exchangeSign (𝓕|>ₛFieldOp.outAsymp φ)) (ofList 𝓕.fieldOpStatistic φ') •
    normalOrder (ofFieldOpList φ' * ofCrAnOp ⟨FieldOp.outAsymp φ, ()⟩)
    rflAll goals completed! 🐙

lemma normalOrder_ofFieldOpList_anPart_swap (φ : 𝓕.FieldOp) (φ' : List 𝓕.FieldOp) :
    𝓝(ofFieldOpList φ' * anPart φ) = 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') • 𝓝(anPart φ * ofFieldOpList φ') := by𝓕:FieldSpecificationφ:𝓕.FieldOpφ':List 𝓕.FieldOp⊢ normalOrder (ofFieldOpList φ' * anPart φ) =
  (exchangeSign (𝓕|>ₛφ)) (ofList 𝓕.fieldOpStatistic φ') • normalOrder (anPart φ * ofFieldOpList φ')
  rw [normalOrder_anPart_ofFieldOpList_swap𝓕:FieldSpecificationφ:𝓕.FieldOpφ':List 𝓕.FieldOp⊢ normalOrder (ofFieldOpList φ' * anPart φ) =
  (exchangeSign (𝓕|>ₛφ)) (ofList 𝓕.fieldOpStatistic φ') •
    (exchangeSign (𝓕|>ₛφ)) (ofList 𝓕.fieldOpStatistic φ') • normalOrder (ofFieldOpList φ' * anPart φ)𝓕:FieldSpecificationφ:𝓕.FieldOpφ':List 𝓕.FieldOp⊢ normalOrder (ofFieldOpList φ' * anPart φ) =
  (exchangeSign (𝓕|>ₛφ)) (ofList 𝓕.fieldOpStatistic φ') •
    (exchangeSign (𝓕|>ₛφ)) (ofList 𝓕.fieldOpStatistic φ') • normalOrder (ofFieldOpList φ' * anPart φ)]𝓕:FieldSpecificationφ:𝓕.FieldOpφ':List 𝓕.FieldOp⊢ normalOrder (ofFieldOpList φ' * anPart φ) =
  (exchangeSign (𝓕|>ₛφ)) (ofList 𝓕.fieldOpStatistic φ') •
    (exchangeSign (𝓕|>ₛφ)) (ofList 𝓕.fieldOpStatistic φ') • normalOrder (ofFieldOpList φ' * anPart φ)
  erw [smul_smul𝓕:FieldSpecificationφ:𝓕.FieldOpφ':List 𝓕.FieldOp⊢ normalOrder (ofFieldOpList φ' * anPart φ) =
  ((exchangeSign (𝓕|>ₛφ)) (ofList 𝓕.fieldOpStatistic φ') * (exchangeSign (𝓕|>ₛφ)) (ofList 𝓕.fieldOpStatistic φ')) •
    normalOrder (ofFieldOpList φ' * anPart φ)]𝓕:FieldSpecificationφ:𝓕.FieldOpφ':List 𝓕.FieldOp⊢ normalOrder (ofFieldOpList φ' * anPart φ) =
  ((exchangeSign (𝓕|>ₛφ)) (ofList 𝓕.fieldOpStatistic φ') * (exchangeSign (𝓕|>ₛφ)) (ofList 𝓕.fieldOpStatistic φ')) •
    normalOrder (ofFieldOpList φ' * anPart φ)
  simp [FieldStatistic.exchangeSign_mul_self]All goals completed! 🐙

lemma normalOrder_ofFieldOpList_mul_anPart_swap (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) :
    𝓝(ofFieldOpList φs) * anPart φ = 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φs) • 𝓝(anPart φ * ofFieldOpList φs) := by𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOp⊢ normalOrder (ofFieldOpList φs) * anPart φ =
  (exchangeSign (𝓕|>ₛφ)) (ofList 𝓕.fieldOpStatistic φs) • normalOrder (anPart φ * ofFieldOpList φs)
  rw [← normalOrder_mul_anPart𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOp⊢ normalOrder (ofFieldOpList φs * anPart φ) =
  (exchangeSign (𝓕|>ₛφ)) (ofList 𝓕.fieldOpStatistic φs) • normalOrder (anPart φ * ofFieldOpList φs)𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOp⊢ normalOrder (ofFieldOpList φs * anPart φ) =
  (exchangeSign (𝓕|>ₛφ)) (ofList 𝓕.fieldOpStatistic φs) • normalOrder (anPart φ * ofFieldOpList φs)]𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOp⊢ normalOrder (ofFieldOpList φs * anPart φ) =
  (exchangeSign (𝓕|>ₛφ)) (ofList 𝓕.fieldOpStatistic φs) • normalOrder (anPart φ * ofFieldOpList φs)
  rw [normalOrder_ofFieldOpList_anPart_swap𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOp⊢ (exchangeSign (𝓕|>ₛφ)) (ofList 𝓕.fieldOpStatistic φs) • normalOrder (anPart φ * ofFieldOpList φs) =
  (exchangeSign (𝓕|>ₛφ)) (ofList 𝓕.fieldOpStatistic φs) • normalOrder (anPart φ * ofFieldOpList φs)All goals completed! 🐙]All goals completed! 🐙

lemma anPart_mul_normalOrder_ofFieldOpList_eq_superCommute (φ : 𝓕.FieldOp)
    (φs' : List 𝓕.FieldOp) : anPart φ * 𝓝(ofFieldOpList φs') =
    𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φs') • 𝓝(ofFieldOpList φs' * anPart φ) +
    [anPart φ, 𝓝(ofFieldOpList φs')]ₛ := by𝓕:FieldSpecificationφ:𝓕.FieldOpφs':List 𝓕.FieldOp⊢ anPart φ * normalOrder (ofFieldOpList φs') =
  (exchangeSign (𝓕|>ₛφ)) (ofList 𝓕.fieldOpStatistic φs') • normalOrder (ofFieldOpList φs' * anPart φ) +
    (superCommute (anPart φ)) (normalOrder (ofFieldOpList φs'))
  rw [anPart,𝓕:FieldSpecificationφ:𝓕.FieldOpφs':List 𝓕.FieldOp⊢ ι (anPartF φ) * normalOrder (ofFieldOpList φs') =
  (exchangeSign (𝓕|>ₛφ)) (ofList 𝓕.fieldOpStatistic φs') • normalOrder (ofFieldOpList φs' * ι (anPartF φ)) +
    (superCommute (ι (anPartF φ))) (normalOrder (ofFieldOpList φs'))𝓕:FieldSpecificationφ:𝓕.FieldOpφs':List 𝓕.FieldOp⊢ ι (anPartF φ * normalOrderF (ofFieldOpListF φs')) =
  (exchangeSign (𝓕|>ₛφ)) (ofList 𝓕.fieldOpStatistic φs') • normalOrder (ι (ofFieldOpListF φs') * ι (anPartF φ)) +
    (superCommute (ι (anPartF φ))) (ι (normalOrderF (ofFieldOpListF φs'))) ofFieldOpList,𝓕:FieldSpecificationφ:𝓕.FieldOpφs':List 𝓕.FieldOp⊢ ι (anPartF φ) * normalOrder (ι (ofFieldOpListF φs')) =
  (exchangeSign (𝓕|>ₛφ)) (ofList 𝓕.fieldOpStatistic φs') • normalOrder (ι (ofFieldOpListF φs') * ι (anPartF φ)) +
    (superCommute (ι (anPartF φ))) (normalOrder (ι (ofFieldOpListF φs')))𝓕:FieldSpecificationφ:𝓕.FieldOpφs':List 𝓕.FieldOp⊢ ι (anPartF φ * normalOrderF (ofFieldOpListF φs')) =
  (exchangeSign (𝓕|>ₛφ)) (ofList 𝓕.fieldOpStatistic φs') • normalOrder (ι (ofFieldOpListF φs') * ι (anPartF φ)) +
    (superCommute (ι (anPartF φ))) (ι (normalOrderF (ofFieldOpListF φs'))) normalOrder_eq_ι_normalOrderF,𝓕:FieldSpecificationφ:𝓕.FieldOpφs':List 𝓕.FieldOp⊢ ι (anPartF φ) * ι (normalOrderF (ofFieldOpListF φs')) =
  (exchangeSign (𝓕|>ₛφ)) (ofList 𝓕.fieldOpStatistic φs') • normalOrder (ι (ofFieldOpListF φs') * ι (anPartF φ)) +
    (superCommute (ι (anPartF φ))) (ι (normalOrderF (ofFieldOpListF φs')))𝓕:FieldSpecificationφ:𝓕.FieldOpφs':List 𝓕.FieldOp⊢ ι (anPartF φ * normalOrderF (ofFieldOpListF φs')) =
  (exchangeSign (𝓕|>ₛφ)) (ofList 𝓕.fieldOpStatistic φs') • normalOrder (ι (ofFieldOpListF φs') * ι (anPartF φ)) +
    (superCommute (ι (anPartF φ))) (ι (normalOrderF (ofFieldOpListF φs'))) ← map_mul𝓕:FieldSpecificationφ:𝓕.FieldOpφs':List 𝓕.FieldOp⊢ ι (anPartF φ * normalOrderF (ofFieldOpListF φs')) =
  (exchangeSign (𝓕|>ₛφ)) (ofList 𝓕.fieldOpStatistic φs') • normalOrder (ι (ofFieldOpListF φs') * ι (anPartF φ)) +
    (superCommute (ι (anPartF φ))) (ι (normalOrderF (ofFieldOpListF φs')))𝓕:FieldSpecificationφ:𝓕.FieldOpφs':List 𝓕.FieldOp⊢ ι (anPartF φ * normalOrderF (ofFieldOpListF φs')) =
  (exchangeSign (𝓕|>ₛφ)) (ofList 𝓕.fieldOpStatistic φs') • normalOrder (ι (ofFieldOpListF φs') * ι (anPartF φ)) +
    (superCommute (ι (anPartF φ))) (ι (normalOrderF (ofFieldOpListF φs')))]𝓕:FieldSpecificationφ:𝓕.FieldOpφs':List 𝓕.FieldOp⊢ ι (anPartF φ * normalOrderF (ofFieldOpListF φs')) =
  (exchangeSign (𝓕|>ₛφ)) (ofList 𝓕.fieldOpStatistic φs') • normalOrder (ι (ofFieldOpListF φs') * ι (anPartF φ)) +
    (superCommute (ι (anPartF φ))) (ι (normalOrderF (ofFieldOpListF φs')))
  rw [anPartF_mul_normalOrderF_ofFieldOpListF_eq_superCommuteF𝓕:FieldSpecificationφ:𝓕.FieldOpφs':List 𝓕.FieldOp⊢ ι
    ((exchangeSign (𝓕|>ₛφ)) (ofList 𝓕.fieldOpStatistic φs') • normalOrderF (ofFieldOpListF φs' * anPartF φ) +
      (superCommuteF (anPartF φ)) (normalOrderF (ofFieldOpListF φs'))) =
  (exchangeSign (𝓕|>ₛφ)) (ofList 𝓕.fieldOpStatistic φs') • normalOrder (ι (ofFieldOpListF φs') * ι (anPartF φ)) +
    (superCommute (ι (anPartF φ))) (ι (normalOrderF (ofFieldOpListF φs')))𝓕:FieldSpecificationφ:𝓕.FieldOpφs':List 𝓕.FieldOp⊢ ι
    ((exchangeSign (𝓕|>ₛφ)) (ofList 𝓕.fieldOpStatistic φs') • normalOrderF (ofFieldOpListF φs' * anPartF φ) +
      (superCommuteF (anPartF φ)) (normalOrderF (ofFieldOpListF φs'))) =
  (exchangeSign (𝓕|>ₛφ)) (ofList 𝓕.fieldOpStatistic φs') • normalOrder (ι (ofFieldOpListF φs') * ι (anPartF φ)) +
    (superCommute (ι (anPartF φ))) (ι (normalOrderF (ofFieldOpListF φs')))]𝓕:FieldSpecificationφ:𝓕.FieldOpφs':List 𝓕.FieldOp⊢ ι
    ((exchangeSign (𝓕|>ₛφ)) (ofList 𝓕.fieldOpStatistic φs') • normalOrderF (ofFieldOpListF φs' * anPartF φ) +
      (superCommuteF (anPartF φ)) (normalOrderF (ofFieldOpListF φs'))) =
  (exchangeSign (𝓕|>ₛφ)) (ofList 𝓕.fieldOpStatistic φs') • normalOrder (ι (ofFieldOpListF φs') * ι (anPartF φ)) +
    (superCommute (ι (anPartF φ))) (ι (normalOrderF (ofFieldOpListF φs')))
  simp only [map_add, map_smul]𝓕:FieldSpecificationφ:𝓕.FieldOpφs':List 𝓕.FieldOp⊢ (exchangeSign (𝓕|>ₛφ)) (ofList 𝓕.fieldOpStatistic φs') • ι (normalOrderF (ofFieldOpListF φs' * anPartF φ)) +
    ι ((superCommuteF (anPartF φ)) (normalOrderF (ofFieldOpListF φs'))) =
  (exchangeSign (𝓕|>ₛφ)) (ofList 𝓕.fieldOpStatistic φs') • normalOrder (ι (ofFieldOpListF φs') * ι (anPartF φ)) +
    (superCommute (ι (anPartF φ))) (ι (normalOrderF (ofFieldOpListF φs')))
  rflAll goals completed! 🐙

Super commutators with a normal ordered term as sums

For a field specification 𝓕, an element φ of 𝓕.CrAnFieldOp, a list φs of 𝓕.CrAnFieldOp, the following relation holds

[φ, 𝓝(φ₀…φₙ)]ₛ = ∑ i, 𝓢(φ, φ₀…φᵢ₋₁) • [φ, φᵢ]ₛ * 𝓝(φ₀…φᵢ₋₁φᵢ₊₁…φₙ).

The proof of this result ultimately goes as follows

The definition of normalOrder is used to rewrite 𝓝(φ₀…φₙ) as a scalar multiple of a ofCrAnList φsn where φsn is the normal ordering of φ₀…φₙ.

superCommuteF_ofCrAnListF_ofCrAnListF_eq_sum is used to rewrite the super commutator of φ (considered as a list with one element) with ofCrAnList φsn as a sum of super commutators, one for each element of φsn.

The fact that super-commutators are in the center of 𝓕.WickAlgebra is used to rearrange terms.

Properties of ordered lists, and normalOrderSign_eraseIdx are then used to complete the proof.


lemma ofCrAnOp_superCommute_normalOrder_ofCrAnList_sum (φ : 𝓕.CrAnFieldOp)
    (φs : List 𝓕.CrAnFieldOp) : [ofCrAnOp φ, 𝓝(ofCrAnList φs)]ₛ = ∑ n : Fin φs.length,
    𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ (φs.take n)) • [ofCrAnOp φ, ofCrAnOp φs[n]]ₛ
    * 𝓝(ofCrAnList (φs.eraseIdx n)) := by𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpφs:List 𝓕.CrAnFieldOp⊢ (superCommute (ofCrAnOp φ)) (normalOrder (ofCrAnList φs)) =
  ∑ n,
    (exchangeSign (𝓕.crAnStatistics φ)) (ofList 𝓕.crAnStatistics (List.take (↑n) φs)) •
        (superCommute (ofCrAnOp φ)) (ofCrAnOp φs[n]) *
      normalOrder (ofCrAnList (φs.eraseIdx ↑n))
  rw [normalOrder_ofCrAnList,𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpφs:List 𝓕.CrAnFieldOp⊢ (superCommute (ofCrAnOp φ)) (normalOrderSign φs • ofCrAnList (normalOrderList φs)) =
  ∑ n,
    (exchangeSign (𝓕.crAnStatistics φ)) (ofList 𝓕.crAnStatistics (List.take (↑n) φs)) •
        (superCommute (ofCrAnOp φ)) (ofCrAnOp φs[n]) *
      normalOrder (ofCrAnList (φs.eraseIdx ↑n))𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpφs:List 𝓕.CrAnFieldOp⊢ normalOrderSign φs • (superCommute (ofCrAnOp φ)) (ofCrAnList (normalOrderList φs)) =
  ∑ n,
    (exchangeSign (𝓕.crAnStatistics φ)) (ofList 𝓕.crAnStatistics (List.take (↑n) φs)) •
        (superCommute (ofCrAnOp φ)) (ofCrAnOp φs[n]) *
      normalOrder (ofCrAnList (φs.eraseIdx ↑n)) map_smul𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpφs:List 𝓕.CrAnFieldOp⊢ normalOrderSign φs • (superCommute (ofCrAnOp φ)) (ofCrAnList (normalOrderList φs)) =
  ∑ n,
    (exchangeSign (𝓕.crAnStatistics φ)) (ofList 𝓕.crAnStatistics (List.take (↑n) φs)) •
        (superCommute (ofCrAnOp φ)) (ofCrAnOp φs[n]) *
      normalOrder (ofCrAnList (φs.eraseIdx ↑n))𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpφs:List 𝓕.CrAnFieldOp⊢ normalOrderSign φs • (superCommute (ofCrAnOp φ)) (ofCrAnList (normalOrderList φs)) =
  ∑ n,
    (exchangeSign (𝓕.crAnStatistics φ)) (ofList 𝓕.crAnStatistics (List.take (↑n) φs)) •
        (superCommute (ofCrAnOp φ)) (ofCrAnOp φs[n]) *
      normalOrder (ofCrAnList (φs.eraseIdx ↑n))]𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpφs:List 𝓕.CrAnFieldOp⊢ normalOrderSign φs • (superCommute (ofCrAnOp φ)) (ofCrAnList (normalOrderList φs)) =
  ∑ n,
    (exchangeSign (𝓕.crAnStatistics φ)) (ofList 𝓕.crAnStatistics (List.take (↑n) φs)) •
        (superCommute (ofCrAnOp φ)) (ofCrAnOp φs[n]) *
      normalOrder (ofCrAnList (φs.eraseIdx ↑n))
  erw [superCommute_ofCrAnOp_ofCrAnList_eq_sum,𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpφs:List 𝓕.CrAnFieldOp⊢ normalOrderSign φs •
    ∑ n,
      (exchangeSign (𝓕.crAnStatistics φ)) (ofList 𝓕.crAnStatistics (List.take (↑n) (normalOrderList φs))) •
          (superCommute (ofCrAnOp φ)) (ofCrAnOp ((normalOrderList φs).get n)) *
        ofCrAnList ((normalOrderList φs).eraseIdx ↑n) =
  ∑ n,
    (exchangeSign (𝓕.crAnStatistics φ)) (ofList 𝓕.crAnStatistics (List.take (↑n) φs)) •
        (superCommute (ofCrAnOp φ)) (ofCrAnOp φs[n]) *
      normalOrder (ofCrAnList (φs.eraseIdx ↑n)) Finset.smul_sum,𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpφs:List 𝓕.CrAnFieldOp⊢ ∑ x,
    normalOrderSign φs •
      ((exchangeSign (𝓕.crAnStatistics φ)) (ofList 𝓕.crAnStatistics (List.take (↑x) (normalOrderList φs))) •
          (superCommute (ofCrAnOp φ)) (ofCrAnOp ((normalOrderList φs).get x)) *
        ofCrAnList ((normalOrderList φs).eraseIdx ↑x)) =
  ∑ n,
    (exchangeSign (𝓕.crAnStatistics φ)) (ofList 𝓕.crAnStatistics (List.take (↑n) φs)) •
        (superCommute (ofCrAnOp φ)) (ofCrAnOp φs[n]) *
      normalOrder (ofCrAnList (φs.eraseIdx ↑n))
    sum_normalOrderList_length𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpφs:List 𝓕.CrAnFieldOp⊢ ∑ n,
    normalOrderSign φs •
      ((exchangeSign (𝓕.crAnStatistics φ))
            (ofList 𝓕.crAnStatistics (List.take (↑(normalOrderEquiv n)) (normalOrderList φs))) •
          (superCommute (ofCrAnOp φ)) (ofCrAnOp ((normalOrderList φs).get (normalOrderEquiv n))) *
        ofCrAnList ((normalOrderList φs).eraseIdx ↑(normalOrderEquiv n))) =
  ∑ n,
    (exchangeSign (𝓕.crAnStatistics φ)) (ofList 𝓕.crAnStatistics (List.take (↑n) φs)) •
        (superCommute (ofCrAnOp φ)) (ofCrAnOp φs[n]) *
      normalOrder (ofCrAnList (φs.eraseIdx ↑n))]𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpφs:List 𝓕.CrAnFieldOp⊢ ∑ n,
    normalOrderSign φs •
      ((exchangeSign (𝓕.crAnStatistics φ))
            (ofList 𝓕.crAnStatistics (List.take (↑(normalOrderEquiv n)) (normalOrderList φs))) •
          (superCommute (ofCrAnOp φ)) (ofCrAnOp ((normalOrderList φs).get (normalOrderEquiv n))) *
        ofCrAnList ((normalOrderList φs).eraseIdx ↑(normalOrderEquiv n))) =
  ∑ n,
    (exchangeSign (𝓕.crAnStatistics φ)) (ofList 𝓕.crAnStatistics (List.take (↑n) φs)) •
        (superCommute (ofCrAnOp φ)) (ofCrAnOp φs[n]) *
      normalOrder (ofCrAnList (φs.eraseIdx ↑n))
  congre_f𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpφs:List 𝓕.CrAnFieldOp⊢ (fun n =>
    normalOrderSign φs •
      ((exchangeSign (𝓕.crAnStatistics φ))
            (ofList 𝓕.crAnStatistics (List.take (↑(normalOrderEquiv n)) (normalOrderList φs))) •
          (superCommute (ofCrAnOp φ)) (ofCrAnOp ((normalOrderList φs).get (normalOrderEquiv n))) *
        ofCrAnList ((normalOrderList φs).eraseIdx ↑(normalOrderEquiv n)))) =
  fun n =>
  (exchangeSign (𝓕.crAnStatistics φ)) (ofList 𝓕.crAnStatistics (List.take (↑n) φs)) •
      (superCommute (ofCrAnOp φ)) (ofCrAnOp φs[n]) *
    normalOrder (ofCrAnList (φs.eraseIdx ↑n))
  funext ne_f𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpφs:List 𝓕.CrAnFieldOpn:Fin φs.length⊢ normalOrderSign φs •
    ((exchangeSign (𝓕.crAnStatistics φ))
          (ofList 𝓕.crAnStatistics (List.take (↑(normalOrderEquiv n)) (normalOrderList φs))) •
        (superCommute (ofCrAnOp φ)) (ofCrAnOp ((normalOrderList φs).get (normalOrderEquiv n))) *
      ofCrAnList ((normalOrderList φs).eraseIdx ↑(normalOrderEquiv n))) =
  (exchangeSign (𝓕.crAnStatistics φ)) (ofList 𝓕.crAnStatistics (List.take (↑n) φs)) •
      (superCommute (ofCrAnOp φ)) (ofCrAnOp φs[n]) *
    normalOrder (ofCrAnList (φs.eraseIdx ↑n))
  simp only [List.get_eq_getElem, normalOrderList_get_normalOrderEquiv,
    normalOrderList_eraseIdx_normalOrderEquiv, Algebra.smul_mul_assoc, Fin.getElem_fin]e_f𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpφs:List 𝓕.CrAnFieldOpn:Fin φs.length⊢ normalOrderSign φs •
    (exchangeSign (𝓕.crAnStatistics φ))
        (ofList 𝓕.crAnStatistics (List.take (↑(normalOrderEquiv n)) (normalOrderList φs))) •
      ((superCommute (ofCrAnOp φ)) (ofCrAnOp φs[↑n]) * ofCrAnList (normalOrderList (φs.eraseIdx ↑n))) =
  (exchangeSign (𝓕.crAnStatistics φ)) (ofList 𝓕.crAnStatistics (List.take (↑n) φs)) •
    ((superCommute (ofCrAnOp φ)) (ofCrAnOp φs[↑n]) * normalOrder (ofCrAnList (φs.eraseIdx ↑n)))
  erw [ofCrAnList_eq_normalOrder,e_f𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpφs:List 𝓕.CrAnFieldOpn:Fin φs.length⊢ normalOrderSign φs •
    (exchangeSign (𝓕.crAnStatistics φ))
        (ofList 𝓕.crAnStatistics (List.take (↑(normalOrderEquiv n)) (normalOrderList φs))) •
      ((superCommute (ofCrAnOp φ)) (ofCrAnOp φs[↑n]) *
        normalOrderSign (φs.eraseIdx ↑n) • normalOrder (ofCrAnList (φs.eraseIdx ↑n))) =
  (exchangeSign (𝓕.crAnStatistics φ)) (ofList 𝓕.crAnStatistics (List.take (↑n) φs)) •
    ((superCommute (ofCrAnOp φ)) (ofCrAnOp φs[↑n]) * normalOrder (ofCrAnList (φs.eraseIdx ↑n))) mul_smul_comm,e_f𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpφs:List 𝓕.CrAnFieldOpn:Fin φs.length⊢ normalOrderSign φs •
    (exchangeSign (𝓕.crAnStatistics φ))
        (ofList 𝓕.crAnStatistics (List.take (↑(normalOrderEquiv n)) (normalOrderList φs))) •
      normalOrderSign (φs.eraseIdx ↑n) •
        ((superCommute (ofCrAnOp φ)) (ofCrAnOp φs[↑n]) * normalOrder (ofCrAnList (φs.eraseIdx ↑n))) =
  (exchangeSign (𝓕.crAnStatistics φ)) (ofList 𝓕.crAnStatistics (List.take (↑n) φs)) •
    ((superCommute (ofCrAnOp φ)) (ofCrAnOp φs[↑n]) * normalOrder (ofCrAnList (φs.eraseIdx ↑n))) smul_smul,e_f𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpφs:List 𝓕.CrAnFieldOpn:Fin φs.length⊢ (normalOrderSign φs *
      (exchangeSign (𝓕.crAnStatistics φ))
        (ofList 𝓕.crAnStatistics (List.take (↑(normalOrderEquiv n)) (normalOrderList φs)))) •
    normalOrderSign (φs.eraseIdx ↑n) •
      ((superCommute (ofCrAnOp φ)) (ofCrAnOp φs[↑n]) * normalOrder (ofCrAnList (φs.eraseIdx ↑n))) =
  (exchangeSign (𝓕.crAnStatistics φ)) (ofList 𝓕.crAnStatistics (List.take (↑n) φs)) •
    ((superCommute (ofCrAnOp φ)) (ofCrAnOp φs[↑n]) * normalOrder (ofCrAnList (φs.eraseIdx ↑n))) smul_smule_f𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpφs:List 𝓕.CrAnFieldOpn:Fin φs.length⊢ (normalOrderSign φs *
        (exchangeSign (𝓕.crAnStatistics φ))
          (ofList 𝓕.crAnStatistics (List.take (↑(normalOrderEquiv n)) (normalOrderList φs))) *
      normalOrderSign (φs.eraseIdx ↑n)) •
    ((superCommute (ofCrAnOp φ)) (ofCrAnOp φs[↑n]) * normalOrder (ofCrAnList (φs.eraseIdx ↑n))) =
  (exchangeSign (𝓕.crAnStatistics φ)) (ofList 𝓕.crAnStatistics (List.take (↑n) φs)) •
    ((superCommute (ofCrAnOp φ)) (ofCrAnOp φs[↑n]) * normalOrder (ofCrAnList (φs.eraseIdx ↑n)))]e_f𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpφs:List 𝓕.CrAnFieldOpn:Fin φs.length⊢ (normalOrderSign φs *
        (exchangeSign (𝓕.crAnStatistics φ))
          (ofList 𝓕.crAnStatistics (List.take (↑(normalOrderEquiv n)) (normalOrderList φs))) *
      normalOrderSign (φs.eraseIdx ↑n)) •
    ((superCommute (ofCrAnOp φ)) (ofCrAnOp φs[↑n]) * normalOrder (ofCrAnList (φs.eraseIdx ↑n))) =
  (exchangeSign (𝓕.crAnStatistics φ)) (ofList 𝓕.crAnStatistics (List.take (↑n) φs)) •
    ((superCommute (ofCrAnOp φ)) (ofCrAnOp φs[↑n]) * normalOrder (ofCrAnList (φs.eraseIdx ↑n)))
  by_cases hs : (𝓕 |>ₛ φ) = (𝓕 |>ₛ φs[n])pos𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpφs:List 𝓕.CrAnFieldOpn:Fin φs.lengthhs:𝓕.crAnStatistics φ = 𝓕.crAnStatistics φs[n]⊢ (normalOrderSign φs *
        (exchangeSign (𝓕.crAnStatistics φ))
          (ofList 𝓕.crAnStatistics (List.take (↑(normalOrderEquiv n)) (normalOrderList φs))) *
      normalOrderSign (φs.eraseIdx ↑n)) •
    ((superCommute (ofCrAnOp φ)) (ofCrAnOp φs[↑n]) * normalOrder (ofCrAnList (φs.eraseIdx ↑n))) =
  (exchangeSign (𝓕.crAnStatistics φ)) (ofList 𝓕.crAnStatistics (List.take (↑n) φs)) •
    ((superCommute (ofCrAnOp φ)) (ofCrAnOp φs[↑n]) * normalOrder (ofCrAnList (φs.eraseIdx ↑n)))neg𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpφs:List 𝓕.CrAnFieldOpn:Fin φs.lengthhs:¬𝓕.crAnStatistics φ = 𝓕.crAnStatistics φs[n]⊢ (normalOrderSign φs *
        (exchangeSign (𝓕.crAnStatistics φ))
          (ofList 𝓕.crAnStatistics (List.take (↑(normalOrderEquiv n)) (normalOrderList φs))) *
      normalOrderSign (φs.eraseIdx ↑n)) •
    ((superCommute (ofCrAnOp φ)) (ofCrAnOp φs[↑n]) * normalOrder (ofCrAnList (φs.eraseIdx ↑n))) =
  (exchangeSign (𝓕.crAnStatistics φ)) (ofList 𝓕.crAnStatistics (List.take (↑n) φs)) •
    ((superCommute (ofCrAnOp φ)) (ofCrAnOp φs[↑n]) * normalOrder (ofCrAnList (φs.eraseIdx ↑n)))
  ·pos𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpφs:List 𝓕.CrAnFieldOpn:Fin φs.lengthhs:𝓕.crAnStatistics φ = 𝓕.crAnStatistics φs[n]⊢ (normalOrderSign φs *
        (exchangeSign (𝓕.crAnStatistics φ))
          (ofList 𝓕.crAnStatistics (List.take (↑(normalOrderEquiv n)) (normalOrderList φs))) *
      normalOrderSign (φs.eraseIdx ↑n)) •
    ((superCommute (ofCrAnOp φ)) (ofCrAnOp φs[↑n]) * normalOrder (ofCrAnList (φs.eraseIdx ↑n))) =
  (exchangeSign (𝓕.crAnStatistics φ)) (ofList 𝓕.crAnStatistics (List.take (↑n) φs)) •
    ((superCommute (ofCrAnOp φ)) (ofCrAnOp φs[↑n]) * normalOrder (ofCrAnList (φs.eraseIdx ↑n))) congrpos.e_a𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpφs:List 𝓕.CrAnFieldOpn:Fin φs.lengthhs:𝓕.crAnStatistics φ = 𝓕.crAnStatistics φs[n]⊢ normalOrderSign φs *
      (exchangeSign (𝓕.crAnStatistics φ))
        (ofList 𝓕.crAnStatistics (List.take (↑(normalOrderEquiv n)) (normalOrderList φs))) *
    normalOrderSign (φs.eraseIdx ↑n) =
  (exchangeSign (𝓕.crAnStatistics φ)) (ofList 𝓕.crAnStatistics (List.take (↑n) φs))
    erw [normalOrderSign_eraseIdx,pos.e_a𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpφs:List 𝓕.CrAnFieldOpn:Fin φs.lengthhs:𝓕.crAnStatistics φ = 𝓕.crAnStatistics φs[n]⊢ normalOrderSign φs *
      (exchangeSign (𝓕.crAnStatistics φ))
        (ofList 𝓕.crAnStatistics (List.take (↑(normalOrderEquiv n)) (normalOrderList φs))) *
    (normalOrderSign φs * (exchangeSign (𝓕.crAnStatistics (φs.get n))) (ofList 𝓕.crAnStatistics (List.take (↑n) φs)) *
      (exchangeSign (𝓕.crAnStatistics (φs.get n)))
        (ofList 𝓕.crAnStatistics (List.take (↑(normalOrderEquiv n)) (normalOrderList φs)))) =
  (exchangeSign (𝓕.crAnStatistics φ)) (ofList 𝓕.crAnStatistics (List.take (↑n) φs)) ← hspos.e_a𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpφs:List 𝓕.CrAnFieldOpn:Fin φs.lengthhs:𝓕.crAnStatistics φ = 𝓕.crAnStatistics φs[n]⊢ normalOrderSign φs *
      (exchangeSign (𝓕.crAnStatistics φ))
        (ofList 𝓕.crAnStatistics (List.take (↑(normalOrderEquiv n)) (normalOrderList φs))) *
    (normalOrderSign φs * (exchangeSign (𝓕.crAnStatistics φ)) (ofList 𝓕.crAnStatistics (List.take (↑n) φs)) *
      (exchangeSign (𝓕.crAnStatistics φ))
        (ofList 𝓕.crAnStatistics (List.take (↑(normalOrderEquiv n)) (normalOrderList φs)))) =
  (exchangeSign (𝓕.crAnStatistics φ)) (ofList 𝓕.crAnStatistics (List.take (↑n) φs))]pos.e_a𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpφs:List 𝓕.CrAnFieldOpn:Fin φs.lengthhs:𝓕.crAnStatistics φ = 𝓕.crAnStatistics φs[n]⊢ normalOrderSign φs *
      (exchangeSign (𝓕.crAnStatistics φ))
        (ofList 𝓕.crAnStatistics (List.take (↑(normalOrderEquiv n)) (normalOrderList φs))) *
    (normalOrderSign φs * (exchangeSign (𝓕.crAnStatistics φ)) (ofList 𝓕.crAnStatistics (List.take (↑n) φs)) *
      (exchangeSign (𝓕.crAnStatistics φ))
        (ofList 𝓕.crAnStatistics (List.take (↑(normalOrderEquiv n)) (normalOrderList φs)))) =
  (exchangeSign (𝓕.crAnStatistics φ)) (ofList 𝓕.crAnStatistics (List.take (↑n) φs))
    trans (normalOrderSign φs * normalOrderSign φs) *
      (𝓢(𝓕 |>ₛ (φs.get n), 𝓕 |>ₛ ((normalOrderList φs).take (normalOrderEquiv n))) *
      𝓢(𝓕 |>ₛ (φs.get n), 𝓕 |>ₛ ((normalOrderList φs).take (normalOrderEquiv n))))
      * 𝓢(𝓕 |>ₛ (φs.get n), 𝓕 |>ₛ (φs.take n))𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpφs:List 𝓕.CrAnFieldOpn:Fin φs.lengthhs:𝓕.crAnStatistics φ = 𝓕.crAnStatistics φs[n]⊢ normalOrderSign φs *
      (exchangeSign (𝓕.crAnStatistics φ))
        (ofList 𝓕.crAnStatistics (List.take (↑(normalOrderEquiv n)) (normalOrderList φs))) *
    (normalOrderSign φs * (exchangeSign (𝓕.crAnStatistics φ)) (ofList 𝓕.crAnStatistics (List.take (↑n) φs)) *
      (exchangeSign (𝓕.crAnStatistics φ))
        (ofList 𝓕.crAnStatistics (List.take (↑(normalOrderEquiv n)) (normalOrderList φs)))) =
  normalOrderSign φs * normalOrderSign φs *
      ((exchangeSign (𝓕.crAnStatistics (φs.get n)))
          (ofList 𝓕.crAnStatistics (List.take (↑(normalOrderEquiv n)) (normalOrderList φs))) *
        (exchangeSign (𝓕.crAnStatistics (φs.get n)))
          (ofList 𝓕.crAnStatistics (List.take (↑(normalOrderEquiv n)) (normalOrderList φs)))) *
    (exchangeSign (𝓕.crAnStatistics (φs.get n))) (ofList 𝓕.crAnStatistics (List.take (↑n) φs))𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpφs:List 𝓕.CrAnFieldOpn:Fin φs.lengthhs:𝓕.crAnStatistics φ = 𝓕.crAnStatistics φs[n]⊢ normalOrderSign φs * normalOrderSign φs *
      ((exchangeSign (𝓕.crAnStatistics (φs.get n)))
          (ofList 𝓕.crAnStatistics (List.take (↑(normalOrderEquiv n)) (normalOrderList φs))) *
        (exchangeSign (𝓕.crAnStatistics (φs.get n)))
          (ofList 𝓕.crAnStatistics (List.take (↑(normalOrderEquiv n)) (normalOrderList φs)))) *
    (exchangeSign (𝓕.crAnStatistics (φs.get n))) (ofList 𝓕.crAnStatistics (List.take (↑n) φs)) =
  (exchangeSign (𝓕.crAnStatistics φ)) (ofList 𝓕.crAnStatistics (List.take (↑n) φs))
    ·𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpφs:List 𝓕.CrAnFieldOpn:Fin φs.lengthhs:𝓕.crAnStatistics φ = 𝓕.crAnStatistics φs[n]⊢ normalOrderSign φs *
      (exchangeSign (𝓕.crAnStatistics φ))
        (ofList 𝓕.crAnStatistics (List.take (↑(normalOrderEquiv n)) (normalOrderList φs))) *
    (normalOrderSign φs * (exchangeSign (𝓕.crAnStatistics φ)) (ofList 𝓕.crAnStatistics (List.take (↑n) φs)) *
      (exchangeSign (𝓕.crAnStatistics φ))
        (ofList 𝓕.crAnStatistics (List.take (↑(normalOrderEquiv n)) (normalOrderList φs)))) =
  normalOrderSign φs * normalOrderSign φs *
      ((exchangeSign (𝓕.crAnStatistics (φs.get n)))
          (ofList 𝓕.crAnStatistics (List.take (↑(normalOrderEquiv n)) (normalOrderList φs))) *
        (exchangeSign (𝓕.crAnStatistics (φs.get n)))
          (ofList 𝓕.crAnStatistics (List.take (↑(normalOrderEquiv n)) (normalOrderList φs)))) *
    (exchangeSign (𝓕.crAnStatistics (φs.get n))) (ofList 𝓕.crAnStatistics (List.take (↑n) φs)) ring_nf𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpφs:List 𝓕.CrAnFieldOpn:Fin φs.lengthhs:𝓕.crAnStatistics φ = 𝓕.crAnStatistics φs[n]⊢ normalOrderSign φs ^ 2 *
      (exchangeSign (𝓕.crAnStatistics φ))
          (ofList 𝓕.crAnStatistics (List.take (↑(normalOrderEquiv n)) (normalOrderList φs))) ^
        2 *
    (exchangeSign (𝓕.crAnStatistics φ)) (ofList 𝓕.crAnStatistics (List.take (↑n) φs)) =
  normalOrderSign φs ^ 2 *
      (exchangeSign (𝓕.crAnStatistics (φs.get n)))
          (ofList 𝓕.crAnStatistics (List.take (↑(normalOrderEquiv n)) (normalOrderList φs))) ^
        2 *
    (exchangeSign (𝓕.crAnStatistics (φs.get n))) (ofList 𝓕.crAnStatistics (List.take (↑n) φs))
      rw [hs𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpφs:List 𝓕.CrAnFieldOpn:Fin φs.lengthhs:𝓕.crAnStatistics φ = 𝓕.crAnStatistics φs[n]⊢ normalOrderSign φs ^ 2 *
      (exchangeSign (𝓕.crAnStatistics φs[n]))
          (ofList 𝓕.crAnStatistics (List.take (↑(normalOrderEquiv n)) (normalOrderList φs))) ^
        2 *
    (exchangeSign (𝓕.crAnStatistics φs[n])) (ofList 𝓕.crAnStatistics (List.take (↑n) φs)) =
  normalOrderSign φs ^ 2 *
      (exchangeSign (𝓕.crAnStatistics (φs.get n)))
          (ofList 𝓕.crAnStatistics (List.take (↑(normalOrderEquiv n)) (normalOrderList φs))) ^
        2 *
    (exchangeSign (𝓕.crAnStatistics (φs.get n))) (ofList 𝓕.crAnStatistics (List.take (↑n) φs))𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpφs:List 𝓕.CrAnFieldOpn:Fin φs.lengthhs:𝓕.crAnStatistics φ = 𝓕.crAnStatistics φs[n]⊢ normalOrderSign φs ^ 2 *
      (exchangeSign (𝓕.crAnStatistics φs[n]))
          (ofList 𝓕.crAnStatistics (List.take (↑(normalOrderEquiv n)) (normalOrderList φs))) ^
        2 *
    (exchangeSign (𝓕.crAnStatistics φs[n])) (ofList 𝓕.crAnStatistics (List.take (↑n) φs)) =
  normalOrderSign φs ^ 2 *
      (exchangeSign (𝓕.crAnStatistics (φs.get n)))
          (ofList 𝓕.crAnStatistics (List.take (↑(normalOrderEquiv n)) (normalOrderList φs))) ^
        2 *
    (exchangeSign (𝓕.crAnStatistics (φs.get n))) (ofList 𝓕.crAnStatistics (List.take (↑n) φs))]𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpφs:List 𝓕.CrAnFieldOpn:Fin φs.lengthhs:𝓕.crAnStatistics φ = 𝓕.crAnStatistics φs[n]⊢ normalOrderSign φs ^ 2 *
      (exchangeSign (𝓕.crAnStatistics φs[n]))
          (ofList 𝓕.crAnStatistics (List.take (↑(normalOrderEquiv n)) (normalOrderList φs))) ^
        2 *
    (exchangeSign (𝓕.crAnStatistics φs[n])) (ofList 𝓕.crAnStatistics (List.take (↑n) φs)) =
  normalOrderSign φs ^ 2 *
      (exchangeSign (𝓕.crAnStatistics (φs.get n)))
          (ofList 𝓕.crAnStatistics (List.take (↑(normalOrderEquiv n)) (normalOrderList φs))) ^
        2 *
    (exchangeSign (𝓕.crAnStatistics (φs.get n))) (ofList 𝓕.crAnStatistics (List.take (↑n) φs))
      rflAll goals completed! 🐙
    ·𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpφs:List 𝓕.CrAnFieldOpn:Fin φs.lengthhs:𝓕.crAnStatistics φ = 𝓕.crAnStatistics φs[n]⊢ normalOrderSign φs * normalOrderSign φs *
      ((exchangeSign (𝓕.crAnStatistics (φs.get n)))
          (ofList 𝓕.crAnStatistics (List.take (↑(normalOrderEquiv n)) (normalOrderList φs))) *
        (exchangeSign (𝓕.crAnStatistics (φs.get n)))
          (ofList 𝓕.crAnStatistics (List.take (↑(normalOrderEquiv n)) (normalOrderList φs)))) *
    (exchangeSign (𝓕.crAnStatistics (φs.get n))) (ofList 𝓕.crAnStatistics (List.take (↑n) φs)) =
  (exchangeSign (𝓕.crAnStatistics φ)) (ofList 𝓕.crAnStatistics (List.take (↑n) φs)) simp [hs]All goals completed! 🐙
  ·neg𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpφs:List 𝓕.CrAnFieldOpn:Fin φs.lengthhs:¬𝓕.crAnStatistics φ = 𝓕.crAnStatistics φs[n]⊢ (normalOrderSign φs *
        (exchangeSign (𝓕.crAnStatistics φ))
          (ofList 𝓕.crAnStatistics (List.take (↑(normalOrderEquiv n)) (normalOrderList φs))) *
      normalOrderSign (φs.eraseIdx ↑n)) •
    ((superCommute (ofCrAnOp φ)) (ofCrAnOp φs[↑n]) * normalOrder (ofCrAnList (φs.eraseIdx ↑n))) =
  (exchangeSign (𝓕.crAnStatistics φ)) (ofList 𝓕.crAnStatistics (List.take (↑n) φs)) •
    ((superCommute (ofCrAnOp φ)) (ofCrAnOp φs[↑n]) * normalOrder (ofCrAnList (φs.eraseIdx ↑n))) erw [superCommute_diff_statistic hsneg𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpφs:List 𝓕.CrAnFieldOpn:Fin φs.lengthhs:¬𝓕.crAnStatistics φ = 𝓕.crAnStatistics φs[n]⊢ (normalOrderSign φs *
        (exchangeSign (𝓕.crAnStatistics φ))
          (ofList 𝓕.crAnStatistics (List.take (↑(normalOrderEquiv n)) (normalOrderList φs))) *
      normalOrderSign (φs.eraseIdx ↑n)) •
    (0 * normalOrder (ofCrAnList (φs.eraseIdx ↑n))) =
  (exchangeSign (𝓕.crAnStatistics φ)) (ofList 𝓕.crAnStatistics (List.take (↑n) φs)) •
    (0 * normalOrder (ofCrAnList (φs.eraseIdx ↑n)))]neg𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpφs:List 𝓕.CrAnFieldOpn:Fin φs.lengthhs:¬𝓕.crAnStatistics φ = 𝓕.crAnStatistics φs[n]⊢ (normalOrderSign φs *
        (exchangeSign (𝓕.crAnStatistics φ))
          (ofList 𝓕.crAnStatistics (List.take (↑(normalOrderEquiv n)) (normalOrderList φs))) *
      normalOrderSign (φs.eraseIdx ↑n)) •
    (0 * normalOrder (ofCrAnList (φs.eraseIdx ↑n))) =
  (exchangeSign (𝓕.crAnStatistics φ)) (ofList 𝓕.crAnStatistics (List.take (↑n) φs)) •
    (0 * normalOrder (ofCrAnList (φs.eraseIdx ↑n)))
    simp only [zero_mul, smul_zero]All goals completed! 🐙



lemma ofCrAnOp_superCommute_normalOrder_ofFieldOpList_sum (φ : 𝓕.CrAnFieldOp)
    (φs : List 𝓕.FieldOp) :
    [ofCrAnOp φ, 𝓝(ofFieldOpList φs)]ₛ = ∑ n : Fin φs.length, 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ (φs.take n)) •
    [ofCrAnOp φ, ofFieldOp φs[n]]ₛ * 𝓝(ofFieldOpList (φs.eraseIdx n)) := by𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpφs:List 𝓕.FieldOp⊢ (superCommute (ofCrAnOp φ)) (normalOrder (ofFieldOpList φs)) =
  ∑ n,
    (exchangeSign (𝓕.crAnStatistics φ)) (ofList 𝓕.fieldOpStatistic (List.take (↑n) φs)) •
        (superCommute (ofCrAnOp φ)) (ofFieldOp φs[n]) *
      normalOrder (ofFieldOpList (φs.eraseIdx ↑n))
  conv_lhs =>
    rw [ofFieldOpList_eq_sum, map_sum, map_sum]𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpφs:List 𝓕.FieldOp| ∑ x, (superCommute (ofCrAnOp φ)) (normalOrder (ofCrAnList ↑x))
    enter [2, s]𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpφs:List 𝓕.FieldOps:CrAnSection φs| (superCommute (ofCrAnOp φ)) (normalOrder (ofCrAnList ↑s))
    rw [ofCrAnOp_superCommute_normalOrder_ofCrAnList_sum, CrAnSection.sum_over_length]𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpφs:List 𝓕.FieldOps:CrAnSection φs| ∑ n,
  (exchangeSign (𝓕.crAnStatistics φ)) (ofList 𝓕.crAnStatistics (List.take ↑(Fin.cast ⋯ n) ↑s)) •
      (superCommute (ofCrAnOp φ)) (ofCrAnOp (↑s)[Fin.cast ⋯ n]) *
    normalOrder (ofCrAnList ((↑s).eraseIdx ↑(Fin.cast ⋯ n)))
    enter [2, n]𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpφs:List 𝓕.FieldOps:CrAnSection φsn:Fin φs.length| (exchangeSign (𝓕.crAnStatistics φ)) (ofList 𝓕.crAnStatistics (List.take ↑(Fin.cast ⋯ n) ↑s)) •
    (superCommute (ofCrAnOp φ)) (ofCrAnOp (↑s)[Fin.cast ⋯ n]) *
  normalOrder (ofCrAnList ((↑s).eraseIdx ↑(Fin.cast ⋯ n)))
    rw [CrAnSection.take_statistics_eq_take_state_statistics, smul_mul_assoc]𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpφs:List 𝓕.FieldOps:CrAnSection φsn:Fin φs.length| (exchangeSign (𝓕.crAnStatistics φ)) (ofList 𝓕.fieldOpStatistic (List.take (↑(Fin.cast ⋯ n)) φs)) •
  ((superCommute (ofCrAnOp φ)) (ofCrAnOp (↑s)[Fin.cast ⋯ n]) * normalOrder (ofCrAnList ((↑s).eraseIdx ↑(Fin.cast ⋯ n))))
  rw [Finset.sum_comm𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpφs:List 𝓕.FieldOp⊢ ∑ y,
    ∑ x,
      (exchangeSign (𝓕.crAnStatistics φ)) (ofList 𝓕.fieldOpStatistic (List.take (↑(Fin.cast ⋯ y)) φs)) •
        ((superCommute (ofCrAnOp φ)) (ofCrAnOp (↑x)[Fin.cast ⋯ y]) *
          normalOrder (ofCrAnList ((↑x).eraseIdx ↑(Fin.cast ⋯ y)))) =
  ∑ n,
    (exchangeSign (𝓕.crAnStatistics φ)) (ofList 𝓕.fieldOpStatistic (List.take (↑n) φs)) •
        (superCommute (ofCrAnOp φ)) (ofFieldOp φs[n]) *
      normalOrder (ofFieldOpList (φs.eraseIdx ↑n))𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpφs:List 𝓕.FieldOp⊢ ∑ y,
    ∑ x,
      (exchangeSign (𝓕.crAnStatistics φ)) (ofList 𝓕.fieldOpStatistic (List.take (↑(Fin.cast ⋯ y)) φs)) •
        ((superCommute (ofCrAnOp φ)) (ofCrAnOp (↑x)[Fin.cast ⋯ y]) *
          normalOrder (ofCrAnList ((↑x).eraseIdx ↑(Fin.cast ⋯ y)))) =
  ∑ n,
    (exchangeSign (𝓕.crAnStatistics φ)) (ofList 𝓕.fieldOpStatistic (List.take (↑n) φs)) •
        (superCommute (ofCrAnOp φ)) (ofFieldOp φs[n]) *
      normalOrder (ofFieldOpList (φs.eraseIdx ↑n))]𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpφs:List 𝓕.FieldOp⊢ ∑ y,
    ∑ x,
      (exchangeSign (𝓕.crAnStatistics φ)) (ofList 𝓕.fieldOpStatistic (List.take (↑(Fin.cast ⋯ y)) φs)) •
        ((superCommute (ofCrAnOp φ)) (ofCrAnOp (↑x)[Fin.cast ⋯ y]) *
          normalOrder (ofCrAnList ((↑x).eraseIdx ↑(Fin.cast ⋯ y)))) =
  ∑ n,
    (exchangeSign (𝓕.crAnStatistics φ)) (ofList 𝓕.fieldOpStatistic (List.take (↑n) φs)) •
        (superCommute (ofCrAnOp φ)) (ofFieldOp φs[n]) *
      normalOrder (ofFieldOpList (φs.eraseIdx ↑n))
  refine Finset.sum_congr rfl (fun n _ => ?_)𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpφs:List 𝓕.FieldOpn:Fin φs.lengthx✝:n ∈ Finset.univ⊢ ∑ x,
    (exchangeSign (𝓕.crAnStatistics φ)) (ofList 𝓕.fieldOpStatistic (List.take (↑(Fin.cast ⋯ n)) φs)) •
      ((superCommute (ofCrAnOp φ)) (ofCrAnOp (↑x)[Fin.cast ⋯ n]) *
        normalOrder (ofCrAnList ((↑x).eraseIdx ↑(Fin.cast ⋯ n)))) =
  (exchangeSign (𝓕.crAnStatistics φ)) (ofList 𝓕.fieldOpStatistic (List.take (↑n) φs)) •
      (superCommute (ofCrAnOp φ)) (ofFieldOp φs[n]) *
    normalOrder (ofFieldOpList (φs.eraseIdx ↑n))
  simp only [Fin.val_cast, Fin.getElem_fin,
    CrAnSection.sum_eraseIdxEquiv n _ n.prop,
    CrAnSection.eraseIdxEquiv_symm_getElem,
    CrAnSection.eraseIdxEquiv_symm_eraseIdx, ← Finset.smul_sum, Algebra.smul_mul_assoc]𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpφs:List 𝓕.FieldOpn:Fin φs.lengthx✝:n ∈ Finset.univ⊢ (exchangeSign (𝓕.crAnStatistics φ)) (ofList 𝓕.fieldOpStatistic (List.take (↑n) φs)) •
    ∑ x, ∑ x_1, (superCommute (ofCrAnOp φ)) (ofCrAnOp ⟨φs[↑n], x⟩) * normalOrder (ofCrAnList ↑x_1) =
  (exchangeSign (𝓕.crAnStatistics φ)) (ofList 𝓕.fieldOpStatistic (List.take (↑n) φs)) •
    ((superCommute (ofCrAnOp φ)) (ofFieldOp φs[↑n]) * normalOrder (ofFieldOpList (φs.eraseIdx ↑n)))
  conv_lhs =>
    enter [2, 2, n]𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpφs:List 𝓕.FieldOpn✝:Fin φs.lengthx✝:n ∈ Finset.univn:𝓕.fieldOpToCrAnType φs[↑n✝]| ∑ x, (superCommute (ofCrAnOp φ)) (ofCrAnOp ⟨φs[↑n✝], n⟩) * normalOrder (ofCrAnList ↑x)
    rw [← Finset.mul_sum]𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpφs:List 𝓕.FieldOpn✝:Fin φs.lengthx✝:n ∈ Finset.univn:𝓕.fieldOpToCrAnType φs[↑n✝]| (superCommute (ofCrAnOp φ)) (ofCrAnOp ⟨φs[↑n✝], n⟩) * ∑ i, normalOrder (ofCrAnList ↑i)
  rw [← Finset.sum_mul,𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpφs:List 𝓕.FieldOpn:Fin φs.lengthx✝:n ∈ Finset.univ⊢ (exchangeSign (𝓕.crAnStatistics φ)) (ofList 𝓕.fieldOpStatistic (List.take (↑n) φs)) •
    ((∑ i, (superCommute (ofCrAnOp φ)) (ofCrAnOp ⟨φs[↑n], i⟩)) * ∑ i, normalOrder (ofCrAnList ↑i)) =
  (exchangeSign (𝓕.crAnStatistics φ)) (ofList 𝓕.fieldOpStatistic (List.take (↑n) φs)) •
    ((superCommute (ofCrAnOp φ)) (ofFieldOp φs[↑n]) * normalOrder (ofFieldOpList (φs.eraseIdx ↑n)))All goals completed! 🐙 ← map_sum,𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpφs:List 𝓕.FieldOpn:Fin φs.lengthx✝:n ∈ Finset.univ⊢ (exchangeSign (𝓕.crAnStatistics φ)) (ofList 𝓕.fieldOpStatistic (List.take (↑n) φs)) •
    ((superCommute (ofCrAnOp φ)) (∑ x, ofCrAnOp ⟨φs[↑n], x⟩) * ∑ i, normalOrder (ofCrAnList ↑i)) =
  (exchangeSign (𝓕.crAnStatistics φ)) (ofList 𝓕.fieldOpStatistic (List.take (↑n) φs)) •
    ((superCommute (ofCrAnOp φ)) (ofFieldOp φs[↑n]) * normalOrder (ofFieldOpList (φs.eraseIdx ↑n)))All goals completed! 🐙 ← map_sum,𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpφs:List 𝓕.FieldOpn:Fin φs.lengthx✝:n ∈ Finset.univ⊢ (exchangeSign (𝓕.crAnStatistics φ)) (ofList 𝓕.fieldOpStatistic (List.take (↑n) φs)) •
    ((superCommute (ofCrAnOp φ)) (∑ x, ofCrAnOp ⟨φs[↑n], x⟩) * normalOrder (∑ x, ofCrAnList ↑x)) =
  (exchangeSign (𝓕.crAnStatistics φ)) (ofList 𝓕.fieldOpStatistic (List.take (↑n) φs)) •
    ((superCommute (ofCrAnOp φ)) (ofFieldOp φs[↑n]) * normalOrder (ofFieldOpList (φs.eraseIdx ↑n)))All goals completed! 🐙 ← ofFieldOp_eq_sum,𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpφs:List 𝓕.FieldOpn:Fin φs.lengthx✝:n ∈ Finset.univ⊢ (exchangeSign (𝓕.crAnStatistics φ)) (ofList 𝓕.fieldOpStatistic (List.take (↑n) φs)) •
    ((superCommute (ofCrAnOp φ)) (ofFieldOp φs[↑n]) * normalOrder (∑ x, ofCrAnList ↑x)) =
  (exchangeSign (𝓕.crAnStatistics φ)) (ofList 𝓕.fieldOpStatistic (List.take (↑n) φs)) •
    ((superCommute (ofCrAnOp φ)) (ofFieldOp φs[↑n]) * normalOrder (ofFieldOpList (φs.eraseIdx ↑n)))All goals completed! 🐙 ← ofFieldOpList_eq_sum𝓕:FieldSpecificationφ:𝓕.CrAnFieldOpφs:List 𝓕.FieldOpn:Fin φs.lengthx✝:n ∈ Finset.univ⊢ (exchangeSign (𝓕.crAnStatistics φ)) (ofList 𝓕.fieldOpStatistic (List.take (↑n) φs)) •
    ((superCommute (ofCrAnOp φ)) (ofFieldOp φs[↑n]) * normalOrder (ofFieldOpList (φs.eraseIdx ↑n))) =
  (exchangeSign (𝓕.crAnStatistics φ)) (ofList 𝓕.fieldOpStatistic (List.take (↑n) φs)) •
    ((superCommute (ofCrAnOp φ)) (ofFieldOp φs[↑n]) * normalOrder (ofFieldOpList (φs.eraseIdx ↑n)))All goals completed! 🐙]All goals completed! 🐙

The commutator of the annihilation part of a field operator with a normal ordered list of field operators can be decomposed into the sum of the commutators of the annihilation part with each element of the list of field operators, i.e. [anPart φ, 𝓝(φ₀…φₙ)]ₛ= ∑ i, 𝓢(φ, φ₀…φᵢ₋₁) • [anPart φ, φᵢ]ₛ * 𝓝(φ₀…φᵢ₋₁φᵢ₊₁…φₙ).


lemma anPart_superCommute_normalOrder_ofFieldOpList_sum (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) :
    [anPart φ, 𝓝(ofFieldOpList φs)]ₛ = ∑ n : Fin φs.length, 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ (φs.take n)) •
    [anPart φ, ofFieldOpF φs[n]]ₛ * 𝓝(ofFieldOpList (φs.eraseIdx n)) := by𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOp⊢ (superCommute (anPart φ)) (normalOrder (ofFieldOpList φs)) =
  ∑ n,
    (exchangeSign (𝓕|>ₛφ)) (ofList 𝓕.fieldOpStatistic (List.take (↑n) φs)) •
        (superCommute (anPart φ)) ↑(ofFieldOpF φs[n]) *
      normalOrder (ofFieldOpList (φs.eraseIdx ↑n))
  match φ with
  | .inAsymp φ =>𝓕:FieldSpecificationφ✝:𝓕.FieldOpφs:List 𝓕.FieldOpφ:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ (superCommute (anPart (FieldOp.inAsymp φ))) (normalOrder (ofFieldOpList φs)) =
  ∑ n,
    (exchangeSign (𝓕|>ₛFieldOp.inAsymp φ)) (ofList 𝓕.fieldOpStatistic (List.take (↑n) φs)) •
        (superCommute (anPart (FieldOp.inAsymp φ))) ↑(ofFieldOpF φs[n]) *
      normalOrder (ofFieldOpList (φs.eraseIdx ↑n))
    simp only [anPart_inAsymp, map_zero, LinearMap.zero_apply, Fin.getElem_fin,
      Algebra.smul_mul_assoc, zero_mul]𝓕:FieldSpecificationφ✝:𝓕.FieldOpφs:List 𝓕.FieldOpφ:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ 0 = ∑ x, (exchangeSign (𝓕|>ₛFieldOp.inAsymp φ)) (ofList 𝓕.fieldOpStatistic (List.take (↑x) φs)) • 0
    conv_rhs =>
      enter [2, s]𝓕:FieldSpecificationφ✝:𝓕.FieldOpφs:List 𝓕.FieldOpφ:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentums:Fin φs.length| (exchangeSign (𝓕|>ₛFieldOp.inAsymp φ)) (ofList 𝓕.fieldOpStatistic (List.take (↑s) φs)) • 0
      rw [smul_zero]𝓕:FieldSpecificationφ✝:𝓕.FieldOpφs:List 𝓕.FieldOpφ:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentums:Fin φs.length| 0
    simpAll goals completed! 🐙
  | .position φ =>𝓕:FieldSpecificationφ✝:𝓕.FieldOpφs:List 𝓕.FieldOpφ:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTime⊢ (superCommute (anPart (FieldOp.position φ))) (normalOrder (ofFieldOpList φs)) =
  ∑ n,
    (exchangeSign (𝓕|>ₛFieldOp.position φ)) (ofList 𝓕.fieldOpStatistic (List.take (↑n) φs)) •
        (superCommute (anPart (FieldOp.position φ))) ↑(ofFieldOpF φs[n]) *
      normalOrder (ofFieldOpList (φs.eraseIdx ↑n))
    simp only [anPart_position, Fin.getElem_fin, Algebra.smul_mul_assoc]𝓕:FieldSpecificationφ✝:𝓕.FieldOpφs:List 𝓕.FieldOpφ:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTime⊢ (superCommute (ofCrAnOp ⟨FieldOp.position φ, CreateAnnihilate.annihilate⟩)) (normalOrder (ofFieldOpList φs)) =
  ∑ x,
    (exchangeSign (𝓕|>ₛFieldOp.position φ)) (ofList 𝓕.fieldOpStatistic (List.take (↑x) φs)) •
      ((superCommute (ofCrAnOp ⟨FieldOp.position φ, CreateAnnihilate.annihilate⟩)) ↑(ofFieldOpF φs[↑x]) *
        normalOrder (ofFieldOpList (φs.eraseIdx ↑x)))
    rw [ofCrAnOp_superCommute_normalOrder_ofFieldOpList_sum𝓕:FieldSpecificationφ✝:𝓕.FieldOpφs:List 𝓕.FieldOpφ:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTime⊢ ∑ n,
    (exchangeSign (𝓕.crAnStatistics ⟨FieldOp.position φ, CreateAnnihilate.annihilate⟩))
          (ofList 𝓕.fieldOpStatistic (List.take (↑n) φs)) •
        (superCommute (ofCrAnOp ⟨FieldOp.position φ, CreateAnnihilate.annihilate⟩)) (ofFieldOp φs[n]) *
      normalOrder (ofFieldOpList (φs.eraseIdx ↑n)) =
  ∑ x,
    (exchangeSign (𝓕|>ₛFieldOp.position φ)) (ofList 𝓕.fieldOpStatistic (List.take (↑x) φs)) •
      ((superCommute (ofCrAnOp ⟨FieldOp.position φ, CreateAnnihilate.annihilate⟩)) ↑(ofFieldOpF φs[↑x]) *
        normalOrder (ofFieldOpList (φs.eraseIdx ↑x)))𝓕:FieldSpecificationφ✝:𝓕.FieldOpφs:List 𝓕.FieldOpφ:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTime⊢ ∑ n,
    (exchangeSign (𝓕.crAnStatistics ⟨FieldOp.position φ, CreateAnnihilate.annihilate⟩))
          (ofList 𝓕.fieldOpStatistic (List.take (↑n) φs)) •
        (superCommute (ofCrAnOp ⟨FieldOp.position φ, CreateAnnihilate.annihilate⟩)) (ofFieldOp φs[n]) *
      normalOrder (ofFieldOpList (φs.eraseIdx ↑n)) =
  ∑ x,
    (exchangeSign (𝓕|>ₛFieldOp.position φ)) (ofList 𝓕.fieldOpStatistic (List.take (↑x) φs)) •
      ((superCommute (ofCrAnOp ⟨FieldOp.position φ, CreateAnnihilate.annihilate⟩)) ↑(ofFieldOpF φs[↑x]) *
        normalOrder (ofFieldOpList (φs.eraseIdx ↑x)))]𝓕:FieldSpecificationφ✝:𝓕.FieldOpφs:List 𝓕.FieldOpφ:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTime⊢ ∑ n,
    (exchangeSign (𝓕.crAnStatistics ⟨FieldOp.position φ, CreateAnnihilate.annihilate⟩))
          (ofList 𝓕.fieldOpStatistic (List.take (↑n) φs)) •
        (superCommute (ofCrAnOp ⟨FieldOp.position φ, CreateAnnihilate.annihilate⟩)) (ofFieldOp φs[n]) *
      normalOrder (ofFieldOpList (φs.eraseIdx ↑n)) =
  ∑ x,
    (exchangeSign (𝓕|>ₛFieldOp.position φ)) (ofList 𝓕.fieldOpStatistic (List.take (↑x) φs)) •
      ((superCommute (ofCrAnOp ⟨FieldOp.position φ, CreateAnnihilate.annihilate⟩)) ↑(ofFieldOpF φs[↑x]) *
        normalOrder (ofFieldOpList (φs.eraseIdx ↑x)))
    simp only [crAnStatistics, Function.comp_apply, crAnFieldOpToFieldOp_prod,
      Fin.getElem_fin, Algebra.smul_mul_assoc]𝓕:FieldSpecificationφ✝:𝓕.FieldOpφs:List 𝓕.FieldOpφ:((f : 𝓕.Field) × 𝓕.PositionLabel f) × SpaceTime⊢ ∑ x,
    (exchangeSign (𝓕|>ₛFieldOp.position φ)) (ofList 𝓕.fieldOpStatistic (List.take (↑x) φs)) •
      ((superCommute (ofCrAnOp ⟨FieldOp.position φ, CreateAnnihilate.annihilate⟩)) (ofFieldOp φs[↑x]) *
        normalOrder (ofFieldOpList (φs.eraseIdx ↑x))) =
  ∑ x,
    (exchangeSign (𝓕|>ₛFieldOp.position φ)) (ofList 𝓕.fieldOpStatistic (List.take (↑x) φs)) •
      ((superCommute (ofCrAnOp ⟨FieldOp.position φ, CreateAnnihilate.annihilate⟩)) ↑(ofFieldOpF φs[↑x]) *
        normalOrder (ofFieldOpList (φs.eraseIdx ↑x)))
    rflAll goals completed! 🐙
  | .outAsymp φ =>𝓕:FieldSpecificationφ✝:𝓕.FieldOpφs:List 𝓕.FieldOpφ:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ (superCommute (anPart (FieldOp.outAsymp φ))) (normalOrder (ofFieldOpList φs)) =
  ∑ n,
    (exchangeSign (𝓕|>ₛFieldOp.outAsymp φ)) (ofList 𝓕.fieldOpStatistic (List.take (↑n) φs)) •
        (superCommute (anPart (FieldOp.outAsymp φ))) ↑(ofFieldOpF φs[n]) *
      normalOrder (ofFieldOpList (φs.eraseIdx ↑n))
    simp only [anPart_outAsymp, Fin.getElem_fin, Algebra.smul_mul_assoc]𝓕:FieldSpecificationφ✝:𝓕.FieldOpφs:List 𝓕.FieldOpφ:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ (superCommute (ofCrAnOp ⟨FieldOp.outAsymp φ, ()⟩)) (normalOrder (ofFieldOpList φs)) =
  ∑ x,
    (exchangeSign (𝓕|>ₛFieldOp.outAsymp φ)) (ofList 𝓕.fieldOpStatistic (List.take (↑x) φs)) •
      ((superCommute (ofCrAnOp ⟨FieldOp.outAsymp φ, ()⟩)) ↑(ofFieldOpF φs[↑x]) *
        normalOrder (ofFieldOpList (φs.eraseIdx ↑x)))
    rw [ofCrAnOp_superCommute_normalOrder_ofFieldOpList_sum𝓕:FieldSpecificationφ✝:𝓕.FieldOpφs:List 𝓕.FieldOpφ:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ ∑ n,
    (exchangeSign (𝓕.crAnStatistics ⟨FieldOp.outAsymp φ, ()⟩)) (ofList 𝓕.fieldOpStatistic (List.take (↑n) φs)) •
        (superCommute (ofCrAnOp ⟨FieldOp.outAsymp φ, ()⟩)) (ofFieldOp φs[n]) *
      normalOrder (ofFieldOpList (φs.eraseIdx ↑n)) =
  ∑ x,
    (exchangeSign (𝓕|>ₛFieldOp.outAsymp φ)) (ofList 𝓕.fieldOpStatistic (List.take (↑x) φs)) •
      ((superCommute (ofCrAnOp ⟨FieldOp.outAsymp φ, ()⟩)) ↑(ofFieldOpF φs[↑x]) *
        normalOrder (ofFieldOpList (φs.eraseIdx ↑x)))𝓕:FieldSpecificationφ✝:𝓕.FieldOpφs:List 𝓕.FieldOpφ:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ ∑ n,
    (exchangeSign (𝓕.crAnStatistics ⟨FieldOp.outAsymp φ, ()⟩)) (ofList 𝓕.fieldOpStatistic (List.take (↑n) φs)) •
        (superCommute (ofCrAnOp ⟨FieldOp.outAsymp φ, ()⟩)) (ofFieldOp φs[n]) *
      normalOrder (ofFieldOpList (φs.eraseIdx ↑n)) =
  ∑ x,
    (exchangeSign (𝓕|>ₛFieldOp.outAsymp φ)) (ofList 𝓕.fieldOpStatistic (List.take (↑x) φs)) •
      ((superCommute (ofCrAnOp ⟨FieldOp.outAsymp φ, ()⟩)) ↑(ofFieldOpF φs[↑x]) *
        normalOrder (ofFieldOpList (φs.eraseIdx ↑x)))]𝓕:FieldSpecificationφ✝:𝓕.FieldOpφs:List 𝓕.FieldOpφ:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ ∑ n,
    (exchangeSign (𝓕.crAnStatistics ⟨FieldOp.outAsymp φ, ()⟩)) (ofList 𝓕.fieldOpStatistic (List.take (↑n) φs)) •
        (superCommute (ofCrAnOp ⟨FieldOp.outAsymp φ, ()⟩)) (ofFieldOp φs[n]) *
      normalOrder (ofFieldOpList (φs.eraseIdx ↑n)) =
  ∑ x,
    (exchangeSign (𝓕|>ₛFieldOp.outAsymp φ)) (ofList 𝓕.fieldOpStatistic (List.take (↑x) φs)) •
      ((superCommute (ofCrAnOp ⟨FieldOp.outAsymp φ, ()⟩)) ↑(ofFieldOpF φs[↑x]) *
        normalOrder (ofFieldOpList (φs.eraseIdx ↑x)))
    simp only [crAnStatistics, Function.comp_apply, crAnFieldOpToFieldOp_prod,
      Fin.getElem_fin, Algebra.smul_mul_assoc]𝓕:FieldSpecificationφ✝:𝓕.FieldOpφs:List 𝓕.FieldOpφ:((f : 𝓕.Field) × 𝓕.AsymptoticLabel f) × Momentum⊢ ∑ x,
    (exchangeSign (𝓕|>ₛFieldOp.outAsymp φ)) (ofList 𝓕.fieldOpStatistic (List.take (↑x) φs)) •
      ((superCommute (ofCrAnOp ⟨FieldOp.outAsymp φ, ()⟩)) (ofFieldOp φs[↑x]) *
        normalOrder (ofFieldOpList (φs.eraseIdx ↑x))) =
  ∑ x,
    (exchangeSign (𝓕|>ₛFieldOp.outAsymp φ)) (ofList 𝓕.fieldOpStatistic (List.take (↑x) φs)) •
      ((superCommute (ofCrAnOp ⟨FieldOp.outAsymp φ, ()⟩)) ↑(ofFieldOpF φs[↑x]) *
        normalOrder (ofFieldOpList (φs.eraseIdx ↑x)))
    rflAll goals completed! 🐙

Multiplying with normal ordered terms

Within a proto-operator algebra we have that anPartF φ * 𝓝(φ₀φ₁…φₙ) = 𝓝((anPart φ)φ₀φ₁…φₙ) + [anpart φ, 𝓝(φ₀φ₁…φₙ)]ₛ.


lemma anPart_mul_normalOrder_ofFieldOpList_eq_superCommute_reorder (φ : 𝓕.FieldOp)
    (φs : List 𝓕.FieldOp) : anPart φ * 𝓝(ofFieldOpList φs) =
    𝓝(anPart φ * ofFieldOpList φs) + [anPart φ, 𝓝(ofFieldOpList φs)]ₛ := by𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOp⊢ anPart φ * normalOrder (ofFieldOpList φs) =
  normalOrder (anPart φ * ofFieldOpList φs) + (superCommute (anPart φ)) (normalOrder (ofFieldOpList φs))
  rw [anPart_mul_normalOrder_ofFieldOpList_eq_superCommute𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOp⊢ (exchangeSign (𝓕|>ₛφ)) (ofList 𝓕.fieldOpStatistic φs) • normalOrder (ofFieldOpList φs * anPart φ) +
    (superCommute (anPart φ)) (normalOrder (ofFieldOpList φs)) =
  normalOrder (anPart φ * ofFieldOpList φs) + (superCommute (anPart φ)) (normalOrder (ofFieldOpList φs))𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOp⊢ (exchangeSign (𝓕|>ₛφ)) (ofList 𝓕.fieldOpStatistic φs) • normalOrder (ofFieldOpList φs * anPart φ) +
    (superCommute (anPart φ)) (normalOrder (ofFieldOpList φs)) =
  normalOrder (anPart φ * ofFieldOpList φs) + (superCommute (anPart φ)) (normalOrder (ofFieldOpList φs))]𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOp⊢ (exchangeSign (𝓕|>ₛφ)) (ofList 𝓕.fieldOpStatistic φs) • normalOrder (ofFieldOpList φs * anPart φ) +
    (superCommute (anPart φ)) (normalOrder (ofFieldOpList φs)) =
  normalOrder (anPart φ * ofFieldOpList φs) + (superCommute (anPart φ)) (normalOrder (ofFieldOpList φs))
  simp only [add_left_inj]𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOp⊢ (exchangeSign (𝓕|>ₛφ)) (ofList 𝓕.fieldOpStatistic φs) • normalOrder (ofFieldOpList φs * anPart φ) =
  normalOrder (anPart φ * ofFieldOpList φs)
  rw [normalOrder_anPart_ofFieldOpList_swap𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOp⊢ (exchangeSign (𝓕|>ₛφ)) (ofList 𝓕.fieldOpStatistic φs) • normalOrder (ofFieldOpList φs * anPart φ) =
  (exchangeSign (𝓕|>ₛφ)) (ofList 𝓕.fieldOpStatistic φs) • normalOrder (ofFieldOpList φs * anPart φ)All goals completed! 🐙]All goals completed! 🐙

Within a proto-operator algebra we have that φ * 𝓝ᶠ(φ₀φ₁…φₙ) = 𝓝ᶠ(φφ₀φ₁…φₙ) + [anpart φ, 𝓝ᶠ(φ₀φ₁…φₙ)]ₛF.


lemma ofFieldOp_mul_normalOrder_ofFieldOpList_eq_superCommute (φ : 𝓕.FieldOp)
    (φs : List 𝓕.FieldOp) : ofFieldOp φ * 𝓝(ofFieldOpList φs) =
    𝓝(ofFieldOp φ * ofFieldOpList φs) + [anPart φ, 𝓝(ofFieldOpList φs)]ₛ := by𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOp⊢ ofFieldOp φ * normalOrder (ofFieldOpList φs) =
  normalOrder (ofFieldOp φ * ofFieldOpList φs) + (superCommute (anPart φ)) (normalOrder (ofFieldOpList φs))
  conv_lhs => rw [ofFieldOp_eq_crPart_add_anPart]𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOp| (crPart φ + anPart φ) * normalOrder (ofFieldOpList φs)
  rw [add_mul,𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOp⊢ crPart φ * normalOrder (ofFieldOpList φs) + anPart φ * normalOrder (ofFieldOpList φs) =
  normalOrder (ofFieldOp φ * ofFieldOpList φs) + (superCommute (anPart φ)) (normalOrder (ofFieldOpList φs))𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOp⊢ normalOrder (crPart φ * ofFieldOpList φs + anPart φ * ofFieldOpList φs) +
    (superCommute (anPart φ)) (normalOrder (ofFieldOpList φs)) =
  normalOrder (ofFieldOp φ * ofFieldOpList φs) + (superCommute (anPart φ)) (normalOrder (ofFieldOpList φs)) anPart_mul_normalOrder_ofFieldOpList_eq_superCommute_reorder,𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOp⊢ crPart φ * normalOrder (ofFieldOpList φs) +
    (normalOrder (anPart φ * ofFieldOpList φs) + (superCommute (anPart φ)) (normalOrder (ofFieldOpList φs))) =
  normalOrder (ofFieldOp φ * ofFieldOpList φs) + (superCommute (anPart φ)) (normalOrder (ofFieldOpList φs))𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOp⊢ normalOrder (crPart φ * ofFieldOpList φs + anPart φ * ofFieldOpList φs) +
    (superCommute (anPart φ)) (normalOrder (ofFieldOpList φs)) =
  normalOrder (ofFieldOp φ * ofFieldOpList φs) + (superCommute (anPart φ)) (normalOrder (ofFieldOpList φs)) ← add_assoc,𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOp⊢ crPart φ * normalOrder (ofFieldOpList φs) + normalOrder (anPart φ * ofFieldOpList φs) +
    (superCommute (anPart φ)) (normalOrder (ofFieldOpList φs)) =
  normalOrder (ofFieldOp φ * ofFieldOpList φs) + (superCommute (anPart φ)) (normalOrder (ofFieldOpList φs))𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOp⊢ normalOrder (crPart φ * ofFieldOpList φs + anPart φ * ofFieldOpList φs) +
    (superCommute (anPart φ)) (normalOrder (ofFieldOpList φs)) =
  normalOrder (ofFieldOp φ * ofFieldOpList φs) + (superCommute (anPart φ)) (normalOrder (ofFieldOpList φs))
    ← crPart_mul_normalOrder,𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOp⊢ normalOrder (crPart φ * ofFieldOpList φs) + normalOrder (anPart φ * ofFieldOpList φs) +
    (superCommute (anPart φ)) (normalOrder (ofFieldOpList φs)) =
  normalOrder (ofFieldOp φ * ofFieldOpList φs) + (superCommute (anPart φ)) (normalOrder (ofFieldOpList φs))𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOp⊢ normalOrder (crPart φ * ofFieldOpList φs + anPart φ * ofFieldOpList φs) +
    (superCommute (anPart φ)) (normalOrder (ofFieldOpList φs)) =
  normalOrder (ofFieldOp φ * ofFieldOpList φs) + (superCommute (anPart φ)) (normalOrder (ofFieldOpList φs)) ← map_add𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOp⊢ normalOrder (crPart φ * ofFieldOpList φs + anPart φ * ofFieldOpList φs) +
    (superCommute (anPart φ)) (normalOrder (ofFieldOpList φs)) =
  normalOrder (ofFieldOp φ * ofFieldOpList φs) + (superCommute (anPart φ)) (normalOrder (ofFieldOpList φs))𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOp⊢ normalOrder (crPart φ * ofFieldOpList φs + anPart φ * ofFieldOpList φs) +
    (superCommute (anPart φ)) (normalOrder (ofFieldOpList φs)) =
  normalOrder (ofFieldOp φ * ofFieldOpList φs) + (superCommute (anPart φ)) (normalOrder (ofFieldOpList φs))]𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOp⊢ normalOrder (crPart φ * ofFieldOpList φs + anPart φ * ofFieldOpList φs) +
    (superCommute (anPart φ)) (normalOrder (ofFieldOpList φs)) =
  normalOrder (ofFieldOp φ * ofFieldOpList φs) + (superCommute (anPart φ)) (normalOrder (ofFieldOpList φs))
  conv_lhs =>
    lhs𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOp| normalOrder (crPart φ * ofFieldOpList φs + anPart φ * ofFieldOpList φs)
    rw [← add_mul, ← ofFieldOp_eq_crPart_add_anPart]𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOp| normalOrder (ofFieldOp φ * ofFieldOpList φs)

For a field specification 𝓕, a φ in 𝓕.FieldOp and a list φs of 𝓕.FieldOp then φ * 𝓝(φ₀φ₁…φₙ) is equal to

𝓝(φφ₀φ₁…φₙ) + ∑ i, (𝓢(φ,φ₀φ₁…φᵢ₋₁) • [anPart φ, φᵢ]ₛ) * 𝓝(φ₀…φᵢ₋₁φᵢ₊₁…φₙ).

The proof ultimately goes as follows:

ofFieldOp_eq_crPart_add_anPart is used to split φ into its creation and annihilation parts.

The following relation is then used

crPart φ * 𝓝(φ₀φ₁…φₙ) = 𝓝(crPart φ * φ₀φ₁…φₙ).

It used that anPart φ * 𝓝(φ₀φ₁…φₙ) is equal to

𝓢(φ, φ₀φ₁…φₙ) 𝓝(φ₀φ₁…φₙ) * anPart φ + [anPart φ, 𝓝(φ₀φ₁…φₙ)]

Then it is used that

𝓢(φ, φ₀φ₁…φₙ) 𝓝(φ₀φ₁…φₙ) * anPart φ = 𝓝(anPart φ * φ₀φ₁…φₙ)

The result ofCrAnOp_superCommute_normalOrder_ofCrAnList_sum is used to expand [anPart φ, 𝓝(φ₀φ₁…φₙ)] as a sum.


lemma ofFieldOp_mul_normalOrder_ofFieldOpList_eq_sum (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) :
    ofFieldOp φ * 𝓝(ofFieldOpList φs) =
    ∑ n : Option (Fin φs.length), contractStateAtIndex φ φs n *
    𝓝(ofFieldOpList (optionEraseZ φs φ n)) := by𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOp⊢ ofFieldOp φ * normalOrder (ofFieldOpList φs) =
  ∑ n, contractStateAtIndex φ φs n * normalOrder (ofFieldOpList (optionEraseZ φs φ n))
  rw [ofFieldOp_mul_normalOrder_ofFieldOpList_eq_superCommute𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOp⊢ normalOrder (ofFieldOp φ * ofFieldOpList φs) + (superCommute (anPart φ)) (normalOrder (ofFieldOpList φs)) =
  ∑ n, contractStateAtIndex φ φs n * normalOrder (ofFieldOpList (optionEraseZ φs φ n))𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOp⊢ normalOrder (ofFieldOp φ * ofFieldOpList φs) + (superCommute (anPart φ)) (normalOrder (ofFieldOpList φs)) =
  ∑ n, contractStateAtIndex φ φs n * normalOrder (ofFieldOpList (optionEraseZ φs φ n))]𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOp⊢ normalOrder (ofFieldOp φ * ofFieldOpList φs) + (superCommute (anPart φ)) (normalOrder (ofFieldOpList φs)) =
  ∑ n, contractStateAtIndex φ φs n * normalOrder (ofFieldOpList (optionEraseZ φs φ n))
  rw [anPart_superCommute_normalOrder_ofFieldOpList_sum𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOp⊢ normalOrder (ofFieldOp φ * ofFieldOpList φs) +
    ∑ n,
      (exchangeSign (𝓕|>ₛφ)) (ofList 𝓕.fieldOpStatistic (List.take (↑n) φs)) •
          (superCommute (anPart φ)) ↑(ofFieldOpF φs[n]) *
        normalOrder (ofFieldOpList (φs.eraseIdx ↑n)) =
  ∑ n, contractStateAtIndex φ φs n * normalOrder (ofFieldOpList (optionEraseZ φs φ n))𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOp⊢ normalOrder (ofFieldOp φ * ofFieldOpList φs) +
    ∑ n,
      (exchangeSign (𝓕|>ₛφ)) (ofList 𝓕.fieldOpStatistic (List.take (↑n) φs)) •
          (superCommute (anPart φ)) ↑(ofFieldOpF φs[n]) *
        normalOrder (ofFieldOpList (φs.eraseIdx ↑n)) =
  ∑ n, contractStateAtIndex φ φs n * normalOrder (ofFieldOpList (optionEraseZ φs φ n))]𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOp⊢ normalOrder (ofFieldOp φ * ofFieldOpList φs) +
    ∑ n,
      (exchangeSign (𝓕|>ₛφ)) (ofList 𝓕.fieldOpStatistic (List.take (↑n) φs)) •
          (superCommute (anPart φ)) ↑(ofFieldOpF φs[n]) *
        normalOrder (ofFieldOpList (φs.eraseIdx ↑n)) =
  ∑ n, contractStateAtIndex φ φs n * normalOrder (ofFieldOpList (optionEraseZ φs φ n))
  simp only [Fin.getElem_fin, Algebra.smul_mul_assoc, contractStateAtIndex,
    Fintype.sum_option, one_mul]𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOp⊢ normalOrder (ofFieldOp φ * ofFieldOpList φs) +
    ∑ x,
      (exchangeSign (𝓕|>ₛφ)) (ofList 𝓕.fieldOpStatistic (List.take (↑x) φs)) •
        ((superCommute (anPart φ)) ↑(ofFieldOpF φs[↑x]) * normalOrder (ofFieldOpList (φs.eraseIdx ↑x))) =
  normalOrder (ofFieldOpList (optionEraseZ φs φ none)) +
    ∑ x,
      (exchangeSign (𝓕|>ₛφ)) (ofList 𝓕.fieldOpStatistic (List.take (↑x) φs)) •
        ((superCommute (anPart φ)) (ofFieldOp φs[↑x]) * normalOrder (ofFieldOpList (optionEraseZ φs φ (some x))))
  rflAll goals completed! 🐙

Cons vs insertIdx for a normal ordered term.

Within a proto-operator algebra, N(φφ₀φ₁…φₙ) = s • N(φ₀…φₖ₋₁φφₖ…φₙ), where s is the exchange sign for φ and φ₀…φₖ₋₁.


lemma ofFieldOpList_normalOrder_insert (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
    (k : Fin φs.length.succ) : 𝓝(ofFieldOpList (φ :: φs)) =
    𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φs.take k) • 𝓝(ofFieldOpList (φs.insertIdx k φ)) := by𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpk:Fin φs.length.succ⊢ normalOrder (ofFieldOpList (φ :: φs)) =
  (exchangeSign (𝓕|>ₛφ)) (ofList 𝓕.fieldOpStatistic (List.take (↑k) φs)) •
    normalOrder (ofFieldOpList (φs.insertIdx (↑k) φ))
  have hl : φs.insertIdx k φ = φs.take k ++ [φ] ++ φs.drop k := by
    rw [Physlib.List.insertIdx_eq_take_drop𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpk:Fin φs.length.succ⊢ List.take (↑k) φs ++ φ :: List.drop (↑k) φs = List.take (↑k) φs ++ [φ] ++ List.drop (↑k) φs𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpk:Fin φs.length.succ⊢ List.take (↑k) φs ++ φ :: List.drop (↑k) φs = List.take (↑k) φs ++ [φ] ++ List.drop (↑k) φs𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpk:Fin φs.length.succhl:φs.insertIdx (↑k) φ = List.take (↑k) φs ++ [φ] ++ List.drop (↑k) φs⊢ normalOrder (ofFieldOpList (φ :: φs)) =
  (exchangeSign (𝓕|>ₛφ)) (ofList 𝓕.fieldOpStatistic (List.take (↑k) φs)) •
    normalOrder (ofFieldOpList (φs.insertIdx (↑k) φ))]𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpk:Fin φs.length.succ⊢ List.take (↑k) φs ++ φ :: List.drop (↑k) φs = List.take (↑k) φs ++ [φ] ++ List.drop (↑k) φs𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpk:Fin φs.length.succhl:φs.insertIdx (↑k) φ = List.take (↑k) φs ++ [φ] ++ List.drop (↑k) φs⊢ normalOrder (ofFieldOpList (φ :: φs)) =
  (exchangeSign (𝓕|>ₛφ)) (ofList 𝓕.fieldOpStatistic (List.take (↑k) φs)) •
    normalOrder (ofFieldOpList (φs.insertIdx (↑k) φ))
    simp𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpk:Fin φs.length.succhl:φs.insertIdx (↑k) φ = List.take (↑k) φs ++ [φ] ++ List.drop (↑k) φs⊢ normalOrder (ofFieldOpList (φ :: φs)) =
  (exchangeSign (𝓕|>ₛφ)) (ofList 𝓕.fieldOpStatistic (List.take (↑k) φs)) •
    normalOrder (ofFieldOpList (φs.insertIdx (↑k) φ))𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpk:Fin φs.length.succhl:φs.insertIdx (↑k) φ = List.take (↑k) φs ++ [φ] ++ List.drop (↑k) φs⊢ normalOrder (ofFieldOpList (φ :: φs)) =
  (exchangeSign (𝓕|>ₛφ)) (ofList 𝓕.fieldOpStatistic (List.take (↑k) φs)) •
    normalOrder (ofFieldOpList (φs.insertIdx (↑k) φ))
  rw [hl𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpk:Fin φs.length.succhl:φs.insertIdx (↑k) φ = List.take (↑k) φs ++ [φ] ++ List.drop (↑k) φs⊢ normalOrder (ofFieldOpList (φ :: φs)) =
  (exchangeSign (𝓕|>ₛφ)) (ofList 𝓕.fieldOpStatistic (List.take (↑k) φs)) •
    normalOrder (ofFieldOpList (List.take (↑k) φs ++ [φ] ++ List.drop (↑k) φs))𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpk:Fin φs.length.succhl:φs.insertIdx (↑k) φ = List.take (↑k) φs ++ [φ] ++ List.drop (↑k) φs⊢ normalOrder (ofFieldOpList (φ :: φs)) =
  (exchangeSign (𝓕|>ₛφ)) (ofList 𝓕.fieldOpStatistic (List.take (↑k) φs)) •
    normalOrder (ofFieldOpList (List.take (↑k) φs ++ [φ] ++ List.drop (↑k) φs))]𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpk:Fin φs.length.succhl:φs.insertIdx (↑k) φ = List.take (↑k) φs ++ [φ] ++ List.drop (↑k) φs⊢ normalOrder (ofFieldOpList (φ :: φs)) =
  (exchangeSign (𝓕|>ₛφ)) (ofList 𝓕.fieldOpStatistic (List.take (↑k) φs)) •
    normalOrder (ofFieldOpList (List.take (↑k) φs ++ [φ] ++ List.drop (↑k) φs))
  rw [ofFieldOpList_append,𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpk:Fin φs.length.succhl:φs.insertIdx (↑k) φ = List.take (↑k) φs ++ [φ] ++ List.drop (↑k) φs⊢ normalOrder (ofFieldOpList (φ :: φs)) =
  (exchangeSign (𝓕|>ₛφ)) (ofList 𝓕.fieldOpStatistic (List.take (↑k) φs)) •
    normalOrder (ofFieldOpList (List.take (↑k) φs ++ [φ]) * ofFieldOpList (List.drop (↑k) φs))𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpk:Fin φs.length.succhl:φs.insertIdx (↑k) φ = List.take (↑k) φs ++ [φ] ++ List.drop (↑k) φs⊢ normalOrder (ofFieldOpList (φ :: φs)) =
  (exchangeSign (𝓕|>ₛφ)) (ofList 𝓕.fieldOpStatistic (List.take (↑k) φs)) •
    normalOrder (ofFieldOpList (List.take (↑k) φs) * ofFieldOpList [φ] * ofFieldOpList (List.drop (↑k) φs)) ofFieldOpList_append𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpk:Fin φs.length.succhl:φs.insertIdx (↑k) φ = List.take (↑k) φs ++ [φ] ++ List.drop (↑k) φs⊢ normalOrder (ofFieldOpList (φ :: φs)) =
  (exchangeSign (𝓕|>ₛφ)) (ofList 𝓕.fieldOpStatistic (List.take (↑k) φs)) •
    normalOrder (ofFieldOpList (List.take (↑k) φs) * ofFieldOpList [φ] * ofFieldOpList (List.drop (↑k) φs))𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpk:Fin φs.length.succhl:φs.insertIdx (↑k) φ = List.take (↑k) φs ++ [φ] ++ List.drop (↑k) φs⊢ normalOrder (ofFieldOpList (φ :: φs)) =
  (exchangeSign (𝓕|>ₛφ)) (ofList 𝓕.fieldOpStatistic (List.take (↑k) φs)) •
    normalOrder (ofFieldOpList (List.take (↑k) φs) * ofFieldOpList [φ] * ofFieldOpList (List.drop (↑k) φs))]𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpk:Fin φs.length.succhl:φs.insertIdx (↑k) φ = List.take (↑k) φs ++ [φ] ++ List.drop (↑k) φs⊢ normalOrder (ofFieldOpList (φ :: φs)) =
  (exchangeSign (𝓕|>ₛφ)) (ofList 𝓕.fieldOpStatistic (List.take (↑k) φs)) •
    normalOrder (ofFieldOpList (List.take (↑k) φs) * ofFieldOpList [φ] * ofFieldOpList (List.drop (↑k) φs))
  rw [ofFieldOpList_mul_ofFieldOpList_eq_superCommute,𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpk:Fin φs.length.succhl:φs.insertIdx (↑k) φ = List.take (↑k) φs ++ [φ] ++ List.drop (↑k) φs⊢ normalOrder (ofFieldOpList (φ :: φs)) =
  (exchangeSign (𝓕|>ₛφ)) (ofList 𝓕.fieldOpStatistic (List.take (↑k) φs)) •
    normalOrder
      (((exchangeSign (ofList 𝓕.fieldOpStatistic (List.take (↑k) φs))) (ofList 𝓕.fieldOpStatistic [φ]) •
              ofFieldOpList [φ] *
            ofFieldOpList (List.take (↑k) φs) +
          (superCommute (ofFieldOpList (List.take (↑k) φs))) (ofFieldOpList [φ])) *
        ofFieldOpList (List.drop (↑k) φs))𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpk:Fin φs.length.succhl:φs.insertIdx (↑k) φ = List.take (↑k) φs ++ [φ] ++ List.drop (↑k) φs⊢ normalOrder (ofFieldOpList (φ :: φs)) =
  (exchangeSign (𝓕|>ₛφ)) (ofList 𝓕.fieldOpStatistic (List.take (↑k) φs)) •
    normalOrder
      ((exchangeSign (ofList 𝓕.fieldOpStatistic (List.take (↑k) φs))) (ofList 𝓕.fieldOpStatistic [φ]) •
              ofFieldOpList [φ] *
            ofFieldOpList (List.take (↑k) φs) *
          ofFieldOpList (List.drop (↑k) φs) +
        (superCommute (ofFieldOpList (List.take (↑k) φs))) (ofFieldOpList [φ]) * ofFieldOpList (List.drop (↑k) φs)) add_mul𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpk:Fin φs.length.succhl:φs.insertIdx (↑k) φ = List.take (↑k) φs ++ [φ] ++ List.drop (↑k) φs⊢ normalOrder (ofFieldOpList (φ :: φs)) =
  (exchangeSign (𝓕|>ₛφ)) (ofList 𝓕.fieldOpStatistic (List.take (↑k) φs)) •
    normalOrder
      ((exchangeSign (ofList 𝓕.fieldOpStatistic (List.take (↑k) φs))) (ofList 𝓕.fieldOpStatistic [φ]) •
              ofFieldOpList [φ] *
            ofFieldOpList (List.take (↑k) φs) *
          ofFieldOpList (List.drop (↑k) φs) +
        (superCommute (ofFieldOpList (List.take (↑k) φs))) (ofFieldOpList [φ]) * ofFieldOpList (List.drop (↑k) φs))𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpk:Fin φs.length.succhl:φs.insertIdx (↑k) φ = List.take (↑k) φs ++ [φ] ++ List.drop (↑k) φs⊢ normalOrder (ofFieldOpList (φ :: φs)) =
  (exchangeSign (𝓕|>ₛφ)) (ofList 𝓕.fieldOpStatistic (List.take (↑k) φs)) •
    normalOrder
      ((exchangeSign (ofList 𝓕.fieldOpStatistic (List.take (↑k) φs))) (ofList 𝓕.fieldOpStatistic [φ]) •
              ofFieldOpList [φ] *
            ofFieldOpList (List.take (↑k) φs) *
          ofFieldOpList (List.drop (↑k) φs) +
        (superCommute (ofFieldOpList (List.take (↑k) φs))) (ofFieldOpList [φ]) * ofFieldOpList (List.drop (↑k) φs))]𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpk:Fin φs.length.succhl:φs.insertIdx (↑k) φ = List.take (↑k) φs ++ [φ] ++ List.drop (↑k) φs⊢ normalOrder (ofFieldOpList (φ :: φs)) =
  (exchangeSign (𝓕|>ₛφ)) (ofList 𝓕.fieldOpStatistic (List.take (↑k) φs)) •
    normalOrder
      ((exchangeSign (ofList 𝓕.fieldOpStatistic (List.take (↑k) φs))) (ofList 𝓕.fieldOpStatistic [φ]) •
              ofFieldOpList [φ] *
            ofFieldOpList (List.take (↑k) φs) *
          ofFieldOpList (List.drop (↑k) φs) +
        (superCommute (ofFieldOpList (List.take (↑k) φs))) (ofFieldOpList [φ]) * ofFieldOpList (List.drop (↑k) φs))
  simp only [Nat.succ_eq_add_one, ofList_singleton, Algebra.smul_mul_assoc,
    map_add, map_smul, normalOrder_superCommute_left_eq_zero, add_zero, smul_smul,
    exchangeSign_mul_self_swap, one_smul]𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpk:Fin φs.length.succhl:φs.insertIdx (↑k) φ = List.take (↑k) φs ++ [φ] ++ List.drop (↑k) φs⊢ normalOrder (ofFieldOpList (φ :: φs)) =
  normalOrder (ofFieldOpList [φ] * ofFieldOpList (List.take (↑k) φs) * ofFieldOpList (List.drop (↑k) φs))
  rw [← ofFieldOpList_append,𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpk:Fin φs.length.succhl:φs.insertIdx (↑k) φ = List.take (↑k) φs ++ [φ] ++ List.drop (↑k) φs⊢ normalOrder (ofFieldOpList (φ :: φs)) =
  normalOrder (ofFieldOpList ([φ] ++ List.take (↑k) φs) * ofFieldOpList (List.drop (↑k) φs))𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpk:Fin φs.length.succhl:φs.insertIdx (↑k) φ = List.take (↑k) φs ++ [φ] ++ List.drop (↑k) φs⊢ normalOrder (ofFieldOpList (φ :: φs)) = normalOrder (ofFieldOpList ([φ] ++ List.take (↑k) φs ++ List.drop (↑k) φs)) ← ofFieldOpList_append𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpk:Fin φs.length.succhl:φs.insertIdx (↑k) φ = List.take (↑k) φs ++ [φ] ++ List.drop (↑k) φs⊢ normalOrder (ofFieldOpList (φ :: φs)) = normalOrder (ofFieldOpList ([φ] ++ List.take (↑k) φs ++ List.drop (↑k) φs))𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpk:Fin φs.length.succhl:φs.insertIdx (↑k) φ = List.take (↑k) φs ++ [φ] ++ List.drop (↑k) φs⊢ normalOrder (ofFieldOpList (φ :: φs)) = normalOrder (ofFieldOpList ([φ] ++ List.take (↑k) φs ++ List.drop (↑k) φs))]𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpk:Fin φs.length.succhl:φs.insertIdx (↑k) φ = List.take (↑k) φs ++ [φ] ++ List.drop (↑k) φs⊢ normalOrder (ofFieldOpList (φ :: φs)) = normalOrder (ofFieldOpList ([φ] ++ List.take (↑k) φs ++ List.drop (↑k) φs))
  simpAll goals completed! 🐙

The normal ordering of a product of two states

              

@[simp]
lemma normalOrder_crPart_mul_crPart (φ φ' : 𝓕.FieldOp) :
    𝓝(crPart φ * crPart φ') = crPart φ * crPart φ' := by𝓕:FieldSpecificationφ:𝓕.FieldOpφ':𝓕.FieldOp⊢ normalOrder (crPart φ * crPart φ') = crPart φ * crPart φ'
  rw [crPart,𝓕:FieldSpecificationφ:𝓕.FieldOpφ':𝓕.FieldOp⊢ normalOrder (ι (crPartF φ) * crPart φ') = ι (crPartF φ) * crPart φ'All goals completed! 🐙 crPart,𝓕:FieldSpecificationφ:𝓕.FieldOpφ':𝓕.FieldOp⊢ normalOrder (ι (crPartF φ) * ι (crPartF φ')) = ι (crPartF φ) * ι (crPartF φ')All goals completed! 🐙 ← map_mul,𝓕:FieldSpecificationφ:𝓕.FieldOpφ':𝓕.FieldOp⊢ normalOrder (ι (crPartF φ * crPartF φ')) = ι (crPartF φ * crPartF φ')All goals completed! 🐙 normalOrder_eq_ι_normalOrderF,𝓕:FieldSpecificationφ:𝓕.FieldOpφ':𝓕.FieldOp⊢ ι (normalOrderF (crPartF φ * crPartF φ')) = ι (crPartF φ * crPartF φ')All goals completed! 🐙 normalOrderF_crPartF_mul_crPartF𝓕:FieldSpecificationφ:𝓕.FieldOpφ':𝓕.FieldOp⊢ ι (crPartF φ * crPartF φ') = ι (crPartF φ * crPartF φ')All goals completed! 🐙]All goals completed! 🐙

@[simp]
lemma normalOrder_anPart_mul_anPart (φ φ' : 𝓕.FieldOp) :
    𝓝(anPart φ * anPart φ') = anPart φ * anPart φ' := by𝓕:FieldSpecificationφ:𝓕.FieldOpφ':𝓕.FieldOp⊢ normalOrder (anPart φ * anPart φ') = anPart φ * anPart φ'
  rw [anPart,𝓕:FieldSpecificationφ:𝓕.FieldOpφ':𝓕.FieldOp⊢ normalOrder (ι (anPartF φ) * anPart φ') = ι (anPartF φ) * anPart φ'All goals completed! 🐙 anPart,𝓕:FieldSpecificationφ:𝓕.FieldOpφ':𝓕.FieldOp⊢ normalOrder (ι (anPartF φ) * ι (anPartF φ')) = ι (anPartF φ) * ι (anPartF φ')All goals completed! 🐙 ← map_mul,𝓕:FieldSpecificationφ:𝓕.FieldOpφ':𝓕.FieldOp⊢ normalOrder (ι (anPartF φ * anPartF φ')) = ι (anPartF φ * anPartF φ')All goals completed! 🐙 normalOrder_eq_ι_normalOrderF,𝓕:FieldSpecificationφ:𝓕.FieldOpφ':𝓕.FieldOp⊢ ι (normalOrderF (anPartF φ * anPartF φ')) = ι (anPartF φ * anPartF φ')All goals completed! 🐙 normalOrderF_anPartF_mul_anPartF𝓕:FieldSpecificationφ:𝓕.FieldOpφ':𝓕.FieldOp⊢ ι (anPartF φ * anPartF φ') = ι (anPartF φ * anPartF φ')All goals completed! 🐙]All goals completed! 🐙

@[simp]
lemma normalOrder_crPart_mul_anPart (φ φ' : 𝓕.FieldOp) :
    𝓝(crPart φ * anPart φ') = crPart φ * anPart φ' := by𝓕:FieldSpecificationφ:𝓕.FieldOpφ':𝓕.FieldOp⊢ normalOrder (crPart φ * anPart φ') = crPart φ * anPart φ'
  rw [crPart,𝓕:FieldSpecificationφ:𝓕.FieldOpφ':𝓕.FieldOp⊢ normalOrder (ι (crPartF φ) * anPart φ') = ι (crPartF φ) * anPart φ'All goals completed! 🐙 anPart,𝓕:FieldSpecificationφ:𝓕.FieldOpφ':𝓕.FieldOp⊢ normalOrder (ι (crPartF φ) * ι (anPartF φ')) = ι (crPartF φ) * ι (anPartF φ')All goals completed! 🐙 ← map_mul,𝓕:FieldSpecificationφ:𝓕.FieldOpφ':𝓕.FieldOp⊢ normalOrder (ι (crPartF φ * anPartF φ')) = ι (crPartF φ * anPartF φ')All goals completed! 🐙 normalOrder_eq_ι_normalOrderF,𝓕:FieldSpecificationφ:𝓕.FieldOpφ':𝓕.FieldOp⊢ ι (normalOrderF (crPartF φ * anPartF φ')) = ι (crPartF φ * anPartF φ')All goals completed! 🐙 normalOrderF_crPartF_mul_anPartF𝓕:FieldSpecificationφ:𝓕.FieldOpφ':𝓕.FieldOp⊢ ι (crPartF φ * anPartF φ') = ι (crPartF φ * anPartF φ')All goals completed! 🐙]All goals completed! 🐙

@[simp]
lemma normalOrder_anPart_mul_crPart (φ φ' : 𝓕.FieldOp) :
    𝓝(anPart φ * crPart φ') = 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') • crPart φ' * anPart φ := by𝓕:FieldSpecificationφ:𝓕.FieldOpφ':𝓕.FieldOp⊢ normalOrder (anPart φ * crPart φ') = (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛφ') • crPart φ' * anPart φ
  rw [anPart,𝓕:FieldSpecificationφ:𝓕.FieldOpφ':𝓕.FieldOp⊢ normalOrder (ι (anPartF φ) * crPart φ') = (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛφ') • crPart φ' * ι (anPartF φ)𝓕:FieldSpecificationφ:𝓕.FieldOpφ':𝓕.FieldOp⊢ ι ((exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛφ') • (crPartF φ' * anPartF φ)) =
  (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛφ') • ι (crPartF φ') * ι (anPartF φ) crPart,𝓕:FieldSpecificationφ:𝓕.FieldOpφ':𝓕.FieldOp⊢ normalOrder (ι (anPartF φ) * ι (crPartF φ')) = (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛφ') • ι (crPartF φ') * ι (anPartF φ)𝓕:FieldSpecificationφ:𝓕.FieldOpφ':𝓕.FieldOp⊢ ι ((exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛφ') • (crPartF φ' * anPartF φ)) =
  (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛφ') • ι (crPartF φ') * ι (anPartF φ) ← map_mul,𝓕:FieldSpecificationφ:𝓕.FieldOpφ':𝓕.FieldOp⊢ normalOrder (ι (anPartF φ * crPartF φ')) = (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛφ') • ι (crPartF φ') * ι (anPartF φ)𝓕:FieldSpecificationφ:𝓕.FieldOpφ':𝓕.FieldOp⊢ ι ((exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛφ') • (crPartF φ' * anPartF φ)) =
  (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛφ') • ι (crPartF φ') * ι (anPartF φ) normalOrder_eq_ι_normalOrderF,𝓕:FieldSpecificationφ:𝓕.FieldOpφ':𝓕.FieldOp⊢ ι (normalOrderF (anPartF φ * crPartF φ')) = (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛφ') • ι (crPartF φ') * ι (anPartF φ)𝓕:FieldSpecificationφ:𝓕.FieldOpφ':𝓕.FieldOp⊢ ι ((exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛφ') • (crPartF φ' * anPartF φ)) =
  (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛφ') • ι (crPartF φ') * ι (anPartF φ) normalOrderF_anPartF_mul_crPartF𝓕:FieldSpecificationφ:𝓕.FieldOpφ':𝓕.FieldOp⊢ ι ((exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛφ') • (crPartF φ' * anPartF φ)) =
  (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛφ') • ι (crPartF φ') * ι (anPartF φ)𝓕:FieldSpecificationφ:𝓕.FieldOpφ':𝓕.FieldOp⊢ ι ((exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛφ') • (crPartF φ' * anPartF φ)) =
  (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛφ') • ι (crPartF φ') * ι (anPartF φ)]𝓕:FieldSpecificationφ:𝓕.FieldOpφ':𝓕.FieldOp⊢ ι ((exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛφ') • (crPartF φ' * anPartF φ)) =
  (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛφ') • ι (crPartF φ') * ι (anPartF φ)
  simpAll goals completed! 🐙

lemma normalOrder_ofFieldOp_mul_ofFieldOp (φ φ' : 𝓕.FieldOp) : 𝓝(ofFieldOp φ * ofFieldOp φ') =
    crPart φ * crPart φ' + 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') • (crPart φ' * anPart φ) +
    crPart φ * anPart φ' + anPart φ * anPart φ' := by𝓕:FieldSpecificationφ:𝓕.FieldOpφ':𝓕.FieldOp⊢ normalOrder (ofFieldOp φ * ofFieldOp φ') =
  crPart φ * crPart φ' + (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛφ') • (crPart φ' * anPart φ) + crPart φ * anPart φ' +
    anPart φ * anPart φ'
  rw [ofFieldOp,𝓕:FieldSpecificationφ:𝓕.FieldOpφ':𝓕.FieldOp⊢ normalOrder (ι (ofFieldOpF φ) * ofFieldOp φ') =
  crPart φ * crPart φ' + (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛφ') • (crPart φ' * anPart φ) + crPart φ * anPart φ' +
    anPart φ * anPart φ'𝓕:FieldSpecificationφ:𝓕.FieldOpφ':𝓕.FieldOp⊢ ι
    (crPartF φ * crPartF φ' + (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛφ') • (crPartF φ' * anPartF φ) + crPartF φ * anPartF φ' +
      anPartF φ * anPartF φ') =
  crPart φ * crPart φ' + (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛφ') • (crPart φ' * anPart φ) + crPart φ * anPart φ' +
    anPart φ * anPart φ' ofFieldOp,𝓕:FieldSpecificationφ:𝓕.FieldOpφ':𝓕.FieldOp⊢ normalOrder (ι (ofFieldOpF φ) * ι (ofFieldOpF φ')) =
  crPart φ * crPart φ' + (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛφ') • (crPart φ' * anPart φ) + crPart φ * anPart φ' +
    anPart φ * anPart φ'𝓕:FieldSpecificationφ:𝓕.FieldOpφ':𝓕.FieldOp⊢ ι
    (crPartF φ * crPartF φ' + (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛφ') • (crPartF φ' * anPartF φ) + crPartF φ * anPartF φ' +
      anPartF φ * anPartF φ') =
  crPart φ * crPart φ' + (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛφ') • (crPart φ' * anPart φ) + crPart φ * anPart φ' +
    anPart φ * anPart φ' ← map_mul,𝓕:FieldSpecificationφ:𝓕.FieldOpφ':𝓕.FieldOp⊢ normalOrder (ι (ofFieldOpF φ * ofFieldOpF φ')) =
  crPart φ * crPart φ' + (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛφ') • (crPart φ' * anPart φ) + crPart φ * anPart φ' +
    anPart φ * anPart φ'𝓕:FieldSpecificationφ:𝓕.FieldOpφ':𝓕.FieldOp⊢ ι
    (crPartF φ * crPartF φ' + (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛφ') • (crPartF φ' * anPartF φ) + crPartF φ * anPartF φ' +
      anPartF φ * anPartF φ') =
  crPart φ * crPart φ' + (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛφ') • (crPart φ' * anPart φ) + crPart φ * anPart φ' +
    anPart φ * anPart φ' normalOrder_eq_ι_normalOrderF,𝓕:FieldSpecificationφ:𝓕.FieldOpφ':𝓕.FieldOp⊢ ι (normalOrderF (ofFieldOpF φ * ofFieldOpF φ')) =
  crPart φ * crPart φ' + (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛφ') • (crPart φ' * anPart φ) + crPart φ * anPart φ' +
    anPart φ * anPart φ'𝓕:FieldSpecificationφ:𝓕.FieldOpφ':𝓕.FieldOp⊢ ι
    (crPartF φ * crPartF φ' + (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛφ') • (crPartF φ' * anPartF φ) + crPartF φ * anPartF φ' +
      anPartF φ * anPartF φ') =
  crPart φ * crPart φ' + (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛφ') • (crPart φ' * anPart φ) + crPart φ * anPart φ' +
    anPart φ * anPart φ'
    normalOrderF_ofFieldOpF_mul_ofFieldOpF𝓕:FieldSpecificationφ:𝓕.FieldOpφ':𝓕.FieldOp⊢ ι
    (crPartF φ * crPartF φ' + (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛφ') • (crPartF φ' * anPartF φ) + crPartF φ * anPartF φ' +
      anPartF φ * anPartF φ') =
  crPart φ * crPart φ' + (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛφ') • (crPart φ' * anPart φ) + crPart φ * anPart φ' +
    anPart φ * anPart φ'𝓕:FieldSpecificationφ:𝓕.FieldOpφ':𝓕.FieldOp⊢ ι
    (crPartF φ * crPartF φ' + (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛφ') • (crPartF φ' * anPartF φ) + crPartF φ * anPartF φ' +
      anPartF φ * anPartF φ') =
  crPart φ * crPart φ' + (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛφ') • (crPart φ' * anPart φ) + crPart φ * anPart φ' +
    anPart φ * anPart φ']𝓕:FieldSpecificationφ:𝓕.FieldOpφ':𝓕.FieldOp⊢ ι
    (crPartF φ * crPartF φ' + (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛφ') • (crPartF φ' * anPartF φ) + crPartF φ * anPartF φ' +
      anPartF φ * anPartF φ') =
  crPart φ * crPart φ' + (exchangeSign (𝓕|>ₛφ)) (𝓕|>ₛφ') • (crPart φ' * anPart φ) + crPart φ * anPart φ' +
    anPart φ * anPart φ'
  rflAll goals completed! 🐙