refactor: Organize supercommute for CrAnAlgebra

2025-01-22 05:51:52 +00:00 · 2025-01-22 05:51:52 +00:00 · 509d536577
commit 509d536577
parent 2fcafb1796
4 changed files with 228 additions and 207 deletions
--- a/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/NormalOrder.lean
+++ b/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/NormalOrder.lean
@ -153,7 +153,7 @@ lemma normalOrder_superCommute_create_annihilate (φc φa : 𝓕.CrAnStates)
    (hφa : 𝓕 |>ᶜ φa = CreateAnnihilate.annihilate)
    (a b : 𝓕.CrAnAlgebra) :
    normalOrder (a * superCommute (ofCrAnState φc) (ofCrAnState φa) * b) = 0 := by
-  rw [superCommute_ofCrAnState]
+  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]
@ -166,7 +166,7 @@ lemma normalOrder_superCommute_annihilate_create (φc φa : 𝓕.CrAnStates)
    (hφa : 𝓕 |>ᶜ φa = CreateAnnihilate.annihilate)
    (a b : 𝓕.CrAnAlgebra) :
    normalOrder (a * superCommute (ofCrAnState φa) (ofCrAnState φc) * b) = 0 := by
-  rw [superCommute_ofCrAnState_symm]
+  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
@ -298,7 +298,7 @@ lemma normalOrder_superCommute_ofCrAnList_create_create_ofCrAnList
      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 +372,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
@ -495,7 +495,7 @@ lemma ofCrAnList_superCommute_normalOrder_ofCrAnList (φs φs' : List 𝓕.CrAnS
    ⟨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)
--- 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,184 @@ 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 +291,18 @@ 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 +310,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 +348,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 +361,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,11 +406,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) →
@ -391,7 +414,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 +423,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/OperatorAlgebra/NormalOrder.lean
+++ b/HepLean/PerturbationTheory/Algebras/OperatorAlgebra/NormalOrder.lean
@ -111,7 +111,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]
@ -189,8 +189,8 @@ lemma crAnF_normalOrder_ofState_ofState_swap (φ φ' : 𝓕.States) :
    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]
+    rw [crPart_mul_crPart_eq_superCommute, crPart_mul_anPart_eq_superCommute,
+      anPart_mul_anPart_eq_superCommute, anPart_mul_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]
--- 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.

 -/