refactor: Change notation for normal order

2025-01-27 12:19:21 +00:00 · 2025-01-27 12:19:21 +00:00 · 835c47dbf8
commit 835c47dbf8
parent ec2e1e7df9
7 changed files with 144 additions and 108 deletions
--- a/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/NormTimeOrder.lean
+++ b/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/NormTimeOrder.lean
@ -0,0 +1,47 @@
+/-
+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.TimeOrder
+import HepLean.PerturbationTheory.Algebras.CrAnAlgebra.SuperCommute
+import HepLean.PerturbationTheory.Koszul.KoszulSign
+/-!
+
+# Norm-time Ordering in the CrAnAlgebra
+
+-/
+
+namespace FieldSpecification
+variable {𝓕 : FieldSpecification}
+open FieldStatistic
+
+namespace CrAnAlgebra
+
+noncomputable section
+open HepLean.List
+
+/-!
+
+## Norm-time order
+
+-/
+
+/-- The normal-time ordering on `CrAnAlgebra`. -/
+def normTimeOrder : CrAnAlgebra 𝓕 →ₗ[ℂ] CrAnAlgebra 𝓕 :=
+  Basis.constr ofCrAnListBasis ℂ fun φs =>
+  normTimeOrderSign φs • ofCrAnList (normTimeOrderList φs)
+
+@[inherit_doc normTimeOrder]
+scoped[FieldSpecification.CrAnAlgebra] notation "𝓣𝓝ᶠ(" a ")" => normTimeOrder a
+
+lemma normTimeOrder_ofCrAnList (φs : List 𝓕.CrAnStates) :
+    𝓣𝓝ᶠ(ofCrAnList φs) = normTimeOrderSign φs • ofCrAnList (normTimeOrderList φs) := by
+  rw [← ofListBasis_eq_ofList]
+  simp only [normTimeOrder, Basis.constr_basis]
+
+end
+
+end CrAnAlgebra
+
+end FieldSpecification
--- a/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/NormalOrder.lean
+++ b/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/NormalOrder.lean
@ -37,14 +37,14 @@ def normalOrder : CrAnAlgebra 𝓕 →ₗ[ℂ] CrAnAlgebra 𝓕 :=
  normalOrderSign φs • ofCrAnList (normalOrderList φs)

@[inherit_doc normalOrder]
-scoped[FieldSpecification.CrAnAlgebra] notation "𝓝(" a ")" => normalOrder a
+scoped[FieldSpecification.CrAnAlgebra] notation "𝓝ᶠ(" a ")" => normalOrder a

 lemma normalOrder_ofCrAnList (φs : List 𝓕.CrAnStates) :
-    𝓝(ofCrAnList φs) = normalOrderSign φs • ofCrAnList (normalOrderList φs) := by
+    𝓝ᶠ(ofCrAnList φs) = normalOrderSign φs • ofCrAnList (normalOrderList φs) := by
  rw [← ofListBasis_eq_ofList, normalOrder, Basis.constr_basis]

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

@ -60,13 +60,13 @@ lemma normalOrder_one : normalOrder (𝓕 := 𝓕) 1 = 1 := by

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

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

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

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

 lemma normalOrder_crPart_mul (φ : 𝓕.States) (a : CrAnAlgebra 𝓕) :
-    𝓝(crPart φ * a) =
-    crPart φ * 𝓝(a) := by
+    𝓝ᶠ(crPart φ * a) =
+    crPart φ * 𝓝ᶠ(a) := by
  match φ with
  | .inAsymp φ =>
    rw [crPart]
