refactor: supercommute notation

2025-01-23 15:06:11 +00:00 · 2025-01-23 15:06:11 +00:00 · 7d053695dd
commit 7d053695dd
parent 5a25cd0f5c
5 changed files with 113 additions and 127 deletions
--- a/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/NormalOrder.lean
+++ b/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/NormalOrder.lean
@ -36,12 +36,14 @@ def normalOrder : CrAnAlgebra 𝓕 →ₗ[ℂ] CrAnAlgebra 𝓕 :=
  Basis.constr ofCrAnListBasis ℂ fun φs =>
  normalOrderSign φs • ofCrAnList (normalOrderList φs)

+scoped[FieldSpecification.CrAnAlgebra] notation "𝓝(" a ")" => normalOrder a
+
 lemma normalOrder_ofCrAnList (φs : List 𝓕.CrAnStates) :
-    normalOrder (ofCrAnList φs) = normalOrderSign φs • ofCrAnList (normalOrderList φs) := by
+    𝓝(ofCrAnList φs) = normalOrderSign φs • ofCrAnList (normalOrderList φs) := by
  rw [← ofListBasis_eq_ofList, normalOrder, Basis.constr_basis]

 lemma ofCrAnList_eq_normalOrder (φs : List 𝓕.CrAnStates) :
-    ofCrAnList (normalOrderList φs) = normalOrderSign φs • normalOrder (ofCrAnList φs) := by
+    ofCrAnList (normalOrderList φs) = normalOrderSign φs • 𝓝(ofCrAnList φs) := by
  rw [normalOrder_ofCrAnList, normalOrderList, smul_smul, normalOrderSign, Wick.koszulSign_mul_self,
    one_smul]

@ -57,15 +59,13 @@ lemma normalOrder_one : normalOrder (𝓕 := 𝓕) 1 = 1 := by

 lemma normalOrder_ofCrAnList_cons_create (φ : 𝓕.CrAnStates)
    (hφ : 𝓕 |>ᶜ φ = CreateAnnihilate.create) (φs : List 𝓕.CrAnStates) :
-    normalOrder (ofCrAnList (φ :: φs)) =
-    ofCrAnState φ * normalOrder (ofCrAnList φs) := by
+    𝓝(ofCrAnList (φ :: φs)) = ofCrAnState φ * 𝓝(ofCrAnList φs) := by
  rw [normalOrder_ofCrAnList, normalOrderSign_cons_create φ hφ, normalOrderList_cons_create φ hφ φs]
  rw [ofCrAnList_cons, normalOrder_ofCrAnList, mul_smul_comm]

 lemma normalOrder_create_mul (φ : 𝓕.CrAnStates)
-    (hφ : 𝓕 |>ᶜ φ = CreateAnnihilate.create)
-    (a : CrAnAlgebra 𝓕) :
-    normalOrder (ofCrAnState φ * a) = ofCrAnState φ * normalOrder a := by
+    (hφ : 𝓕 |>ᶜ φ = CreateAnnihilate.create) (a : CrAnAlgebra 𝓕) :
+    𝓝(ofCrAnState φ * a) = ofCrAnState φ * 𝓝(a) := by
  change (normalOrder ∘ₗ mulLinearMap (ofCrAnState φ)) a =
    (mulLinearMap (ofCrAnState φ) ∘ₗ normalOrder) a
  refine LinearMap.congr_fun (ofCrAnListBasis.ext fun l ↦ ?_) a
@ -75,16 +75,14 @@ lemma normalOrder_create_mul (φ : 𝓕.CrAnStates)

 lemma normalOrder_ofCrAnList_append_annihilate (φ : 𝓕.CrAnStates)
    (hφ : 𝓕 |>ᶜ φ = CreateAnnihilate.annihilate) (φs : List 𝓕.CrAnStates) :
-    normalOrder (ofCrAnList (φs ++ [φ])) =
-    normalOrder (ofCrAnList φs) * ofCrAnState φ := by
+    𝓝(ofCrAnList (φs ++ [φ])) = 𝓝(ofCrAnList φs) * ofCrAnState φ := by
  rw [normalOrder_ofCrAnList, normalOrderSign_append_annihlate φ hφ φs,
    normalOrderList_append_annihilate φ hφ φs, ofCrAnList_append, ofCrAnList_singleton,
      normalOrder_ofCrAnList, smul_mul_assoc]

 lemma normalOrder_mul_annihilate (φ : 𝓕.CrAnStates)
    (hφ : 𝓕 |>ᶜ φ = CreateAnnihilate.annihilate)
-    (a : CrAnAlgebra 𝓕) :
-    normalOrder (a * ofCrAnState φ) = normalOrder a * ofCrAnState φ := by
+    (a : CrAnAlgebra 𝓕) : 𝓝(a * ofCrAnState φ) = 𝓝(a) * ofCrAnState φ := by
  change (normalOrder ∘ₗ mulLinearMap.flip (ofCrAnState φ)) a =
    (mulLinearMap.flip (ofCrAnState φ) ∘ₗ normalOrder) a
  refine LinearMap.congr_fun (ofCrAnListBasis.ext fun l ↦ ?_) a
@ -94,8 +92,8 @@ lemma normalOrder_mul_annihilate (φ : 𝓕.CrAnStates)
    normalOrder_ofCrAnList_append_annihilate φ hφ]

 lemma normalOrder_crPart_mul (φ : 𝓕.States) (a : CrAnAlgebra 𝓕) :
-    normalOrder (crPart (StateAlgebra.ofState φ) * a) =
-    crPart (StateAlgebra.ofState φ) * normalOrder a := by
+    𝓝(crPart (StateAlgebra.ofState φ) * a) =
+    crPart (StateAlgebra.ofState φ) * 𝓝(a) := by
  match φ with
  | .inAsymp φ =>
    rw [crPart, StateAlgebra.ofState, FreeAlgebra.lift_ι_apply]
@ -106,8 +104,8 @@ lemma normalOrder_crPart_mul (φ : 𝓕.States) (a : CrAnAlgebra 𝓕) :
  | .outAsymp φ => simp

 lemma normalOrder_mul_anPart (φ : 𝓕.States) (a : CrAnAlgebra 𝓕) :
-    normalOrder (a * anPart (StateAlgebra.ofState φ)) =
-    normalOrder a * anPart (StateAlgebra.ofState φ) := by
+    𝓝(a * anPart (StateAlgebra.ofState φ)) =
+    𝓝(a) * anPart (StateAlgebra.ofState φ) := by
  match φ with
  | .inAsymp φ => simp
  | .position φ =>
