refactor: Docs around Wick's theorem (#289)

* refactor: Organize supercommute for CrAnAlgebra * refactor: Normal order results * refactor: Uncontracted List organization * refactor: Rename OperatorAlgebra * refactor: Lint
2025-01-22 09:15:13 +00:00 · 2025-01-22 09:15:13 +00:00 · 36d3be1cbf
commit 36d3be1cbf
parent 7b396501e7
17 changed files with 685 additions and 619 deletions
--- a/HepLean.lean
+++ b/HepLean.lean
@ -121,9 +121,9 @@ import HepLean.Meta.TransverseTactics
 import HepLean.PerturbationTheory.Algebras.CrAnAlgebra.Basic
 import HepLean.PerturbationTheory.Algebras.CrAnAlgebra.NormalOrder
 import HepLean.PerturbationTheory.Algebras.CrAnAlgebra.SuperCommute
-import HepLean.PerturbationTheory.Algebras.OperatorAlgebra.Basic
-import HepLean.PerturbationTheory.Algebras.OperatorAlgebra.NormalOrder
-import HepLean.PerturbationTheory.Algebras.OperatorAlgebra.TimeContraction
+import HepLean.PerturbationTheory.Algebras.ProtoOperatorAlgebra.Basic
+import HepLean.PerturbationTheory.Algebras.ProtoOperatorAlgebra.NormalOrder
+import HepLean.PerturbationTheory.Algebras.ProtoOperatorAlgebra.TimeContraction
 import HepLean.PerturbationTheory.Algebras.StateAlgebra.Basic
 import HepLean.PerturbationTheory.Algebras.StateAlgebra.TimeOrder
 import HepLean.PerturbationTheory.CreateAnnihilate
--- a/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/NormalOrder.lean
+++ b/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/NormalOrder.lean
@ -10,17 +10,19 @@ import HepLean.PerturbationTheory.Koszul.KoszulSign

 # Normal Ordering in the CrAnAlgebra

+In the module
+`HepLean.PerturbationTheory.FieldSpecification.NormalOrder`
+we defined the normal ordering of a list of `CrAnStates`.
+In this module we extend the normal ordering to a linear map on `CrAnAlgebra`.
+
+We derive properties of this normal ordering.

 -/

 namespace FieldSpecification
 variable {𝓕 : FieldSpecification}
 open FieldStatistic
-/-!

-## Normal order on the CrAnAlgebra
-
-/
 namespace CrAnAlgebra

 noncomputable section
@ -51,6 +53,12 @@ lemma normalOrder_one : normalOrder (𝓕 := 𝓕) 1 = 1 := by
  rw [← ofCrAnList_nil, normalOrder_ofCrAnList]
  simp

+/-!
+
+## Normal ordering with a creation operator on the left or annihilation on the right
+
+-/
+
 lemma normalOrder_ofCrAnList_cons_create (φ : 𝓕.CrAnStates)
    (hφ : 𝓕 |>ᶜ φ = CreateAnnihilate.create) (φs : List 𝓕.CrAnStates) :
    normalOrder (ofCrAnList (φ :: φs)) =
@ -95,83 +103,6 @@ lemma normalOrder_mul_annihilate (φ : 𝓕.CrAnStates)
  rw [← ofCrAnList_singleton, ← ofCrAnList_append, ofCrAnList_singleton]
  rw [normalOrder_ofCrAnList_append_annihilate φ hφ]

-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
-  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]
-  rw [← smul_smul, ← normalOrder_ofCrAnList]
-  congr
-  rw [ofCrAnList_append, ofCrAnList_cons, ofCrAnList_cons]
-  noncomm_ring
-
-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
-  change (normalOrder ∘ₗ mulLinearMap (ofCrAnList φs * ofCrAnState φc * ofCrAnState φa)) a =
-    (smulLinearMap _ ∘ₗ normalOrder ∘ₗ
-    mulLinearMap (ofCrAnList φs * ofCrAnState φa * ofCrAnState φc)) a
-  refine LinearMap.congr_fun ?h a
-  apply ofCrAnListBasis.ext
-  intro l
-  simp only [mulLinearMap, LinearMap.coe_mk, AddHom.coe_mk, ofListBasis_eq_ofList,
-    LinearMap.coe_comp, Function.comp_apply, instCommGroup.eq_1]
-  rw [normalOrder_swap_create_annihlate_ofCrAnList_ofCrAnList φc φa hφc hφa]
-  rfl
-
-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
-  rw [mul_assoc, mul_assoc, mul_assoc, mul_assoc]
-  change (normalOrder ∘ₗ mulLinearMap.flip (ofCrAnState φc * (ofCrAnState φa * b))) a =
-    (smulLinearMap (𝓢(𝓕 |>ₛ φc, 𝓕 |>ₛ φa)) ∘ₗ
-    normalOrder ∘ₗ mulLinearMap.flip (ofCrAnState φa * (ofCrAnState φc * b))) a
-  apply LinearMap.congr_fun
-  apply ofCrAnListBasis.ext
-  intro l
-  simp only [mulLinearMap, ofListBasis_eq_ofList, LinearMap.coe_comp, Function.comp_apply,
-    LinearMap.flip_apply, LinearMap.coe_mk, AddHom.coe_mk, instCommGroup.eq_1]
-  repeat rw [← mul_assoc]
-  rw [normalOrder_swap_create_annihlate_ofCrAnList φc φa hφc hφa]
-  rfl
-
-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
-  rw [superCommute_ofCrAnState]
-  simp only [instCommGroup.eq_1, Algebra.smul_mul_assoc]
-  rw [mul_sub, sub_mul, map_sub, ← smul_mul_assoc]
-  rw [← mul_assoc, ← mul_assoc]
-  rw [normalOrder_swap_create_annihlate φc φa hφc hφa]
-  simp only [FieldStatistic.instCommGroup.eq_1, Algebra.mul_smul_comm, Algebra.smul_mul_assoc,
-    map_smul, sub_self]
-
-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
-  rw [superCommute_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]
-  apply Or.inr
-  exact normalOrder_superCommute_create_annihilate φc φa hφc hφa a b
-
 lemma normalOrder_crPart_mul (φ : 𝓕.States) (a : CrAnAlgebra 𝓕) :
    normalOrder (crPart (StateAlgebra.ofState φ) * a) =
    crPart (StateAlgebra.ofState φ) * normalOrder a := by
@ -205,6 +136,85 @@ lemma normalOrder_mul_anPart (φ : 𝓕.States) (a : CrAnAlgebra 𝓕) :
    refine normalOrder_mul_annihilate _ ?_ _
    simp [crAnStatesToCreateAnnihilate]