@ -105,8 +105,8 @@ lemma normalOrder_crPart_mul (φ : 𝓕.States) (a : CrAnAlgebra 𝓕) :
  | .outAsymp φ => simp

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

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

 lemma normalOrder_swap_anPart_crPart (φ φ' : 𝓕.States) (a b : CrAnAlgebra 𝓕) :
-    𝓝(a * (anPart φ) * (crPart φ') * b) =
-    𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') • 𝓝(a * (crPart φ') *
+    𝓝ᶠ(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
+    𝓝ᶠ(a * superCommute
      (crPart φ) (anPart φ') * b) = 0 := by
  match φ, φ' with
  | _, .inAsymp φ' => simp
@ -243,7 +243,7 @@ lemma normalOrder_superCommute_crPart_anPart (φ φ' : 𝓕.States) (a b : CrAnA
    exact normalOrder_superCommute_create_annihilate _ _ rfl rfl ..

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

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

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

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

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

 lemma normalOrder_ofState_mul_ofState (φ φ' : 𝓕.States) :
-    𝓝(ofState φ * ofState φ') =
+    𝓝ᶠ(ofState φ * ofState φ') =
    crPart φ * crPart φ' +
    𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') •
    (crPart φ' * anPart φ) +
@ -328,7 +328,7 @@ 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) :
-    (𝓝(ofCrAnList φs * [ofCrAnState φc, ofCrAnState φc']ₛca * ofCrAnList φs')) =
+    (𝓝ᶠ(ofCrAnList φs * [ofCrAnState φc, ofCrAnState φc']ₛca * ofCrAnList φs')) =
      normalOrderSign (φs ++ φc' :: φc :: φs') •
    (ofCrAnList (createFilter φs) * [ofCrAnState φc, ofCrAnState φc']ₛca *
      ofCrAnList (createFilter φs') * ofCrAnList (annihilateFilter (φs ++ φs'))) := by
@ -389,7 +389,7 @@ lemma normalOrder_superCommute_ofCrAnList_annihilate_annihilate_ofCrAnList
    (hφa : 𝓕 |>ᶜ φa = CreateAnnihilate.annihilate)
    (hφa' : 𝓕 |>ᶜ φa' = CreateAnnihilate.annihilate)
    (φs φs' : List 𝓕.CrAnStates) :
-    𝓝(ofCrAnList φs * [ofCrAnState φa, ofCrAnState φa']ₛca * ofCrAnList φs') =
+    𝓝ᶠ(ofCrAnList φs * [ofCrAnState φa, ofCrAnState φa']ₛca * ofCrAnList φs') =
      normalOrderSign (φs ++ φa' :: φa :: φs') •
    (ofCrAnList (createFilter (φs ++ φs'))
      * ofCrAnList (annihilateFilter φs) * [ofCrAnState φa, ofCrAnState φa']ₛca
@ -459,16 +459,16 @@ lemma normalOrder_superCommute_ofCrAnList_annihilate_annihilate_ofCrAnList
 -/

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

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

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

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

 lemma anPart_mul_normalOrder_ofStateList_eq_superCommute (φ : 𝓕.States)
    (φs' : List 𝓕.States) :
-    anPart φ * 𝓝(ofStateList φs') =
-    𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φs') • 𝓝(ofStateList φs' * anPart φ)
-    + [anPart φ, 𝓝(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/TimeOrder.lean
+++ b/HepLean/PerturbationTheory/Algebras/CrAnAlgebra/TimeOrder.lean
@ -52,7 +52,6 @@ lemma timeOrder_ofStateList (φs : List 𝓕.States) :
  rw [ofStateList_sum, sum_crAnSections_timeOrder]
  rfl

-
 lemma timeOrder_ofStateList_nil : timeOrder (𝓕 := 𝓕) (ofStateList []) = 1 := by
  rw [timeOrder_ofStateList]
  simp [timeOrderSign, Wick.koszulSign, timeOrderList]
@ -149,16 +148,6 @@ lemma timeOrder_eq_maxTimeField_mul_finset (φ : 𝓕.States) (φs : List 𝓕.S
        (Finset.filter (fun x => (maxTimeFieldPosFin φ φs).succAbove x < maxTimeFieldPosFin φ φs)
          Finset.univ)

-
-/-!
-
-## 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
--- a/HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/NormalOrder.lean
+++ b/HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/NormalOrder.lean
@ -33,7 +33,7 @@ is zero.

 lemma ι_normalOrder_superCommute_ofCrAnList_ofCrAnList_eq_zero
    (φa φa' : 𝓕.CrAnStates) (φs φs' : List 𝓕.CrAnStates) :
-    ι 𝓝(ofCrAnList φs * [ofCrAnState φa, ofCrAnState φa']ₛca * ofCrAnList φs') = 0 := by
+    ι 𝓝ᶠ(ofCrAnList φs * [ofCrAnState φa, ofCrAnState φa']ₛca * ofCrAnList φs') = 0 := by
  rcases CreateAnnihilate.eq_create_or_annihilate (𝓕 |>ᶜ φa) with hφa | hφa
  <;> rcases CreateAnnihilate.eq_create_or_annihilate (𝓕 |>ᶜ φa') with hφa' | hφa'
  · rw [normalOrder_superCommute_ofCrAnList_create_create_ofCrAnList φa φa' hφa hφa' φs φs']
@ -52,7 +52,7 @@ lemma ι_normalOrder_superCommute_ofCrAnList_ofCrAnList_eq_zero

 lemma ι_normalOrder_superCommute_ofCrAnList_eq_zero
    (φa φa' : 𝓕.CrAnStates) (φs : List 𝓕.CrAnStates)
-    (a : 𝓕.CrAnAlgebra) : ι 𝓝(ofCrAnList φs * [ofCrAnState φa, ofCrAnState φa']ₛca * a) = 0 := by
+    (a : 𝓕.CrAnAlgebra) : ι 𝓝ᶠ(ofCrAnList φs * [ofCrAnState φa, ofCrAnState φa']ₛca * a) = 0 := by
  have hf : ι.toLinearMap ∘ₗ normalOrder ∘ₗ
      mulLinearMap (ofCrAnList φs * [ofCrAnState φa, ofCrAnState φa']ₛca) = 0 := by
    apply ofCrAnListBasis.ext
@ -67,7 +67,7 @@ lemma ι_normalOrder_superCommute_ofCrAnList_eq_zero

 lemma ι_normalOrder_superCommute_ofCrAnState_eq_zero_mul (φa φa' : 𝓕.CrAnStates)
    (a b : 𝓕.CrAnAlgebra) :
-    ι 𝓝(a * [ofCrAnState φa, ofCrAnState φa']ₛca * b) = 0 := by
+    ι 𝓝ᶠ(a * [ofCrAnState φa, ofCrAnState φa']ₛca * b) = 0 := by
  rw [mul_assoc]
  change (ι.toLinearMap ∘ₗ normalOrder ∘ₗ mulLinearMap.flip
    ([ofCrAnState φa, ofCrAnState φa']ₛca * b)) a = 0
@ -86,7 +86,7 @@ lemma ι_normalOrder_superCommute_ofCrAnState_eq_zero_mul (φa φa' : 𝓕.CrAnS
 lemma ι_normalOrder_superCommute_ofCrAnState_ofCrAnList_eq_zero_mul (φa : 𝓕.CrAnStates)
    (φs : List 𝓕.CrAnStates)
    (a b : 𝓕.CrAnAlgebra) :
-    ι 𝓝(a * [ofCrAnState φa, ofCrAnList φs]ₛca * b) = 0 := by
+    ι 𝓝ᶠ(a * [ofCrAnState φa, ofCrAnList φs]ₛca * b) = 0 := by
  rw [← ofCrAnList_singleton, superCommute_ofCrAnList_ofCrAnList_eq_sum]
  rw [Finset.mul_sum, Finset.sum_mul]
  rw [map_sum, map_sum]
@ -98,7 +98,7 @@ lemma ι_normalOrder_superCommute_ofCrAnState_ofCrAnList_eq_zero_mul (φa : 𝓕

 lemma ι_normalOrder_superCommute_ofCrAnList_ofCrAnState_eq_zero_mul (φa : 𝓕.CrAnStates)
    (φs : List 𝓕.CrAnStates) (a b : 𝓕.CrAnAlgebra) :
-    ι 𝓝(a * [ofCrAnList φs, ofCrAnState φa]ₛca * b) = 0 := by
+    ι 𝓝ᶠ(a * [ofCrAnList φs, ofCrAnState φa]ₛca * b) = 0 := by
  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]
@ -107,7 +107,7 @@ lemma ι_normalOrder_superCommute_ofCrAnList_ofCrAnState_eq_zero_mul (φa : 𝓕

 lemma ι_normalOrder_superCommute_ofCrAnList_ofCrAnList_eq_zero_mul
    (φs φs' : List 𝓕.CrAnStates) (a b : 𝓕.CrAnAlgebra) :
-    ι 𝓝(a * [ofCrAnList φs, ofCrAnList φs']ₛca * b) = 0 := by
+    ι 𝓝ᶠ(a * [ofCrAnList φs, ofCrAnList φs']ₛca * b) = 0 := by
  rw [superCommute_ofCrAnList_ofCrAnList_eq_sum, Finset.mul_sum, Finset.sum_mul]
  rw [map_sum, map_sum]
  apply Fintype.sum_eq_zero
@ -119,7 +119,7 @@ lemma ι_normalOrder_superCommute_ofCrAnList_ofCrAnList_eq_zero_mul
 lemma ι_normalOrder_superCommute_ofCrAnList_eq_zero_mul
    (φs : List 𝓕.CrAnStates)
    (a b c : 𝓕.CrAnAlgebra) :
-    ι 𝓝(a * [ofCrAnList φs, c]ₛca * b) = 0 := by
+    ι 𝓝ᶠ(a * [ofCrAnList φs, c]ₛca * b) = 0 := by
  change (ι.toLinearMap ∘ₗ normalOrder ∘ₗ
    mulLinearMap.flip b ∘ₗ mulLinearMap a ∘ₗ superCommute (ofCrAnList φs)) c = 0
  have hf : (ι.toLinearMap ∘ₗ normalOrder ∘ₗ
@ -135,7 +135,7 @@ lemma ι_normalOrder_superCommute_ofCrAnList_eq_zero_mul

@[simp]
 lemma ι_normalOrder_superCommute_eq_zero_mul
-    (a b c d : 𝓕.CrAnAlgebra) : ι 𝓝(a * [d, c]ₛca * b) = 0 := by
+    (a b c d : 𝓕.CrAnAlgebra) : ι 𝓝ᶠ(a * [d, c]ₛca * b) = 0 := by
  change (ι.toLinearMap ∘ₗ normalOrder ∘ₗ
    mulLinearMap.flip b ∘ₗ mulLinearMap a ∘ₗ superCommute.flip c) d = 0
  have hf : (ι.toLinearMap ∘ₗ normalOrder ∘ₗ
@ -151,25 +151,25 @@ lemma ι_normalOrder_superCommute_eq_zero_mul

@[simp]
 lemma ι_normalOrder_superCommute_eq_zero_mul_right (b c d : 𝓕.CrAnAlgebra) :
-    ι 𝓝([d, c]ₛca * b) = 0 := by
+    ι 𝓝ᶠ([d, c]ₛca * b) = 0 := by
  rw [← ι_normalOrder_superCommute_eq_zero_mul 1 b c d]
  simp

@[simp]
 lemma ι_normalOrder_superCommute_eq_zero_mul_left (a c d : 𝓕.CrAnAlgebra) :
-    ι 𝓝(a * [d, c]ₛca) = 0 := by
+    ι 𝓝ᶠ(a * [d, c]ₛca) = 0 := by
  rw [← ι_normalOrder_superCommute_eq_zero_mul a 1 c d]
  simp

@[simp]
 lemma ι_normalOrder_superCommute_eq_zero_mul_mul_right (a b1 b2 c d: 𝓕.CrAnAlgebra) :
-    ι 𝓝(a * [d, c]ₛca * b1 * b2) = 0 := by
+    ι 𝓝ᶠ(a * [d, c]ₛca * b1 * b2) = 0 := by
  rw [← ι_normalOrder_superCommute_eq_zero_mul a (b1 * b2) c d]
  congr 2
  noncomm_ring

@[simp]
-lemma ι_normalOrder_superCommute_eq_zero (c d : 𝓕.CrAnAlgebra) : ι 𝓝([d, c]ₛca) = 0 := by
+lemma ι_normalOrder_superCommute_eq_zero (c d : 𝓕.CrAnAlgebra) : ι 𝓝ᶠ([d, c]ₛca) = 0 := by
  rw [← ι_normalOrder_superCommute_eq_zero_mul 1 1 c d]
  simp

@ -180,9 +180,9 @@ lemma ι_normalOrder_superCommute_eq_zero (c d : 𝓕.CrAnAlgebra) : ι 𝓝([d,
 -/

 lemma ι_normalOrder_zero_of_mem_ideal (a : 𝓕.CrAnAlgebra)
-    (h : a ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet) : ι 𝓝(a) = 0 := by
+    (h : a ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet) : ι 𝓝ᶠ(a) = 0 := by
  rw [TwoSidedIdeal.mem_span_iff_mem_addSubgroup_closure] at h
-  let p {k : Set 𝓕.CrAnAlgebra} (a : CrAnAlgebra 𝓕) (h : a ∈ AddSubgroup.closure k) := ι 𝓝(a) = 0
+  let p {k : Set 𝓕.CrAnAlgebra} (a : CrAnAlgebra 𝓕) (h : a ∈ AddSubgroup.closure k) := ι 𝓝ᶠ(a) = 0
  change p a h
  apply AddSubgroup.closure_induction
  · intro x hx
@ -212,7 +212,7 @@ lemma ι_normalOrder_zero_of_mem_ideal (a : 𝓕.CrAnAlgebra)
    simp [p]

 lemma ι_normalOrder_eq_of_equiv (a b : 𝓕.CrAnAlgebra) (h : a ≈ b) :
-    ι 𝓝(a) = ι 𝓝(b) := by
+    ι 𝓝ᶠ(a) = ι 𝓝ᶠ(b) := by
  rw [equiv_iff_sub_mem_ideal] at h
  rw [LinearMap.sub_mem_ker_iff.mp]
  simp only [LinearMap.mem_ker, ← map_sub]
--- a/HepLean/PerturbationTheory/Algebras/ProtoOperatorAlgebra/NormalOrder.lean
+++ b/HepLean/PerturbationTheory/Algebras/ProtoOperatorAlgebra/NormalOrder.lean
@ -31,7 +31,7 @@ The main result of this section is
 lemma crAnF_normalOrder_superCommute_ofCrAnList_create_create_ofCrAnList
    (φc φc' : 𝓕.CrAnStates) (hφc : 𝓕 |>ᶜ φc = CreateAnnihilate.create)
    (hφc' : 𝓕 |>ᶜ φc' = CreateAnnihilate.create) (φs φs' : List 𝓕.CrAnStates) :
-    𝓞.crAnF (𝓝(ofCrAnList φs * [ofCrAnState φc, ofCrAnState φc']ₛca * ofCrAnList φs')) = 0 := by
+    𝓞.crAnF (𝓝ᶠ(ofCrAnList φs * [ofCrAnState φc, ofCrAnState φc']ₛca * ofCrAnList φs')) = 0 := by
  rw [normalOrder_superCommute_ofCrAnList_create_create_ofCrAnList φc φc' hφc hφc' φs φs']
  rw [map_smul, map_mul, map_mul, map_mul, 𝓞.superCommute_create_create φc φc' hφc hφc']
  simp
@ -39,7 +39,7 @@ lemma crAnF_normalOrder_superCommute_ofCrAnList_create_create_ofCrAnList
 lemma crAnF_normalOrder_superCommute_ofCrAnList_annihilate_annihilate_ofCrAnList
    (φa φa' : 𝓕.CrAnStates) (hφa : 𝓕 |>ᶜ φa = CreateAnnihilate.annihilate)
    (hφa' : 𝓕 |>ᶜ φa' = CreateAnnihilate.annihilate) (φs φs' : List 𝓕.CrAnStates) :
-    𝓞.crAnF (𝓝(ofCrAnList φs * [ofCrAnState φa, ofCrAnState φa']ₛca * ofCrAnList φs')) = 0 := by
+    𝓞.crAnF (𝓝ᶠ(ofCrAnList φs * [ofCrAnState φa, ofCrAnState φa']ₛca * ofCrAnList φs')) = 0 := by
  rw [normalOrder_superCommute_ofCrAnList_annihilate_annihilate_ofCrAnList φa φa' hφa hφa' φs φs']
  rw [map_smul, map_mul, map_mul, map_mul, 𝓞.superCommute_annihilate_annihilate φa φa' hφa hφa']
  simp
@ -300,16 +300,16 @@ lemma crAnF_ofCrAnState_superCommute_normalOrder_ofStateList_eq_sum (φ : 𝓕.C

 /--
 Within a proto-operator algebra we have that
-`[anPart φ, 𝓝(φs)] = ∑ i, sᵢ • [anPart φ, φᵢ]ₛca * 𝓝(φ₀…φᵢ₋₁φᵢ₊₁…φₙ)`
+`[anPart φ, 𝓝ᶠ(φs)] = ∑ i, sᵢ • [anPart φ, φᵢ]ₛca * 𝓝ᶠ(φ₀…φᵢ₋₁φᵢ₊₁…φₙ)`
 where `sᵢ` is the exchange sign for `φ` and `φ₀…φᵢ₋₁`.

 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 φ, 𝓝(φs)]ₛca) =
+    𝓞.crAnF ([anPart φ, 𝓝ᶠ(φs)]ₛca) =
    ∑ n : Fin φs.length, 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ (φs.take n)) •
-    𝓞.crAnF ([anPart φ, ofState φs[n]]ₛca) * 𝓞.crAnF 𝓝(φs.eraseIdx n) := by
+    𝓞.crAnF ([anPart φ, ofState φs[n]]ₛca) * 𝓞.crAnF 𝓝ᶠ(φs.eraseIdx n) := by
  match φ with
  | .inAsymp φ =>
    simp
@ -329,7 +329,7 @@ lemma crAnF_anPart_superCommute_normalOrder_ofStateList_eq_sum (φ : 𝓕.States
 -/
 /--
 Within a proto-operator algebra we have that
-`anPart φ * 𝓝(φ₀φ₁…φₙ) = 𝓝((anPart φ)φ₀φ₁…φₙ) + [anpart φ, 𝓝(φ₀φ₁…φₙ)]ₛca`.
+`anPart φ * 𝓝ᶠ(φ₀φ₁…φₙ) = 𝓝ᶠ((anPart φ)φ₀φ₁…φₙ) + [anpart φ, 𝓝ᶠ(φ₀φ₁…φₙ)]ₛca`.
 -/
 lemma crAnF_anPart_mul_normalOrder_ofStatesList_eq_superCommute (φ : 𝓕.States)
    (φ' : List 𝓕.States) :
@ -343,12 +343,12 @@ lemma crAnF_anPart_mul_normalOrder_ofStatesList_eq_superCommute (φ : 𝓕.State

 /--
 Within a proto-operator algebra we have that
-`φ * 𝓝(φ₀φ₁…φₙ) = 𝓝(φφ₀φ₁…φₙ) + [anpart φ, 𝓝(φ₀φ₁…φₙ)]ₛca`.
+`φ * 𝓝ᶠ(φ₀φ₁…φₙ) = 𝓝ᶠ(φφ₀φ₁…φₙ) + [anpart φ, 𝓝ᶠ(φ₀φ₁…φₙ)]ₛca`.
 -/
 lemma crAnF_ofState_mul_normalOrder_ofStatesList_eq_superCommute (φ : 𝓕.States)
-    (φs : List 𝓕.States) : 𝓞.crAnF (ofState φ * 𝓝(φs)) =
+    (φs : List 𝓕.States) : 𝓞.crAnF (ofState φ * 𝓝ᶠ(φs)) =
    𝓞.crAnF (normalOrder (ofState φ * ofStateList φs)) +
-    𝓞.crAnF ([anPart φ, 𝓝(φ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]
--- a/HepLean/PerturbationTheory/Algebras/ProtoOperatorAlgebra/TimeContraction.lean
+++ b/HepLean/PerturbationTheory/Algebras/ProtoOperatorAlgebra/TimeContraction.lean
@ -28,11 +28,11 @@ 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 (𝓣ᶠ(ofState φ * ofState ψ) - 𝓝(ofState φ * ofState ψ))
+  𝓞.crAnF (𝓣ᶠ(ofState φ * ofState ψ) - 𝓝ᶠ(ofState φ * ofState ψ))

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

 lemma timeContract_of_timeOrderRel (φ ψ : 𝓕.States) (h : timeOrderRel φ ψ) :
    𝓞.timeContract φ ψ = 𝓞.crAnF ([anPart φ, ofState ψ]ₛca) := by
--- a/HepLean/PerturbationTheory/WicksTheorem.lean
+++ b/HepLean/PerturbationTheory/WicksTheorem.lean
@ -32,18 +32,18 @@ open FieldStatistic

 /--
 Let `c` be a Wick Contraction for `φs := φ₀φ₁…φₙ`.
-We have (roughly) `𝓝([φsΛ ↩Λ φ i none]ᵘᶜ) = s • 𝓝(φ :: [φsΛ]ᵘᶜ)`
+We have (roughly) `𝓝ᶠ([φsΛ ↩Λ φ i none]ᵘᶜ) = s • 𝓝ᶠ(φ :: [φsΛ]ᵘᶜ)`
 Where `s` is the exchange sign for `φ` and the uncontracted fields in `φ₀φ₁…φᵢ₋₁`.
 -/
 lemma normalOrder_uncontracted_none (φ : 𝓕.States) (φs : List 𝓕.States)
    (i : Fin φs.length.succ) (φsΛ : WickContraction φs.length) :
-    𝓞.crAnF (𝓝([φsΛ ↩Λ φ i none]ᵘᶜ))
+    𝓞.crAnF (𝓝ᶠ([φsΛ ↩Λ φ i none]ᵘᶜ))
    = 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ⟨φs.get, φsΛ.uncontracted.filter (fun x => i.succAbove x < i)⟩) •
-    𝓞.crAnF 𝓝(φ :: [φsΛ]ᵘᶜ) := by
+    𝓞.crAnF 𝓝ᶠ(φ :: [φsΛ]ᵘᶜ) := by
  simp only [Nat.succ_eq_add_one, instCommGroup.eq_1]
  rw [crAnF_ofState_normalOrder_insert φ [φsΛ]ᵘᶜ
    ⟨(φsΛ.uncontractedListOrderPos i), by simp [uncontractedListGet]⟩, smul_smul]
-  trans (1 : ℂ) • 𝓞.crAnF (𝓝(ofStateList [φsΛ ↩Λ φ i none]ᵘᶜ))
+  trans (1 : ℂ) • 𝓞.crAnF (𝓝ᶠ(ofStateList [φsΛ ↩Λ φ i none]ᵘᶜ))
  · simp
  congr 1
  simp only [instCommGroup.eq_1, uncontractedListGet]
@ -107,8 +107,8 @@ where `k'` is the position in `c.uncontractedList` corresponding to `k`.
 -/
 lemma normalOrder_uncontracted_some (φ : 𝓕.States) (φs : List 𝓕.States)
    (i : Fin φs.length.succ) (φsΛ : WickContraction φs.length) (k : φsΛ.uncontracted) :
-    𝓞.crAnF 𝓝([φsΛ ↩Λ φ i (some k)]ᵘᶜ)
-    = 𝓞.crAnF 𝓝((optionEraseZ [φsΛ]ᵘᶜ φ ((uncontractedStatesEquiv φs φsΛ) k))) := by
+    𝓞.crAnF 𝓝ᶠ([φsΛ ↩Λ φ i (some k)]ᵘᶜ)
+    = 𝓞.crAnF 𝓝ᶠ((optionEraseZ [φsΛ]ᵘᶜ φ ((uncontractedStatesEquiv φs φsΛ) k))) := by
  simp only [Nat.succ_eq_add_one, insertAndContract, optionEraseZ, uncontractedStatesEquiv,
    Equiv.optionCongr_apply, Equiv.coe_trans, Option.map_some', Function.comp_apply, finCongr_apply,
    Fin.coe_cast, uncontractedListGet]
@ -127,24 +127,24 @@ lemma normalOrder_uncontracted_some (φ : 𝓕.States) (φs : List 𝓕.States)

 remark wick_term_terminology := "
  Let `φsΛ` be a Wick contraction. We informally call the term
-  `(φsΛ.sign • φsΛ.timeContract 𝓞) * 𝓞.crAnF 𝓝([φsΛ]ᵘᶜ)` the Wick term
+  `(φsΛ.sign • φsΛ.timeContract 𝓞) * 𝓞.crAnF 𝓝ᶠ([φsΛ]ᵘᶜ)` the Wick term
  associated with `φsΛ`. We do not make this a fully-fledge definition, as
  in most cases we want to consider slight modifications of this term."

 /--
 Let `φsΛ` be a Wick Contraction for `φs = φ₀φ₁…φₙ`. Then the wick-term of ` (φsΛ ↩Λ φ i none)`

-```(φsΛ ↩Λ φ i none).sign • (φsΛ ↩Λ φ i none).timeContract 𝓞 * 𝓞.crAnF 𝓝([φsΛ ↩Λ φ i none]ᵘᶜ)```
+```(φsΛ ↩Λ φ i none).sign • (φsΛ ↩Λ φ i none).timeContract 𝓞 * 𝓞.crAnF 𝓝ᶠ([φsΛ ↩Λ φ i none]ᵘᶜ)```

 is equal to

-`s • (φsΛ.sign • φsΛ.timeContract 𝓞 * 𝓞.crAnF 𝓝(φ :: [φsΛ]ᵘᶜ))`
+`s • (φsΛ.sign • φsΛ.timeContract 𝓞 * 𝓞.crAnF 𝓝ᶠ(φ :: [φsΛ]ᵘᶜ))`

 where `s` is the exchange sign of `φ` and the uncontracted fields in `φ₀φ₁…φᵢ₋₁`.

 The proof of this result relies primarily on:
- `normalOrder_uncontracted_none` which replaces `𝓝([φsΛ ↩Λ φ i none]ᵘᶜ)` with
-  `𝓝(φ :: [φsΛ]ᵘᶜ)` up to a sign.
+- `normalOrder_uncontracted_none` which replaces `𝓝ᶠ([φsΛ ↩Λ φ i none]ᵘᶜ)` with
+  `𝓝ᶠ(φ :: [φsΛ]ᵘᶜ)` up to a sign.
 - `timeContract_insertAndContract_none` which replaces `(φsΛ ↩Λ φ i none).timeContract 𝓞` with
  `φsΛ.timeContract 𝓞`.
 - `sign_insert_none` and `signInsertNone_eq_filterset` which are used to take account of
@ -153,9 +153,9 @@ The proof of this result relies primarily on:
 lemma wick_term_none_eq_wick_term_cons (φ : 𝓕.States) (φs : List 𝓕.States)
    (i : Fin φs.length.succ) (φsΛ : WickContraction φs.length) :
    (φsΛ ↩Λ φ i none).sign • (φsΛ ↩Λ φ i none).timeContract 𝓞
-    * 𝓞.crAnF 𝓝([φsΛ ↩Λ φ i none]ᵘᶜ) =
+    * 𝓞.crAnF 𝓝ᶠ([φsΛ ↩Λ φ i none]ᵘᶜ) =
    𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ⟨φs.get, (Finset.univ.filter (fun k => i.succAbove k < i))⟩)
-    • (φsΛ.sign • φsΛ.timeContract 𝓞 * 𝓞.crAnF 𝓝(φ :: [φsΛ]ᵘᶜ)) := by
+    • (φsΛ.sign • φsΛ.timeContract 𝓞 * 𝓞.crAnF 𝓝ᶠ(φ :: [φsΛ]ᵘᶜ)) := by
  by_cases hg : GradingCompliant φs φsΛ
  · rw [normalOrder_uncontracted_none, sign_insert_none]
    simp only [Nat.succ_eq_add_one, timeContract_insertAndContract_none, instCommGroup.eq_1,
@ -203,11 +203,11 @@ lemma wick_term_some_eq_wick_term_optionEraseZ (φ : 𝓕.States) (φs : List
    (hlt : ∀ (k : Fin φs.length), timeOrderRel φ φs[k])
    (hn : ∀ (k : Fin φs.length), i.succAbove k < i → ¬ timeOrderRel φs[k] φ) :
    (φsΛ ↩Λ φ i (some k)).sign • (φsΛ ↩Λ φ i (some k)).timeContract 𝓞
-      * 𝓞.crAnF 𝓝([φsΛ ↩Λ φ i (some k)]ᵘᶜ) =
+      * 𝓞.crAnF 𝓝ᶠ([φsΛ ↩Λ φ i (some k)]ᵘᶜ) =
    𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ⟨φs.get, (Finset.univ.filter (fun x => i.succAbove x < i))⟩)
    • (φsΛ.sign • (𝓞.contractStateAtIndex φ [φsΛ]ᵘᶜ
      ((uncontractedStatesEquiv φs φsΛ) (some k)) * φsΛ.timeContract 𝓞)
-    * 𝓞.crAnF 𝓝((optionEraseZ [φsΛ]ᵘᶜ φ (uncontractedStatesEquiv φs φsΛ k)))) := by
+    * 𝓞.crAnF 𝓝ᶠ((optionEraseZ [φsΛ]ᵘᶜ φ (uncontractedStatesEquiv φs φsΛ k)))) := by
  by_cases hg : GradingCompliant φs φsΛ ∧ (𝓕 |>ₛ φ) = (𝓕 |>ₛ φs[k.1])
  · by_cases hk : i.succAbove k < i
    · rw [WickContraction.timeConract_insertAndContract_some_eq_mul_contractStateAtIndex_not_lt]
@ -263,24 +263,24 @@ lemma wick_term_some_eq_wick_term_optionEraseZ (φ : 𝓕.States) (φs : List

 /--
 Given a Wick contraction `φsΛ` of `φs = φ₀φ₁…φₙ` and an `i`, we have that
-`(φsΛ.sign • φsΛ.timeContract 𝓞) * 𝓞.crAnF (φ * 𝓝([φsΛ]ᵘᶜ))`
+`(φsΛ.sign • φsΛ.timeContract 𝓞) * 𝓞.crAnF (φ * 𝓝ᶠ([φsΛ]ᵘᶜ))`
 is equal to the product of
 - the exchange sign of `φ` and `φ₀φ₁…φᵢ₋₁`,
- the sum of `((φsΛ ↩Λ φ i k).sign • (φsΛ ↩Λ φ i k).timeContract 𝓞) * 𝓞.crAnF 𝓝([φsΛ ↩Λ φ i k]ᵘᶜ)`
+- the sum of `((φsΛ ↩Λ φ i k).sign • (φsΛ ↩Λ φ i k).timeContract 𝓞) * 𝓞.crAnF 𝓝ᶠ([φsΛ ↩Λ φ i k]ᵘᶜ)`
  over all `k` in `Option φsΛ.uncontracted`.

 The proof of this result primarily depends on
- `crAnF_ofState_mul_normalOrder_ofStatesList_eq_sum` to rewrite `𝓞.crAnF (φ * 𝓝([φsΛ]ᵘᶜ))`
+- `crAnF_ofState_mul_normalOrder_ofStatesList_eq_sum` to rewrite `𝓞.crAnF (φ * 𝓝ᶠ([φsΛ]ᵘᶜ))`
 - `wick_term_none_eq_wick_term_cons`
 - `wick_term_some_eq_wick_term_optionEraseZ`
 -/
 lemma wick_term_cons_eq_sum_wick_term (φ : 𝓕.States) (φs : List 𝓕.States) (i : Fin φs.length.succ)
    (φsΛ : WickContraction φs.length) (hlt : ∀ (k : Fin φs.length), timeOrderRel φ φs[k])
    (hn : ∀ (k : Fin φs.length), i.succAbove k < i → ¬timeOrderRel φs[k] φ) :
-    (φsΛ.sign • φsΛ.timeContract 𝓞) * 𝓞.crAnF ((CrAnAlgebra.ofState φ) * 𝓝([φsΛ]ᵘᶜ)) =
+    (φsΛ.sign • φsΛ.timeContract 𝓞) * 𝓞.crAnF ((CrAnAlgebra.ofState φ) * 𝓝ᶠ([φsΛ]ᵘᶜ)) =
    𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ⟨φs.get, (Finset.univ.filter (fun x => i.succAbove x < i))⟩) •
    ∑ (k : Option φsΛ.uncontracted), ((φsΛ ↩Λ φ i k).sign •
-    (φsΛ ↩Λ φ i k).timeContract 𝓞 * 𝓞.crAnF (𝓝([φsΛ ↩Λ φ i k]ᵘᶜ))) := by
+    (φsΛ ↩Λ φ i k).timeContract 𝓞 * 𝓞.crAnF (𝓝ᶠ([φsΛ ↩Λ φ i k]ᵘᶜ))) := by
  rw [crAnF_ofState_mul_normalOrder_ofStatesList_eq_sum, Finset.mul_sum,
    uncontractedStatesEquiv_list_sum, Finset.smul_sum]
  simp only [instCommGroup.eq_1, Nat.succ_eq_add_one]
@ -318,7 +318,7 @@ lemma wick_term_cons_eq_sum_wick_term (φ : 𝓕.States) (φs : List 𝓕.States
 /-- Wick's theorem for the empty list. -/
 lemma wicks_theorem_nil :
    𝓞.crAnF (𝓣ᶠ(ofStateList [])) = ∑ (nilΛ : WickContraction [].length),
-    (nilΛ.sign • nilΛ.timeContract 𝓞) * 𝓞.crAnF 𝓝([nilΛ]ᵘᶜ) := by
+    (nilΛ.sign • nilΛ.timeContract 𝓞) * 𝓞.crAnF 𝓝ᶠ([nilΛ]ᵘᶜ) := by
  rw [timeOrder_ofStateList_nil]
  simp only [map_one, List.length_nil, Algebra.smul_mul_assoc]
  rw [sum_WickContraction_nil, uncontractedListGet, nil_zero_uncontractedList]
@ -329,9 +329,9 @@ lemma wicks_theorem_nil :

 lemma wicks_theorem_congr {φs φs' : List 𝓕.States} (h : φs = φs') :
    ∑ (φsΛ : WickContraction φs.length), (φsΛ.sign • φsΛ.timeContract 𝓞) *
-      𝓞.crAnF 𝓝([φsΛ]ᵘᶜ)
+      𝓞.crAnF 𝓝ᶠ([φsΛ]ᵘᶜ)
    = ∑ (φs'Λ : WickContraction φs'.length), (φs'Λ.sign • φs'Λ.timeContract 𝓞) *
-      𝓞.crAnF 𝓝([φs'Λ]ᵘᶜ) := by
+      𝓞.crAnF 𝓝ᶠ([φs'Λ]ᵘᶜ) := by
  subst h
  simp

@ -352,7 +352,7 @@ remark wicks_theorem_context := "
 - The normal-ordering of the uncontracted fields in `c`.
 -/
 theorem wicks_theorem : (φs : List 𝓕.States) → 𝓞.crAnF (𝓣ᶠ(ofStateList φs)) =
-    ∑ (φsΛ : WickContraction φs.length), (φsΛ.sign • φsΛ.timeContract 𝓞) * 𝓞.crAnF 𝓝([φsΛ]ᵘᶜ)
+    ∑ (φsΛ : WickContraction φs.length), (φsΛ.sign • φsΛ.timeContract 𝓞) * 𝓞.crAnF 𝓝ᶠ([φsΛ]ᵘᶜ)
  | [] => wicks_theorem_nil
  | φ :: φs => by
    have ih := wicks_theorem (eraseMaxTimeField φ φs)
@ -375,7 +375,7 @@ theorem wicks_theorem : (φs : List 𝓕.States) → 𝓞.crAnF (𝓣ᶠ(ofState
      (List.insertIdx (↑(maxTimeFieldPosFin φ φs)) (maxTimeField φ φs) (eraseMaxTimeField φ φs))
      (c ↩Λ (maxTimeField φ φs) (maxTimeFieldPosFin φ φs) k) •
      ↑((c ↩Λ (maxTimeField φ φs) (maxTimeFieldPosFin φ φs) k).timeContract 𝓞) *
-      𝓞.crAnF 𝓝(ofStateList (List.map (List.insertIdx (↑(maxTimeFieldPosFin φ φs))
+      𝓞.crAnF 𝓝ᶠ(ofStateList (List.map (List.insertIdx (↑(maxTimeFieldPosFin φ φs))
      (maxTimeField φ φs) (eraseMaxTimeField φ φs)).get
        (c ↩Λ (maxTimeField φ φs) (maxTimeFieldPosFin φ φs) k).uncontractedList))
    swap