@ -127,9 +125,8 @@ The main result of this section is `normalOrder_superCommute_annihilate_create`.
 lemma normalOrder_swap_create_annihlate_ofCrAnList_ofCrAnList (φc φa : 𝓕.CrAnStates)
    (hφc : 𝓕 |>ᶜ φc = CreateAnnihilate.create) (hφa : 𝓕 |>ᶜ φa = CreateAnnihilate.annihilate)
    (φs φs' : List 𝓕.CrAnStates) :
-    normalOrder (ofCrAnList φs' * ofCrAnState φc * ofCrAnState φa * ofCrAnList φs) =
-    𝓢(𝓕 |>ₛ φc, 𝓕 |>ₛ φa) •
-    normalOrder (ofCrAnList φs' * ofCrAnState φa * ofCrAnState φc * ofCrAnList φs) := by
+    𝓝(ofCrAnList φs' * ofCrAnState φc * ofCrAnState φa * ofCrAnList φs) = 𝓢(𝓕 |>ₛ φc, 𝓕 |>ₛ φa) •
+    𝓝(ofCrAnList φs' * ofCrAnState φa * ofCrAnState φc * ofCrAnList φs) := by
  rw [mul_assoc, mul_assoc, ← ofCrAnList_cons, ← ofCrAnList_cons, ← ofCrAnList_append]
  rw [normalOrder_ofCrAnList, normalOrderSign_swap_create_annihlate φc φa hφc hφa]
  rw [normalOrderList_swap_create_annihlate φc φa hφc hφa, ← smul_smul, ← normalOrder_ofCrAnList]
@ -139,9 +136,8 @@ lemma normalOrder_swap_create_annihlate_ofCrAnList_ofCrAnList (φc φa : 𝓕.Cr
 lemma normalOrder_swap_create_annihlate_ofCrAnList (φc φa : 𝓕.CrAnStates)
    (hφc : 𝓕 |>ᶜ φc = CreateAnnihilate.create) (hφa : 𝓕 |>ᶜ φa = CreateAnnihilate.annihilate)
    (φs : List 𝓕.CrAnStates) (a : 𝓕.CrAnAlgebra) :
-    normalOrder (ofCrAnList φs * ofCrAnState φc * ofCrAnState φa * a) =
-    𝓢(𝓕 |>ₛ φc, 𝓕 |>ₛ φa) •
-    normalOrder (ofCrAnList φs * ofCrAnState φa * ofCrAnState φc * a) := by
+    𝓝(ofCrAnList φs * ofCrAnState φc * ofCrAnState φa * a) = 𝓢(𝓕 |>ₛ φc, 𝓕 |>ₛ φa) •
+    𝓝(ofCrAnList φs * ofCrAnState φa * ofCrAnState φc * a) := by
  change (normalOrder ∘ₗ mulLinearMap (ofCrAnList φs * ofCrAnState φc * ofCrAnState φa)) a =
    (smulLinearMap _ ∘ₗ normalOrder ∘ₗ
    mulLinearMap (ofCrAnList φs * ofCrAnState φa * ofCrAnState φc)) a
@ -154,9 +150,8 @@ lemma normalOrder_swap_create_annihlate_ofCrAnList (φc φa : 𝓕.CrAnStates)
 lemma normalOrder_swap_create_annihlate (φc φa : 𝓕.CrAnStates)
    (hφc : 𝓕 |>ᶜ φc = CreateAnnihilate.create) (hφa : 𝓕 |>ᶜ φa = CreateAnnihilate.annihilate)
    (a b : 𝓕.CrAnAlgebra) :
-    normalOrder (a * ofCrAnState φc * ofCrAnState φa * b) =
-    𝓢(𝓕 |>ₛ φc, 𝓕 |>ₛ φa) •
-    normalOrder (a * ofCrAnState φa * ofCrAnState φc * b) := by
+    𝓝(a * ofCrAnState φc * ofCrAnState φa * b) = 𝓢(𝓕 |>ₛ φc, 𝓕 |>ₛ φa) •
+    𝓝(a * ofCrAnState φa * ofCrAnState φc * b) := by
  rw [mul_assoc, mul_assoc, mul_assoc, mul_assoc]
  change (normalOrder ∘ₗ mulLinearMap.flip (ofCrAnState φc * (ofCrAnState φa * b))) a =
    (smulLinearMap (𝓢(𝓕 |>ₛ φc, 𝓕 |>ₛ φa)) ∘ₗ
@ -170,7 +165,7 @@ lemma normalOrder_swap_create_annihlate (φc φa : 𝓕.CrAnStates)
 lemma normalOrder_superCommute_create_annihilate (φc φa : 𝓕.CrAnStates)
    (hφc : 𝓕 |>ᶜ φc = CreateAnnihilate.create) (hφa : 𝓕 |>ᶜ φa = CreateAnnihilate.annihilate)
    (a b : 𝓕.CrAnAlgebra) :
-    normalOrder (a * superCommute (ofCrAnState φc) (ofCrAnState φa) * b) = 0 := by
+    𝓝(a * [ofCrAnState φc, ofCrAnState φa]ₛca * b) = 0 := by
  simp only [superCommute_ofCrAnState_ofCrAnState, instCommGroup.eq_1, Algebra.smul_mul_assoc]
  rw [mul_sub, sub_mul, map_sub, ← smul_mul_assoc, ← mul_assoc, ← mul_assoc,
    normalOrder_swap_create_annihlate φc φa hφc hφa]
@ -179,17 +174,16 @@ lemma normalOrder_superCommute_create_annihilate (φc φa : 𝓕.CrAnStates)
 lemma normalOrder_superCommute_annihilate_create (φc φa : 𝓕.CrAnStates)
    (hφc : 𝓕 |>ᶜ φc = CreateAnnihilate.create) (hφa : 𝓕 |>ᶜ φa = CreateAnnihilate.annihilate)
    (a b : 𝓕.CrAnAlgebra) :
-    normalOrder (a * superCommute (ofCrAnState φa) (ofCrAnState φc) * b) = 0 := by
+    𝓝(a * [ofCrAnState φa, ofCrAnState φc]ₛca * b) = 0 := by
  rw [superCommute_ofCrAnState_ofCrAnState_symm]
  simp only [instCommGroup.eq_1, neg_smul, mul_neg, Algebra.mul_smul_comm, neg_mul,
    Algebra.smul_mul_assoc, map_neg, map_smul, neg_eq_zero, smul_eq_zero]
  exact Or.inr (normalOrder_superCommute_create_annihilate φc φa hφc hφa ..)

 lemma normalOrder_swap_crPart_anPart (φ φ' : 𝓕.States) (a b : CrAnAlgebra 𝓕) :
-    normalOrder (a * (crPart (StateAlgebra.ofState φ)) * (anPart (StateAlgebra.ofState φ')) * b) =
+    𝓝(a * (crPart (StateAlgebra.ofState φ)) * (anPart (StateAlgebra.ofState φ')) * b) =
    𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') •
-    normalOrder (a * (anPart (StateAlgebra.ofState φ')) *
-      (crPart (StateAlgebra.ofState φ)) * b) := by
+    𝓝(a * (anPart (StateAlgebra.ofState φ')) * (crPart (StateAlgebra.ofState φ)) * b) := by
  match φ, φ' with
  | _, .inAsymp φ' => simp
  | .outAsymp φ, _ => simp
@ -223,14 +217,14 @@ Using the results from above.
 -/

 lemma normalOrder_swap_anPart_crPart (φ φ' : 𝓕.States) (a b : CrAnAlgebra 𝓕) :
-    normalOrder (a * (anPart (StateAlgebra.ofState φ)) * (crPart (StateAlgebra.ofState φ')) * b) =
-    𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') • normalOrder (a * (crPart (StateAlgebra.ofState φ')) *
+    𝓝(a * (anPart (StateAlgebra.ofState φ)) * (crPart (StateAlgebra.ofState φ')) * b) =
+    𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') • 𝓝(a * (crPart (StateAlgebra.ofState φ')) *
      (anPart (StateAlgebra.ofState φ)) * b) := by
  simp [normalOrder_swap_crPart_anPart, smul_smul]

 lemma normalOrder_superCommute_crPart_anPart (φ φ' : 𝓕.States) (a b : CrAnAlgebra 𝓕) :
-    normalOrder (a * superCommute
-    (crPart (StateAlgebra.ofState φ)) (anPart (StateAlgebra.ofState φ')) * b) = 0 := by
+    𝓝(a * superCommute
+      (crPart (StateAlgebra.ofState φ)) (anPart (StateAlgebra.ofState φ')) * b) = 0 := by
  match φ, φ' with
  | _, .inAsymp φ' => simp
  | .outAsymp φ', _ => simp
@ -248,7 +242,7 @@ lemma normalOrder_superCommute_crPart_anPart (φ φ' : 𝓕.States) (a b : CrAnA
    exact normalOrder_superCommute_create_annihilate _ _ rfl rfl ..

 lemma normalOrder_superCommute_anPart_crPart (φ φ' : 𝓕.States) (a b : CrAnAlgebra 𝓕) :
-    normalOrder (a * superCommute
+    𝓝(a * superCommute
    (anPart (StateAlgebra.ofState φ)) (crPart (StateAlgebra.ofState φ')) * b) = 0 := by
  match φ, φ' with
  | .inAsymp φ', _ => simp
@ -274,7 +268,7 @@ lemma normalOrder_superCommute_anPart_crPart (φ φ' : 𝓕.States) (a b : CrAnA

@[simp]
 lemma normalOrder_crPart_mul_crPart (φ φ' : 𝓕.States) :
-    normalOrder (crPart (StateAlgebra.ofState φ) * crPart (StateAlgebra.ofState φ')) =
+    𝓝(crPart (StateAlgebra.ofState φ) * crPart (StateAlgebra.ofState φ')) =
    crPart (StateAlgebra.ofState φ) * crPart (StateAlgebra.ofState φ') := by
  rw [normalOrder_crPart_mul]
  conv_lhs => rw [← mul_one (crPart (StateAlgebra.ofState φ'))]
@ -283,7 +277,7 @@ lemma normalOrder_crPart_mul_crPart (φ φ' : 𝓕.States) :

@[simp]
 lemma normalOrder_anPart_mul_anPart (φ φ' : 𝓕.States) :
-    normalOrder (anPart (StateAlgebra.ofState φ) * anPart (StateAlgebra.ofState φ')) =
+    𝓝(anPart (StateAlgebra.ofState φ) * anPart (StateAlgebra.ofState φ')) =
    anPart (StateAlgebra.ofState φ) * anPart (StateAlgebra.ofState φ') := by
  rw [normalOrder_mul_anPart]
  conv_lhs => rw [← one_mul (anPart (StateAlgebra.ofState φ))]
@ -292,7 +286,7 @@ lemma normalOrder_anPart_mul_anPart (φ φ' : 𝓕.States) :

@[simp]
 lemma normalOrder_crPart_mul_anPart (φ φ' : 𝓕.States) :
-    normalOrder (crPart (StateAlgebra.ofState φ) * anPart (StateAlgebra.ofState φ')) =
+    𝓝(crPart (StateAlgebra.ofState φ) * anPart (StateAlgebra.ofState φ')) =
    crPart (StateAlgebra.ofState φ) * anPart (StateAlgebra.ofState φ') := by
  rw [normalOrder_crPart_mul]
  conv_lhs => rw [← one_mul (anPart (StateAlgebra.ofState φ'))]
@ -301,7 +295,7 @@ lemma normalOrder_crPart_mul_anPart (φ φ' : 𝓕.States) :

@[simp]
 lemma normalOrder_anPart_mul_crPart (φ φ' : 𝓕.States) :
-    normalOrder (anPart (StateAlgebra.ofState φ) * crPart (StateAlgebra.ofState φ')) =
+    𝓝(anPart (StateAlgebra.ofState φ) * crPart (StateAlgebra.ofState φ')) =
    𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') •
    (crPart (StateAlgebra.ofState φ') * anPart (StateAlgebra.ofState φ)) := by
  conv_lhs => rw [← one_mul (anPart (StateAlgebra.ofState φ) * crPart (StateAlgebra.ofState φ'))]
@ -311,7 +305,7 @@ lemma normalOrder_anPart_mul_crPart (φ φ' : 𝓕.States) :
  simp

 lemma normalOrder_ofState_mul_ofState (φ φ' : 𝓕.States) :
-    normalOrder (ofState φ * ofState φ') =
+    𝓝(ofState φ * ofState φ') =
    crPart (StateAlgebra.ofState φ) * crPart (StateAlgebra.ofState φ') +
    𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') •
    (crPart (StateAlgebra.ofState φ') * anPart (StateAlgebra.ofState φ)) +
@ -333,10 +327,9 @@ TODO "Split the following two lemmas up into smaller parts."
 lemma normalOrder_superCommute_ofCrAnList_create_create_ofCrAnList
    (φc φc' : 𝓕.CrAnStates) (hφc : 𝓕 |>ᶜ φc = CreateAnnihilate.create)
    (hφc' : 𝓕 |>ᶜ φc' = CreateAnnihilate.create) (φs φs' : List 𝓕.CrAnStates) :
-    (normalOrder (ofCrAnList φs *
-      superCommute (ofCrAnState φc) (ofCrAnState φc') * ofCrAnList φs')) =
+    (𝓝(ofCrAnList φs * [ofCrAnState φc, ofCrAnState φc']ₛca * ofCrAnList φs')) =
      normalOrderSign (φs ++ φc' :: φc :: φs') •
-    (ofCrAnList (createFilter φs) * superCommute (ofCrAnState φc) (ofCrAnState φc') *
+    (ofCrAnList (createFilter φs) * [ofCrAnState φc, ofCrAnState φc']ₛca *
      ofCrAnList (createFilter φs') * ofCrAnList (annihilateFilter (φs ++ φs'))) := by
  rw [superCommute_ofCrAnState_ofCrAnState, mul_sub, sub_mul, map_sub]
  conv_lhs =>
@ -395,8 +388,7 @@ lemma normalOrder_superCommute_ofCrAnList_annihilate_annihilate_ofCrAnList
    (hφa : 𝓕 |>ᶜ φa = CreateAnnihilate.annihilate)
    (hφa' : 𝓕 |>ᶜ φa' = CreateAnnihilate.annihilate)
    (φs φs' : List 𝓕.CrAnStates) :
-    (normalOrder (ofCrAnList φs *
-      superCommute (ofCrAnState φa) (ofCrAnState φa') * ofCrAnList φs')) =
+    𝓝(ofCrAnList φs * [ofCrAnState φa, ofCrAnState φa']ₛca * ofCrAnList φs') =
      normalOrderSign (φs ++ φa' :: φa :: φs') •
    (ofCrAnList (createFilter (φs ++ φs'))
      * ofCrAnList (annihilateFilter φs) * superCommute (ofCrAnState φa) (ofCrAnState φa')
@ -466,16 +458,16 @@ lemma normalOrder_superCommute_ofCrAnList_annihilate_annihilate_ofCrAnList
 -/

 lemma ofCrAnList_superCommute_normalOrder_ofCrAnList (φs φs' : List 𝓕.CrAnStates) :
-    ⟨ofCrAnList φs, normalOrder (ofCrAnList φs')⟩ₛca =
-    ofCrAnList φs * normalOrder (ofCrAnList φs') -
-    𝓢(𝓕 |>ₛ φs, 𝓕 |>ₛ φs') • normalOrder (ofCrAnList φs') * ofCrAnList φs := by
+    [ofCrAnList φs, 𝓝(ofCrAnList φs')]ₛca =
+    ofCrAnList φs * 𝓝(ofCrAnList φs') -
+    𝓢(𝓕 |>ₛ φs, 𝓕 |>ₛ φs') • 𝓝(ofCrAnList φs') * ofCrAnList φs := by
  simp [normalOrder_ofCrAnList, map_smul, superCommute_ofCrAnList_ofCrAnList, ofCrAnList_append,
    smul_sub, smul_smul, mul_comm]

 lemma ofCrAnList_superCommute_normalOrder_ofStateList (φs : List 𝓕.CrAnStates)
-    (φs' : List 𝓕.States) : ⟨ofCrAnList φs, normalOrder (ofStateList φs')⟩ₛca =
-    ofCrAnList φs * normalOrder (ofStateList φs') -
-    𝓢(𝓕 |>ₛ φs, 𝓕 |>ₛ φs') • normalOrder (ofStateList φs') * ofCrAnList φs := by
+    (φs' : List 𝓕.States) : [ofCrAnList φs, 𝓝(ofStateList φs')]ₛca =
+    ofCrAnList φs * 𝓝(ofStateList φs') -
+    𝓢(𝓕 |>ₛ φs, 𝓕 |>ₛ φs') • 𝓝(ofStateList φs') * ofCrAnList φs := by
  rw [ofStateList_sum, map_sum, Finset.mul_sum, Finset.smul_sum, Finset.sum_mul,
    ← Finset.sum_sub_distrib, map_sum]
  congr
@ -491,23 +483,22 @@ lemma ofCrAnList_superCommute_normalOrder_ofStateList (φs : List 𝓕.CrAnState

 lemma ofCrAnList_mul_normalOrder_ofStateList_eq_superCommute (φs : List 𝓕.CrAnStates)
    (φs' : List 𝓕.States) :
-    ofCrAnList φs * normalOrder (ofStateList φs') =
-    𝓢(𝓕 |>ₛ φs, 𝓕 |>ₛ φs') • normalOrder (ofStateList φs') * ofCrAnList φs
-    + ⟨ofCrAnList φs, normalOrder (ofStateList φs')⟩ₛca := by
+    ofCrAnList φs * 𝓝(ofStateList φs') =
+    𝓢(𝓕 |>ₛ φs, 𝓕 |>ₛ φs') • 𝓝(ofStateList φs') * ofCrAnList φs
+    + [ofCrAnList φs, 𝓝(ofStateList φs')]ₛca := by
  simp [ofCrAnList_superCommute_normalOrder_ofStateList]

 lemma ofCrAnState_mul_normalOrder_ofStateList_eq_superCommute (φ : 𝓕.CrAnStates)
    (φs' : List 𝓕.States) :
-    ofCrAnState φ * normalOrder (ofStateList φs') =
-    𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φs') • normalOrder (ofStateList φs') * ofCrAnState φ
-    + ⟨ofCrAnState φ, normalOrder (ofStateList φs')⟩ₛca := by
+    ofCrAnState φ * 𝓝(ofStateList φs') = 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φs') • 𝓝(ofStateList φs') * ofCrAnState φ
+    + [ofCrAnState φ, 𝓝(ofStateList φs')]ₛca := by
  simp [← ofCrAnList_singleton, ofCrAnList_mul_normalOrder_ofStateList_eq_superCommute]

 lemma anPart_mul_normalOrder_ofStateList_eq_superCommute (φ : 𝓕.States)
    (φs' : List 𝓕.States) :
-    anPart (StateAlgebra.ofState φ) * normalOrder (ofStateList φs') =
-    𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φs') • normalOrder (ofStateList φs' * anPart (StateAlgebra.ofState φ))
-    + ⟨anPart (StateAlgebra.ofState φ), normalOrder (ofStateList φs')⟩ₛca := by
+    anPart (StateAlgebra.ofState φ) * 𝓝(ofStateList φs') =
+    𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φs') • 𝓝(ofStateList φs' * anPart (StateAlgebra.ofState φ))
+    + [anPart (StateAlgebra.ofState φ), 𝓝(ofStateList φs')]ₛca := by
  rw [normalOrder_mul_anPart]
  match φ with
  | .inAsymp φ => simp
--- a/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/SuperCommute.lean
+++ b/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/SuperCommute.lean
@ -35,7 +35,7 @@ noncomputable def superCommute : 𝓕.CrAnAlgebra →ₗ[ℂ] 𝓕.CrAnAlgebra
 /-- The super commutor on the creation and annihlation algebra. For two bosonic operators
  or a bosonic and fermionic operator this corresponds to the usual commutator
  whilst for two fermionic operators this corresponds to the anti-commutator. -/
-scoped[FieldSpecification.CrAnAlgebra] notation "⟨" φs "," φs' "⟩ₛca" => superCommute φs φs'
+scoped[FieldSpecification.CrAnAlgebra] notation "[" φs "," φs' "]ₛca" => superCommute φs φs'

 /-!

@ -44,13 +44,13 @@ scoped[FieldSpecification.CrAnAlgebra] notation "⟨" φs "," φs' "⟩ₛca" =>
 -/

 lemma superCommute_ofCrAnList_ofCrAnList (φs φs' : List 𝓕.CrAnStates) :
-    ⟨ofCrAnList φs, ofCrAnList φs'⟩ₛca =
+    [ofCrAnList φs, ofCrAnList φs']ₛca =
    ofCrAnList (φs ++ φs') - 𝓢(𝓕 |>ₛ φs, 𝓕 |>ₛ φs') • ofCrAnList (φs' ++ φs) := by
  rw [← ofListBasis_eq_ofList, ← ofListBasis_eq_ofList]
  simp only [superCommute, Basis.constr_basis]

 lemma superCommute_ofCrAnState_ofCrAnState (φ φ' : 𝓕.CrAnStates) :
-    ⟨ofCrAnState φ, ofCrAnState φ'⟩ₛca =
+    [ofCrAnState φ, ofCrAnState φ']ₛca =
    ofCrAnState φ * ofCrAnState φ' - 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') • ofCrAnState φ' * ofCrAnState φ := by
  rw [← ofCrAnList_singleton, ← ofCrAnList_singleton]
  rw [superCommute_ofCrAnList_ofCrAnList, ofCrAnList_append]
@ -59,7 +59,7 @@ lemma superCommute_ofCrAnState_ofCrAnState (φ φ' : 𝓕.CrAnStates) :
  rw [FieldStatistic.ofList_singleton, FieldStatistic.ofList_singleton, smul_mul_assoc]

 lemma superCommute_ofCrAnList_ofStatesList (φcas : List 𝓕.CrAnStates) (φs : List 𝓕.States) :
-    ⟨ofCrAnList φcas, ofStateList φs⟩ₛca = ofCrAnList φcas * ofStateList φs -
+    [ofCrAnList φcas, ofStateList φs]ₛca = ofCrAnList φcas * ofStateList φs -
    𝓢(𝓕 |>ₛ φcas, 𝓕 |>ₛ φs) • ofStateList φs * ofCrAnList φcas := by
  conv_lhs => rw [ofStateList_sum]
  rw [map_sum]
@ -72,7 +72,7 @@ lemma superCommute_ofCrAnList_ofStatesList (φcas : List 𝓕.CrAnStates) (φs :
  simp

 lemma superCommute_ofStateList_ofStatesList (φ : List 𝓕.States) (φs : List 𝓕.States) :
-    ⟨ofStateList φ, ofStateList φs⟩ₛca = ofStateList φ * ofStateList φs -
+    [ofStateList φ, ofStateList φs]ₛca = ofStateList φ * ofStateList φs -
    𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φs) • ofStateList φs * ofStateList φ := by
  conv_lhs => rw [ofStateList_sum]
  simp only [map_sum, LinearMap.coeFn_sum, Finset.sum_apply, instCommGroup.eq_1,
@ -85,19 +85,19 @@ lemma superCommute_ofStateList_ofStatesList (φ : List 𝓕.States) (φs : List
  rw [← Finset.sum_mul, ← Finset.smul_sum, ← Finset.mul_sum, ← ofStateList_sum]

 lemma superCommute_ofState_ofStatesList (φ : 𝓕.States) (φs : List 𝓕.States) :
-    ⟨ofState φ, ofStateList φs⟩ₛca = ofState φ * ofStateList φs -
+    [ofState φ, ofStateList φs]ₛca = ofState φ * ofStateList φs -
    𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φs) • ofStateList φs * ofState φ := by
  rw [← ofStateList_singleton, superCommute_ofStateList_ofStatesList, ofStateList_singleton]
  simp

 lemma superCommute_ofStateList_ofState (φs : List 𝓕.States) (φ : 𝓕.States) :
-    ⟨ofStateList φs, ofState φ⟩ₛca = ofStateList φs * ofState φ -
+    [ofStateList φs, ofState φ]ₛca = ofStateList φs * ofState φ -
    𝓢(𝓕 |>ₛ φs, 𝓕 |>ₛ φ) • ofState φ * ofStateList φs := by
  rw [← ofStateList_singleton, superCommute_ofStateList_ofStatesList, ofStateList_singleton]
  simp

 lemma superCommute_anPart_crPart (φ φ' : 𝓕.States) :
-    ⟨anPart (StateAlgebra.ofState φ), crPart (StateAlgebra.ofState φ')⟩ₛca =
+    [anPart (StateAlgebra.ofState φ), crPart (StateAlgebra.ofState φ')]ₛca =
    anPart (StateAlgebra.ofState φ) * crPart (StateAlgebra.ofState φ') -
    𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') • crPart (StateAlgebra.ofState φ') * anPart (StateAlgebra.ofState φ) := by
  match φ, φ' with
@ -126,7 +126,7 @@ lemma superCommute_anPart_crPart (φ φ' : 𝓕.States) :
    simp [crAnStatistics, ← ofCrAnList_append]

 lemma superCommute_crPart_anPart (φ φ' : 𝓕.States) :
-    ⟨crPart (StateAlgebra.ofState φ), anPart (StateAlgebra.ofState φ')⟩ₛca =
+    [crPart (StateAlgebra.ofState φ), anPart (StateAlgebra.ofState φ')]ₛca =
    crPart (StateAlgebra.ofState φ) * anPart (StateAlgebra.ofState φ') -
    𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') •
    anPart (StateAlgebra.ofState φ') * crPart (StateAlgebra.ofState φ) := by
@ -155,7 +155,7 @@ lemma superCommute_crPart_anPart (φ φ' : 𝓕.States) :
    simp [crAnStatistics, ← ofCrAnList_append]

 lemma superCommute_crPart_crPart (φ φ' : 𝓕.States) :
-    ⟨crPart (StateAlgebra.ofState φ), crPart (StateAlgebra.ofState φ')⟩ₛca =
+    [crPart (StateAlgebra.ofState φ), crPart (StateAlgebra.ofState φ')]ₛca =
    crPart (StateAlgebra.ofState φ) * crPart (StateAlgebra.ofState φ') -
    𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') •
    crPart (StateAlgebra.ofState φ') * crPart (StateAlgebra.ofState φ) := by
@ -183,7 +183,7 @@ lemma superCommute_crPart_crPart (φ φ' : 𝓕.States) :
  simp [crAnStatistics, ← ofCrAnList_append]

 lemma superCommute_anPart_anPart (φ φ' : 𝓕.States) :
-    ⟨anPart (StateAlgebra.ofState φ), anPart (StateAlgebra.ofState φ')⟩ₛca =
+    [anPart (StateAlgebra.ofState φ), anPart (StateAlgebra.ofState φ')]ₛca =
    anPart (StateAlgebra.ofState φ) * anPart (StateAlgebra.ofState φ') -
    𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') •
    anPart (StateAlgebra.ofState φ') * anPart (StateAlgebra.ofState φ) := by
@ -210,7 +210,7 @@ lemma superCommute_anPart_anPart (φ φ' : 𝓕.States) :
    simp [crAnStatistics, ← ofCrAnList_append]

 lemma superCommute_crPart_ofStateList (φ : 𝓕.States) (φs : List 𝓕.States) :
-    ⟨crPart (StateAlgebra.ofState φ), ofStateList φs⟩ₛca =
+    [crPart (StateAlgebra.ofState φ), ofStateList φs]ₛca =
    crPart (StateAlgebra.ofState φ) * ofStateList φs - 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φs) • ofStateList φs *
    crPart (StateAlgebra.ofState φ) := by
  match φ with
@ -226,7 +226,7 @@ lemma superCommute_crPart_ofStateList (φ : 𝓕.States) (φs : List 𝓕.States
    simp

 lemma superCommute_anPart_ofStateList (φ : 𝓕.States) (φs : List 𝓕.States) :
-    ⟨anPart (StateAlgebra.ofState φ), ofStateList φs⟩ₛca =
+    [anPart (StateAlgebra.ofState φ), ofStateList φs]ₛca =
    anPart (StateAlgebra.ofState φ) * ofStateList φs - 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φs) •
    ofStateList φs * anPart (StateAlgebra.ofState φ) := by
  match φ with
@ -242,14 +242,14 @@ lemma superCommute_anPart_ofStateList (φ : 𝓕.States) (φs : List 𝓕.States
    simp [crAnStatistics]

 lemma superCommute_crPart_ofState (φ φ' : 𝓕.States) :
-    ⟨crPart (StateAlgebra.ofState φ), ofState φ'⟩ₛca =
+    [crPart (StateAlgebra.ofState φ), ofState φ']ₛca =
    crPart (StateAlgebra.ofState φ) * ofState φ' -
    𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') • ofState φ' * crPart (StateAlgebra.ofState φ) := by
  rw [← ofStateList_singleton, superCommute_crPart_ofStateList]
  simp

 lemma superCommute_anPart_ofState (φ φ' : 𝓕.States) :
-    ⟨anPart (StateAlgebra.ofState φ), ofState φ'⟩ₛca =
+    [anPart (StateAlgebra.ofState φ), ofState φ']ₛca =
    anPart (StateAlgebra.ofState φ) * ofState φ' -
    𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') • ofState φ' * anPart (StateAlgebra.ofState φ) := by
  rw [← ofStateList_singleton, superCommute_anPart_ofStateList]
@ -265,38 +265,38 @@ multiplication with a sign plus the super commutor.
 -/
 lemma ofCrAnList_mul_ofCrAnList_eq_superCommute (φs φs' : List 𝓕.CrAnStates) :
    ofCrAnList φs * ofCrAnList φs' = 𝓢(𝓕 |>ₛ φs, 𝓕 |>ₛ φs') • ofCrAnList φs' * ofCrAnList φs
-    + ⟨ofCrAnList φs, ofCrAnList φs'⟩ₛca := by
+    + [ofCrAnList φs, ofCrAnList φs']ₛca := by
  rw [superCommute_ofCrAnList_ofCrAnList]
  simp [ofCrAnList_append]

 lemma ofCrAnState_mul_ofCrAnList_eq_superCommute (φ : 𝓕.CrAnStates) (φs' : List 𝓕.CrAnStates) :
    ofCrAnState φ * ofCrAnList φs' = 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φs') • ofCrAnList φs' * ofCrAnState φ
-    + ⟨ofCrAnState φ, ofCrAnList φs'⟩ₛca := by
+    + [ofCrAnState φ, ofCrAnList φs']ₛca := by
  rw [← ofCrAnList_singleton, ofCrAnList_mul_ofCrAnList_eq_superCommute]
  simp

 lemma ofStateList_mul_ofStateList_eq_superCommute (φs φs' : List 𝓕.States) :
    ofStateList φs * ofStateList φs' = 𝓢(𝓕 |>ₛ φs, 𝓕 |>ₛ φs') • ofStateList φs' * ofStateList φs
-    + ⟨ofStateList φs, ofStateList φs'⟩ₛca := by
+    + [ofStateList φs, ofStateList φs']ₛca := by
  rw [superCommute_ofStateList_ofStatesList]
  simp

 lemma ofState_mul_ofStateList_eq_superCommute (φ : 𝓕.States) (φs' : List 𝓕.States) :
    ofState φ * ofStateList φs' = 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φs') • ofStateList φs' * ofState φ
-    + ⟨ofState φ, ofStateList φs'⟩ₛca := by
+    + [ofState φ, ofStateList φs']ₛca := by
  rw [superCommute_ofState_ofStatesList]
  simp

 lemma ofStateList_mul_ofState_eq_superCommute (φs : List 𝓕.States) (φ : 𝓕.States) :
    ofStateList φs * ofState φ = 𝓢(𝓕 |>ₛ φs, 𝓕 |>ₛ φ) • ofState φ * ofStateList φs
-    + ⟨ofStateList φs, ofState φ⟩ₛca := by
+    + [ofStateList φs, ofState φ]ₛca := by
  rw [superCommute_ofStateList_ofState]
  simp

 lemma crPart_mul_anPart_eq_superCommute (φ φ' : 𝓕.States) :
    crPart (StateAlgebra.ofState φ) * anPart (StateAlgebra.ofState φ') =
    𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') • anPart (StateAlgebra.ofState φ') * crPart (StateAlgebra.ofState φ) +
-    ⟨crPart (StateAlgebra.ofState φ), anPart (StateAlgebra.ofState φ')⟩ₛca := by
+    [crPart (StateAlgebra.ofState φ), anPart (StateAlgebra.ofState φ')]ₛca := by
  rw [superCommute_crPart_anPart]
  simp

@ -304,27 +304,27 @@ lemma anPart_mul_crPart_eq_superCommute (φ φ' : 𝓕.States) :
    anPart (StateAlgebra.ofState φ) * crPart (StateAlgebra.ofState φ') =
    𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') •
    crPart (StateAlgebra.ofState φ') * anPart (StateAlgebra.ofState φ) +
-    ⟨anPart (StateAlgebra.ofState φ), crPart (StateAlgebra.ofState φ')⟩ₛca := by
+    [anPart (StateAlgebra.ofState φ), crPart (StateAlgebra.ofState φ')]ₛca := by
  rw [superCommute_anPart_crPart]
  simp

 lemma crPart_mul_crPart_eq_superCommute (φ φ' : 𝓕.States) :
    crPart (StateAlgebra.ofState φ) * crPart (StateAlgebra.ofState φ') =
    𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') • crPart (StateAlgebra.ofState φ') * crPart (StateAlgebra.ofState φ) +
-    ⟨crPart (StateAlgebra.ofState φ), crPart (StateAlgebra.ofState φ')⟩ₛca := by
+    [crPart (StateAlgebra.ofState φ), crPart (StateAlgebra.ofState φ')]ₛca := by
  rw [superCommute_crPart_crPart]
  simp

 lemma anPart_mul_anPart_eq_superCommute (φ φ' : 𝓕.States) :
    anPart (StateAlgebra.ofState φ) * anPart (StateAlgebra.ofState φ') =
    𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') • anPart (StateAlgebra.ofState φ') * anPart (StateAlgebra.ofState φ) +
-    ⟨anPart (StateAlgebra.ofState φ), anPart (StateAlgebra.ofState φ')⟩ₛca := by
+    [anPart (StateAlgebra.ofState φ), anPart (StateAlgebra.ofState φ')]ₛca := by
  rw [superCommute_anPart_anPart]
  simp

 lemma ofCrAnList_mul_ofStateList_eq_superCommute (φs : List 𝓕.CrAnStates) (φs' : List 𝓕.States) :
    ofCrAnList φs * ofStateList φs' = 𝓢(𝓕 |>ₛ φs, 𝓕 |>ₛ φs') • ofStateList φs' * ofCrAnList φs
-    + ⟨ofCrAnList φs, ofStateList φs'⟩ₛca := by
+    + [ofCrAnList φs, ofStateList φs']ₛca := by
  rw [superCommute_ofCrAnList_ofStatesList]
  simp

@ -335,8 +335,8 @@ lemma ofCrAnList_mul_ofStateList_eq_superCommute (φs : List 𝓕.CrAnStates) (
 -/

 lemma superCommute_ofCrAnList_ofCrAnList_symm (φs φs' : List 𝓕.CrAnStates) :
-    ⟨ofCrAnList φs, ofCrAnList φs'⟩ₛca =
-    (- 𝓢(𝓕 |>ₛ φs, 𝓕 |>ₛ φs')) • ⟨ofCrAnList φs', ofCrAnList φs⟩ₛca := by
+    [ofCrAnList φs, ofCrAnList φs']ₛca =
+    (- 𝓢(𝓕 |>ₛ φs, 𝓕 |>ₛ φs')) • [ofCrAnList φs', ofCrAnList φs]ₛca := by
  rw [superCommute_ofCrAnList_ofCrAnList, superCommute_ofCrAnList_ofCrAnList, smul_sub]
  simp only [instCommGroup.eq_1, neg_smul, sub_neg_eq_add]
  rw [smul_smul]
@ -347,8 +347,8 @@ lemma superCommute_ofCrAnList_ofCrAnList_symm (φs φs' : List 𝓕.CrAnStates)
  abel

 lemma superCommute_ofCrAnState_ofCrAnState_symm (φ φ' : 𝓕.CrAnStates) :
-    ⟨ofCrAnState φ, ofCrAnState φ'⟩ₛca =
-    (- 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ')) • ⟨ofCrAnState φ', ofCrAnState φ⟩ₛca := by
+    [ofCrAnState φ, ofCrAnState φ']ₛca =
+    (- 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ')) • [ofCrAnState φ', ofCrAnState φ]ₛca := by
  rw [superCommute_ofCrAnState_ofCrAnState, superCommute_ofCrAnState_ofCrAnState]
  rw [smul_sub]
  simp only [instCommGroup.eq_1, Algebra.smul_mul_assoc, neg_smul, sub_neg_eq_add]
@ -365,10 +365,10 @@ lemma superCommute_ofCrAnState_ofCrAnState_symm (φ φ' : 𝓕.CrAnStates) :

 -/
 lemma superCommute_ofCrAnList_ofCrAnList_cons (φ : 𝓕.CrAnStates) (φs φs' : List 𝓕.CrAnStates) :
-    ⟨ofCrAnList φs, ofCrAnList (φ :: φs')⟩ₛca =
-    ⟨ofCrAnList φs, ofCrAnState φ⟩ₛca * ofCrAnList φs' +
+    [ofCrAnList φs, ofCrAnList (φ :: φs')]ₛca =
+    [ofCrAnList φs, ofCrAnState φ]ₛca * ofCrAnList φs' +
    𝓢(𝓕 |>ₛ φs, 𝓕 |>ₛ φ)
-    • ofCrAnState φ * ⟨ofCrAnList φs, ofCrAnList φs'⟩ₛca := by
+    • ofCrAnState φ * [ofCrAnList φs, ofCrAnList φs']ₛca := by
  rw [superCommute_ofCrAnList_ofCrAnList]
  conv_rhs =>
    lhs
@ -385,9 +385,9 @@ lemma superCommute_ofCrAnList_ofCrAnList_cons (φ : 𝓕.CrAnStates) (φs φs' :
  simp only [instCommGroup, map_mul, mul_comm]

 lemma superCommute_ofCrAnList_ofStateList_cons (φ : 𝓕.States) (φs : List 𝓕.CrAnStates)
-    (φs' : List 𝓕.States) : ⟨ofCrAnList φs, ofStateList (φ :: φs')⟩ₛca =
-    ⟨ofCrAnList φs, ofState φ⟩ₛca * ofStateList φs' +
-    𝓢(𝓕 |>ₛ φs, 𝓕 |>ₛ φ) • ofState φ * ⟨ofCrAnList φs, ofStateList φs'⟩ₛca := by
+    (φs' : List 𝓕.States) : [ofCrAnList φs, ofStateList (φ :: φs')]ₛca =
+    [ofCrAnList φs, ofState φ]ₛca * ofStateList φs' +
+    𝓢(𝓕 |>ₛ φs, 𝓕 |>ₛ φ) • ofState φ * [ofCrAnList φs, ofStateList φs']ₛca := by
  rw [superCommute_ofCrAnList_ofStatesList]
  conv_rhs =>
    lhs
@ -406,9 +406,9 @@ lemma superCommute_ofCrAnList_ofStateList_cons (φ : 𝓕.States) (φs : List

 lemma superCommute_ofCrAnList_ofCrAnList_eq_sum (φs : List 𝓕.CrAnStates) :
    (φs' : List 𝓕.CrAnStates) →
-    ⟨ofCrAnList φs, ofCrAnList φs'⟩ₛca =
+    [ofCrAnList φs, ofCrAnList φs']ₛca =
    ∑ (n : Fin φs'.length), 𝓢(𝓕 |>ₛ φs, 𝓕 |>ₛ (List.take n φs')) •
-    ofCrAnList (φs'.take n) * ⟨ofCrAnList φs, ofCrAnState (φs'.get n)⟩ₛca *
+    ofCrAnList (φs'.take n) * [ofCrAnList φs, ofCrAnState (φs'.get n)]ₛca *
    ofCrAnList (φs'.drop (n + 1))
  | [] => by
    simp [← ofCrAnList_nil, superCommute_ofCrAnList_ofCrAnList]
@ -421,9 +421,9 @@ lemma superCommute_ofCrAnList_ofCrAnList_eq_sum (φs : List 𝓕.CrAnStates) :
        FieldStatistic.ofList_cons_eq_mul, mul_comm]

 lemma superCommute_ofCrAnList_ofStateList_eq_sum (φs : List 𝓕.CrAnStates) : (φs' : List 𝓕.States) →
-    ⟨ofCrAnList φs, ofStateList φs'⟩ₛca =
+    [ofCrAnList φs, ofStateList φs']ₛca =
    ∑ (n : Fin φs'.length), 𝓢(𝓕 |>ₛ φs, 𝓕 |>ₛ List.take n φs') •
-      ofStateList (φs'.take n) * ⟨ofCrAnList φs, ofState (φs'.get n)⟩ₛca *
+      ofStateList (φs'.take n) * [ofCrAnList φs, ofState (φs'.get n)]ₛca *
      ofStateList (φs'.drop (n + 1))
  | [] => by
    simp only [superCommute_ofCrAnList_ofStatesList, instCommGroup, ofList_empty,
--- a/HepLean/PerturbationTheory/Algebras/ProtoOperatorAlgebra/Basic.lean
+++ b/HepLean/PerturbationTheory/Algebras/ProtoOperatorAlgebra/Basic.lean
@ -61,7 +61,7 @@ lemma crAnF_superCommute_ofCrAnState_ofState_mem_center (φ : 𝓕.CrAnStates) (
  exact 𝓞.superCommute_crAn_center φ ⟨ψ, x⟩

 lemma crAnF_superCommute_anPart_ofState_mem_center (φ ψ : 𝓕.States) :
-    𝓞.crAnF ⟨anPart (StateAlgebra.ofState φ), ofState ψ⟩ₛca ∈ Subalgebra.center ℂ 𝓞.A := by
+    𝓞.crAnF [anPart (StateAlgebra.ofState φ), ofState ψ]ₛca ∈ Subalgebra.center ℂ 𝓞.A := by
  match φ with
  | States.inAsymp _ =>
    simp only [anPart_negAsymp, map_zero, LinearMap.zero_apply]
@ -106,7 +106,7 @@ lemma crAnF_superCommute_ofState_ofState_mem_center (φ ψ : 𝓕.States) :
  exact crAnF_superCommute_ofCrAnState_ofState_mem_center 𝓞 ⟨φ, x⟩ ψ

 lemma crAnF_superCommute_anPart_anPart (φ ψ : 𝓕.States) :
-    𝓞.crAnF ⟨anPart (StateAlgebra.ofState φ), anPart (StateAlgebra.ofState ψ)⟩ₛca = 0 := by
+    𝓞.crAnF [anPart (StateAlgebra.ofState φ), anPart (StateAlgebra.ofState ψ)]ₛca = 0 := by
  match φ, ψ with
  | _, States.inAsymp _ =>
    simp
@ -134,7 +134,7 @@ lemma crAnF_superCommute_anPart_anPart (φ ψ : 𝓕.States) :
    rfl

 lemma crAnF_superCommute_crPart_crPart (φ ψ : 𝓕.States) :
-    𝓞.crAnF ⟨crPart (StateAlgebra.ofState φ), crPart (StateAlgebra.ofState ψ)⟩ₛca = 0 := by
+    𝓞.crAnF [crPart (StateAlgebra.ofState φ), crPart (StateAlgebra.ofState ψ)]ₛca = 0 := by
  match φ, ψ with
  | _, States.outAsymp _ =>
    simp
@ -162,9 +162,9 @@ lemma crAnF_superCommute_crPart_crPart (φ ψ : 𝓕.States) :
    rfl

 lemma crAnF_superCommute_ofCrAnState_ofCrAnList_eq_sum (φ : 𝓕.CrAnStates) (φs : List 𝓕.CrAnStates) :
-    𝓞.crAnF ⟨ofCrAnState φ, ofCrAnList φs⟩ₛca
+    𝓞.crAnF [ofCrAnState φ, ofCrAnList φs]ₛca
    = 𝓞.crAnF (∑ (n : Fin φs.length), 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ (List.take n φs)) •
-    ⟨ofCrAnState φ, ofCrAnState (φs.get n)⟩ₛca * ofCrAnList (φs.eraseIdx n)) := by
+    [ofCrAnState φ, ofCrAnState (φs.get n)]ₛca * ofCrAnList (φs.eraseIdx n)) := by
  conv_lhs =>
    rw [← ofCrAnList_singleton, superCommute_ofCrAnList_ofCrAnList_eq_sum]
  rw [map_sum, map_sum]
@ -180,9 +180,9 @@ lemma crAnF_superCommute_ofCrAnState_ofCrAnList_eq_sum (φ : 𝓕.CrAnStates) (
    rw [← map_mul, ← ofCrAnList_append, ← List.eraseIdx_eq_take_drop_succ]

 lemma crAnF_superCommute_ofCrAnState_ofStateList_eq_sum (φ : 𝓕.CrAnStates) (φs : List 𝓕.States) :
-    𝓞.crAnF ⟨ofCrAnState φ, ofStateList φs⟩ₛca
+    𝓞.crAnF [ofCrAnState φ, ofStateList φs]ₛca
    = 𝓞.crAnF (∑ (n : Fin φs.length), 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ (List.take n φs)) •
-    ⟨ofCrAnState φ, ofState (φs.get n)⟩ₛca * ofStateList (φs.eraseIdx n)) := by
+    [ofCrAnState φ, ofState (φs.get n)]ₛca * ofStateList (φs.eraseIdx n)) := by
  conv_lhs =>
    rw [← ofCrAnList_singleton, superCommute_ofCrAnList_ofStateList_eq_sum]
  rw [map_sum, map_sum]
--- a/HepLean/PerturbationTheory/Algebras/ProtoOperatorAlgebra/NormalOrder.lean
+++ b/HepLean/PerturbationTheory/Algebras/ProtoOperatorAlgebra/NormalOrder.lean
@ -27,24 +27,19 @@ The main result of this section is
 `crAnF_normalOrder_superCommute_eq_zero_mul`.

 -/
+
 lemma crAnF_normalOrder_superCommute_ofCrAnList_create_create_ofCrAnList
-    (φc φc' : 𝓕.CrAnStates)
-    (hφc : 𝓕 |>ᶜ φc = CreateAnnihilate.create)
-    (hφc' : 𝓕 |>ᶜ φc' = CreateAnnihilate.create)
-    (φs φs' : List 𝓕.CrAnStates) :
-    𝓞.crAnF (normalOrder
-    (ofCrAnList φs * superCommute (ofCrAnState φc) (ofCrAnState φc') * ofCrAnList φs')) = 0 := by
+    (φc φc' : 𝓕.CrAnStates) (hφc : 𝓕 |>ᶜ φc = CreateAnnihilate.create)
+    (hφc' : 𝓕 |>ᶜ φc' = CreateAnnihilate.create) (φs φs' : List 𝓕.CrAnStates) :
+    𝓞.crAnF (𝓝(ofCrAnList φs * [ofCrAnState φc, ofCrAnState φc']ₛca * ofCrAnList φs')) = 0 := by
  rw [normalOrder_superCommute_ofCrAnList_create_create_ofCrAnList φc φc' hφc hφc' φs φs']
  rw [map_smul, map_mul, map_mul, map_mul, 𝓞.superCommute_create_create φc φc' hφc hφc']
  simp

 lemma crAnF_normalOrder_superCommute_ofCrAnList_annihilate_annihilate_ofCrAnList
-    (φa φa' : 𝓕.CrAnStates)
-    (hφa : 𝓕 |>ᶜ φa = CreateAnnihilate.annihilate)
-    (hφa' : 𝓕 |>ᶜ φa' = CreateAnnihilate.annihilate)
-    (φs φs' : List 𝓕.CrAnStates) :
-    𝓞.crAnF (normalOrder
-    (ofCrAnList φs * superCommute (ofCrAnState φa) (ofCrAnState φa') * ofCrAnList φs')) = 0 := by
+    (φa φa' : 𝓕.CrAnStates) (hφa : 𝓕 |>ᶜ φa = CreateAnnihilate.annihilate)
+    (hφa' : 𝓕 |>ᶜ φa' = CreateAnnihilate.annihilate) (φs φs' : List 𝓕.CrAnStates) :
+    𝓞.crAnF (𝓝(ofCrAnList φs * [ofCrAnState φa, ofCrAnState φa']ₛca * ofCrAnList φs')) = 0 := by
  rw [normalOrder_superCommute_ofCrAnList_annihilate_annihilate_ofCrAnList φa φa' hφa hφa' φs φs']
  rw [map_smul, map_mul, map_mul, map_mul, 𝓞.superCommute_annihilate_annihilate φa φa' hφa hφa']
  simp
@ -254,9 +249,9 @@ lemma crAnF_normalOrder_ofStatesList_mul_anPart_swap (φ : 𝓕.States)

 -/
 lemma crAnF_ofCrAnState_superCommute_normalOrder_ofCrAnList_eq_sum (φ : 𝓕.CrAnStates)
-    (φs : List 𝓕.CrAnStates) : 𝓞.crAnF (⟨ofCrAnState φ, normalOrder (ofCrAnList φs)⟩ₛca) =
+    (φs : List 𝓕.CrAnStates) : 𝓞.crAnF ([ofCrAnState φ, normalOrder (ofCrAnList φs)]ₛca) =
    ∑ n : Fin φs.length, 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ (φs.take n)) •
-      𝓞.crAnF (⟨ofCrAnState φ, ofCrAnState φs[n]⟩ₛca)
+      𝓞.crAnF ([ofCrAnState φ, ofCrAnState φs[n]]ₛca)
      * 𝓞.crAnF (normalOrder (ofCrAnList (φs.eraseIdx n))) := by
  rw [normalOrder_ofCrAnList, map_smul, map_smul]
  rw [crAnF_superCommute_ofCrAnState_ofCrAnList_eq_sum, sum_normalOrderList_length]
@ -281,9 +276,9 @@ lemma crAnF_ofCrAnState_superCommute_normalOrder_ofCrAnList_eq_sum (φ : 𝓕.Cr
    simp

 lemma crAnF_ofCrAnState_superCommute_normalOrder_ofStateList_eq_sum (φ : 𝓕.CrAnStates)
-    (φs : List 𝓕.States) : 𝓞.crAnF (⟨ofCrAnState φ, normalOrder (ofStateList φs)⟩ₛca) =
+    (φs : List 𝓕.States) : 𝓞.crAnF ([ofCrAnState φ, normalOrder (ofStateList φs)]ₛca) =
    ∑ n : Fin φs.length, 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ (φs.take n)) •
-    𝓞.crAnF (⟨ofCrAnState φ, ofState φs[n]⟩ₛca)
+    𝓞.crAnF ([ofCrAnState φ, ofState φs[n]]ₛca)
    * 𝓞.crAnF (normalOrder (ofStateList (φs.eraseIdx n))) := by
  conv_lhs =>
    rw [ofStateList_sum, map_sum, map_sum, map_sum]
@ -304,9 +299,9 @@ lemma crAnF_ofCrAnState_superCommute_normalOrder_ofStateList_eq_sum (φ : 𝓕.C
  rw [← Finset.sum_mul, ← map_sum, ← map_sum, ← ofState, ← map_sum, ← map_sum, ← ofStateList_sum]

 lemma crAnF_anPart_superCommute_normalOrder_ofStateList_eq_sum (φ : 𝓕.States) (φs : List 𝓕.States) :
-    𝓞.crAnF (⟨anPart (StateAlgebra.ofState φ), normalOrder (ofStateList φs)⟩ₛca) =
+    𝓞.crAnF ([anPart (StateAlgebra.ofState φ), normalOrder (ofStateList φs)]ₛca) =
    ∑ n : Fin φs.length, 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ (φs.take n)) •
-    𝓞.crAnF (⟨anPart (StateAlgebra.ofState φ), ofState φs[n]⟩ₛca)
+    𝓞.crAnF ([anPart (StateAlgebra.ofState φ), ofState φs[n]]ₛca)
    * 𝓞.crAnF (normalOrder (ofStateList (φs.eraseIdx n))) := by
  match φ with
  | .inAsymp φ =>
@ -329,7 +324,7 @@ lemma crAnF_anPart_mul_normalOrder_ofStatesList_eq_superCommute (φ : 𝓕.State
    (φ' : List 𝓕.States) :
    𝓞.crAnF (anPart (StateAlgebra.ofState φ) * normalOrder (ofStateList φ')) =
    𝓞.crAnF (normalOrder (anPart (StateAlgebra.ofState φ) * ofStateList φ')) +
-    𝓞.crAnF (⟨anPart (StateAlgebra.ofState φ), normalOrder (ofStateList φ')⟩ₛca) := by
+    𝓞.crAnF ([anPart (StateAlgebra.ofState φ), normalOrder (ofStateList φ')]ₛca) := by
  rw [anPart_mul_normalOrder_ofStateList_eq_superCommute]
  simp only [instCommGroup.eq_1, map_add, map_smul]
  congr
@ -339,7 +334,7 @@ lemma crAnF_ofState_mul_normalOrder_ofStatesList_eq_superCommute (φ : 𝓕.Stat
    (φ' : List 𝓕.States) :
    𝓞.crAnF (ofState φ * normalOrder (ofStateList φ')) =
    𝓞.crAnF (normalOrder (ofState φ * ofStateList φ')) +
-    𝓞.crAnF (⟨anPart (StateAlgebra.ofState φ), normalOrder (ofStateList φ')⟩ₛca) := by
+    𝓞.crAnF ([anPart (StateAlgebra.ofState φ), normalOrder (ofStateList φ')]ₛca) := by
  conv_lhs => rw [ofState_eq_crPart_add_anPart]
  rw [add_mul, map_add, crAnF_anPart_mul_normalOrder_ofStatesList_eq_superCommute, ← add_assoc,
    ← normalOrder_crPart_mul, ← map_add]
@ -354,7 +349,7 @@ noncomputable def contractStateAtIndex (φ : 𝓕.States) (φs : List 𝓕.State
  match n with
  | none => 1
  | some n => 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ (φs.take n)) •
-        𝓞.crAnF (⟨anPart (StateAlgebra.ofState φ), ofState φs[n]⟩ₛca)
+    𝓞.crAnF ([anPart (StateAlgebra.ofState φ), ofState φs[n]]ₛca)

 /--
 Within a proto-operator algebra,
--- a/HepLean/PerturbationTheory/Algebras/ProtoOperatorAlgebra/TimeContraction.lean
+++ b/HepLean/PerturbationTheory/Algebras/ProtoOperatorAlgebra/TimeContraction.lean
@ -37,7 +37,7 @@ lemma timeContract_eq_smul (φ ψ : 𝓕.States) : 𝓞.timeContract φ ψ =
    + (-1 : ℂ) • normalOrder (ofState φ * ofState ψ)) := by rfl

 lemma timeContract_of_timeOrderRel (φ ψ : 𝓕.States) (h : timeOrderRel φ ψ) :
-    𝓞.timeContract φ ψ = 𝓞.crAnF (⟨anPart (StateAlgebra.ofState φ), ofState ψ⟩ₛca) := by
+    𝓞.timeContract φ ψ = 𝓞.crAnF ([anPart (StateAlgebra.ofState φ), ofState ψ]ₛca) := by
  conv_rhs =>
    rw [ofState_eq_crPart_add_anPart]
    rw [map_add, map_add, crAnF_superCommute_anPart_anPart, superCommute_anPart_crPart]