+/-!
+
+## Normal ordering for an adjacent creation and annihliation state
+
+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
+  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]
+  rw [← smul_smul, ← normalOrder_ofCrAnList]
+  congr
+  rw [ofCrAnList_append, ofCrAnList_cons, ofCrAnList_cons]
+  noncomm_ring
+
+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
+  change (normalOrder ∘ₗ mulLinearMap (ofCrAnList φs * ofCrAnState φc * ofCrAnState φa)) a =
+    (smulLinearMap _ ∘ₗ normalOrder ∘ₗ
+    mulLinearMap (ofCrAnList φs * ofCrAnState φa * ofCrAnState φc)) a
+  refine LinearMap.congr_fun ?h a
+  apply ofCrAnListBasis.ext
+  intro l
+  simp only [mulLinearMap, LinearMap.coe_mk, AddHom.coe_mk, ofListBasis_eq_ofList,
+    LinearMap.coe_comp, Function.comp_apply, instCommGroup.eq_1]
+  rw [normalOrder_swap_create_annihlate_ofCrAnList_ofCrAnList φc φa hφc hφa]
+  rfl
+
+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
+  rw [mul_assoc, mul_assoc, mul_assoc, mul_assoc]
+  change (normalOrder ∘ₗ mulLinearMap.flip (ofCrAnState φc * (ofCrAnState φa * b))) a =
+    (smulLinearMap (𝓢(𝓕 |>ₛ φc, 𝓕 |>ₛ φa)) ∘ₗ
+    normalOrder ∘ₗ mulLinearMap.flip (ofCrAnState φa * (ofCrAnState φc * b))) a
+  apply LinearMap.congr_fun
+  apply ofCrAnListBasis.ext
+  intro l
+  simp only [mulLinearMap, ofListBasis_eq_ofList, LinearMap.coe_comp, Function.comp_apply,
+    LinearMap.flip_apply, LinearMap.coe_mk, AddHom.coe_mk, instCommGroup.eq_1]
+  repeat rw [← mul_assoc]
+  rw [normalOrder_swap_create_annihlate_ofCrAnList φc φa hφc hφa]
+  rfl
+
+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
+  rw [superCommute_ofCrAnState_ofCrAnState]
+  simp only [instCommGroup.eq_1, Algebra.smul_mul_assoc]
+  rw [mul_sub, sub_mul, map_sub, ← smul_mul_assoc]
+  rw [← mul_assoc, ← mul_assoc]
+  rw [normalOrder_swap_create_annihlate φc φa hφc hφa]
+  simp only [FieldStatistic.instCommGroup.eq_1, Algebra.mul_smul_comm, Algebra.smul_mul_assoc,
+    map_smul, sub_self]
+
+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
+  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]
+  apply Or.inr
+  exact normalOrder_superCommute_create_annihilate φc φa hφc hφa a b
+
 lemma normalOrder_swap_crPart_anPart (φ φ' : 𝓕.States) (a b : CrAnAlgebra 𝓕) :
    normalOrder (a * (crPart (StateAlgebra.ofState φ)) * (anPart (StateAlgebra.ofState φ')) * b) =
    𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') •
@ -240,6 +250,14 @@ lemma normalOrder_swap_crPart_anPart (φ φ' : 𝓕.States) (a b : CrAnAlgebra
    rfl
    rfl

+/-!
+
+## Normal ordering for an anPart and crPart
+
+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 φ')) *
@ -290,15 +308,80 @@ lemma normalOrder_superCommute_anPart_crPart (φ φ' : 𝓕.States) (a b : CrAnA
    simp only [anPart_posAsymp, crPart_position]
    refine normalOrder_superCommute_annihilate_create _ _ (by rfl) (by rfl) _ _

+/-!
+
+## The normal ordering of a product of two states
+
+-/
+
+@[simp]
+lemma normalOrder_crPart_mul_crPart (φ φ' : 𝓕.States) :
+    normalOrder (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 φ'))]
+  rw [normalOrder_crPart_mul, normalOrder_one]
+  simp
+
+@[simp]
+lemma normalOrder_anPart_mul_anPart (φ φ' : 𝓕.States) :
+    normalOrder (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 φ))]
+  rw [normalOrder_mul_anPart, normalOrder_one]
+  simp
+
+@[simp]
+lemma normalOrder_crPart_mul_anPart (φ φ' : 𝓕.States) :
+    normalOrder (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 φ'))]
+  rw [normalOrder_mul_anPart, normalOrder_one]
+  simp
+
+@[simp]
+lemma normalOrder_anPart_mul_crPart (φ φ' : 𝓕.States) :
+    normalOrder (anPart (StateAlgebra.ofState φ) * crPart (StateAlgebra.ofState φ')) =
+    𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') •
+    (crPart (StateAlgebra.ofState φ') * anPart (StateAlgebra.ofState φ)) := by
+  conv_lhs => rw [← one_mul (anPart (StateAlgebra.ofState φ) * crPart (StateAlgebra.ofState φ'))]
+  conv_lhs => rw [← mul_one (1 * (anPart (StateAlgebra.ofState φ) *
+    crPart (StateAlgebra.ofState φ')))]
+  rw [← mul_assoc, normalOrder_swap_anPart_crPart]
+  simp
+
+lemma normalOrder_ofState_mul_ofState (φ φ' : 𝓕.States) :
+    normalOrder (ofState φ * ofState φ') =
+    crPart (StateAlgebra.ofState φ) * crPart (StateAlgebra.ofState φ') +
+    𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') •
+    (crPart (StateAlgebra.ofState φ') * anPart (StateAlgebra.ofState φ)) +
+    crPart (StateAlgebra.ofState φ) * anPart (StateAlgebra.ofState φ') +
+    anPart (StateAlgebra.ofState φ) * anPart (StateAlgebra.ofState φ') := by
+  rw [ofState_eq_crPart_add_anPart, ofState_eq_crPart_add_anPart]
+  rw [mul_add, add_mul, add_mul]
+  simp only [map_add, normalOrder_crPart_mul_crPart, normalOrder_anPart_mul_crPart,
+    instCommGroup.eq_1, normalOrder_crPart_mul_anPart, normalOrder_anPart_mul_anPart]
+  abel
+
+/-!
+
+## Normal order with super commutors
+
+-/
+
+/-! 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')) =
+      superCommute (ofCrAnState φc) (ofCrAnState φc') * ofCrAnList φs')) =
      normalOrderSign (φs ++ φc' :: φc :: φs') •
    (ofCrAnList (createFilter φs) * superCommute (ofCrAnState φc) (ofCrAnState φc') *
      ofCrAnList (createFilter φs') * ofCrAnList (annihilateFilter (φs ++ φs'))) := by
-  rw [superCommute_ofCrAnState]
+  rw [superCommute_ofCrAnState_ofCrAnState]
  rw [mul_sub, sub_mul, map_sub]
  conv_lhs =>
    lhs
@ -372,7 +455,7 @@ lemma normalOrder_superCommute_ofCrAnList_annihilate_annihilate_ofCrAnList
    (ofCrAnList (createFilter (φs ++ φs'))
      * ofCrAnList (annihilateFilter φs) * superCommute (ofCrAnState φa) (ofCrAnState φa')
      * ofCrAnList (annihilateFilter φs')) := by
-  rw [superCommute_ofCrAnState]
+  rw [superCommute_ofCrAnState_ofCrAnState]
  rw [mul_sub, sub_mul, map_sub]
  conv_lhs =>
    lhs
@ -440,62 +523,17 @@ lemma normalOrder_superCommute_ofCrAnList_annihilate_annihilate_ofCrAnList
  rw [ofCrAnList_append, ofCrAnList_singleton, ofCrAnList_singleton]
  rw [ofCrAnList_append, ofCrAnList_singleton, ofCrAnList_singleton, smul_mul_assoc]

-@[simp]
-lemma normalOrder_crPart_mul_crPart (φ φ' : 𝓕.States) :
-    normalOrder (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 φ'))]
-  rw [normalOrder_crPart_mul, normalOrder_one]
-  simp
+/-!

-@[simp]
-lemma normalOrder_anPart_mul_anPart (φ φ' : 𝓕.States) :
-    normalOrder (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 φ))]
-  rw [normalOrder_mul_anPart, normalOrder_one]
-  simp
+## Super commututators involving a normal order.

-@[simp]
-lemma normalOrder_crPart_mul_anPart (φ φ' : 𝓕.States) :
-    normalOrder (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 φ'))]
-  rw [normalOrder_mul_anPart, normalOrder_one]
-  simp
-
-@[simp]
-lemma normalOrder_anPart_mul_crPart (φ φ' : 𝓕.States) :
-    normalOrder (anPart (StateAlgebra.ofState φ) * crPart (StateAlgebra.ofState φ')) =
-    𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') •
-    (crPart (StateAlgebra.ofState φ') * anPart (StateAlgebra.ofState φ)) := by
-  conv_lhs => rw [← one_mul (anPart (StateAlgebra.ofState φ) * crPart (StateAlgebra.ofState φ'))]
-  conv_lhs => rw [← mul_one (1 * (anPart (StateAlgebra.ofState φ) *
-    crPart (StateAlgebra.ofState φ')))]
-  rw [← mul_assoc, normalOrder_swap_anPart_crPart]
-  simp
-
-lemma normalOrder_ofState_mul_ofState (φ φ' : 𝓕.States) :
-    normalOrder (ofState φ * ofState φ') =
-    crPart (StateAlgebra.ofState φ) * crPart (StateAlgebra.ofState φ') +
-    𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') •
-    (crPart (StateAlgebra.ofState φ') * anPart (StateAlgebra.ofState φ)) +
-    crPart (StateAlgebra.ofState φ) * anPart (StateAlgebra.ofState φ') +
-    anPart (StateAlgebra.ofState φ) * anPart (StateAlgebra.ofState φ') := by
-  rw [ofState_eq_crPart_add_anPart, ofState_eq_crPart_add_anPart]
-  rw [mul_add, add_mul, add_mul]
-  simp only [map_add, normalOrder_crPart_mul_crPart, normalOrder_anPart_mul_crPart,
-    instCommGroup.eq_1, normalOrder_crPart_mul_anPart, normalOrder_anPart_mul_anPart]
-  abel
+-/

 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
-  simp [normalOrder_ofCrAnList, map_smul, superCommute_ofCrAnList, ofCrAnList_append,
+  simp [normalOrder_ofCrAnList, map_smul, superCommute_ofCrAnList_ofCrAnList, ofCrAnList_append,
    smul_sub, smul_smul, mul_comm]

 lemma ofCrAnList_superCommute_normalOrder_ofStateList (φs : List 𝓕.CrAnStates)
@ -509,6 +547,12 @@ lemma ofCrAnList_superCommute_normalOrder_ofStateList (φs : List 𝓕.CrAnState
  rw [ofCrAnList_superCommute_normalOrder_ofCrAnList,
    CrAnSection.statistics_eq_state_statistics]

+/-!
+
+## Multiplications with normal order written in terms of super commute.
+
+-/
+
 lemma ofCrAnList_mul_normalOrder_ofStateList_eq_superCommute (φs : List 𝓕.CrAnStates)
    (φs' : List 𝓕.States) :
    ofCrAnList φs * normalOrder (ofStateList φs') =
--- a/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/SuperCommute.lean
+++ b/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/SuperCommute.lean
@ -37,11 +37,27 @@ noncomputable def superCommute : 𝓕.CrAnAlgebra →ₗ[ℂ] 𝓕.CrAnAlgebra
  whilst for two fermionic operators this corresponds to the anti-commutator. -/
 scoped[FieldSpecification.CrAnAlgebra] notation "⟨" φs "," φs' "⟩ₛca" => superCommute φs φs'

-lemma superCommute_ofCrAnList (φs φs' : List 𝓕.CrAnStates) : ⟨ofCrAnList φs, ofCrAnList φs'⟩ₛca =
+/-!
+
+## The super commutor of different types of elements
+
+-/
+
+lemma superCommute_ofCrAnList_ofCrAnList (φs φs' : List 𝓕.CrAnStates) :
+    ⟨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 φ' - 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') • ofCrAnState φ' * ofCrAnState φ := by
+  rw [← ofCrAnList_singleton, ← ofCrAnList_singleton]
+  rw [superCommute_ofCrAnList_ofCrAnList, ofCrAnList_append]
+  congr
+  rw [ofCrAnList_append]
+  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 -
    𝓢(𝓕 |>ₛ φcas, 𝓕 |>ₛ φs) • ofStateList φs * ofCrAnList φcas := by
@ -49,7 +65,7 @@ lemma superCommute_ofCrAnList_ofStatesList (φcas : List 𝓕.CrAnStates) (φs :
  rw [map_sum]
  conv_lhs =>
    enter [2, x]
-    rw [superCommute_ofCrAnList, CrAnSection.statistics_eq_state_statistics,
+    rw [superCommute_ofCrAnList_ofCrAnList, CrAnSection.statistics_eq_state_statistics,
      ofCrAnList_append, ofCrAnList_append]
  rw [Finset.sum_sub_distrib, ← Finset.mul_sum, ← Finset.smul_sum,
    ← Finset.sum_mul, ← ofStateList_sum]
@ -74,16 +90,183 @@ lemma superCommute_ofState_ofStatesList (φ : 𝓕.States) (φs : List 𝓕.Stat
  rw [← ofStateList_singleton, superCommute_ofStateList_ofStatesList, ofStateList_singleton]
  simp

-lemma superCommute_ofStateList_ofStates (φs : List 𝓕.States) (φ : 𝓕.States) :
+lemma superCommute_ofStateList_ofState (φs : List 𝓕.States) (φ : 𝓕.States) :
    ⟨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 φ') -
+    𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') • crPart (StateAlgebra.ofState φ') * anPart (StateAlgebra.ofState φ) := by
+  match φ, φ' with
+  | States.negAsymp φ, _ =>
+    simp
+  | _, States.posAsymp φ =>
+    simp only [crPart_posAsymp, map_zero, mul_zero, instCommGroup.eq_1, smul_zero, zero_mul,
+      sub_self]
+  | States.position φ, States.position φ' =>
+    simp only [anPart_position, crPart_position, instCommGroup.eq_1, Algebra.smul_mul_assoc]
+    rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, superCommute_ofCrAnList_ofCrAnList]
+    simp [crAnStatistics, ← ofCrAnList_append]
+  | States.posAsymp φ, States.position φ' =>
+    simp only [anPart_posAsymp, crPart_position, instCommGroup.eq_1, Algebra.smul_mul_assoc]
+    rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, superCommute_ofCrAnList_ofCrAnList]
+    simp [crAnStatistics, ← ofCrAnList_append]
+  | States.position φ, States.negAsymp φ' =>
+    simp only [anPart_position, crPart_negAsymp, instCommGroup.eq_1, Algebra.smul_mul_assoc]
+    rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, superCommute_ofCrAnList_ofCrAnList]
+    simp only [List.singleton_append, instCommGroup.eq_1, crAnStatistics,
+      FieldStatistic.ofList_singleton, Function.comp_apply, crAnStatesToStates_prod, ←
+      ofCrAnList_append]
+  | States.posAsymp φ, States.negAsymp φ' =>
+    simp only [anPart_posAsymp, crPart_negAsymp, instCommGroup.eq_1, Algebra.smul_mul_assoc]
+    rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, superCommute_ofCrAnList_ofCrAnList]
+    simp [crAnStatistics, ← ofCrAnList_append]
+
+lemma superCommute_crPart_anPart (φ φ' : 𝓕.States) :
+    ⟨crPart (StateAlgebra.ofState φ), anPart (StateAlgebra.ofState φ')⟩ₛca =
+    crPart (StateAlgebra.ofState φ) * anPart (StateAlgebra.ofState φ') -
+    𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') •
+    anPart (StateAlgebra.ofState φ') * crPart (StateAlgebra.ofState φ) := by
+    match φ, φ' with
+    | States.posAsymp φ, _ =>
+    simp only [crPart_posAsymp, map_zero, LinearMap.zero_apply, zero_mul, instCommGroup.eq_1,
+      mul_zero, sub_self]
+    | _, States.negAsymp φ =>
+    simp only [anPart_negAsymp, map_zero, mul_zero, instCommGroup.eq_1, smul_zero, zero_mul,
+      sub_self]
+    | States.position φ, States.position φ' =>
+    simp only [crPart_position, anPart_position, instCommGroup.eq_1, Algebra.smul_mul_assoc]
+    rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, superCommute_ofCrAnList_ofCrAnList]
+    simp [crAnStatistics, ← ofCrAnList_append]
+    | States.position φ, States.posAsymp φ' =>
+    simp only [crPart_position, anPart_posAsymp, instCommGroup.eq_1, Algebra.smul_mul_assoc]
+    rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, superCommute_ofCrAnList_ofCrAnList]
+    simp [crAnStatistics, ← ofCrAnList_append]
+    | States.negAsymp φ, States.position φ' =>
+    simp only [crPart_negAsymp, anPart_position, instCommGroup.eq_1, Algebra.smul_mul_assoc]
+    rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, superCommute_ofCrAnList_ofCrAnList]
+    simp [crAnStatistics, ← ofCrAnList_append]
+    | States.negAsymp φ, States.posAsymp φ' =>
+    simp only [crPart_negAsymp, anPart_posAsymp, instCommGroup.eq_1, Algebra.smul_mul_assoc]
+    rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, superCommute_ofCrAnList_ofCrAnList]
+    simp [crAnStatistics, ← ofCrAnList_append]
+
+lemma superCommute_crPart_crPart (φ φ' : 𝓕.States) :
+    ⟨crPart (StateAlgebra.ofState φ), crPart (StateAlgebra.ofState φ')⟩ₛca =
+    crPart (StateAlgebra.ofState φ) * crPart (StateAlgebra.ofState φ') -
+    𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') •
+    crPart (StateAlgebra.ofState φ') * crPart (StateAlgebra.ofState φ) := by
+  match φ, φ' with
+  | States.posAsymp φ, _ =>
+  simp only [crPart_posAsymp, map_zero, LinearMap.zero_apply, zero_mul, instCommGroup.eq_1,
+    mul_zero, sub_self]
+  | _, States.posAsymp φ =>
+  simp only [crPart_posAsymp, map_zero, mul_zero, instCommGroup.eq_1, smul_zero, zero_mul, sub_self]
+  | States.position φ, States.position φ' =>
+  simp only [crPart_position, instCommGroup.eq_1, Algebra.smul_mul_assoc]
+  rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, superCommute_ofCrAnList_ofCrAnList]
+  simp [crAnStatistics, ← ofCrAnList_append]
+  | States.position φ, States.negAsymp φ' =>
+  simp only [crPart_position, crPart_negAsymp, instCommGroup.eq_1, Algebra.smul_mul_assoc]
+  rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, superCommute_ofCrAnList_ofCrAnList]
+  simp [crAnStatistics, ← ofCrAnList_append]
+  | States.negAsymp φ, States.position φ' =>
+  simp only [crPart_negAsymp, crPart_position, instCommGroup.eq_1, Algebra.smul_mul_assoc]
+  rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, superCommute_ofCrAnList_ofCrAnList]
+  simp [crAnStatistics, ← ofCrAnList_append]
+  | States.negAsymp φ, States.negAsymp φ' =>
+  simp only [crPart_negAsymp, instCommGroup.eq_1, Algebra.smul_mul_assoc]
+  rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, superCommute_ofCrAnList_ofCrAnList]
+  simp [crAnStatistics, ← ofCrAnList_append]
+
+lemma superCommute_anPart_anPart (φ φ' : 𝓕.States) :
+    ⟨anPart (StateAlgebra.ofState φ), anPart (StateAlgebra.ofState φ')⟩ₛca =
+    anPart (StateAlgebra.ofState φ) * anPart (StateAlgebra.ofState φ') -
+    𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') •
+    anPart (StateAlgebra.ofState φ') * anPart (StateAlgebra.ofState φ) := by
+  match φ, φ' with
+  | States.negAsymp φ, _ =>
+    simp
+  | _, States.negAsymp φ =>
+    simp
+  | States.position φ, States.position φ' =>
+    simp only [anPart_position, instCommGroup.eq_1, Algebra.smul_mul_assoc]
+    rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, superCommute_ofCrAnList_ofCrAnList]
+    simp [crAnStatistics, ← ofCrAnList_append]
+  | States.position φ, States.posAsymp φ' =>
+    simp only [anPart_position, anPart_posAsymp, instCommGroup.eq_1, Algebra.smul_mul_assoc]
+    rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, superCommute_ofCrAnList_ofCrAnList]
+    simp [crAnStatistics, ← ofCrAnList_append]
+  | States.posAsymp φ, States.position φ' =>
+    simp only [anPart_posAsymp, anPart_position, instCommGroup.eq_1, Algebra.smul_mul_assoc]
+    rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, superCommute_ofCrAnList_ofCrAnList]
+    simp [crAnStatistics, ← ofCrAnList_append]
+  | States.posAsymp φ, States.posAsymp φ' =>
+    simp only [anPart_posAsymp, instCommGroup.eq_1, Algebra.smul_mul_assoc]
+    rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, superCommute_ofCrAnList_ofCrAnList]
+    simp [crAnStatistics, ← ofCrAnList_append]
+
+lemma superCommute_crPart_ofStateList (φ : 𝓕.States) (φs : List 𝓕.States) :
+    ⟨crPart (StateAlgebra.ofState φ), ofStateList φs⟩ₛca =
+    crPart (StateAlgebra.ofState φ) * ofStateList φs - 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φs) • ofStateList φs *
+    crPart (StateAlgebra.ofState φ) := by
+  match φ with
+  | States.negAsymp φ =>
+    simp only [crPart_negAsymp, instCommGroup.eq_1, Algebra.smul_mul_assoc]
+    rw [← ofCrAnList_singleton, superCommute_ofCrAnList_ofStatesList]
+    simp [crAnStatistics]
+  | States.position φ =>
+    simp only [crPart_position, instCommGroup.eq_1, Algebra.smul_mul_assoc]
+    rw [← ofCrAnList_singleton, superCommute_ofCrAnList_ofStatesList]
+    simp [crAnStatistics]
+  | States.posAsymp φ =>
+    simp
+
+lemma superCommute_anPart_ofStateList (φ : 𝓕.States) (φs : List 𝓕.States) :
+    ⟨anPart (StateAlgebra.ofState φ), ofStateList φs⟩ₛca =
+    anPart (StateAlgebra.ofState φ) * ofStateList φs - 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φs) •
+    ofStateList φs * anPart (StateAlgebra.ofState φ) := by
+  match φ with
+  | States.negAsymp φ =>
+    simp
+  | States.position φ =>
+    simp only [anPart_position, instCommGroup.eq_1, Algebra.smul_mul_assoc]
+    rw [← ofCrAnList_singleton, superCommute_ofCrAnList_ofStatesList]
+    simp [crAnStatistics]
+  | States.posAsymp φ =>
+    simp only [anPart_posAsymp, instCommGroup.eq_1, Algebra.smul_mul_assoc]
+    rw [← ofCrAnList_singleton, superCommute_ofCrAnList_ofStatesList]
+    simp [crAnStatistics]
+
+lemma superCommute_crPart_ofState (φ φ' : 𝓕.States) :
+    ⟨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 φ' -
+    𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') • ofState φ' * anPart (StateAlgebra.ofState φ) := by
+  rw [← ofStateList_singleton, superCommute_anPart_ofStateList]
+  simp
+
+/-!
+
+## Mul equal superCommute
+
+Lemmas which rewrite a multiplication of two elements of the algebra as their commuted
+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
-  rw [superCommute_ofCrAnList]
+  rw [superCommute_ofCrAnList_ofCrAnList]
  simp [ofCrAnList_append]

 lemma ofCrAnState_mul_ofCrAnList_eq_superCommute (φ : 𝓕.CrAnStates) (φs' : List 𝓕.CrAnStates) :
@ -107,132 +290,17 @@ lemma ofState_mul_ofStateList_eq_superCommute (φ : 𝓕.States) (φs' : List
 lemma ofStateList_mul_ofState_eq_superCommute (φs : List 𝓕.States) (φ : 𝓕.States) :
    ofStateList φs * ofState φ = 𝓢(𝓕 |>ₛ φs, 𝓕 |>ₛ φ) • ofState φ * ofStateList φs
    + ⟨ofStateList φs, ofState φ⟩ₛca := by
-  rw [superCommute_ofStateList_ofStates]
+  rw [superCommute_ofStateList_ofState]
  simp

-lemma superCommute_anPart_crPart (φ φ' : 𝓕.States) :
-    ⟨anPart (StateAlgebra.ofState φ), crPart (StateAlgebra.ofState φ')⟩ₛca =
-    anPart (StateAlgebra.ofState φ) * crPart (StateAlgebra.ofState φ') -
-    𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') •
-    crPart (StateAlgebra.ofState φ') * anPart (StateAlgebra.ofState φ) := by
-  match φ, φ' with
-  | States.negAsymp φ, _ =>
-    simp
-  | _, States.posAsymp φ =>
-    simp only [crPart_posAsymp, map_zero, mul_zero, instCommGroup.eq_1, smul_zero, zero_mul,
-      sub_self]
-  | States.position φ, States.position φ' =>
-    simp only [anPart_position, crPart_position, instCommGroup.eq_1, Algebra.smul_mul_assoc]
-    rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, superCommute_ofCrAnList]
-    simp [crAnStatistics, ← ofCrAnList_append]
-  | States.posAsymp φ, States.position φ' =>
-    simp only [anPart_posAsymp, crPart_position, instCommGroup.eq_1, Algebra.smul_mul_assoc]
-    rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, superCommute_ofCrAnList]
-    simp [crAnStatistics, ← ofCrAnList_append]
-  | States.position φ, States.negAsymp φ' =>
-    simp only [anPart_position, crPart_negAsymp, instCommGroup.eq_1, Algebra.smul_mul_assoc]
-    rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, superCommute_ofCrAnList]
-    simp only [List.singleton_append, instCommGroup.eq_1, crAnStatistics,
-      FieldStatistic.ofList_singleton, Function.comp_apply, crAnStatesToStates_prod, ←
-      ofCrAnList_append]
-  | States.posAsymp φ, States.negAsymp φ' =>
-    simp only [anPart_posAsymp, crPart_negAsymp, instCommGroup.eq_1, Algebra.smul_mul_assoc]
-    rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, superCommute_ofCrAnList]
-    simp [crAnStatistics, ← ofCrAnList_append]
-
-lemma superCommute_crPart_anPart (φ φ' : 𝓕.States) :
-    ⟨crPart (StateAlgebra.ofState φ), anPart (StateAlgebra.ofState φ')⟩ₛca =
-    crPart (StateAlgebra.ofState φ) * anPart (StateAlgebra.ofState φ') -
-    𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') •
-    anPart (StateAlgebra.ofState φ') * crPart (StateAlgebra.ofState φ) := by
-    match φ, φ' with
-    | States.posAsymp φ, _ =>
-    simp only [crPart_posAsymp, map_zero, LinearMap.zero_apply, zero_mul, instCommGroup.eq_1,
-      mul_zero, sub_self]
-    | _, States.negAsymp φ =>
-    simp only [anPart_negAsymp, map_zero, mul_zero, instCommGroup.eq_1, smul_zero, zero_mul,
-      sub_self]
-    | States.position φ, States.position φ' =>
-    simp only [crPart_position, anPart_position, instCommGroup.eq_1, Algebra.smul_mul_assoc]
-    rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, superCommute_ofCrAnList]
-    simp [crAnStatistics, ← ofCrAnList_append]
-    | States.position φ, States.posAsymp φ' =>
-    simp only [crPart_position, anPart_posAsymp, instCommGroup.eq_1, Algebra.smul_mul_assoc]
-    rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, superCommute_ofCrAnList]
-    simp [crAnStatistics, ← ofCrAnList_append]
-    | States.negAsymp φ, States.position φ' =>
-    simp only [crPart_negAsymp, anPart_position, instCommGroup.eq_1, Algebra.smul_mul_assoc]
-    rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, superCommute_ofCrAnList]
-    simp [crAnStatistics, ← ofCrAnList_append]
-    | States.negAsymp φ, States.posAsymp φ' =>
-    simp only [crPart_negAsymp, anPart_posAsymp, instCommGroup.eq_1, Algebra.smul_mul_assoc]
-    rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, superCommute_ofCrAnList]
-    simp [crAnStatistics, ← ofCrAnList_append]
-
-lemma superCommute_crPart_crPart (φ φ' : 𝓕.States) :
-    ⟨crPart (StateAlgebra.ofState φ), crPart (StateAlgebra.ofState φ')⟩ₛca =
-    crPart (StateAlgebra.ofState φ) * crPart (StateAlgebra.ofState φ') -
-    𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') •
-    crPart (StateAlgebra.ofState φ') * crPart (StateAlgebra.ofState φ) := by
-  match φ, φ' with
-  | States.posAsymp φ, _ =>
-  simp only [crPart_posAsymp, map_zero, LinearMap.zero_apply, zero_mul, instCommGroup.eq_1,
-    mul_zero, sub_self]
-  | _, States.posAsymp φ =>
-  simp only [crPart_posAsymp, map_zero, mul_zero, instCommGroup.eq_1, smul_zero, zero_mul, sub_self]
-  | States.position φ, States.position φ' =>
-  simp only [crPart_position, instCommGroup.eq_1, Algebra.smul_mul_assoc]
-  rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, superCommute_ofCrAnList]
-  simp [crAnStatistics, ← ofCrAnList_append]
-  | States.position φ, States.negAsymp φ' =>
-  simp only [crPart_position, crPart_negAsymp, instCommGroup.eq_1, Algebra.smul_mul_assoc]
-  rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, superCommute_ofCrAnList]
-  simp [crAnStatistics, ← ofCrAnList_append]
-  | States.negAsymp φ, States.position φ' =>
-  simp only [crPart_negAsymp, crPart_position, instCommGroup.eq_1, Algebra.smul_mul_assoc]
-  rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, superCommute_ofCrAnList]
-  simp [crAnStatistics, ← ofCrAnList_append]
-  | States.negAsymp φ, States.negAsymp φ' =>
-  simp only [crPart_negAsymp, instCommGroup.eq_1, Algebra.smul_mul_assoc]
-  rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, superCommute_ofCrAnList]
-  simp [crAnStatistics, ← ofCrAnList_append]
-
-lemma superCommute_anPart_anPart (φ φ' : 𝓕.States) :
-    ⟨anPart (StateAlgebra.ofState φ), anPart (StateAlgebra.ofState φ')⟩ₛca =
-    anPart (StateAlgebra.ofState φ) * anPart (StateAlgebra.ofState φ') -
-    𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') •
-    anPart (StateAlgebra.ofState φ') * anPart (StateAlgebra.ofState φ) := by
-  match φ, φ' with
-  | States.negAsymp φ, _ =>
-    simp
-  | _, States.negAsymp φ =>
-    simp
-  | States.position φ, States.position φ' =>
-    simp only [anPart_position, instCommGroup.eq_1, Algebra.smul_mul_assoc]
-    rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, superCommute_ofCrAnList]
-    simp [crAnStatistics, ← ofCrAnList_append]
-  | States.position φ, States.posAsymp φ' =>
-    simp only [anPart_position, anPart_posAsymp, instCommGroup.eq_1, Algebra.smul_mul_assoc]
-    rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, superCommute_ofCrAnList]
-    simp [crAnStatistics, ← ofCrAnList_append]
-  | States.posAsymp φ, States.position φ' =>
-    simp only [anPart_posAsymp, anPart_position, instCommGroup.eq_1, Algebra.smul_mul_assoc]
-    rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, superCommute_ofCrAnList]
-    simp [crAnStatistics, ← ofCrAnList_append]
-  | States.posAsymp φ, States.posAsymp φ' =>
-    simp only [anPart_posAsymp, instCommGroup.eq_1, Algebra.smul_mul_assoc]
-    rw [← ofCrAnList_singleton, ← ofCrAnList_singleton, superCommute_ofCrAnList]
-    simp [crAnStatistics, ← ofCrAnList_append]
-
-lemma crPart_anPart_eq_superCommute (φ φ' : 𝓕.States) :
+lemma crPart_mul_anPart_eq_superCommute (φ φ' : 𝓕.States) :
    crPart (StateAlgebra.ofState φ) * anPart (StateAlgebra.ofState φ') =
-    𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') •
-    anPart (StateAlgebra.ofState φ') * crPart (StateAlgebra.ofState φ) +
+    𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') • anPart (StateAlgebra.ofState φ') * crPart (StateAlgebra.ofState φ) +
    ⟨crPart (StateAlgebra.ofState φ), anPart (StateAlgebra.ofState φ')⟩ₛca := by
  rw [superCommute_crPart_anPart]
  simp

-lemma anPart_crPart_eq_superCommute (φ φ' : 𝓕.States) :
+lemma anPart_mul_crPart_eq_superCommute (φ φ' : 𝓕.States) :
    anPart (StateAlgebra.ofState φ) * crPart (StateAlgebra.ofState φ') =
    𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') •
    crPart (StateAlgebra.ofState φ') * anPart (StateAlgebra.ofState φ) +
@ -240,83 +308,36 @@ lemma anPart_crPart_eq_superCommute (φ φ' : 𝓕.States) :
  rw [superCommute_anPart_crPart]
  simp

-lemma crPart_crPart_eq_superCommute (φ φ' : 𝓕.States) :
+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 φ) +
    ⟨crPart (StateAlgebra.ofState φ), crPart (StateAlgebra.ofState φ')⟩ₛca := by
  rw [superCommute_crPart_crPart]
  simp

-lemma anPart_anPart_eq_superCommute (φ φ' : 𝓕.States) :
+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 φ) +
    ⟨anPart (StateAlgebra.ofState φ), anPart (StateAlgebra.ofState φ')⟩ₛca := by
  rw [superCommute_anPart_anPart]
  simp

-lemma superCommute_crPart_ofStatesList (φ : 𝓕.States) (φs : List 𝓕.States) :
-    ⟨crPart (StateAlgebra.ofState φ), ofStateList φs⟩ₛca =
-    crPart (StateAlgebra.ofState φ) * ofStateList φs - 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φs) • ofStateList φs *
-    crPart (StateAlgebra.ofState φ) := by
-  match φ with
-  | States.negAsymp φ =>
-    simp only [crPart_negAsymp, instCommGroup.eq_1, Algebra.smul_mul_assoc]
-    rw [← ofCrAnList_singleton, superCommute_ofCrAnList_ofStatesList]
-    simp [crAnStatistics]
-  | States.position φ =>
-    simp only [crPart_position, instCommGroup.eq_1, Algebra.smul_mul_assoc]
-    rw [← ofCrAnList_singleton, superCommute_ofCrAnList_ofStatesList]
-    simp [crAnStatistics]
-  | States.posAsymp φ =>
-    simp
-
-lemma superCommute_anPart_ofStatesList (φ : 𝓕.States) (φs : List 𝓕.States) :
-    ⟨anPart (StateAlgebra.ofState φ), ofStateList φs⟩ₛca =
-    anPart (StateAlgebra.ofState φ) * ofStateList φs - 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φs) •
-    ofStateList φs * anPart (StateAlgebra.ofState φ) := by
-  match φ with
-  | States.negAsymp φ =>
-    simp
-  | States.position φ =>
-    simp only [anPart_position, instCommGroup.eq_1, Algebra.smul_mul_assoc]
-    rw [← ofCrAnList_singleton, superCommute_ofCrAnList_ofStatesList]
-    simp [crAnStatistics]
-  | States.posAsymp φ =>
-    simp only [anPart_posAsymp, instCommGroup.eq_1, Algebra.smul_mul_assoc]
-    rw [← ofCrAnList_singleton, superCommute_ofCrAnList_ofStatesList]
-    simp [crAnStatistics]
-
-lemma superCommute_crPart_ofState (φ φ' : 𝓕.States) :
-    ⟨crPart (StateAlgebra.ofState φ), ofState φ'⟩ₛca =
-    crPart (StateAlgebra.ofState φ) * ofState φ' -
-    𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') •
-    ofState φ' * crPart (StateAlgebra.ofState φ) := by
-  rw [← ofStateList_singleton, superCommute_crPart_ofStatesList]
+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
+  rw [superCommute_ofCrAnList_ofStatesList]
  simp

-lemma superCommute_anPart_ofState (φ φ' : 𝓕.States) :
-    ⟨anPart (StateAlgebra.ofState φ), ofState φ'⟩ₛca =
-    anPart (StateAlgebra.ofState φ) * ofState φ' -
-    𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') •
-    ofState φ' * anPart (StateAlgebra.ofState φ) := by
-  rw [← ofStateList_singleton, superCommute_anPart_ofStatesList]
-  simp
+/-!

-lemma superCommute_ofCrAnState (φ φ' : 𝓕.CrAnStates) : ⟨ofCrAnState φ, ofCrAnState φ'⟩ₛca =
-    ofCrAnState φ * ofCrAnState φ' - 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') • ofCrAnState φ' * ofCrAnState φ := by
-  rw [← ofCrAnList_singleton, ← ofCrAnList_singleton]
-  rw [superCommute_ofCrAnList, ofCrAnList_append]
-  congr
-  rw [ofCrAnList_append]
-  rw [FieldStatistic.ofList_singleton, FieldStatistic.ofList_singleton, smul_mul_assoc]
+## Symmetry of the super commutor.

-lemma superCommute_ofCrAnList_symm (φs φ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
-  rw [superCommute_ofCrAnList, superCommute_ofCrAnList, smul_sub]
+    (- 𝓢(𝓕 |>ₛ φ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]
  conv_rhs =>
@ -325,10 +346,10 @@ lemma superCommute_ofCrAnList_symm (φs φs' : List 𝓕.CrAnStates) :
  simp only [one_smul]
  abel

-lemma superCommute_ofCrAnState_symm (φ φ' : 𝓕.CrAnStates) :
+lemma superCommute_ofCrAnState_ofCrAnState_symm (φ φ' : 𝓕.CrAnStates) :
    ⟨ofCrAnState φ, ofCrAnState φ'⟩ₛca =
    (- 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ')) • ⟨ofCrAnState φ', ofCrAnState φ⟩ₛca := by
-  rw [superCommute_ofCrAnState, superCommute_ofCrAnState]
+  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]
  rw [smul_smul]
@ -338,21 +359,26 @@ lemma superCommute_ofCrAnState_symm (φ φ' : 𝓕.CrAnStates) :
  simp only [one_smul]
  abel

+/-!
+
+## Splitting the super commutor on lists into sums.
+
+-/
 lemma superCommute_ofCrAnList_ofCrAnList_cons (φ : 𝓕.CrAnStates) (φs φs' : List 𝓕.CrAnStates) :
    ⟨ofCrAnList φs, ofCrAnList (φ :: φs')⟩ₛca =
    ⟨ofCrAnList φs, ofCrAnState φ⟩ₛca * ofCrAnList φs' +
    𝓢(𝓕 |>ₛ φs, 𝓕 |>ₛ φ)
    • ofCrAnState φ * ⟨ofCrAnList φs, ofCrAnList φs'⟩ₛca := by
-  rw [superCommute_ofCrAnList]
+  rw [superCommute_ofCrAnList_ofCrAnList]
  conv_rhs =>
    lhs
-    rw [← ofCrAnList_singleton, superCommute_ofCrAnList, sub_mul, ← ofCrAnList_append]
+    rw [← ofCrAnList_singleton, superCommute_ofCrAnList_ofCrAnList, sub_mul, ← ofCrAnList_append]
    rhs
    rw [FieldStatistic.ofList_singleton, ofCrAnList_append, ofCrAnList_singleton, smul_mul_assoc,
      mul_assoc, ← ofCrAnList_append]
  conv_rhs =>
    rhs
-    rw [superCommute_ofCrAnList, mul_sub, smul_mul_assoc]
+    rw [superCommute_ofCrAnList_ofCrAnList, mul_sub, smul_mul_assoc]
  simp only [instCommGroup.eq_1, List.cons_append, List.append_assoc, List.nil_append,
    Algebra.mul_smul_comm, Algebra.smul_mul_assoc, sub_add_sub_cancel, sub_right_inj]
  rw [← ofCrAnList_cons, smul_smul, FieldStatistic.ofList_cons_eq_mul]
@ -378,12 +404,6 @@ lemma superCommute_ofCrAnList_ofStateList_cons (φ : 𝓕.States) (φs : List
  rw [ofStateList_cons, mul_assoc, smul_smul, FieldStatistic.ofList_cons_eq_mul]
  simp [mul_comm]

-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
-  rw [superCommute_ofCrAnList_ofStatesList]
-  simp
-
 lemma superCommute_ofCrAnList_ofCrAnList_eq_sum (φs : List 𝓕.CrAnStates) :
    (φs' : List 𝓕.CrAnStates) →
    ⟨ofCrAnList φs, ofCrAnList φs'⟩ₛca =
@ -391,7 +411,7 @@ lemma superCommute_ofCrAnList_ofCrAnList_eq_sum (φs : List 𝓕.CrAnStates) :
    ofCrAnList (φs'.take n) * ⟨ofCrAnList φs, ofCrAnState (φs'.get n)⟩ₛca *
    ofCrAnList (φs'.drop (n + 1))
  | [] => by
-    simp [← ofCrAnList_nil, superCommute_ofCrAnList]
+    simp [← ofCrAnList_nil, superCommute_ofCrAnList_ofCrAnList]
  | φ :: φs' => by
    rw [superCommute_ofCrAnList_ofCrAnList_cons, superCommute_ofCrAnList_ofCrAnList_eq_sum φs φs']
    conv_rhs => erw [Fin.sum_univ_succ]
@ -400,8 +420,7 @@ lemma superCommute_ofCrAnList_ofCrAnList_eq_sum (φs : List 𝓕.CrAnStates) :
    · simp [Finset.mul_sum, smul_smul, ofCrAnList_cons, mul_assoc,
        FieldStatistic.ofList_cons_eq_mul, mul_comm]

-lemma superCommute_ofCrAnList_ofStateList_eq_sum (φs : List 𝓕.CrAnStates) :
-    (φs' : List 𝓕.States) →
+lemma superCommute_ofCrAnList_ofStateList_eq_sum (φs : List 𝓕.CrAnStates) : (φs' : List 𝓕.States) →
    ⟨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 *
--- a/HepLean/PerturbationTheory/Algebras/ProtoOperatorAlgebra/Basic.lean
+++ b/HepLean/PerturbationTheory/Algebras/ProtoOperatorAlgebra/Basic.lean
@ -18,7 +18,7 @@ open CrAnAlgebra
  to be isomorphic to the actual operator algebra of a field theory.
  These properties are sufficent to prove certain theorems about the Operator algebra
  in particular Wick's theorem. -/
-structure OperatorAlgebra where
+structure ProtoOperatorAlgebra where
  /-- The algebra representing the operator algebra. -/
  A : Type
  /-- The instance of the type `A` as a semi-ring. -/
@ -43,9 +43,9 @@ structure OperatorAlgebra where
    (_ : ¬ (𝓕 |>ₛ φ) = (𝓕 |>ₛ φ')),
    crAnF (superCommute (ofCrAnState φ) (ofCrAnState φ')) = 0

-namespace OperatorAlgebra
+namespace ProtoOperatorAlgebra
 open FieldStatistic
-variable {𝓕 : FieldSpecification} (𝓞 : 𝓕.OperatorAlgebra)
+variable {𝓕 : FieldSpecification} (𝓞 : 𝓕.ProtoOperatorAlgebra)

 /-- The algebra `𝓞.A` carries the instance of a semi-ring induced via `A_seimRing`. -/
 instance : Semiring 𝓞.A := 𝓞.A_semiRing
@ -198,5 +198,5 @@ lemma crAnF_superCommute_ofCrAnState_ofStateList_eq_sum (φ : 𝓕.CrAnStates) (
  · congr
    rw [← map_mul, ← ofStateList_append, ← List.eraseIdx_eq_take_drop_succ]

-end OperatorAlgebra
+end ProtoOperatorAlgebra
 end FieldSpecification
--- a/HepLean/PerturbationTheory/Algebras/ProtoOperatorAlgebra/NormalOrder.lean
+++ b/HepLean/PerturbationTheory/Algebras/ProtoOperatorAlgebra/NormalOrder.lean
@ -14,11 +14,19 @@ import HepLean.PerturbationTheory.Koszul.KoszulSign
 namespace FieldSpecification
 variable {𝓕 : FieldSpecification}

-namespace OperatorAlgebra
-variable {𝓞 : OperatorAlgebra 𝓕}
+namespace ProtoOperatorAlgebra
+variable {𝓞 : ProtoOperatorAlgebra 𝓕}
 open CrAnAlgebra
 open FieldStatistic

+/-!
+
+## Normal order of super-commutators.
+
+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)
@ -111,7 +119,7 @@ lemma crAnF_normalOrder_superCommute_ofCrAnList_ofCrAnState_eq_zero_mul (φa :
    (φs : List 𝓕.CrAnStates)
    (a b : 𝓕.CrAnAlgebra) :
    𝓞.crAnF (normalOrder (a * superCommute (ofCrAnList φs) (ofCrAnState φa) * b)) = 0 := by
-  rw [← ofCrAnList_singleton, superCommute_ofCrAnList_symm, ofCrAnList_singleton]
+  rw [← ofCrAnList_singleton, superCommute_ofCrAnList_ofCrAnList_symm, ofCrAnList_singleton]
  simp only [FieldStatistic.instCommGroup.eq_1, FieldStatistic.ofList_singleton, mul_neg,
    Algebra.mul_smul_comm, neg_mul, Algebra.smul_mul_assoc, map_neg, map_smul]
  rw [crAnF_normalOrder_superCommute_ofCrAnState_ofCrAnList_eq_zero_mul]
@ -180,27 +188,18 @@ lemma crAnF_normalOrder_superCommute_eq_zero
  rw [← crAnF_normalOrder_superCommute_eq_zero_mul 1 1 c d]
  simp

+/-!
+
+## Swapping terms in a normal order.
+
+-/
+
 lemma crAnF_normalOrder_ofState_ofState_swap (φ φ' : 𝓕.States) :
    𝓞.crAnF (normalOrder (ofState φ * ofState φ')) =
-    𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') •
-    𝓞.crAnF (normalOrder (ofState φ' * ofState φ)) := by
-  conv_lhs =>
-    rhs
-    rhs
-    rw [ofState_eq_crPart_add_anPart, ofState_eq_crPart_add_anPart]
-    rw [mul_add, add_mul, add_mul]
-    rw [crPart_crPart_eq_superCommute, crPart_anPart_eq_superCommute,
-      anPart_anPart_eq_superCommute, anPart_crPart_eq_superCommute]
-  simp only [FieldStatistic.instCommGroup.eq_1, Algebra.smul_mul_assoc, map_add, map_smul,
-    normalOrder_crPart_mul_crPart, normalOrder_crPart_mul_anPart, normalOrder_anPart_mul_crPart,
-    normalOrder_anPart_mul_anPart, map_mul, crAnF_normalOrder_superCommute_eq_zero, add_zero]
-  rw [normalOrder_ofState_mul_ofState]
-  simp only [FieldStatistic.instCommGroup.eq_1, map_add, map_mul, map_smul, smul_add]
-  rw [smul_smul]
-  simp only [FieldStatistic.exchangeSign_mul_self_swap, one_smul]
-  abel
-
-open FieldStatistic
+    𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') • 𝓞.crAnF (normalOrder (ofState φ' * ofState φ)) := by
+  rw [← ofStateList_singleton, ← ofStateList_singleton,
+    ofStateList_mul_ofStateList_eq_superCommute]
+  simp

 lemma crAnF_normalOrder_ofCrAnState_ofCrAnList_swap (φ : 𝓕.CrAnStates)
    (φs : List 𝓕.CrAnStates) :
@ -249,6 +248,11 @@ lemma crAnF_normalOrder_ofStatesList_mul_anPart_swap (φ : 𝓕.States)
  rw [← normalOrder_mul_anPart]
  rw [crAnF_normalOrder_ofStatesList_anPart_swap]

+/-!
+
+## Super commutators with a normal ordered term as sums
+
+-/
 lemma crAnF_ofCrAnState_superCommute_normalOrder_ofCrAnList_eq_sum (φ : 𝓕.CrAnStates)
    (φs : List 𝓕.CrAnStates) : 𝓞.crAnF (⟨ofCrAnState φ, normalOrder (ofCrAnList φs)⟩ₛca) =
    ∑ n : Fin φs.length, 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ (φs.take n)) •
@ -316,6 +320,11 @@ lemma crAnF_anPart_superCommute_normalOrder_ofStateList_eq_sum (φ : 𝓕.States
    rw [crAnF_ofCrAnState_superCommute_normalOrder_ofStateList_eq_sum]
    simp [crAnStatistics]

+/-!
+
+## Multiplying with normal ordered terms
+
+-/
 lemma crAnF_anPart_mul_normalOrder_ofStatesList_eq_superCommute (φ : 𝓕.States)
    (φ' : List 𝓕.States) :
    𝓞.crAnF (anPart (StateAlgebra.ofState φ) * normalOrder (ofStateList φ')) =
@ -359,6 +368,12 @@ lemma crAnF_ofState_mul_normalOrder_ofStatesList_eq_sum (φ : 𝓕.States)
    Fintype.sum_option, one_mul]
  rfl

+/-!
+
+## Cons vs insertIdx for a normal ordered term.
+
+-/
+
 lemma crAnF_ofState_normalOrder_insert (φ : 𝓕.States) (φs : List 𝓕.States)
    (k : Fin φs.length.succ) :
    𝓞.crAnF (normalOrder (ofStateList (φ :: φs))) =
@ -375,6 +390,6 @@ lemma crAnF_ofState_normalOrder_insert (φ : 𝓕.States) (φs : List 𝓕.State
  rw [← ofStateList_append, ← ofStateList_append]
  simp

-end OperatorAlgebra
+end ProtoOperatorAlgebra

 end FieldSpecification
--- a/HepLean/PerturbationTheory/Algebras/ProtoOperatorAlgebra/TimeContraction.lean
+++ b/HepLean/PerturbationTheory/Algebras/ProtoOperatorAlgebra/TimeContraction.lean
@ -3,7 +3,7 @@ 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
 -/
-import HepLean.PerturbationTheory.Algebras.OperatorAlgebra.NormalOrder
+import HepLean.PerturbationTheory.Algebras.ProtoOperatorAlgebra.NormalOrder
 import HepLean.PerturbationTheory.Algebras.StateAlgebra.TimeOrder
 /-!

@ -19,9 +19,9 @@ variable {𝓕 : FieldSpecification}
 open CrAnAlgebra
 noncomputable section

-namespace OperatorAlgebra
+namespace ProtoOperatorAlgebra

-variable (𝓞 : 𝓕.OperatorAlgebra)
+variable (𝓞 : 𝓕.ProtoOperatorAlgebra)
 open FieldStatistic

 /-- The time contraction of two States as an element of `𝓞.A` defined
@ -86,7 +86,7 @@ lemma timeContract_zero_of_diff_grade (φ ψ : 𝓕.States) (h : (𝓕 |>ₛ φ)
    have ht := IsTotal.total (r := 𝓕.timeOrderRel) φ ψ
    simp_all

-end OperatorAlgebra
+end ProtoOperatorAlgebra

 end
 end FieldSpecification
--- a/HepLean/PerturbationTheory/Algebras/StateAlgebra/Basic.lean
+++ b/HepLean/PerturbationTheory/Algebras/StateAlgebra/Basic.lean
@ -13,8 +13,7 @@ generated by these states. We call this the state algebra, or the state free-alg

 The state free-algebra has minimal assumptions, yet can be used to concretely define time-ordering.

-In
-`HepLean.PerturbationTheory.Algebras.CrAnAlgebra.Basic`
+In `HepLean.PerturbationTheory.Algebras.CrAnAlgebra.Basic`
 we defined a related free-algebra generated by creation and annihilation states.

 -/
--- a/HepLean/PerturbationTheory/FieldSpecification/Examples.lean
+++ b/HepLean/PerturbationTheory/FieldSpecification/Examples.lean
@ -8,7 +8,6 @@ import HepLean.PerturbationTheory.FieldSpecification.Basic

 # Specific examples of field specifications

-
 -/

 namespace FieldSpecification
--- a/HepLean/PerturbationTheory/FieldSpecification/Filters.lean
+++ b/HepLean/PerturbationTheory/FieldSpecification/Filters.lean
@ -3,7 +3,7 @@ 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
 -/
-import HepLean.PerturbationTheory.Algebras.OperatorAlgebra.Basic
+import HepLean.PerturbationTheory.Algebras.ProtoOperatorAlgebra.Basic
 import HepLean.PerturbationTheory.Koszul.KoszulSign
 /-!

--- a/HepLean/PerturbationTheory/FieldSpecification/NormalOrder.lean
+++ b/HepLean/PerturbationTheory/FieldSpecification/NormalOrder.lean
@ -3,15 +3,13 @@ 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
 -/
-import HepLean.PerturbationTheory.Algebras.OperatorAlgebra.Basic
+import HepLean.PerturbationTheory.Algebras.ProtoOperatorAlgebra.Basic
 import HepLean.PerturbationTheory.Koszul.KoszulSign
 import HepLean.PerturbationTheory.FieldSpecification.Filters
 /-!

 # Normal Ordering of states

-
-
 -/

 namespace FieldSpecification
--- a/HepLean/PerturbationTheory/WickContraction/Basic.lean
+++ b/HepLean/PerturbationTheory/WickContraction/Basic.lean
@ -3,7 +3,7 @@ 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
 -/
-import HepLean.PerturbationTheory.Algebras.OperatorAlgebra.NormalOrder
+import HepLean.PerturbationTheory.Algebras.ProtoOperatorAlgebra.NormalOrder
 import HepLean.Mathematics.List.InsertIdx
 /-!

--- a/HepLean/PerturbationTheory/WickContraction/Involutions.lean
+++ b/HepLean/PerturbationTheory/WickContraction/Involutions.lean
@ -5,7 +5,7 @@ Authors: Joseph Tooby-Smith
 -/
 import HepLean.PerturbationTheory.WickContraction.Uncontracted
 import HepLean.PerturbationTheory.Algebras.StateAlgebra.TimeOrder
-import HepLean.PerturbationTheory.Algebras.OperatorAlgebra.TimeContraction
+import HepLean.PerturbationTheory.Algebras.ProtoOperatorAlgebra.TimeContraction
 import HepLean.PerturbationTheory.WickContraction.InsertList
 /-!

--- a/HepLean/PerturbationTheory/WickContraction/IsFull.lean
+++ b/HepLean/PerturbationTheory/WickContraction/IsFull.lean
@ -19,6 +19,7 @@ namespace WickContraction
 variable {n : ℕ} (c : WickContraction n)
 open HepLean.List
 open FieldStatistic
+open Nat

 /-- A contraction is full if there are no uncontracted fields, i.e. the finite set
  of uncontracted fields is empty. -/
@ -46,8 +47,6 @@ def isFullInvolutionEquiv : {c : WickContraction n // IsFull c} ≃
  left_inv c := by simp
  right_inv f := by simp

-open Nat
-
 /-- If `n` is even then the number of full contractions is `(n-1)!!`. -/
 theorem card_of_isfull_even (he : Even n) :
    Fintype.card {c : WickContraction n // IsFull c} = (n - 1)‼ := by
--- a/HepLean/PerturbationTheory/WickContraction/Sign.lean
+++ b/HepLean/PerturbationTheory/WickContraction/Sign.lean
@ -85,8 +85,7 @@ lemma signFinset_insertList_none (φ : 𝓕.States) (φs : List 𝓕.States)

 lemma stat_ofFinset_of_insertListLiftFinset (φ : 𝓕.States) (φs : List 𝓕.States)
    (i : Fin φs.length.succ) (a : Finset (Fin φs.length)) :
-    (𝓕 |>ₛ ⟨(φs.insertIdx i φ).get, insertListLiftFinset φ i a⟩) =
-    𝓕 |>ₛ ⟨φs.get, a⟩ := by
+    (𝓕 |>ₛ ⟨(φs.insertIdx i φ).get, insertListLiftFinset φ i a⟩) = 𝓕 |>ₛ ⟨φs.get, a⟩ := by
  simp only [ofFinset, Nat.succ_eq_add_one]
  congr 1
  rw [get_eq_insertIdx_succAbove φ _ i]
@ -823,8 +822,7 @@ lemma stat_signFinset_insert_some_self_fst
            simpa [Option.get_map] using hy2

 lemma stat_signFinset_insert_some_self_snd (φ : 𝓕.States) (φs : List 𝓕.States)
-    (c : WickContraction φs.length)
-    (i : Fin φs.length.succ) (j : c.uncontracted) :
+    (c : WickContraction φs.length) (i : Fin φs.length.succ) (j : c.uncontracted) :
    (𝓕 |>ₛ ⟨(φs.insertIdx i φ).get,
    (signFinset (c.insertList φ φs i (some j))
      (finCongr (insertIdx_length_fin φ φs i).symm (i.succAbove j))
@ -832,8 +830,7 @@ lemma stat_signFinset_insert_some_self_snd (φ : 𝓕.States) (φs : List 𝓕.S
    𝓕 |>ₛ ⟨φs.get,
    (Finset.univ.filter (fun x => j < x ∧ i.succAbove x < i ∧ ((c.getDual? x = none) ∨
      ∀ (h : (c.getDual? x).isSome), j < ((c.getDual? x).get h))))⟩ := by
-  rw [get_eq_insertIdx_succAbove φ _ i]
-  rw [ofFinset_finset_map]
+  rw [get_eq_insertIdx_succAbove φ _ i, ofFinset_finset_map]
  swap
  refine
    (Equiv.comp_injective i.succAbove (finCongr (Eq.symm (insertIdx_length_fin φ φs i)))).mpr ?hi.a
@ -905,55 +902,43 @@ lemma stat_signFinset_insert_some_self_snd (φ : 𝓕.States) (φs : List 𝓕.S
            exact Fin.succAbove_lt_succAbove_iff.mpr hy2

 lemma signInsertSomeCoef_eq_finset (φ : 𝓕.States) (φs : List 𝓕.States)
-    (c : WickContraction φs.length)
-    (i : Fin φs.length.succ) (j : c.uncontracted) (hφj : (𝓕 |>ₛ φ) = (𝓕 |>ₛ φs[j.1])) :
-    c.signInsertSomeCoef φ φs i j =
+    (c : WickContraction φs.length) (i : Fin φs.length.succ) (j : c.uncontracted)
+    (hφj : (𝓕 |>ₛ φ) = (𝓕 |>ₛ φs[j.1])) : c.signInsertSomeCoef φ φs i j =
    if i < i.succAbove j then
-    𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ⟨φs.get,
-    (Finset.univ.filter (fun x => i < i.succAbove x ∧ x < j ∧ ((c.getDual? x = none) ∨
-      ∀ (h : (c.getDual? x).isSome), i < i.succAbove ((c.getDual? x).get h))))⟩) else
-    𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ⟨φs.get,
-      (Finset.univ.filter (fun x => j < x ∧ i.succAbove x < i ∧ ((c.getDual? x = none) ∨
-      ∀ (h : (c.getDual? x).isSome), j < ((c.getDual? x).get h))))⟩) := by
-  rw [signInsertSomeCoef_if]
-  rw [stat_signFinset_insert_some_self_snd]
-  rw [stat_signFinset_insert_some_self_fst]
+      𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ⟨φs.get,
+      (Finset.univ.filter (fun x => i < i.succAbove x ∧ x < j ∧ ((c.getDual? x = none) ∨
+        ∀ (h : (c.getDual? x).isSome), i < i.succAbove ((c.getDual? x).get h))))⟩)
+    else
+      𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ⟨φs.get,
+        (Finset.univ.filter (fun x => j < x ∧ i.succAbove x < i ∧ ((c.getDual? x = none) ∨
+        ∀ (h : (c.getDual? x).isSome), j < ((c.getDual? x).get h))))⟩) := by
+  rw [signInsertSomeCoef_if, stat_signFinset_insert_some_self_snd,
+    stat_signFinset_insert_some_self_fst]
  simp [hφj]

 lemma signInsertSome_mul_filter_contracted_of_lt (φ : 𝓕.States) (φs : List 𝓕.States)
    (c : WickContraction φs.length) (i : Fin φs.length.succ) (k : c.uncontracted)
-    (hk : i.succAbove k < i)
-    (hg : GradingCompliant φs c ∧ 𝓕.statesStatistic φ = 𝓕.statesStatistic φs[k.1]) :
+    (hk : i.succAbove k < i) (hg : GradingCompliant φs c ∧ (𝓕 |>ₛ φ) = 𝓕 |>ₛ φs[k.1]) :
    signInsertSome φ φs c i k *
    𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ⟨φs.get, c.uncontracted.filter (fun x => x ≤ ↑k)⟩)
    = 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ⟨φs.get, Finset.univ.filter (fun x => i.succAbove x < i)⟩) := by
-  rw [signInsertSome, signInsertSomeProd_eq_finset, signInsertSomeCoef_eq_finset]
-  rw [if_neg (by omega), ← map_mul, ← map_mul]
+  rw [signInsertSome, signInsertSomeProd_eq_finset (hφj := hg.2) (hg := hg.1),
+    signInsertSomeCoef_eq_finset (hφj := hg.2), if_neg (by omega), ← map_mul, ← map_mul]
  congr 1
  rw [mul_eq_iff_eq_mul, ofFinset_union_disjoint]
  swap
-  · rw [Finset.disjoint_filter]
+  · /- Disjointness needed for `ofFinset_union_disjoint`. -/
+    rw [Finset.disjoint_filter]
    intro j _ h
    simp only [Nat.succ_eq_add_one, not_lt, not_and, not_forall, not_or, not_le]
    intro h1
    use h1
    omega
-  trans 𝓕 |>ₛ ⟨φs.get, (Finset.filter (fun x =>
-      (↑k < x ∧ i.succAbove x < i ∧ (c.getDual? x = none ∨
-      ∀ (h : (c.getDual? x).isSome = true), ↑k < (c.getDual? x).get h))
-      ∨ ((c.getDual? x).isSome = true ∧
-      ∀ (h : (c.getDual? x).isSome = true), x < ↑k ∧
-      (i.succAbove x < i ∧ i < i.succAbove ((c.getDual? x).get h) ∨
-      ↑k < (c.getDual? x).get h ∧ ¬i.succAbove x < i))) Finset.univ)⟩
-  · congr
-    ext j
-    simp
  rw [ofFinset_union, ← mul_eq_one_iff, ofFinset_union]
  simp only [Nat.succ_eq_add_one, not_lt]
-  apply stat_ofFinset_eq_one_of_gradingCompliant
-  · exact hg.1
-  /- the getDual? is none case-/
-  · intro j hn
+  apply stat_ofFinset_eq_one_of_gradingCompliant _ _ _ hg.1
+  · /- The `c.getDual? i = none` case for `stat_ofFinset_eq_one_of_gradingCompliant`. -/
+    intro j hn
    simp only [uncontracted, Finset.mem_sdiff, Finset.mem_union, Finset.mem_filter, Finset.mem_univ,
      hn, Option.isSome_none, Bool.false_eq_true, IsEmpty.forall_iff, or_self, and_true, or_false,
      true_and, and_self, Finset.mem_inter, not_and, not_lt, Classical.not_imp, not_le, and_imp]
@ -978,8 +963,8 @@ lemma signInsertSome_mul_filter_contracted_of_lt (φ : 𝓕.States) (φs : List
          apply Fin.ne_succAbove i j
          omega
        · exact h1'
-  /- the getDual? is some case-/
-  · intro j hj
+  · /- The `(c.getDual? i).isSome` case for `stat_ofFinset_eq_one_of_gradingCompliant`. -/
+    intro j hj
    have hn : ¬ c.getDual? j = none := by exact Option.isSome_iff_ne_none.mp hj
    simp only [uncontracted, Finset.mem_sdiff, Finset.mem_union, Finset.mem_filter, Finset.mem_univ,
      hn, hj, forall_true_left, false_or, true_and, and_false, false_and, Finset.mem_inter,
@ -1033,28 +1018,24 @@ lemma signInsertSome_mul_filter_contracted_of_lt (φ : 𝓕.States) (φs : List
      · simp_all only [Fin.getElem_fin, ne_eq, not_lt, false_and, false_or, or_false, and_self,
        or_true, imp_self]
        omega
-  · exact hg.2
-  · exact hg.2
-  · exact hg.1

 lemma signInsertSome_mul_filter_contracted_of_not_lt (φ : 𝓕.States) (φs : List 𝓕.States)
    (c : WickContraction φs.length) (i : Fin φs.length.succ) (k : c.uncontracted)
-    (hk : ¬ i.succAbove k < i)
-    (hg : GradingCompliant φs c ∧ 𝓕.statesStatistic φ = 𝓕.statesStatistic φs[k.1]) :
+    (hk : ¬ i.succAbove k < i) (hg : GradingCompliant φs c ∧ (𝓕 |>ₛ φ) = 𝓕 |>ₛ φs[k.1]) :
    signInsertSome φ φs c i k *
    𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ⟨φs.get, c.uncontracted.filter (fun x => x < ↑k)⟩)
    = 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ⟨φs.get, Finset.univ.filter (fun x => i.succAbove x < i)⟩) := by
  have hik : i.succAbove ↑k ≠ i := by exact Fin.succAbove_ne i ↑k
-  rw [signInsertSome, signInsertSomeProd_eq_finset, signInsertSomeCoef_eq_finset]
-  rw [if_pos (by omega), ← map_mul, ← map_mul]
+  rw [signInsertSome, signInsertSomeProd_eq_finset (hφj := hg.2) (hg := hg.1),
+    signInsertSomeCoef_eq_finset (hφj := hg.2), if_pos (by omega), ← map_mul, ← map_mul]
  congr 1
  rw [mul_eq_iff_eq_mul, ofFinset_union, ofFinset_union]
  apply (mul_eq_one_iff _ _).mp
  rw [ofFinset_union]
  simp only [Nat.succ_eq_add_one, not_lt]
-  apply stat_ofFinset_eq_one_of_gradingCompliant
-  · exact hg.1
-  · intro j hj
+  apply stat_ofFinset_eq_one_of_gradingCompliant _ _ _ hg.1
+  · /- The `c.getDual? i = none` case for `stat_ofFinset_eq_one_of_gradingCompliant`. -/
+    intro j hj
    have hijsucc : i.succAbove j ≠ i := by exact Fin.succAbove_ne i j
    simp only [uncontracted, Finset.mem_sdiff, Finset.mem_union, Finset.mem_filter, Finset.mem_univ,
      hj, Option.isSome_none, Bool.false_eq_true, IsEmpty.forall_iff, or_self, and_true, true_and,
@ -1072,7 +1053,8 @@ lemma signInsertSome_mul_filter_contracted_of_not_lt (φ : 𝓕.States) (φs : L
          omega
    simp only [hij, true_and] at h ⊢
    omega
-  · intro j hj
+  · /- The `(c.getDual? i).isSome` case for `stat_ofFinset_eq_one_of_gradingCompliant`. -/
+    intro j hj
    have hn : ¬ c.getDual? j = none := by exact Option.isSome_iff_ne_none.mp hj
    have hijSuc : i.succAbove j ≠ i := by exact Fin.succAbove_ne i j
    have hkneqj : ↑k ≠ j := by
@ -1136,8 +1118,5 @@ lemma signInsertSome_mul_filter_contracted_of_not_lt (φ : 𝓕.States) (φs : L
        simp only [hijn, true_and, hijn', and_false, or_false, or_true, imp_false, not_lt,
          forall_const]
        exact fun h => lt_of_le_of_ne h (Fin.succAbove_ne i ((c.getDual? j).get hj))
-  · exact hg.2
-  · exact hg.2
-  · exact hg.1

 end WickContraction
--- a/HepLean/PerturbationTheory/WickContraction/TimeContract.lean
+++ b/HepLean/PerturbationTheory/WickContraction/TimeContract.lean
@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
 import HepLean.PerturbationTheory.WickContraction.Sign
-import HepLean.PerturbationTheory.Algebras.OperatorAlgebra.TimeContraction
+import HepLean.PerturbationTheory.Algebras.ProtoOperatorAlgebra.TimeContraction
 /-!

 # Time contractions
@ -18,23 +18,17 @@ namespace WickContraction
 variable {n : ℕ} (c : WickContraction n)
 open HepLean.List

-/-!
-
-## Time contract.
-
-/
-
 /-- Given a Wick contraction `c` associated with a list `φs`, the
  product of all time-contractions of pairs of contracted elements in `φs`,
  as a member of the center of `𝓞.A`. -/
-noncomputable def timeContract (𝓞 : 𝓕.OperatorAlgebra) {φs : List 𝓕.States}
+noncomputable def timeContract (𝓞 : 𝓕.ProtoOperatorAlgebra) {φs : List 𝓕.States}
    (c : WickContraction φs.length) :
    Subalgebra.center ℂ 𝓞.A :=
  ∏ (a : c.1), ⟨𝓞.timeContract (φs.get (c.fstFieldOfContract a)) (φs.get (c.sndFieldOfContract a)),
    𝓞.timeContract_mem_center _ _⟩

@[simp]
-lemma timeContract_insertList_none (𝓞 : 𝓕.OperatorAlgebra) (φ : 𝓕.States) (φs : List 𝓕.States)
+lemma timeContract_insertList_none (𝓞 : 𝓕.ProtoOperatorAlgebra) (φ : 𝓕.States) (φs : List 𝓕.States)
    (c : WickContraction φs.length) (i : Fin φs.length.succ) :
    (c.insertList φ φs i none).timeContract 𝓞 = c.timeContract 𝓞 := by
  rw [timeContract, insertList_none_prod_contractions]
@ -42,7 +36,7 @@ lemma timeContract_insertList_none (𝓞 : 𝓕.OperatorAlgebra) (φ : 𝓕.Stat
  ext a
  simp

-lemma timeConract_insertList_some (𝓞 : 𝓕.OperatorAlgebra) (φ : 𝓕.States) (φs : List 𝓕.States)
+lemma timeConract_insertList_some (𝓞 : 𝓕.ProtoOperatorAlgebra) (φ : 𝓕.States) (φs : List 𝓕.States)
    (c : WickContraction φs.length) (i : Fin φs.length.succ) (j : c.uncontracted) :
    (c.insertList φ φs i (some j)).timeContract 𝓞 =
    (if i < i.succAbove j then
@ -62,7 +56,7 @@ lemma timeConract_insertList_some (𝓞 : 𝓕.OperatorAlgebra) (φ : 𝓕.State
 open FieldStatistic

 lemma timeConract_insertList_some_eq_mul_contractStateAtIndex_lt
-    (𝓞 : 𝓕.OperatorAlgebra) (φ : 𝓕.States) (φs : List 𝓕.States)
+    (𝓞 : 𝓕.ProtoOperatorAlgebra) (φ : 𝓕.States) (φs : List 𝓕.States)
    (c : WickContraction φs.length) (i : Fin φs.length.succ) (k : c.uncontracted)
    (ht : 𝓕.timeOrderRel φ φs[k.1]) (hik : i < i.succAbove k) :
    (c.insertList φ φs i (some k)).timeContract 𝓞 =
@ -71,9 +65,9 @@ lemma timeConract_insertList_some_eq_mul_contractStateAtIndex_lt
    ((uncontractedStatesEquiv φs c) (some k)) * c.timeContract 𝓞) := by
  rw [timeConract_insertList_some]
  simp only [Nat.succ_eq_add_one, Fin.getElem_fin, ite_mul, instCommGroup.eq_1,
-    OperatorAlgebra.contractStateAtIndex, uncontractedStatesEquiv, Equiv.optionCongr_apply,
+    ProtoOperatorAlgebra.contractStateAtIndex, uncontractedStatesEquiv, Equiv.optionCongr_apply,
    Equiv.coe_trans, Option.map_some', Function.comp_apply, finCongr_apply, Fin.coe_cast,
-    List.getElem_map, uncontractedList_getElem_uncontractedFinEquiv_symm, List.get_eq_getElem,
+    List.getElem_map, uncontractedList_getElem_uncontractedIndexEquiv_symm, List.get_eq_getElem,
    Algebra.smul_mul_assoc]
  · simp only [hik, ↓reduceIte, MulMemClass.coe_mul]
    rw [𝓞.timeContract_of_timeOrderRel]
@ -83,21 +77,21 @@ lemma timeConract_insertList_some_eq_mul_contractStateAtIndex_lt
    · simp
    simp only [smul_smul]
    congr
-    have h1 : ofList 𝓕.statesStatistic (List.take (↑(c.uncontractedFinEquiv.symm k))
+    have h1 : ofList 𝓕.statesStatistic (List.take (↑(c.uncontractedIndexEquiv.symm k))
        (List.map φs.get c.uncontractedList))
        = (𝓕 |>ₛ ⟨φs.get, (Finset.filter (fun x => x < k) c.uncontracted)⟩) := by
      simp only [ofFinset]
      congr
      rw [← List.map_take]
      congr
-      rw [take_uncontractedFinEquiv_symm]
+      rw [take_uncontractedIndexEquiv_symm]
      rw [filter_uncontractedList]
    rw [h1]
    simp only [exchangeSign_mul_self]
    · exact ht

 lemma timeConract_insertList_some_eq_mul_contractStateAtIndex_not_lt
-    (𝓞 : 𝓕.OperatorAlgebra) (φ : 𝓕.States) (φs : List 𝓕.States)
+    (𝓞 : 𝓕.ProtoOperatorAlgebra) (φ : 𝓕.States) (φs : List 𝓕.States)
    (c : WickContraction φs.length) (i : Fin φs.length.succ) (k : c.uncontracted)
    (ht : ¬ 𝓕.timeOrderRel φs[k.1] φ) (hik : ¬ i < i.succAbove k) :
    (c.insertList φ φs i (some k)).timeContract 𝓞 =
@ -106,22 +100,22 @@ lemma timeConract_insertList_some_eq_mul_contractStateAtIndex_not_lt
    ((uncontractedStatesEquiv φs c) (some k)) * c.timeContract 𝓞) := by
  rw [timeConract_insertList_some]
  simp only [Nat.succ_eq_add_one, Fin.getElem_fin, ite_mul, instCommGroup.eq_1,
-    OperatorAlgebra.contractStateAtIndex, uncontractedStatesEquiv, Equiv.optionCongr_apply,
+    ProtoOperatorAlgebra.contractStateAtIndex, uncontractedStatesEquiv, Equiv.optionCongr_apply,
    Equiv.coe_trans, Option.map_some', Function.comp_apply, finCongr_apply, Fin.coe_cast,
-    List.getElem_map, uncontractedList_getElem_uncontractedFinEquiv_symm, List.get_eq_getElem,
+    List.getElem_map, uncontractedList_getElem_uncontractedIndexEquiv_symm, List.get_eq_getElem,
    Algebra.smul_mul_assoc]
  simp only [hik, ↓reduceIte, MulMemClass.coe_mul]
  rw [𝓞.timeContract_of_not_timeOrderRel, 𝓞.timeContract_of_timeOrderRel]
  simp only [instCommGroup.eq_1, Algebra.smul_mul_assoc, smul_smul]
  congr
-  have h1 : ofList 𝓕.statesStatistic (List.take (↑(c.uncontractedFinEquiv.symm k))
+  have h1 : ofList 𝓕.statesStatistic (List.take (↑(c.uncontractedIndexEquiv.symm k))
      (List.map φs.get c.uncontractedList))
      = (𝓕 |>ₛ ⟨φs.get, (Finset.filter (fun x => x < k) c.uncontracted)⟩) := by
    simp only [ofFinset]
    congr
    rw [← List.map_take]
    congr
-    rw [take_uncontractedFinEquiv_symm, filter_uncontractedList]
+    rw [take_uncontractedIndexEquiv_symm, filter_uncontractedList]
  rw [h1]
  trans 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ⟨φs.get, {k.1}⟩)
  · rw [exchangeSign_symm, ofFinset_singleton]
@ -148,7 +142,7 @@ lemma timeConract_insertList_some_eq_mul_contractStateAtIndex_not_lt
  simp_all only [Fin.getElem_fin, Nat.succ_eq_add_one, not_lt, false_or]
  exact ht

-lemma timeContract_of_not_gradingCompliant (𝓞 : 𝓕.OperatorAlgebra) (φs : List 𝓕.States)
+lemma timeContract_of_not_gradingCompliant (𝓞 : 𝓕.ProtoOperatorAlgebra) (φs : List 𝓕.States)
    (c : WickContraction φs.length) (h : ¬ GradingCompliant φs c) :
    c.timeContract 𝓞 = 0 := by
  rw [timeContract]
@ -159,7 +153,7 @@ lemma timeContract_of_not_gradingCompliant (𝓞 : 𝓕.OperatorAlgebra) (φs :
  simp only [Finset.univ_eq_attach, Finset.mem_attach]
  apply Subtype.eq
  simp only [List.get_eq_getElem, ZeroMemClass.coe_zero]
-  rw [OperatorAlgebra.timeContract_zero_of_diff_grade]
+  rw [ProtoOperatorAlgebra.timeContract_zero_of_diff_grade]
  simp [ha2]

 end WickContraction
--- a/HepLean/PerturbationTheory/WickContraction/UncontractedList.lean
+++ b/HepLean/PerturbationTheory/WickContraction/UncontractedList.lean
@ -219,6 +219,99 @@ lemma uncontractedList_length_eq_card (c : WickContraction n) :
  rw [uncontractedList_eq_sort]
  exact Finset.length_sort fun x1 x2 => x1 ≤ x2

+lemma filter_uncontractedList (c : WickContraction n) (p : Fin n → Prop) [DecidablePred p] :
+    (c.uncontractedList.filter p) = (c.uncontracted.filter p).sort (· ≤ ·) := by
+  have h1 : (c.uncontractedList.filter p).Sorted (· ≤ ·) := by
+    apply List.Sorted.filter
+    exact uncontractedList_sorted c
+  have h2 : (c.uncontractedList.filter p).Nodup := by
+    refine List.Nodup.filter _ ?_
+    exact uncontractedList_nodup c
+  have h3 : (c.uncontractedList.filter p).toFinset = (c.uncontracted.filter p) := by
+    ext a
+    simp only [List.toFinset_filter, decide_eq_true_eq, Finset.mem_filter, List.mem_toFinset,
+      and_congr_left_iff]
+    rw [uncontractedList_mem_iff]
+    simp
+  have hx := (List.toFinset_sort (· ≤ ·) h2).mpr h1
+  rw [← hx, h3]
+
+/-!
+
+## uncontractedIndexEquiv
+
+-/
+
+/-- The equivalence between the positions of `c.uncontractedList` i.e. elements of
+  `Fin (c.uncontractedList).length` and the finite set `c.uncontracted` considered as a finite type.
+-/
+def uncontractedIndexEquiv (c : WickContraction n) :
+    Fin (c.uncontractedList).length ≃ c.uncontracted where
+  toFun i := ⟨c.uncontractedList.get i, c.uncontractedList_get_mem_uncontracted i⟩
+  invFun i := ⟨List.indexOf i.1 c.uncontractedList,
+    List.indexOf_lt_length.mpr ((c.uncontractedList_mem_iff i.1).mpr i.2)⟩
+  left_inv i := by
+    ext
+    exact List.get_indexOf (uncontractedList_nodup c) _
+  right_inv i := by
+    ext
+    simp
+
+@[simp]
+lemma uncontractedList_getElem_uncontractedIndexEquiv_symm (k : c.uncontracted) :
+    c.uncontractedList[(c.uncontractedIndexEquiv.symm k).val] = k := by
+  simp [uncontractedIndexEquiv]
+
+lemma uncontractedIndexEquiv_symm_eq_filter_length (k : c.uncontracted) :
+    (c.uncontractedIndexEquiv.symm k).val =
+    (List.filter (fun i => i < k.val) c.uncontractedList).length := by
+  simp only [uncontractedIndexEquiv, List.get_eq_getElem, Equiv.coe_fn_symm_mk]
+  rw [fin_list_sorted_indexOf_mem]
+  · simp
+  · exact uncontractedList_sorted c
+  · rw [uncontractedList_mem_iff]
+    exact k.2
+
+lemma take_uncontractedIndexEquiv_symm (k : c.uncontracted) :
+    c.uncontractedList.take (c.uncontractedIndexEquiv.symm k).val =
+    c.uncontractedList.filter (fun i => i < k.val) := by
+  have hl := fin_list_sorted_split c.uncontractedList (uncontractedList_sorted c) k.val
+  conv_lhs =>
+    rhs
+    rw [hl]
+  rw [uncontractedIndexEquiv_symm_eq_filter_length]
+  simp
+
+/-!
+
+## uncontractedStatesEquiv
+
+-/
+
+/-- The equivalence between the type `Option c.uncontracted` for `WickContraction φs.length` and
+  `Option (Fin (c.uncontractedList.map φs.get).length)`, that is optional positions of
+  `c.uncontractedList.map φs.get` induced by `uncontractedIndexEquiv`. -/
+def uncontractedStatesEquiv (φs : List 𝓕.States) (c : WickContraction φs.length) :
+    Option c.uncontracted ≃ Option (Fin (c.uncontractedList.map φs.get).length) :=
+  Equiv.optionCongr (c.uncontractedIndexEquiv.symm.trans (finCongr (by simp)))
+
+@[simp]
+lemma uncontractedStatesEquiv_none (φs : List 𝓕.States) (c : WickContraction φs.length) :
+    (uncontractedStatesEquiv φs c).toFun none = none := by
+  simp [uncontractedStatesEquiv]
+
+lemma uncontractedStatesEquiv_list_sum [AddCommMonoid α] (φs : List 𝓕.States)
+    (c : WickContraction φs.length) (f : Option (Fin (c.uncontractedList.map φs.get).length) → α) :
+    ∑ (i : Option (Fin (c.uncontractedList.map φs.get).length)), f i =
+    ∑ (i : Option c.uncontracted), f (c.uncontractedStatesEquiv φs i) := by
+  rw [(c.uncontractedStatesEquiv φs).sum_comp]
+
+/-!
+
+## Uncontracted List for extractEquiv symm none
+
+-/
+
 lemma uncontractedList_succAboveEmb_sorted (c : WickContraction n) (i : Fin n.succ) :
    ((List.map i.succAboveEmb c.uncontractedList)).Sorted (· ≤ ·) := by
  apply fin_list_sorted_succAboveEmb_sorted
@ -230,33 +323,54 @@ lemma uncontractedList_succAboveEmb_nodup (c : WickContraction n) (i : Fin n.suc
  · exact Function.Embedding.injective i.succAboveEmb
  · exact uncontractedList_nodup c

-lemma uncontractedList_succAboveEmb_toFinset (c : WickContraction n) (i : Fin n.succ) :
-    (List.map i.succAboveEmb c.uncontractedList).toFinset =
-    (Finset.map i.succAboveEmb c.uncontracted) := by
-  ext a
-  simp only [Fin.coe_succAboveEmb, List.mem_toFinset, List.mem_map, Finset.mem_map,
-    Fin.succAboveEmb_apply]
-  rw [← c.uncontractedList_toFinset]
-  simp
-
-lemma uncontractedList_succAboveEmb_eq_sort(c : WickContraction n) (i : Fin n.succ) :
-    (List.map i.succAboveEmb c.uncontractedList) =
-    (c.uncontracted.map i.succAboveEmb).sort (· ≤ ·) := by
-  rw [← uncontractedList_succAboveEmb_toFinset]
-  symm
-  refine (List.toFinset_sort (α := Fin n.succ) (· ≤ ·) ?_).mpr ?_
+lemma uncontractedList_succAbove_orderedInsert_nodup (c : WickContraction n) (i : Fin n.succ) :
+    (List.orderedInsert (· ≤ ·) i (List.map i.succAboveEmb c.uncontractedList)).Nodup := by
+  have h1 : (List.orderedInsert (· ≤ ·) i (List.map i.succAboveEmb c.uncontractedList)).Perm
+    (i :: List.map i.succAboveEmb c.uncontractedList) := by
+    exact List.perm_orderedInsert (fun x1 x2 => x1 ≤ x2) i _
+  apply List.Perm.nodup h1.symm
+  simp only [Nat.succ_eq_add_one, List.nodup_cons, List.mem_map, not_exists,
+    not_and]
+  apply And.intro
+  · intro x _
+    exact Fin.succAbove_ne i x
  · exact uncontractedList_succAboveEmb_nodup c i
-  · exact uncontractedList_succAboveEmb_sorted c i

-lemma uncontractedList_succAboveEmb_eraseIdx_sorted (c : WickContraction n) (i : Fin n.succ)
-    (k: ℕ) : ((List.map i.succAboveEmb c.uncontractedList).eraseIdx k).Sorted (· ≤ ·) := by
-  apply HepLean.List.eraseIdx_sorted
+lemma uncontractedList_succAbove_orderedInsert_sorted (c : WickContraction n) (i : Fin n.succ) :
+    (List.orderedInsert (· ≤ ·) i
+      (List.map i.succAboveEmb c.uncontractedList)).Sorted (· ≤ ·) := by
+  refine List.Sorted.orderedInsert i (List.map (⇑i.succAboveEmb) c.uncontractedList) ?_
  exact uncontractedList_succAboveEmb_sorted c i

-lemma uncontractedList_succAboveEmb_eraseIdx_nodup (c : WickContraction n) (i : Fin n.succ) (k: ℕ) :
-    ((List.map i.succAboveEmb c.uncontractedList).eraseIdx k).Nodup := by
-  refine List.Nodup.eraseIdx k ?_
-  exact uncontractedList_succAboveEmb_nodup c i
+lemma uncontractedList_succAbove_orderedInsert_toFinset (c : WickContraction n) (i : Fin n.succ) :
+    (List.orderedInsert (· ≤ ·) i (List.map i.succAboveEmb c.uncontractedList)).toFinset =
+    (Insert.insert i (Finset.map i.succAboveEmb c.uncontracted)) := by
+  ext a
+  simp only [Nat.succ_eq_add_one, Fin.coe_succAboveEmb, List.mem_toFinset, List.mem_orderedInsert,
+    List.mem_map, Finset.mem_insert, Finset.mem_map, Fin.succAboveEmb_apply]
+  rw [← uncontractedList_toFinset]
+  simp
+
+lemma uncontractedList_succAbove_orderedInsert_eq_sort (c : WickContraction n) (i : Fin n.succ) :
+    (List.orderedInsert (· ≤ ·) i (List.map i.succAboveEmb c.uncontractedList)) =
+    (Insert.insert i (Finset.map i.succAboveEmb c.uncontracted)).sort (· ≤ ·) := by
+  rw [← uncontractedList_succAbove_orderedInsert_toFinset]
+  symm
+  refine (List.toFinset_sort (α := Fin n.succ) (· ≤ ·) ?_).mpr ?_
+  · exact uncontractedList_succAbove_orderedInsert_nodup c i
+  · exact uncontractedList_succAbove_orderedInsert_sorted c i
+
+lemma uncontractedList_extractEquiv_symm_none (c : WickContraction n) (i : Fin n.succ) :
+    ((extractEquiv i).symm ⟨c, none⟩).uncontractedList =
+    List.orderedInsert (· ≤ ·) i (List.map i.succAboveEmb c.uncontractedList) := by
+  rw [uncontractedList_eq_sort, extractEquiv_symm_none_uncontracted]
+  rw [uncontractedList_succAbove_orderedInsert_eq_sort]
+
+/-!
+
+## Uncontracted List for extractEquiv symm some
+
+-/

 lemma uncontractedList_succAboveEmb_eraseIdx_toFinset (c : WickContraction n) (i : Fin n.succ)
    (k : ℕ) (hk : k < c.uncontractedList.length) :
@ -286,6 +400,16 @@ lemma uncontractedList_succAboveEmb_eraseIdx_toFinset (c : WickContraction n) (i
    simp_all [uncontractedList]
  exact uncontractedList_succAboveEmb_nodup c i

+lemma uncontractedList_succAboveEmb_eraseIdx_sorted (c : WickContraction n) (i : Fin n.succ)
+    (k: ℕ) : ((List.map i.succAboveEmb c.uncontractedList).eraseIdx k).Sorted (· ≤ ·) := by
+  apply HepLean.List.eraseIdx_sorted
+  exact uncontractedList_succAboveEmb_sorted c i
+
+lemma uncontractedList_succAboveEmb_eraseIdx_nodup (c : WickContraction n) (i : Fin n.succ) (k: ℕ) :
+    ((List.map i.succAboveEmb c.uncontractedList).eraseIdx k).Nodup := by
+  refine List.Nodup.eraseIdx k ?_
+  exact uncontractedList_succAboveEmb_nodup c i
+
 lemma uncontractedList_succAboveEmb_eraseIdx_eq_sort (c : WickContraction n) (i : Fin n.succ)
    (k : ℕ) (hk : k < c.uncontractedList.length) :
    ((List.map i.succAboveEmb c.uncontractedList).eraseIdx k) =
@ -297,48 +421,34 @@ lemma uncontractedList_succAboveEmb_eraseIdx_eq_sort (c : WickContraction n) (i
  · exact uncontractedList_succAboveEmb_eraseIdx_nodup c i k
  · exact uncontractedList_succAboveEmb_eraseIdx_sorted c i k

-lemma uncontractedList_succAbove_orderedInsert_sorted (c : WickContraction n) (i : Fin n.succ) :
-    (List.orderedInsert (· ≤ ·) i
-      (List.map i.succAboveEmb c.uncontractedList)).Sorted (· ≤ ·) := by
-  refine List.Sorted.orderedInsert i (List.map (⇑i.succAboveEmb) c.uncontractedList) ?_
-  exact uncontractedList_succAboveEmb_sorted c i
-
-lemma uncontractedList_succAbove_orderedInsert_nodup (c : WickContraction n) (i : Fin n.succ) :
-    (List.orderedInsert (· ≤ ·) i (List.map i.succAboveEmb c.uncontractedList)).Nodup := by
-  have h1 : (List.orderedInsert (· ≤ ·) i (List.map i.succAboveEmb c.uncontractedList)).Perm
-    (i :: List.map i.succAboveEmb c.uncontractedList) := by
-    exact List.perm_orderedInsert (fun x1 x2 => x1 ≤ x2) i _
-  apply List.Perm.nodup h1.symm
-  simp only [Nat.succ_eq_add_one, List.nodup_cons, List.mem_map, not_exists,
-    not_and]
-  apply And.intro
-  · intro x _
-    exact Fin.succAbove_ne i x
-  · exact uncontractedList_succAboveEmb_nodup c i
-
-lemma uncontractedList_succAbove_orderedInsert_toFinset (c : WickContraction n) (i : Fin n.succ) :
-    (List.orderedInsert (· ≤ ·) i (List.map i.succAboveEmb c.uncontractedList)).toFinset =
-    (Insert.insert i (Finset.map i.succAboveEmb c.uncontracted)) := by
+lemma uncontractedList_extractEquiv_symm_some (c : WickContraction n) (i : Fin n.succ)
+    (k : c.uncontracted) : ((extractEquiv i).symm ⟨c, some k⟩).uncontractedList =
+    ((c.uncontractedList).map i.succAboveEmb).eraseIdx (c.uncontractedIndexEquiv.symm k) := by
+  rw [uncontractedList_eq_sort]
+  rw [uncontractedList_succAboveEmb_eraseIdx_eq_sort]
+  swap
+  simp only [Fin.is_lt]
+  congr
+  simp only [Nat.succ_eq_add_one, extractEquiv, Equiv.coe_fn_symm_mk,
+    uncontractedList_getElem_uncontractedIndexEquiv_symm, Fin.succAboveEmb_apply]
+  rw [insert_some_uncontracted]
  ext a
-  simp only [Nat.succ_eq_add_one, Fin.coe_succAboveEmb, List.mem_toFinset, List.mem_orderedInsert,
-    List.mem_map, Finset.mem_insert, Finset.mem_map, Fin.succAboveEmb_apply]
-  rw [← uncontractedList_toFinset]
  simp

-lemma uncontractedList_succAbove_orderedInsert_eq_sort (c : WickContraction n) (i : Fin n.succ) :
-    (List.orderedInsert (· ≤ ·) i (List.map i.succAboveEmb c.uncontractedList)) =
-    (Insert.insert i (Finset.map i.succAboveEmb c.uncontracted)).sort (· ≤ ·) := by
-  rw [← uncontractedList_succAbove_orderedInsert_toFinset]
-  symm
-  refine (List.toFinset_sort (α := Fin n.succ) (· ≤ ·) ?_).mpr ?_
-  · exact uncontractedList_succAbove_orderedInsert_nodup c i
-  · exact uncontractedList_succAbove_orderedInsert_sorted c i
+lemma uncontractedList_succAboveEmb_toFinset (c : WickContraction n) (i : Fin n.succ) :
+    (List.map i.succAboveEmb c.uncontractedList).toFinset =
+    (Finset.map i.succAboveEmb c.uncontracted) := by
+  ext a
+  simp only [Fin.coe_succAboveEmb, List.mem_toFinset, List.mem_map, Finset.mem_map,
+    Fin.succAboveEmb_apply]
+  rw [← c.uncontractedList_toFinset]
+  simp

-lemma uncontractedList_extractEquiv_symm_none (c : WickContraction n) (i : Fin n.succ) :
-    ((extractEquiv i).symm ⟨c, none⟩).uncontractedList =
-    List.orderedInsert (· ≤ ·) i (List.map i.succAboveEmb c.uncontractedList) := by
-  rw [uncontractedList_eq_sort, extractEquiv_symm_none_uncontracted]
-  rw [uncontractedList_succAbove_orderedInsert_eq_sort]
+/-!
+
+## uncontractedListOrderPos
+
+-/

 /-- Given a Wick contraction `c : WickContraction n` and a `Fin n.succ`, the number of elements
  of `c.uncontractedList` which are less then `i`.
@ -383,108 +493,18 @@ lemma orderedInsert_succAboveEmb_uncontractedList_eq_insertIdx (c : WickContract
    (List.orderedInsert (· ≤ ·) i (List.map i.succAboveEmb c.uncontractedList)) =
    (List.map i.succAboveEmb c.uncontractedList).insertIdx (uncontractedListOrderPos c i) i := by
  rw [orderedInsert_eq_insertIdx_of_fin_list_sorted]
-  swap
-  exact uncontractedList_succAboveEmb_sorted c i
-  congr 1
-  simp only [Nat.succ_eq_add_one, Fin.val_fin_lt, Fin.coe_succAboveEmb, uncontractedListOrderPos]
-  rw [List.filter_map]
-  simp only [List.length_map]
-  congr
-  funext x
-  simp only [Function.comp_apply, Fin.succAbove, decide_eq_decide]
-  split
-  simp only [Fin.lt_def, Fin.coe_castSucc]
-  rename_i h
-  simp_all only [Fin.lt_def, Fin.coe_castSucc, not_lt, Fin.val_succ]
-  omega
-
-/-- The equivalence between the positions of `c.uncontractedList` i.e. elements of
-  `Fin (c.uncontractedList).length` and the finite set `c.uncontracted` considered as a finite type.
-/
-def uncontractedFinEquiv (c : WickContraction n) :
-    Fin (c.uncontractedList).length ≃ c.uncontracted where
-  toFun i := ⟨c.uncontractedList.get i, c.uncontractedList_get_mem_uncontracted i⟩
-  invFun i := ⟨List.indexOf i.1 c.uncontractedList,
-    List.indexOf_lt_length.mpr ((c.uncontractedList_mem_iff i.1).mpr i.2)⟩
-  left_inv i := by
-    ext
-    exact List.get_indexOf (uncontractedList_nodup c) _
-  right_inv i := by
-    ext
-    simp
-
-@[simp]
-lemma uncontractedList_getElem_uncontractedFinEquiv_symm (k : c.uncontracted) :
-    c.uncontractedList[(c.uncontractedFinEquiv.symm k).val] = k := by
-  simp [uncontractedFinEquiv]
-
-lemma uncontractedFinEquiv_symm_eq_filter_length (k : c.uncontracted) :
-    (c.uncontractedFinEquiv.symm k).val =
-    (List.filter (fun i => i < k.val) c.uncontractedList).length := by
-  simp only [uncontractedFinEquiv, List.get_eq_getElem, Equiv.coe_fn_symm_mk]
-  rw [fin_list_sorted_indexOf_mem]
-  · simp
-  · exact uncontractedList_sorted c
-  · rw [uncontractedList_mem_iff]
-    exact k.2
-
-lemma take_uncontractedFinEquiv_symm (k : c.uncontracted) :
-    c.uncontractedList.take (c.uncontractedFinEquiv.symm k).val =
-    c.uncontractedList.filter (fun i => i < k.val) := by
-  have hl := fin_list_sorted_split c.uncontractedList (uncontractedList_sorted c) k.val
-  conv_lhs =>
-    rhs
-    rw [hl]
-  rw [uncontractedFinEquiv_symm_eq_filter_length]
-  simp
-
-/-- The equivalence between the type `Option c.uncontracted` for `WickContraction φs.length` and
-  `Option (Fin (c.uncontractedList.map φs.get).length)`, that is optional positions of
-  `c.uncontractedList.map φs.get` induced by `uncontractedFinEquiv`. -/
-def uncontractedStatesEquiv (φs : List 𝓕.States) (c : WickContraction φs.length) :
-    Option c.uncontracted ≃ Option (Fin (c.uncontractedList.map φs.get).length) :=
-  Equiv.optionCongr (c.uncontractedFinEquiv.symm.trans (finCongr (by simp)))
-
-@[simp]
-lemma uncontractedStatesEquiv_none (φs : List 𝓕.States) (c : WickContraction φs.length) :
-    (uncontractedStatesEquiv φs c).toFun none = none := by
-  simp [uncontractedStatesEquiv]
-
-lemma uncontractedStatesEquiv_list_sum [AddCommMonoid α] (φs : List 𝓕.States)
-    (c : WickContraction φs.length) (f : Option (Fin (c.uncontractedList.map φs.get).length) → α) :
-    ∑ (i : Option (Fin (c.uncontractedList.map φs.get).length)), f i =
-    ∑ (i : Option c.uncontracted), f (c.uncontractedStatesEquiv φs i) := by
-  rw [(c.uncontractedStatesEquiv φs).sum_comp]
-
-lemma uncontractedList_extractEquiv_symm_some (c : WickContraction n) (i : Fin n.succ)
-    (k : c.uncontracted) : ((extractEquiv i).symm ⟨c, some k⟩).uncontractedList =
-    ((c.uncontractedList).map i.succAboveEmb).eraseIdx (c.uncontractedFinEquiv.symm k) := by
-  rw [uncontractedList_eq_sort]
-  rw [uncontractedList_succAboveEmb_eraseIdx_eq_sort]
-  swap
-  simp only [Fin.is_lt]
-  congr
-  simp only [Nat.succ_eq_add_one, extractEquiv, Equiv.coe_fn_symm_mk,
-    uncontractedList_getElem_uncontractedFinEquiv_symm, Fin.succAboveEmb_apply]
-  rw [insert_some_uncontracted]
-  ext a
-  simp
-
-lemma filter_uncontractedList (c : WickContraction n) (p : Fin n → Prop) [DecidablePred p] :
-    (c.uncontractedList.filter p) = (c.uncontracted.filter p).sort (· ≤ ·) := by
-  have h1 : (c.uncontractedList.filter p).Sorted (· ≤ ·) := by
-    apply List.Sorted.filter
-    exact uncontractedList_sorted c
-  have h2 : (c.uncontractedList.filter p).Nodup := by
-    refine List.Nodup.filter _ ?_
-    exact uncontractedList_nodup c
-  have h3 : (c.uncontractedList.filter p).toFinset = (c.uncontracted.filter p) := by
-    ext a
-    simp only [List.toFinset_filter, decide_eq_true_eq, Finset.mem_filter, List.mem_toFinset,
-      and_congr_left_iff]
-    rw [uncontractedList_mem_iff]
-    simp
-  have hx := (List.toFinset_sort (· ≤ ·) h2).mpr h1
-  rw [← hx, h3]
+  · congr 1
+    simp only [Nat.succ_eq_add_one, Fin.val_fin_lt, Fin.coe_succAboveEmb, uncontractedListOrderPos]
+    rw [List.filter_map]
+    simp only [List.length_map]
+    congr
+    funext x
+    simp only [Function.comp_apply, Fin.succAbove, decide_eq_decide]
+    split
+    · simp only [Fin.lt_def, Fin.coe_castSucc]
+    · rename_i h
+      simp_all only [Fin.lt_def, Fin.coe_castSucc, not_lt, Fin.val_succ]
+      omega
+  · exact uncontractedList_succAboveEmb_sorted c i

 end WickContraction
--- a/HepLean/PerturbationTheory/WicksTheorem.lean
+++ b/HepLean/PerturbationTheory/WicksTheorem.lean
@ -16,10 +16,10 @@ Wick's theorem is related to Isserlis' theorem in mathematics.
 -/

 namespace FieldSpecification
-variable {𝓕 : FieldSpecification} {𝓞 : 𝓕.OperatorAlgebra}
+variable {𝓕 : FieldSpecification} {𝓞 : 𝓕.ProtoOperatorAlgebra}
 open CrAnAlgebra
 open StateAlgebra
-open OperatorAlgebra
+open ProtoOperatorAlgebra
 open HepLean.List
 open WickContraction
 open FieldStatistic
@ -192,7 +192,7 @@ lemma sign_timeContract_normalOrder_insertList_some (φ : 𝓕.States) (φs : Li
      simp only [Nat.succ_eq_add_one, Fin.getElem_fin, ite_mul, Algebra.smul_mul_assoc,
        instCommGroup.eq_1, contractStateAtIndex, uncontractedStatesEquiv, Equiv.optionCongr_apply,
        Equiv.coe_trans, Option.map_some', Function.comp_apply, finCongr_apply, Fin.coe_cast,
-        List.getElem_map, uncontractedList_getElem_uncontractedFinEquiv_symm, List.get_eq_getElem]
+        List.getElem_map, uncontractedList_getElem_uncontractedIndexEquiv_symm, List.get_eq_getElem]
      by_cases h1 : i < i.succAbove ↑k
      · simp only [h1, ↓reduceIte, MulMemClass.coe_mul]
        rw [timeContract_zero_of_diff_grade]