Merge pull request #299 from HEPLean/FieldOpAlgebra

feat: Remove state algebra, add time order CrAnAlgebra
2025-01-27 11:52:04 +00:00 · 2025-01-27 11:52:04 +00:00 · acfd0edcdc
commit acfd0edcdc
parent 0dfb2b725d ec2e1e7df9
20 changed files with 497 additions and 294 deletions
--- a/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/Basic.lean
+++ b/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/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.StateAlgebra.Basic
+import HepLean.PerturbationTheory.FieldSpecification.CrAnStates
 import HepLean.PerturbationTheory.FieldSpecification.CrAnSection
 /-!

@ -43,8 +43,6 @@ abbrev CrAnAlgebra (𝓕 : FieldSpecification) : Type := FreeAlgebra ℂ 𝓕.Cr

 namespace CrAnAlgebra

-open StateAlgebra
-
 /-- Maps a creation and annihlation state to the creation and annihlation free-algebra. -/
 def ofCrAnState (φ : 𝓕.CrAnStates) : CrAnAlgebra 𝓕 :=
  FreeAlgebra.ι ℂ φ
@ -71,15 +69,6 @@ lemma ofCrAnList_singleton (φ : 𝓕.CrAnStates) :
 def ofState (φ : 𝓕.States) : CrAnAlgebra 𝓕 :=
  ∑ (i : 𝓕.statesToCrAnType φ), ofCrAnState ⟨φ, i⟩

-/-- The algebra map from the state free-algebra to the creation and annihlation free-algebra. -/
-def ofStateAlgebra : StateAlgebra 𝓕 →ₐ[ℂ] CrAnAlgebra 𝓕 :=
-  FreeAlgebra.lift ℂ ofState
-
-@[simp]
-lemma ofStateAlgebra_ofState (φ : 𝓕.States) :
-    ofStateAlgebra (StateAlgebra.ofState φ) = ofState φ := by
-  simp [ofStateAlgebra, StateAlgebra.ofState]
-
 /-- Maps a list of states to the creation and annihilation free-algebra by taking
  the product of their sums of creation and annihlation operators.
  Roughly `[φ1, φ2]` gets sent to `(φ1ᶜ+ φ1ᵃ) * (φ2ᶜ+ φ2ᵃ)` etc. -/
@ -102,14 +91,6 @@ lemma ofStateList_append (φs φs' : List 𝓕.States) :
  dsimp only [ofStateList]
  rw [List.map_append, List.prod_append]

-lemma ofStateAlgebra_ofList_eq_ofStateList : (φs : List 𝓕.States) →
-    ofStateAlgebra (ofList φs) = ofStateList φs
-  | [] => by simp [ofStateList]
-  | φ :: φs => by
-    rw [ofStateList_cons, StateAlgebra.ofList_cons, map_mul, ofStateAlgebra_ofState,
-      mul_eq_mul_left_iff]
-    exact .inl (ofStateAlgebra_ofList_eq_ofStateList φs)
-
 lemma ofStateList_sum (φs : List 𝓕.States) :
    ofStateList φs = ∑ (s : CrAnSection φs), ofCrAnList s.1 := by
  induction φs with
@ -132,8 +113,7 @@ lemma ofStateList_sum (φs : List 𝓕.States) :
 /-- The algebra map taking an element of the free-state algbra to
  the part of it in the creation and annihlation free algebra
  spanned by creation operators. -/
-def crPart : 𝓕.StateAlgebra →ₐ[ℂ] 𝓕.CrAnAlgebra :=
-  FreeAlgebra.lift ℂ fun φ =>
+def crPart : 𝓕.States → 𝓕.CrAnAlgebra := fun φ =>
  match φ with
  | States.inAsymp φ => ofCrAnState ⟨States.inAsymp φ, ()⟩
  | States.position φ => ofCrAnState ⟨States.position φ, CreateAnnihilate.create⟩
@ -141,25 +121,24 @@ def crPart : 𝓕.StateAlgebra →ₐ[ℂ] 𝓕.CrAnAlgebra :=

@[simp]
 lemma crPart_negAsymp (φ : 𝓕.IncomingAsymptotic) :
-    crPart (StateAlgebra.ofState (States.inAsymp φ)) = ofCrAnState ⟨States.inAsymp φ, ()⟩ := by
-  simp [crPart, StateAlgebra.ofState]
+    crPart (States.inAsymp φ) = ofCrAnState ⟨States.inAsymp φ, ()⟩ := by
+  simp [crPart]

@[simp]
 lemma crPart_position (φ : 𝓕.PositionStates) :
-    crPart (StateAlgebra.ofState (States.position φ)) =
+    crPart (States.position φ) =
    ofCrAnState ⟨States.position φ, CreateAnnihilate.create⟩ := by
-  simp [crPart, StateAlgebra.ofState]
+  simp [crPart]

@[simp]
 lemma crPart_posAsymp (φ : 𝓕.OutgoingAsymptotic) :
-    crPart (StateAlgebra.ofState (States.outAsymp φ)) = 0 := by
-  simp [crPart, StateAlgebra.ofState]
+    crPart (States.outAsymp φ) = 0 := by
+  simp [crPart]

 /-- The algebra map taking an element of the free-state algbra to
  the part of it in the creation and annihilation free algebra
  spanned by annihilation operators. -/
-def anPart : 𝓕.StateAlgebra →ₐ[ℂ] 𝓕.CrAnAlgebra :=
-  FreeAlgebra.lift ℂ fun φ =>
+def anPart : 𝓕.States → 𝓕.CrAnAlgebra := fun φ =>
  match φ with
  | States.inAsymp _ => 0
  | States.position φ => ofCrAnState ⟨States.position φ, CreateAnnihilate.annihilate⟩
@ -167,22 +146,22 @@ def anPart : 𝓕.StateAlgebra →ₐ[ℂ] 𝓕.CrAnAlgebra :=

@[simp]
 lemma anPart_negAsymp (φ : 𝓕.IncomingAsymptotic) :
-    anPart (StateAlgebra.ofState (States.inAsymp φ)) = 0 := by
-  simp [anPart, StateAlgebra.ofState]
+    anPart (States.inAsymp φ) = 0 := by
+  simp [anPart]

@[simp]
 lemma anPart_position (φ : 𝓕.PositionStates) :
-    anPart (StateAlgebra.ofState (States.position φ)) =
+    anPart (States.position φ) =
    ofCrAnState ⟨States.position φ, CreateAnnihilate.annihilate⟩ := by
-  simp [anPart, StateAlgebra.ofState]
+  simp [anPart]

@[simp]
 lemma anPart_posAsymp (φ : 𝓕.OutgoingAsymptotic) :
-    anPart (StateAlgebra.ofState (States.outAsymp φ)) = ofCrAnState ⟨States.outAsymp φ, ()⟩ := by
-  simp [anPart, StateAlgebra.ofState]
+    anPart (States.outAsymp φ) = ofCrAnState ⟨States.outAsymp φ, ()⟩ := by
+  simp [anPart]

 lemma ofState_eq_crPart_add_anPart (φ : 𝓕.States) :
-    ofState φ = crPart (StateAlgebra.ofState φ) + anPart (StateAlgebra.ofState φ) := by
+    ofState φ = crPart φ + anPart φ := by
  rw [ofState]
  cases φ with
  | inAsymp φ => simp [statesToCrAnType]
--- a/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/NormalOrder.lean
+++ b/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/NormalOrder.lean
@ -93,27 +93,27 @@ lemma normalOrder_mul_annihilate (φ : 𝓕.CrAnStates)
    normalOrder_ofCrAnList_append_annihilate φ hφ]

 lemma normalOrder_crPart_mul (φ : 𝓕.States) (a : CrAnAlgebra 𝓕) :
-    𝓝(crPart (StateAlgebra.ofState φ) * a) =
-    crPart (StateAlgebra.ofState φ) * 𝓝(a) := by
+    𝓝(crPart φ * a) =
+    crPart φ * 𝓝(a) := by
  match φ with
  | .inAsymp φ =>
-    rw [crPart, StateAlgebra.ofState, FreeAlgebra.lift_ι_apply]
+    rw [crPart]
    exact normalOrder_create_mul ⟨States.inAsymp φ, ()⟩ rfl a
  | .position φ =>
-    rw [crPart, StateAlgebra.ofState, FreeAlgebra.lift_ι_apply]
+    rw [crPart]
    exact normalOrder_create_mul _ rfl _
  | .outAsymp φ => simp

 lemma normalOrder_mul_anPart (φ : 𝓕.States) (a : CrAnAlgebra 𝓕) :
-    𝓝(a * anPart (StateAlgebra.ofState φ)) =
-    𝓝(a) * anPart (StateAlgebra.ofState φ) := by
+    𝓝(a * anPart φ) =
+    𝓝(a) * anPart φ := by
  match φ with
  | .inAsymp φ => simp
  | .position φ =>
-    rw [anPart, StateAlgebra.ofState, FreeAlgebra.lift_ι_apply]
+    rw [anPart]
    exact normalOrder_mul_annihilate _ rfl _
  | .outAsymp φ =>
-    rw [anPart, StateAlgebra.ofState, FreeAlgebra.lift_ι_apply]
+    rw [anPart]
    refine normalOrder_mul_annihilate _ rfl _

 /-!
@ -182,9 +182,9 @@ lemma normalOrder_superCommute_annihilate_create (φc φa : 𝓕.CrAnStates)
  exact Or.inr (normalOrder_superCommute_create_annihilate φc φa hφc hφa ..)

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

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

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

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

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

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

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

@[simp]
 lemma normalOrder_anPart_mul_crPart (φ φ' : 𝓕.States) :
-    𝓝(anPart (StateAlgebra.ofState φ) * crPart (StateAlgebra.ofState φ')) =
+    𝓝(anPart φ * crPart φ') =
    𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') •
-    (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 φ')))]
+    (crPart φ' * anPart φ) := by
+  conv_lhs => rw [← one_mul (anPart φ * crPart φ')]
+  conv_lhs => rw [← mul_one (1 * (anPart φ *
+    crPart φ'))]
  rw [← mul_assoc, normalOrder_swap_anPart_crPart]
  simp

 lemma normalOrder_ofState_mul_ofState (φ φ' : 𝓕.States) :
    𝓝(ofState φ * ofState φ') =
-    crPart (StateAlgebra.ofState φ) * crPart (StateAlgebra.ofState φ') +
+    crPart φ * crPart φ' +
    𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') •
-    (crPart (StateAlgebra.ofState φ') * anPart (StateAlgebra.ofState φ)) +
-    crPart (StateAlgebra.ofState φ) * anPart (StateAlgebra.ofState φ') +
-    anPart (StateAlgebra.ofState φ) * anPart (StateAlgebra.ofState φ') := by
+    (crPart φ' * anPart φ) +
+    crPart φ * anPart φ' +
+    anPart φ * anPart φ' := by
  rw [ofState_eq_crPart_add_anPart, ofState_eq_crPart_add_anPart, 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]
@ -497,9 +497,9 @@ lemma ofCrAnState_mul_normalOrder_ofStateList_eq_superCommute (φ : 𝓕.CrAnSta

 lemma anPart_mul_normalOrder_ofStateList_eq_superCommute (φ : 𝓕.States)
    (φs' : List 𝓕.States) :
-    anPart (StateAlgebra.ofState φ) * 𝓝(ofStateList φs') =
-    𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φs') • 𝓝(ofStateList φs' * anPart (StateAlgebra.ofState φ))
-    + [anPart (StateAlgebra.ofState φ), 𝓝(ofStateList φs')]ₛca := by
+    anPart φ * 𝓝(ofStateList φs') =
+    𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φs') • 𝓝(ofStateList φs' * anPart φ)
+    + [anPart φ, 𝓝(ofStateList φs')]ₛca := by
  rw [normalOrder_mul_anPart]
  match φ with
  | .inAsymp φ => simp
--- a/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/SuperCommute.lean
+++ b/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/SuperCommute.lean
@ -14,8 +14,6 @@ variable {𝓕 : FieldSpecification}

 namespace CrAnAlgebra

-open StateAlgebra
-
 /-!

 ## The super commutor on the CrAnAlgebra.
@ -97,9 +95,9 @@ lemma superCommute_ofStateList_ofState (φs : List 𝓕.States) (φ : 𝓕.State
  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
+    [anPart φ, crPart φ']ₛca =
+    anPart φ * crPart φ' -
+    𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') • crPart φ' * anPart φ := by
  match φ, φ' with
  | States.inAsymp φ, _ =>
    simp
@ -126,10 +124,10 @@ lemma superCommute_anPart_crPart (φ φ' : 𝓕.States) :
    simp [crAnStatistics, ← ofCrAnList_append]

 lemma superCommute_crPart_anPart (φ φ' : 𝓕.States) :
-    [crPart (StateAlgebra.ofState φ), anPart (StateAlgebra.ofState φ')]ₛca =
-    crPart (StateAlgebra.ofState φ) * anPart (StateAlgebra.ofState φ') -
+    [crPart φ, anPart φ']ₛca =
+    crPart φ * anPart φ' -
    𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') •
-    anPart (StateAlgebra.ofState φ') * crPart (StateAlgebra.ofState φ) := by
+    anPart φ' * crPart φ := by
    match φ, φ' with
    | States.outAsymp φ, _ =>
    simp only [crPart_posAsymp, map_zero, LinearMap.zero_apply, zero_mul, instCommGroup.eq_1,
@ -155,10 +153,10 @@ lemma superCommute_crPart_anPart (φ φ' : 𝓕.States) :
    simp [crAnStatistics, ← ofCrAnList_append]

 lemma superCommute_crPart_crPart (φ φ' : 𝓕.States) :
-    [crPart (StateAlgebra.ofState φ), crPart (StateAlgebra.ofState φ')]ₛca =
-    crPart (StateAlgebra.ofState φ) * crPart (StateAlgebra.ofState φ') -
+    [crPart φ, crPart φ']ₛca =
+    crPart φ * crPart φ' -
    𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') •
-    crPart (StateAlgebra.ofState φ') * crPart (StateAlgebra.ofState φ) := by
+    crPart φ' * crPart φ := by
  match φ, φ' with
  | States.outAsymp φ, _ =>
  simp only [crPart_posAsymp, map_zero, LinearMap.zero_apply, zero_mul, instCommGroup.eq_1,
@ -183,10 +181,10 @@ lemma superCommute_crPart_crPart (φ φ' : 𝓕.States) :
  simp [crAnStatistics, ← ofCrAnList_append]

 lemma superCommute_anPart_anPart (φ φ' : 𝓕.States) :
-    [anPart (StateAlgebra.ofState φ), anPart (StateAlgebra.ofState φ')]ₛca =
-    anPart (StateAlgebra.ofState φ) * anPart (StateAlgebra.ofState φ') -
+    [anPart φ, anPart φ']ₛca =
+    anPart φ * anPart φ' -
    𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') •
-    anPart (StateAlgebra.ofState φ') * anPart (StateAlgebra.ofState φ) := by
+    anPart φ' * anPart φ := by
  match φ, φ' with
  | States.inAsymp φ, _ =>
    simp
@ -210,9 +208,9 @@ lemma superCommute_anPart_anPart (φ φ' : 𝓕.States) :
    simp [crAnStatistics, ← ofCrAnList_append]

 lemma superCommute_crPart_ofStateList (φ : 𝓕.States) (φs : List 𝓕.States) :
-    [crPart (StateAlgebra.ofState φ), ofStateList φs]ₛca =
-    crPart (StateAlgebra.ofState φ) * ofStateList φs - 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φs) • ofStateList φs *
-    crPart (StateAlgebra.ofState φ) := by
+    [crPart φ, ofStateList φs]ₛca =
+    crPart φ * ofStateList φs - 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φs) • ofStateList φs *
+    crPart φ := by
  match φ with
  | States.inAsymp φ =>
    simp only [crPart_negAsymp, instCommGroup.eq_1, Algebra.smul_mul_assoc]
@ -226,9 +224,9 @@ lemma superCommute_crPart_ofStateList (φ : 𝓕.States) (φs : List 𝓕.States
    simp

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

 lemma superCommute_crPart_ofState (φ φ' : 𝓕.States) :
-    [crPart (StateAlgebra.ofState φ), ofState φ']ₛca =
-    crPart (StateAlgebra.ofState φ) * ofState φ' -
-    𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') • ofState φ' * crPart (StateAlgebra.ofState φ) := by
+    [crPart φ, ofState φ']ₛca =
+    crPart φ * ofState φ' -
+    𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') • ofState φ' * crPart φ := 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
+    [anPart φ, ofState φ']ₛca =
+    anPart φ * ofState φ' -
+    𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') • ofState φ' * anPart φ := by
  rw [← ofStateList_singleton, superCommute_anPart_ofStateList]
  simp

@ -294,31 +292,30 @@ lemma ofStateList_mul_ofState_eq_superCommute (φs : List 𝓕.States) (φ :
  simp

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

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

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

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

--- a/HepLean/PerturbationTheory/Algebras/StateAlgebra/TimeOrder.lean
+++ b/HepLean/PerturbationTheory/Algebras/StateAlgebra/TimeOrder.lean
@ -4,61 +4,80 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
 import HepLean.PerturbationTheory.FieldSpecification.TimeOrder
+import HepLean.PerturbationTheory.Algebras.CrAnAlgebra.SuperCommute
 import HepLean.PerturbationTheory.Koszul.KoszulSign
 /-!

-# Time ordering on the state algebra
+# Time Ordering in the CrAnAlgebra

 -/

 namespace FieldSpecification
 variable {𝓕 : FieldSpecification}
-noncomputable section
-
-namespace StateAlgebra
-
 open FieldStatistic
+
+namespace CrAnAlgebra
+
+noncomputable section
 open HepLean.List
+/-!

-/-- The linear map on the free state algebra defined as the map taking
-  a list of states to the time-ordered list of states multiplied by
-  the sign corresponding to the number of fermionic-fermionic
-  exchanges done in ordering. -/
-def timeOrder : StateAlgebra 𝓕 →ₗ[ℂ] StateAlgebra 𝓕 :=
-  Basis.constr ofListBasis ℂ fun φs =>
-  timeOrderSign φs • ofList (timeOrderList φs)
+## Time order

-lemma timeOrder_ofList (φs : List 𝓕.States) :
-    timeOrder (ofList φs) = timeOrderSign φs • ofList (timeOrderList φs) := by
+-/
+
+/-- Time ordering for the `CrAnAlgebra`. -/
+def timeOrder : CrAnAlgebra 𝓕 →ₗ[ℂ] CrAnAlgebra 𝓕 :=
+  Basis.constr ofCrAnListBasis ℂ fun φs =>
+  crAnTimeOrderSign φs • ofCrAnList (crAnTimeOrderList φs)
+
+
+@[inherit_doc timeOrder]
+scoped[FieldSpecification.CrAnAlgebra] notation "𝓣ᶠ(" a ")" => timeOrder a
+
+lemma timeOrder_ofCrAnList (φs : List 𝓕.CrAnStates) :
+    𝓣ᶠ(ofCrAnList φs) = crAnTimeOrderSign φs • ofCrAnList (crAnTimeOrderList φs) := by
  rw [← ofListBasis_eq_ofList]
  simp only [timeOrder, Basis.constr_basis]

-lemma timeOrder_ofList_nil : timeOrder (𝓕 := 𝓕) (ofList []) = 1 := by
-  rw [timeOrder_ofList]
+lemma timeOrder_ofStateList (φs : List 𝓕.States) :
+    𝓣ᶠ(ofStateList φs) = timeOrderSign φs • ofStateList (timeOrderList φs) := by
+  conv_lhs =>
+    rw [ofStateList_sum, map_sum]
+    enter [2, x]
+    rw [timeOrder_ofCrAnList]
+  simp only [crAnTimeOrderSign_crAnSection]
+  rw [← Finset.smul_sum]
+  congr
+  rw [ofStateList_sum, sum_crAnSections_timeOrder]
+  rfl
+
+
+lemma timeOrder_ofStateList_nil : timeOrder (𝓕 := 𝓕) (ofStateList []) = 1 := by
+  rw [timeOrder_ofStateList]
  simp [timeOrderSign, Wick.koszulSign, timeOrderList]

@[simp]
-lemma timeOrder_ofList_singleton (φ : 𝓕.States) : timeOrder (ofList [φ]) = ofList [φ] := by
-  simp [timeOrder_ofList, timeOrderSign, timeOrderList]
+lemma timeOrder_ofStateList_singleton (φ : 𝓕.States) : 𝓣ᶠ(ofStateList [φ]) = ofStateList [φ] := by
+  simp [timeOrder_ofStateList, timeOrderSign, timeOrderList]

 lemma timeOrder_ofState_ofState_ordered {φ ψ : 𝓕.States} (h : timeOrderRel φ ψ) :
-    timeOrder (ofState φ * ofState ψ) = ofState φ * ofState ψ := by
-  rw [← ofList_singleton, ← ofList_singleton, ← ofList_append, timeOrder_ofList]
+    𝓣ᶠ(ofState φ * ofState ψ) = ofState φ * ofState ψ := by
+  rw [← ofStateList_singleton, ← ofStateList_singleton, ← ofStateList_append, timeOrder_ofStateList]
  simp only [List.singleton_append]
  rw [timeOrderSign_pair_ordered h, timeOrderList_pair_ordered h]
  simp

-lemma timeOrder_ofState_ofState_not_ordered {φ ψ : 𝓕.States} (h :¬ timeOrderRel φ ψ) :
-    timeOrder (ofState φ * ofState ψ) =
-    𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ψ) • ofState ψ * ofState φ := by
-  rw [← ofList_singleton, ← ofList_singleton, ← ofList_append, timeOrder_ofList]
+lemma timeOrder_ofState_ofState_not_ordered {φ ψ : 𝓕.States} (h : ¬ timeOrderRel φ ψ) :
+    𝓣ᶠ(ofState φ * ofState ψ) = 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ψ) • ofState ψ * ofState φ := by
+  rw [← ofStateList_singleton, ← ofStateList_singleton,
+    ← ofStateList_append, timeOrder_ofStateList]
  simp only [List.singleton_append, instCommGroup.eq_1, Algebra.smul_mul_assoc]
  rw [timeOrderSign_pair_not_ordered h, timeOrderList_pair_not_ordered h]
-  simp [← ofList_append]
+  simp [← ofStateList_append]

-lemma timeOrder_ofState_ofState_not_ordered_eq_timeOrder {φ ψ : 𝓕.States} (h :¬ timeOrderRel φ ψ) :
-    timeOrder (ofState φ * ofState ψ) =
-    𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ψ) • timeOrder (ofState ψ * ofState φ) := by
+lemma timeOrder_ofState_ofState_not_ordered_eq_timeOrder {φ ψ : 𝓕.States} (h : ¬ timeOrderRel φ ψ) :
+    𝓣ᶠ(ofState φ * ofState ψ) = 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ψ) • 𝓣ᶠ(ofState ψ * ofState φ) := by
  rw [timeOrder_ofState_ofState_not_ordered h]
  rw [timeOrder_ofState_ofState_ordered]
  simp only [instCommGroup.eq_1, Algebra.smul_mul_assoc]
@ -69,11 +88,11 @@ lemma timeOrder_ofState_ofState_not_ordered_eq_timeOrder {φ ψ : 𝓕.States} (
  where `φᵢ` is the state
  which has maximum time and `s` is the exchange sign of `φᵢ` and `φ₀φ₁…φᵢ₋₁`. -/
 lemma timeOrder_eq_maxTimeField_mul (φ : 𝓕.States) (φs : List 𝓕.States) :
-    timeOrder (ofList (φ :: φs)) =
+    𝓣ᶠ(ofStateList (φ :: φs)) =
    𝓢(𝓕 |>ₛ maxTimeField φ φs, 𝓕 |>ₛ (φ :: φs).take (maxTimeFieldPos φ φs)) •
-    ofState (maxTimeField φ φs) * timeOrder (ofList (eraseMaxTimeField φ φs)) := by
-  rw [timeOrder_ofList, timeOrderList_eq_maxTimeField_timeOrderList]
-  rw [ofList_cons, timeOrder_ofList]
+    ofState (maxTimeField φ φs) * 𝓣ᶠ(ofStateList (eraseMaxTimeField φ φs)) := by
+  rw [timeOrder_ofStateList, timeOrderList_eq_maxTimeField_timeOrderList]
+  rw [ofStateList_cons, timeOrder_ofStateList]
  simp only [instCommGroup.eq_1, Algebra.mul_smul_comm, Algebra.smul_mul_assoc, smul_smul]
  congr
  rw [timerOrderSign_of_eraseMaxTimeField, mul_assoc]
@ -84,10 +103,10 @@ lemma timeOrder_eq_maxTimeField_mul (φ : 𝓕.States) (φs : List 𝓕.States)
  which has maximum time and `s` is the exchange sign of `φᵢ` and `φ₀φ₁…φᵢ₋₁`.
  Here `s` is written using finite sets. -/
 lemma timeOrder_eq_maxTimeField_mul_finset (φ : 𝓕.States) (φs : List 𝓕.States) :
-    timeOrder (ofList (φ :: φs)) = 𝓢(𝓕 |>ₛ maxTimeField φ φs, 𝓕 |>ₛ ⟨(eraseMaxTimeField φ φs).get,
+    𝓣ᶠ(ofStateList (φ :: φs)) = 𝓢(𝓕 |>ₛ maxTimeField φ φs, 𝓕 |>ₛ ⟨(eraseMaxTimeField φ φs).get,
      (Finset.filter (fun x =>
        (maxTimeFieldPosFin φ φs).succAbove x < maxTimeFieldPosFin φ φs) Finset.univ)⟩) •
-    StateAlgebra.ofState (maxTimeField φ φs) * timeOrder (ofList (eraseMaxTimeField φ φs)) := by
+     ofState (maxTimeField φ φs) * 𝓣ᶠ(ofStateList (eraseMaxTimeField φ φs)) := by
  rw [timeOrder_eq_maxTimeField_mul]
  congr 3
  apply FieldStatistic.ofList_perm
@ -130,6 +149,18 @@ lemma timeOrder_eq_maxTimeField_mul_finset (φ : 𝓕.States) (φs : List 𝓕.S
        (Finset.filter (fun x => (maxTimeFieldPosFin φ φs).succAbove x < maxTimeFieldPosFin φ φs)
          Finset.univ)

-end StateAlgebra
+
+/-!
+
+## Norm-time order
+
+-/
+/-- The normal-time ordering on `CrAnAlgebra`. -/
+def normTimeOrder : CrAnAlgebra 𝓕 →ₗ[ℂ] CrAnAlgebra 𝓕 :=
+  Basis.constr ofCrAnListBasis ℂ fun φs =>
+  normTimeOrderSign φs • ofCrAnList (normTimeOrderList φs)
 end
+
+end CrAnAlgebra
+
 end FieldSpecification
--- a/HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/Basic.lean
+++ b/HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/Basic.lean
@ -15,7 +15,6 @@ import Mathlib.Algebra.RingQuot

 namespace FieldSpecification
 open CrAnAlgebra
-open StateAlgebra
 open ProtoOperatorAlgebra
 open HepLean.List
 open WickContraction
@ -43,6 +42,7 @@ abbrev FieldOpAlgebra : Type := (TwoSidedIdeal.span 𝓕.fieldOpIdealSet).ringCo
 namespace FieldOpAlgebra
 variable {𝓕 : FieldSpecification}

+/-- The instance of a setoid on `CrAnAlgebra` from the ideal `TwoSidedIdeal`. -/
 instance : Setoid (CrAnAlgebra 𝓕) := (TwoSidedIdeal.span 𝓕.fieldOpIdealSet).ringCon.toSetoid

 lemma equiv_iff_sub_mem_ideal (x y : CrAnAlgebra 𝓕) :
@ -76,7 +76,7 @@ lemma ι_of_mem_fieldOpIdealSet (x : CrAnAlgebra 𝓕) (hx : x ∈ 𝓕.fieldOpI
  simpa using hx

 lemma ι_superCommute_ofCrAnState_ofCrAnState_mem_center (φ ψ : 𝓕.CrAnStates) :
-    ι [ofCrAnState φ, ofCrAnState ψ]ₛca ∈ Subalgebra.center ℂ (FieldOpAlgebra 𝓕) := by
+    ι [ofCrAnState φ, ofCrAnState ψ]ₛca ∈ Subalgebra.center ℂ 𝓕.FieldOpAlgebra := by
  rw [Subalgebra.mem_center_iff]
  intro b
  obtain ⟨b, rfl⟩ := ι_surjective b
--- a/HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/NormalOrder.lean
+++ b/HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/NormalOrder.lean
@ -12,7 +12,6 @@ import HepLean.PerturbationTheory.Algebras.FieldOpAlgebra.Basic

 namespace FieldSpecification
 open CrAnAlgebra
-open StateAlgebra
 open ProtoOperatorAlgebra
 open HepLean.List
 open WickContraction
--- a/HepLean/PerturbationTheory/Algebras/ProtoOperatorAlgebra/Basic.lean
+++ b/HepLean/PerturbationTheory/Algebras/ProtoOperatorAlgebra/Basic.lean
@ -60,7 +60,7 @@ lemma crAnF_superCommute_ofCrAnState_ofState_mem_center (φ : 𝓕.CrAnStates) (
  exact 𝓞.superCommute_crAn_center φ ⟨ψ, x⟩

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

 lemma crAnF_superCommute_anPart_ofState_diff_grade_zero (φ ψ : 𝓕.States)
    (h : (𝓕 |>ₛ φ) ≠ (𝓕 |>ₛ ψ)) :
-    𝓞.crAnF [anPart (StateAlgebra.ofState φ), ofState ψ]ₛca = 0 := by
+    𝓞.crAnF [anPart φ, ofState ψ]ₛca = 0 := by
  match φ with
  | States.inAsymp _ =>
    simp
@ -105,7 +105,7 @@ lemma crAnF_superCommute_ofState_ofState_mem_center (φ ψ : 𝓕.States) :
  exact crAnF_superCommute_ofCrAnState_ofState_mem_center 𝓞 ⟨φ, x⟩ ψ

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

 lemma crAnF_superCommute_crPart_crPart (φ ψ : 𝓕.States) :
-    𝓞.crAnF [crPart (StateAlgebra.ofState φ), crPart (StateAlgebra.ofState ψ)]ₛca = 0 := by
+    𝓞.crAnF [crPart φ, crPart ψ]ₛca = 0 := by
  match φ, ψ with
  | _, States.outAsymp _ =>
    simp
--- a/HepLean/PerturbationTheory/Algebras/ProtoOperatorAlgebra/NormalOrder.lean
+++ b/HepLean/PerturbationTheory/Algebras/ProtoOperatorAlgebra/NormalOrder.lean
@ -213,9 +213,9 @@ lemma crAnF_normalOrder_ofCrAnState_ofStatesList_swap (φ : 𝓕.CrAnStates)

 lemma crAnF_normalOrder_anPart_ofStatesList_swap (φ : 𝓕.States)
    (φ' : List 𝓕.States) :
-    𝓞.crAnF (normalOrder (anPart (StateAlgebra.ofState φ) * ofStateList φ')) =
+    𝓞.crAnF (normalOrder (anPart φ * ofStateList φ')) =
    𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') •
-    𝓞.crAnF (normalOrder (ofStateList φ' * anPart (StateAlgebra.ofState φ))) := by
+    𝓞.crAnF (normalOrder (ofStateList φ' * anPart φ)) := by
  match φ with
  | .inAsymp φ =>
    simp
@ -229,17 +229,17 @@ lemma crAnF_normalOrder_anPart_ofStatesList_swap (φ : 𝓕.States)
    rfl

 lemma crAnF_normalOrder_ofStatesList_anPart_swap (φ : 𝓕.States) (φ' : List 𝓕.States) :
-    𝓞.crAnF (normalOrder (ofStateList φ' * anPart (StateAlgebra.ofState φ)))
+    𝓞.crAnF (normalOrder (ofStateList φ' * anPart φ))
    = 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') •
-    𝓞.crAnF (normalOrder (anPart (StateAlgebra.ofState φ) * ofStateList φ')) := by
+    𝓞.crAnF (normalOrder (anPart φ * ofStateList φ')) := by
  rw [crAnF_normalOrder_anPart_ofStatesList_swap]
  simp [smul_smul, FieldStatistic.exchangeSign_mul_self]

 lemma crAnF_normalOrder_ofStatesList_mul_anPart_swap (φ : 𝓕.States)
    (φ' : List 𝓕.States) :
-    𝓞.crAnF (normalOrder (ofStateList φ') * anPart (StateAlgebra.ofState φ)) =
+    𝓞.crAnF (normalOrder (ofStateList φ') * anPart φ) =
    𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') •
-    𝓞.crAnF (normalOrder (anPart (StateAlgebra.ofState φ) * ofStateList φ')) := by
+    𝓞.crAnF (normalOrder (anPart φ * ofStateList φ')) := by
  rw [← normalOrder_mul_anPart]
  rw [crAnF_normalOrder_ofStatesList_anPart_swap]

@ -307,9 +307,9 @@ The origin of this result is
 - `superCommute_ofCrAnList_ofCrAnList_eq_sum`
 -/
 lemma crAnF_anPart_superCommute_normalOrder_ofStateList_eq_sum (φ : 𝓕.States) (φs : List 𝓕.States) :
-    𝓞.crAnF ([anPart (StateAlgebra.ofState φ), 𝓝(φs)]ₛca) =
+    𝓞.crAnF ([anPart φ, 𝓝(φs)]ₛca) =
    ∑ n : Fin φs.length, 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ (φs.take n)) •
-    𝓞.crAnF ([anPart (StateAlgebra.ofState φ), ofState φs[n]]ₛca) * 𝓞.crAnF 𝓝(φs.eraseIdx n) := by
+    𝓞.crAnF ([anPart φ, ofState φs[n]]ₛca) * 𝓞.crAnF 𝓝(φs.eraseIdx n) := by
  match φ with
  | .inAsymp φ =>
    simp
@ -333,9 +333,9 @@ Within a proto-operator algebra we have that
 -/
 lemma crAnF_anPart_mul_normalOrder_ofStatesList_eq_superCommute (φ : 𝓕.States)
    (φ' : List 𝓕.States) :
-    𝓞.crAnF (anPart (StateAlgebra.ofState φ) * normalOrder (ofStateList φ')) =
-    𝓞.crAnF (normalOrder (anPart (StateAlgebra.ofState φ) * ofStateList φ')) +
-    𝓞.crAnF ([anPart (StateAlgebra.ofState φ), normalOrder (ofStateList φ')]ₛca) := by
+    𝓞.crAnF (anPart φ * normalOrder (ofStateList φ')) =
+    𝓞.crAnF (normalOrder (anPart φ * ofStateList φ')) +
+    𝓞.crAnF ([anPart φ, normalOrder (ofStateList φ')]ₛca) := by
  rw [anPart_mul_normalOrder_ofStateList_eq_superCommute]
  simp only [instCommGroup.eq_1, map_add, map_smul]
  congr
@ -348,7 +348,7 @@ Within a proto-operator algebra we have that
 lemma crAnF_ofState_mul_normalOrder_ofStatesList_eq_superCommute (φ : 𝓕.States)
    (φs : List 𝓕.States) : 𝓞.crAnF (ofState φ * 𝓝(φs)) =
    𝓞.crAnF (normalOrder (ofState φ * ofStateList φs)) +
-    𝓞.crAnF ([anPart (StateAlgebra.ofState φ), 𝓝(φs)]ₛca) := by
+    𝓞.crAnF ([anPart φ, 𝓝(φs)]ₛca) := by
  conv_lhs => rw [ofState_eq_crPart_add_anPart]
  rw [add_mul, map_add, crAnF_anPart_mul_normalOrder_ofStatesList_eq_superCommute, ← add_assoc,
    ← normalOrder_crPart_mul, ← map_add]
@ -363,7 +363,7 @@ noncomputable def contractStateAtIndex (φ : 𝓕.States) (φs : List 𝓕.State
  match n with
  | none => 1
  | some n => 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ (φs.take n)) •
-    𝓞.crAnF ([anPart (StateAlgebra.ofState φ), ofState φs[n]]ₛca)
+    𝓞.crAnF ([anPart φ, ofState φs[n]]ₛca)

 /--
 Within a proto-operator algebra,
--- a/HepLean/PerturbationTheory/Algebras/ProtoOperatorAlgebra/TimeContraction.lean
+++ b/HepLean/PerturbationTheory/Algebras/ProtoOperatorAlgebra/TimeContraction.lean
@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
 import HepLean.PerturbationTheory.Algebras.ProtoOperatorAlgebra.NormalOrder
-import HepLean.PerturbationTheory.Algebras.StateAlgebra.TimeOrder
+import HepLean.PerturbationTheory.Algebras.CrAnAlgebra.TimeOrder
 /-!

 # Time contractions
@ -28,24 +28,21 @@ open FieldStatistic
  as their time ordering in the state algebra minus their normal ordering in the
  creation and annihlation algebra, both mapped to `𝓞.A`.. -/
 def timeContract (φ ψ : 𝓕.States) : 𝓞.A :=
-  𝓞.crAnF (ofStateAlgebra (StateAlgebra.timeOrder (StateAlgebra.ofState φ * StateAlgebra.ofState ψ))
-  - 𝓝(ofState φ * ofState ψ))
+  𝓞.crAnF (𝓣ᶠ(ofState φ * ofState ψ) - 𝓝(ofState φ * ofState ψ))

 lemma timeContract_eq_smul (φ ψ : 𝓕.States) : 𝓞.timeContract φ ψ =
-    𝓞.crAnF (ofStateAlgebra (StateAlgebra.timeOrder
-    (StateAlgebra.ofState φ * StateAlgebra.ofState ψ))
+    𝓞.crAnF (𝓣ᶠ(ofState φ * ofState ψ)
    + (-1 : ℂ) • 𝓝(ofState φ * ofState ψ)) := by rfl

 lemma timeContract_of_timeOrderRel (φ ψ : 𝓕.States) (h : timeOrderRel φ ψ) :
-    𝓞.timeContract φ ψ = 𝓞.crAnF ([anPart (StateAlgebra.ofState φ), ofState ψ]ₛca) := by
+    𝓞.timeContract φ ψ = 𝓞.crAnF ([anPart φ, ofState ψ]ₛca) := by
  conv_rhs =>
    rw [ofState_eq_crPart_add_anPart]
    rw [map_add, map_add, crAnF_superCommute_anPart_anPart, superCommute_anPart_crPart]
  simp only [timeContract, instCommGroup.eq_1, Algebra.smul_mul_assoc, add_zero]
-  rw [StateAlgebra.timeOrder_ofState_ofState_ordered h]
+  rw [timeOrder_ofState_ofState_ordered h]
  rw [normalOrder_ofState_mul_ofState]
-  rw [map_mul]
-  simp only [ofStateAlgebra_ofState, instCommGroup.eq_1]
+  simp only [instCommGroup.eq_1]
  rw [ofState_eq_crPart_add_anPart, ofState_eq_crPart_add_anPart]
  simp only [mul_add, add_mul]
  abel_nf
@ -56,9 +53,9 @@ lemma timeContract_of_not_timeOrderRel (φ ψ : 𝓕.States) (h : ¬ timeOrderRe
  simp only [Int.reduceNeg, one_smul, map_add]
  rw [map_smul]
  rw [crAnF_normalOrder_ofState_ofState_swap]
-  rw [StateAlgebra.timeOrder_ofState_ofState_not_ordered_eq_timeOrder h]
+  rw [timeOrder_ofState_ofState_not_ordered_eq_timeOrder h]
  rw [timeContract_eq_smul]
-  simp only [FieldStatistic.instCommGroup.eq_1, map_smul, one_smul, map_add, smul_add]
+  simp only [instCommGroup.eq_1, map_smul, map_add, smul_add]
  rw [smul_smul, smul_smul, mul_comm]

 lemma timeContract_mem_center (φ ψ : 𝓕.States) : 𝓞.timeContract φ ψ ∈ Subalgebra.center ℂ 𝓞.A := by
--- a/HepLean/PerturbationTheory/Algebras/StateAlgebra/Basic.lean
+++ b/HepLean/PerturbationTheory/Algebras/StateAlgebra/Basic.lean
@ -1,98 +0,0 @@
-/-
-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.FieldSpecification.CrAnStates
-/-!
-
-# State algebra
-
-From the states associated with a field specification we can form a free algebra
-generated by these states. We call this the state algebra, or the state free-algebra.
-
-The state free-algebra has minimal assumptions, yet can be used to concretely define time-ordering.
-
-In `HepLean.PerturbationTheory.Algebras.CrAnAlgebra.Basic`
-we defined a related free-algebra generated by creation and annihilation states.
-
-/
-
-namespace FieldSpecification
-variable {𝓕 : FieldSpecification}
-
-/-- The state free-algebra.
-  The free algebra generated by `States`,
-  that is a position based states or assymptotic states.
-  As a module `StateAlgebra` is spanned by lists of `States`. -/
-abbrev StateAlgebra (𝓕 : FieldSpecification) : Type := FreeAlgebra ℂ 𝓕.States
-
-namespace StateAlgebra
-
-open FieldStatistic
-
-/-- The element of the states free-algebra generated by a single state. -/
-def ofState (φ : 𝓕.States) : StateAlgebra 𝓕 :=
-  FreeAlgebra.ι ℂ φ
-
-/-- The element of the states free-algebra generated by a list of states. -/
-def ofList (φs : List 𝓕.States) : StateAlgebra 𝓕 :=
-  (List.map ofState φs).prod
-
-@[simp]
-lemma ofList_nil : ofList ([] : List 𝓕.States) = 1 := rfl
-
-lemma ofList_singleton (φ : 𝓕.States) : ofList [φ] = ofState φ := by
-  simp [ofList]
-
-lemma ofList_append (φs ψs : List 𝓕.States) :
-    ofList (φs ++ ψs) = ofList φs * ofList ψs := by
-  rw [ofList, List.map_append, List.prod_append]
-  rfl
-
-lemma ofList_cons (φ : 𝓕.States) (φs : List 𝓕.States) :
-    ofList (φ :: φs) = ofState φ * ofList φs := rfl
-
-/-- The basis of the free state algebra formed by lists of states. -/
-noncomputable def ofListBasis : Basis (List 𝓕.States) ℂ 𝓕.StateAlgebra where
-  repr := FreeAlgebra.equivMonoidAlgebraFreeMonoid.toLinearEquiv
-
-@[simp]
-lemma ofListBasis_eq_ofList (φs : List 𝓕.States) :
-    ofListBasis φs = ofList φs := by
-  simp only [ofListBasis, FreeAlgebra.equivMonoidAlgebraFreeMonoid, MonoidAlgebra.of_apply,
-    Basis.coe_ofRepr, AlgEquiv.toLinearEquiv_symm, AlgEquiv.toLinearEquiv_apply,
-    AlgEquiv.ofAlgHom_symm_apply, ofList]
-  erw [MonoidAlgebra.lift_apply]
-  simp only [zero_smul, Finsupp.sum_single_index, one_smul]
-  rw [@FreeMonoid.lift_apply]
-  simp only [List.prod]
-  match φs with
-  | [] => rfl
-  | φ :: φs =>
-    erw [List.map_cons]
-
-/-!
-
-## The super commutor on the state algebra.
-
-/
-
-/-- The super commutor on the free state algebra. For two bosonic operators
-  or a bosonic and fermionic operator this corresponds to the usual commutator
-  whilst for two fermionic operators this corresponds to the anti-commutator. -/
-noncomputable def superCommute : 𝓕.StateAlgebra →ₗ[ℂ] 𝓕.StateAlgebra →ₗ[ℂ] 𝓕.StateAlgebra :=
-  Basis.constr ofListBasis ℂ fun φs =>
-  Basis.constr ofListBasis ℂ fun φs' =>
-  ofList (φs ++ φs') - 𝓢(𝓕 |>ₛ φs, 𝓕 |>ₛ φs') • ofList (φs' ++ φs)
-
-local notation "⟨" φs "," φs' "⟩ₛ" => superCommute φs φs'
-
-lemma superCommute_ofList (φs φs' : List 𝓕.States) : ⟨ofList φs, ofList φs'⟩ₛ =
-    ofList (φs ++ φs') - 𝓢(𝓕 |>ₛ φs, 𝓕 |>ₛ φs') • ofList (φs' ++ φs) := by
-  rw [← ofListBasis_eq_ofList, ← ofListBasis_eq_ofList]
-  simp only [superCommute, Basis.constr_basis]
-
-end StateAlgebra
-
-end FieldSpecification
--- a/HepLean/PerturbationTheory/CreateAnnihilate.lean
+++ b/HepLean/PerturbationTheory/CreateAnnihilate.lean
@ -67,4 +67,8 @@ lemma sum_eq {M : Type} [AddCommMonoid M] (f : CreateAnnihilate → M) :
  change ∑ i in {create, annihilate}, f i = f create + f annihilate
  simp

+@[simp]
+lemma CreateAnnihilate_card_eq_two : Fintype.card CreateAnnihilate = 2 := by
+  rfl
+
 end CreateAnnihilate
--- a/HepLean/PerturbationTheory/FieldSpecification/Basic.lean
+++ b/HepLean/PerturbationTheory/FieldSpecification/Basic.lean
@ -66,6 +66,11 @@ def statesToField : 𝓕.States → 𝓕.Fields
  | States.position φ => φ.1
  | States.outAsymp φ => φ.1

+/-- The bool on `States` which is true only for position states. -/
+def statesIsPosition : 𝓕.States → Bool
+  | States.position _ => true
+  | _ => false
+
 /-- The statistics associated to a state. -/
 def statesStatistic : 𝓕.States → FieldStatistic := 𝓕.statistics ∘ 𝓕.statesToField

--- a/HepLean/PerturbationTheory/FieldSpecification/CrAnSection.lean
+++ b/HepLean/PerturbationTheory/FieldSpecification/CrAnSection.lean
@ -149,6 +149,44 @@ instance fintype : (φs : List 𝓕.States) → Fintype (CrAnSection φs)
    haveI : Fintype (CrAnSection φs) := fintype φs
    Fintype.ofEquiv _ consEquiv.symm

+@[simp]
+lemma card_nil_eq : Fintype.card (CrAnSection (𝓕 := 𝓕) []) = 1 := by
+  rw [Fintype.ofEquiv_card nilEquiv.symm]
+  simp
+
+lemma card_cons_eq {φ : 𝓕.States} {φs : List 𝓕.States} :
+    Fintype.card (CrAnSection (φ :: φs)) = Fintype.card (𝓕.statesToCrAnType φ) *
+    Fintype.card (CrAnSection φs) := by
+  rw [Fintype.ofEquiv_card consEquiv.symm]
+  simp
+
+lemma card_eq_mul : {φs : List 𝓕.States} → Fintype.card (CrAnSection φs) =
+    2 ^ (List.countP 𝓕.statesIsPosition φs)
+  | [] => by
+    simp
+  | States.position _ :: φs => by
+      simp only [statesIsPosition, List.countP_cons_of_pos]
+      rw [card_cons_eq]
+      rw [card_eq_mul]
+      simp only [statesToCrAnType, CreateAnnihilate.CreateAnnihilate_card_eq_two]
+      ring
+  | States.inAsymp x_ :: φs => by
+      simp only [statesIsPosition, Bool.false_eq_true, not_false_eq_true, List.countP_cons_of_neg]
+      rw [card_cons_eq]
+      rw [card_eq_mul]
+      simp [statesToCrAnType]
+  | States.outAsymp _ :: φs => by
+      simp only [statesIsPosition, Bool.false_eq_true, not_false_eq_true, List.countP_cons_of_neg]
+      rw [card_cons_eq]
+      rw [card_eq_mul]
+      simp [statesToCrAnType]
+
+lemma card_perm_eq {φs φs' : List 𝓕.States} (h : φs.Perm φs') :
+    Fintype.card (CrAnSection φs) = Fintype.card (CrAnSection φs') := by
+  rw [card_eq_mul, card_eq_mul]
+  congr 1
+  exact List.Perm.countP_congr h fun x => congrFun rfl
+
@[simp]
 lemma sum_nil (f : CrAnSection (𝓕 := 𝓕) [] → M) [AddCommMonoid M] :
    ∑ (s : CrAnSection []), f s = f ⟨[], rfl⟩ := by
--- a/HepLean/PerturbationTheory/FieldSpecification/TimeOrder.lean
+++ b/HepLean/PerturbationTheory/FieldSpecification/TimeOrder.lean
@ -4,8 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
 import HepLean.Mathematics.List.InsertionSort
-import HepLean.PerturbationTheory.Algebras.StateAlgebra.Basic
-import HepLean.PerturbationTheory.Koszul.KoszulSign
+import HepLean.PerturbationTheory.FieldSpecification.NormalOrder
 /-!

 # Time ordering of states
@ -15,6 +14,12 @@ import HepLean.PerturbationTheory.Koszul.KoszulSign
 namespace FieldSpecification
 variable {𝓕 : FieldSpecification}

+/-!
+
+## Time ordering for states
+
+-/
+
 /-- The time ordering relation on states. We have that `timeOrderRel φ0 φ1` is true
  if and only if `φ1` has a time less-then or equal to `φ0`, or `φ1` is a negative
  asymptotic state, or `φ0` is a positive asymptotic state. -/
@ -123,6 +128,11 @@ lemma timeOrder_maxTimeField (φ : 𝓕.States) (φs : List 𝓕.States)
 def timeOrderSign (φs : List 𝓕.States) : ℂ :=
  Wick.koszulSign 𝓕.statesStatistic 𝓕.timeOrderRel φs

+@[simp]
+lemma timeOrderSign_nil : timeOrderSign (𝓕 := 𝓕) [] = 1 := by
+  simp only [timeOrderSign]
+  rfl
+
 lemma timeOrderSign_pair_ordered {φ ψ : 𝓕.States} (h : timeOrderRel φ ψ) :
    timeOrderSign [φ, ψ] = 1 := by
  simp only [timeOrderSign, Wick.koszulSign, Wick.koszulSignInsert, mul_one, ite_eq_left_iff,
@ -169,5 +179,253 @@ lemma timeOrderList_eq_maxTimeField_timeOrderList (φ : 𝓕.States) (φs : List
    timeOrderList (φ :: φs) = maxTimeField φ φs :: timeOrderList (eraseMaxTimeField φ φs) := by
  exact insertionSort_eq_insertionSortMin_cons timeOrderRel φ φs

+/-!
+
+## Time ordering for CrAnStates
+
+-/
+
+/-!
+
+## timeOrderRel
+
+-/
+
+/-- The time ordering relation on CrAnStates. -/
+def crAnTimeOrderRel (a b : 𝓕.CrAnStates) : Prop := 𝓕.timeOrderRel a.1 b.1
+
+/-- The relation `crAnTimeOrderRel` is decidable, but not computablly so due to
+  `Real.decidableLE`. -/
+noncomputable instance (φ φ' : 𝓕.CrAnStates) : Decidable (crAnTimeOrderRel φ φ') :=
+  inferInstanceAs (Decidable (𝓕.timeOrderRel φ.1 φ'.1))
+
+/-- Time ordering of `CrAnStates` is total. -/
+instance : IsTotal 𝓕.CrAnStates 𝓕.crAnTimeOrderRel where
+  total a b := IsTotal.total (r := 𝓕.timeOrderRel) a.1 b.1
+
+/-- Time ordering of `CrAnStates` is transitive. -/
+instance : IsTrans 𝓕.CrAnStates 𝓕.crAnTimeOrderRel where
+  trans a b c := IsTrans.trans (r := 𝓕.timeOrderRel) a.1 b.1 c.1
+
+/-- The sign associated with putting a list of `CrAnStates` into time order (with
+  the state of greatest time to the left).
+  We pick up a minus sign for every fermion paired crossed. -/
+def crAnTimeOrderSign (φs : List 𝓕.CrAnStates) : ℂ :=
+  Wick.koszulSign 𝓕.crAnStatistics 𝓕.crAnTimeOrderRel φs
+
+@[simp]
+lemma crAnTimeOrderSign_nil : crAnTimeOrderSign (𝓕 := 𝓕) [] = 1 := by
+  simp only [crAnTimeOrderSign]
+  rfl
+
+/-- Sort a list of `CrAnStates` based on `crAnTimeOrderRel`. -/
+def crAnTimeOrderList (φs : List 𝓕.CrAnStates) : List 𝓕.CrAnStates :=
+  List.insertionSort 𝓕.crAnTimeOrderRel φs
+
+@[simp]
+lemma crAnTimeOrderList_nil : crAnTimeOrderList (𝓕 := 𝓕) [] = [] := by
+  simp [crAnTimeOrderList]
+
+/-!
+
+## Relationship to sections
+-/
+
+lemma koszulSignInsert_crAnTimeOrderRel_crAnSection {φ : 𝓕.States} {ψ : 𝓕.CrAnStates}
+    (h : ψ.1 = φ) : {φs : List 𝓕.States} → (ψs : CrAnSection φs) →
+    Wick.koszulSignInsert 𝓕.crAnStatistics 𝓕.crAnTimeOrderRel ψ ψs.1 =
+    Wick.koszulSignInsert 𝓕.statesStatistic 𝓕.timeOrderRel φ φs
+  | [], ⟨[], h⟩ => by
+    simp [Wick.koszulSignInsert]
+  | φ' :: φs, ⟨ψ' :: ψs, h1⟩ => by
+    simp only [Wick.koszulSignInsert, crAnTimeOrderRel, h]
+    simp only [List.map_cons, List.cons.injEq] at h1
+    have hi := koszulSignInsert_crAnTimeOrderRel_crAnSection h (φs := φs) ⟨ψs, h1.2⟩
+    rw [hi]
+    congr
+    · exact h1.1
+    · simp only [crAnStatistics, crAnStatesToStates, Function.comp_apply]
+      congr
+    · simp only [crAnStatistics, crAnStatesToStates, Function.comp_apply]
+      congr
+      exact h1.1
+
+@[simp]
+lemma crAnTimeOrderSign_crAnSection : {φs : List 𝓕.States} → (ψs : CrAnSection φs) →
+    crAnTimeOrderSign ψs.1 = timeOrderSign φs
+  | [], ⟨[], h⟩ => by
+    simp
+  | φ :: φs, ⟨ψ :: ψs, h⟩ => by
+    simp only [crAnTimeOrderSign, Wick.koszulSign, timeOrderSign]
+    simp only [List.map_cons, List.cons.injEq] at h
+    congr 1
+    · rw [koszulSignInsert_crAnTimeOrderRel_crAnSection h.1 ⟨ψs, h.2⟩]
+    · exact crAnTimeOrderSign_crAnSection ⟨ψs, h.2⟩
+
+lemma orderedInsert_crAnTimeOrderRel_crAnSection {φ : 𝓕.States} {ψ : 𝓕.CrAnStates}
+    (h : ψ.1 = φ) : {φs : List 𝓕.States} → (ψs : CrAnSection φs) →
+    (List.orderedInsert 𝓕.crAnTimeOrderRel ψ ψs.1).map 𝓕.crAnStatesToStates =
+    List.orderedInsert 𝓕.timeOrderRel φ φs
+  | [], ⟨[], _⟩ => by
+    simp only [List.orderedInsert, List.map_cons, List.map_nil, List.cons.injEq, and_true]
+    exact h
+  | φ' :: φs, ⟨ψ' :: ψs, h1⟩ => by
+    simp only [List.orderedInsert, crAnTimeOrderRel, h]
+    simp only [List.map_cons, List.cons.injEq] at h1
+    by_cases hr : timeOrderRel φ φ'
+    · simp only [hr, ↓reduceIte]
+      rw [← h1.1] at hr
+      simp only [crAnStatesToStates] at hr
+      simp only [hr, ↓reduceIte, List.map_cons, List.cons.injEq]
+      exact And.intro h (And.intro h1.1 h1.2)
+    · simp only [hr, ↓reduceIte]
+      rw [← h1.1] at hr
+      simp only [crAnStatesToStates] at hr
+      simp only [hr, ↓reduceIte, List.map_cons, List.cons.injEq]
+      apply And.intro h1.1
+      exact orderedInsert_crAnTimeOrderRel_crAnSection h ⟨ψs, h1.2⟩
+
+lemma crAnTimeOrderList_crAnSection_is_crAnSection : {φs : List 𝓕.States} → (ψs : CrAnSection φs) →
+    (crAnTimeOrderList ψs.1).map 𝓕.crAnStatesToStates = timeOrderList φs
+  | [], ⟨[], h⟩ => by
+    simp
+  | φ :: φs, ⟨ψ :: ψs, h⟩ => by
+    simp only [crAnTimeOrderList, List.insertionSort, timeOrderList]
+    simp only [List.map_cons, List.cons.injEq] at h
+    exact orderedInsert_crAnTimeOrderRel_crAnSection h.1 ⟨(List.insertionSort crAnTimeOrderRel ψs),
+      crAnTimeOrderList_crAnSection_is_crAnSection ⟨ψs, h.2⟩⟩
+
+/-- Time ordering of sections of a list of states. -/
+def crAnSectionTimeOrder (φs : List 𝓕.States) (ψs : CrAnSection φs) :
+    CrAnSection (timeOrderList φs) :=
+  ⟨crAnTimeOrderList ψs.1, crAnTimeOrderList_crAnSection_is_crAnSection ψs⟩
+
+lemma orderedInsert_crAnTimeOrderRel_injective {ψ ψ' : 𝓕.CrAnStates} (h : ψ.1 = ψ'.1) :
+    {φs : List 𝓕.States} → (ψs ψs' : 𝓕.CrAnSection φs) →
+    (ho : List.orderedInsert crAnTimeOrderRel ψ ψs.1 =
+    List.orderedInsert crAnTimeOrderRel ψ' ψs'.1) → ψ = ψ' ∧ ψs = ψs'
+  | [], ⟨[], _⟩, ⟨[], _⟩, h => by
+    simp only [List.orderedInsert, List.cons.injEq, and_true] at h
+    simpa using h
+  | φ :: φs, ⟨ψ1 :: ψs, h1⟩, ⟨ψ1' :: ψs', h1'⟩, ho => by
+    simp only [List.map_cons, List.cons.injEq] at h1 h1'
+    have ih := orderedInsert_crAnTimeOrderRel_injective h ⟨ψs, h1.2⟩ ⟨ψs', h1'.2⟩
+    simp only [List.orderedInsert] at ho
+    by_cases hr : crAnTimeOrderRel ψ ψ1
+    · simp_all only [ite_true]
+      by_cases hr2 : crAnTimeOrderRel ψ' ψ1'
+      · simp_all
+      · simp only [crAnTimeOrderRel] at hr hr2
+        simp_all only
+        rw [crAnStatesToStates] at h1 h1'
+        rw [h1.1] at hr
+        rw [h1'.1] at hr2
+        exact False.elim (hr2 hr)
+    · simp_all only [ite_false]
+      by_cases hr2 : crAnTimeOrderRel ψ' ψ1'
+      · simp only [crAnTimeOrderRel] at hr hr2
+        simp_all only
+        rw [crAnStatesToStates] at h1 h1'
+        rw [h1.1] at hr
+        rw [h1'.1] at hr2
+        exact False.elim (hr hr2)
+      · simp only [hr2, ↓reduceIte, List.cons.injEq] at ho
+        have ih' := ih ho.2
+        simp_all only [and_self, implies_true, not_false_eq_true, true_and]
+        apply Subtype.ext
+        simp only [List.cons.injEq, true_and]
+        rw [Subtype.eq_iff] at ih'
+        exact ih'.2
+
+lemma crAnSectionTimeOrder_injective : {φs : List 𝓕.States} →
+    Function.Injective (𝓕.crAnSectionTimeOrder φs)
+  | [], ⟨[], _⟩, ⟨[], _⟩ => by
+    simp
+  | φ :: φs, ⟨ψ :: ψs, h⟩, ⟨ψ' :: ψs', h'⟩ => by
+    intro h1
+    apply Subtype.ext
+    simp only [List.cons.injEq]
+    simp only [crAnSectionTimeOrder] at h1
+    rw [Subtype.eq_iff] at h1
+    simp only [crAnTimeOrderList, List.insertionSort] at h1
+    simp only [List.map_cons, List.cons.injEq] at h h'
+    rw [crAnStatesToStates] at h h'
+    have hin := orderedInsert_crAnTimeOrderRel_injective (by rw [h.1, h'.1])
+      (𝓕.crAnSectionTimeOrder φs ⟨ψs, h.2⟩)
+      (𝓕.crAnSectionTimeOrder φs ⟨ψs', h'.2⟩) h1
+    apply And.intro hin.1
+    have hl := crAnSectionTimeOrder_injective hin.2
+    rw [Subtype.ext_iff] at hl
+    simpa using hl
+
+lemma crAnSectionTimeOrder_bijective (φs : List 𝓕.States) :
+    Function.Bijective (𝓕.crAnSectionTimeOrder φs) := by
+  rw [Fintype.bijective_iff_injective_and_card]
+  apply And.intro crAnSectionTimeOrder_injective
+  apply CrAnSection.card_perm_eq
+  simp only [timeOrderList]
+  exact List.Perm.symm (List.perm_insertionSort timeOrderRel φs)
+
+lemma sum_crAnSections_timeOrder {φs : List 𝓕.States} [AddCommMonoid M]
+    (f : CrAnSection (timeOrderList φs) → M) : ∑ s, f s = ∑ s, f (𝓕.crAnSectionTimeOrder φs s) := by
+  erw [(Equiv.ofBijective _ (𝓕.crAnSectionTimeOrder_bijective φs)).sum_comp]
+
+/-!
+
+## normTimeOrderRel
+
+-/
+
+/-- The time ordering relation on `CrAnStates` such that if two CrAnStates have the same
+  time, we normal order them. -/
+def normTimeOrderRel (a b : 𝓕.CrAnStates) : Prop :=
+  crAnTimeOrderRel a b ∧ (crAnTimeOrderRel b a → normalOrderRel a b)
+
+/-- The relation `normTimeOrderRel` is decidable, but not computablly so due to
+  `Real.decidableLE`. -/
+noncomputable instance (φ φ' : 𝓕.CrAnStates) : Decidable (normTimeOrderRel φ φ') :=
+  instDecidableAnd
+
+/-- Norm-Time ordering of `CrAnStates` is total. -/
+instance : IsTotal 𝓕.CrAnStates 𝓕.normTimeOrderRel where
+  total a b := by
+    simp only [normTimeOrderRel]
+    match IsTotal.total (r := 𝓕.crAnTimeOrderRel) a b,
+      IsTotal.total (r := 𝓕.normalOrderRel) a b with
+    | Or.inl h1, Or.inl h2 => simp [h1, h2]
+    | Or.inr h1, Or.inl h2 =>
+      simp only [h1, h2, imp_self, and_true, true_and]
+      by_cases hn : crAnTimeOrderRel a b
+      · simp [hn]
+      · simp [hn]
+    | Or.inl h1, Or.inr h2 =>
+      simp only [h1, true_and, h2, imp_self, and_true]
+      by_cases hn : crAnTimeOrderRel b a
+      · simp [hn]
+      · simp [hn]
+    | Or.inr h1, Or.inr h2 => simp [h1, h2]
+
+/-- Norm-Time ordering of `CrAnStates` is transitive. -/
+instance : IsTrans 𝓕.CrAnStates 𝓕.normTimeOrderRel where
+  trans a b c := by
+    intro h1 h2
+    simp_all only [normTimeOrderRel]
+    apply And.intro
+    · exact IsTrans.trans _ _ _ h1.1 h2.1
+    · intro hc
+      refine IsTrans.trans _ _ _ (h1.2 ?_) (h2.2 ?_)
+      · exact IsTrans.trans _ _ _ h2.1 hc
+      · exact IsTrans.trans _ _ _ hc h1.1
+
+/-- The sign associated with putting a list of `CrAnStates` into normal-time order (with
+  the state of greatest time to the left).
+  We pick up a minus sign for every fermion paired crossed. -/
+def normTimeOrderSign (φs : List 𝓕.CrAnStates) : ℂ :=
+  Wick.koszulSign 𝓕.crAnStatistics 𝓕.normTimeOrderRel φs
+
+/-- Sort a list of `CrAnStates` based on `normTimeOrderRel`. -/
+def normTimeOrderList (φs : List 𝓕.CrAnStates) : List 𝓕.CrAnStates :=
+  List.insertionSort 𝓕.normTimeOrderRel φs
+
 end
 end FieldSpecification
--- a/HepLean/PerturbationTheory/WickContraction/Involutions.lean
+++ b/HepLean/PerturbationTheory/WickContraction/Involutions.lean
@ -3,10 +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.WickContraction.Uncontracted
-import HepLean.PerturbationTheory.Algebras.StateAlgebra.TimeOrder
-import HepLean.PerturbationTheory.Algebras.ProtoOperatorAlgebra.TimeContraction
-import HepLean.PerturbationTheory.WickContraction.InsertAndContract
+import HepLean.PerturbationTheory.WickContraction.Basic
 /-!

 # Involution associated with a contraction
--- a/HepLean/PerturbationTheory/WickContraction/IsFull.lean
+++ b/HepLean/PerturbationTheory/WickContraction/IsFull.lean
@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
 import HepLean.Mathematics.Fin.Involutions
+import HepLean.PerturbationTheory.WickContraction.ExtractEquiv
 import HepLean.PerturbationTheory.WickContraction.Involutions
 /-!

--- a/HepLean/PerturbationTheory/WickContraction/TimeContract.lean
+++ b/HepLean/PerturbationTheory/WickContraction/TimeContract.lean
@ -88,7 +88,7 @@ lemma timeConract_insertAndContract_some_eq_mul_contractStateAtIndex_lt
  · simp only [hik, ↓reduceIte, MulMemClass.coe_mul]
    rw [𝓞.timeContract_of_timeOrderRel]
    trans (1 : ℂ) • (𝓞.crAnF ((CrAnAlgebra.superCommute
-      (CrAnAlgebra.anPart (StateAlgebra.ofState φ))) (CrAnAlgebra.ofState φs[k.1])) *
+      (CrAnAlgebra.anPart φ)) (CrAnAlgebra.ofState φs[k.1])) *
      ↑(timeContract 𝓞 φsΛ))
    · simp
    simp only [smul_smul]
--- a/HepLean/PerturbationTheory/WicksTheorem.lean
+++ b/HepLean/PerturbationTheory/WicksTheorem.lean
@ -19,7 +19,6 @@ Wick's theorem is related to Isserlis' theorem in mathematics.
 namespace FieldSpecification
 variable {𝓕 : FieldSpecification} {𝓞 : 𝓕.ProtoOperatorAlgebra}
 open CrAnAlgebra
-open StateAlgebra
 open ProtoOperatorAlgebra
 open HepLean.List
 open WickContraction
@ -318,9 +317,9 @@ lemma wick_term_cons_eq_sum_wick_term (φ : 𝓕.States) (φs : List 𝓕.States

 /-- Wick's theorem for the empty list. -/
 lemma wicks_theorem_nil :
-    𝓞.crAnF (ofStateAlgebra (timeOrder (ofList []))) = ∑ (nilΛ : WickContraction [].length),
+    𝓞.crAnF (𝓣ᶠ(ofStateList [])) = ∑ (nilΛ : WickContraction [].length),
    (nilΛ.sign • nilΛ.timeContract 𝓞) * 𝓞.crAnF 𝓝([nilΛ]ᵘᶜ) := by
-  rw [timeOrder_ofList_nil]
+  rw [timeOrder_ofStateList_nil]
  simp only [map_one, List.length_nil, Algebra.smul_mul_assoc]
  rw [sum_WickContraction_nil, uncontractedListGet, nil_zero_uncontractedList]
  simp only [List.map_nil]
@ -352,12 +351,12 @@ remark wicks_theorem_context := "
 - The product of time-contractions of the contracted pairs of `c`.
 - The normal-ordering of the uncontracted fields in `c`.
 -/
-theorem wicks_theorem : (φs : List 𝓕.States) → 𝓞.crAnF (ofStateAlgebra (timeOrder (ofList φs))) =
+theorem wicks_theorem : (φs : List 𝓕.States) → 𝓞.crAnF (𝓣ᶠ(ofStateList φs)) =
    ∑ (φsΛ : WickContraction φs.length), (φsΛ.sign • φsΛ.timeContract 𝓞) * 𝓞.crAnF 𝓝([φsΛ]ᵘᶜ)
  | [] => wicks_theorem_nil
  | φ :: φs => by
    have ih := wicks_theorem (eraseMaxTimeField φ φs)
-    rw [timeOrder_eq_maxTimeField_mul_finset, map_mul, map_mul, ih, Finset.mul_sum]
+    rw [timeOrder_eq_maxTimeField_mul_finset, map_mul, ih, Finset.mul_sum]
    have h1 : φ :: φs =
        (eraseMaxTimeField φ φs).insertIdx (maxTimeFieldPosFin φ φs) (maxTimeField φ φs) := by
      simp only [eraseMaxTimeField, insertionSortDropMinPos, List.length_cons, Nat.succ_eq_add_one,
@ -369,8 +368,8 @@ theorem wicks_theorem : (φs : List 𝓕.States) → 𝓞.crAnF (ofStateAlgebra
    funext c
    have ht := Subalgebra.mem_center_iff.mp (Subalgebra.smul_mem (Subalgebra.center ℂ 𝓞.A)
      (WickContraction.timeContract 𝓞 c).2 (sign (eraseMaxTimeField φ φs) c))
-    rw [map_smul, map_smul, Algebra.smul_mul_assoc, ← mul_assoc, ht, mul_assoc, ← map_mul]
-    rw [ofStateAlgebra_ofState, wick_term_cons_eq_sum_wick_term (𝓞 := 𝓞)
+    rw [map_smul, Algebra.smul_mul_assoc, ← mul_assoc, ht, mul_assoc, ← map_mul]
+    rw [wick_term_cons_eq_sum_wick_term (𝓞 := 𝓞)
      (maxTimeField φ φs) (eraseMaxTimeField φ φs) (maxTimeFieldPosFin φ φs) c]
    trans (1 : ℂ) • ∑ k : Option { x // x ∈ c.uncontracted }, sign
      (List.insertIdx (↑(maxTimeFieldPosFin φ φs)) (maxTimeField φ φs) (eraseMaxTimeField φ φs))