Merge pull request #319 from HEPLean/WickTheoremDoc

refactor: Update Field Specification

HepLean.lean

@@ -136,6 +136,7 @@ import HepLean.PerturbationTheory.FieldOpAlgebra.StaticWickTheorem
 import HepLean.PerturbationTheory.FieldOpAlgebra.SuperCommute
 import HepLean.PerturbationTheory.FieldOpAlgebra.TimeContraction
 import HepLean.PerturbationTheory.FieldOpAlgebra.TimeOrder
+import HepLean.PerturbationTheory.FieldOpAlgebra.Universality
 import HepLean.PerturbationTheory.FieldOpAlgebra.WickTerm
 import HepLean.PerturbationTheory.FieldOpAlgebra.WicksTheorem
 import HepLean.PerturbationTheory.FieldOpAlgebra.WicksTheoremNormal
@@ -148,7 +149,6 @@ import HepLean.PerturbationTheory.FieldOpFreeAlgebra.TimeOrder
 import HepLean.PerturbationTheory.FieldSpecification.Basic
 import HepLean.PerturbationTheory.FieldSpecification.CrAnFieldOp
 import HepLean.PerturbationTheory.FieldSpecification.CrAnSection
-import HepLean.PerturbationTheory.FieldSpecification.Examples
 import HepLean.PerturbationTheory.FieldSpecification.Filters
 import HepLean.PerturbationTheory.FieldSpecification.NormalOrder
 import HepLean.PerturbationTheory.FieldSpecification.TimeOrder

HepLean/PerturbationTheory/CreateAnnihilate.lean

@@ -10,7 +10,9 @@ import Mathlib.Algebra.BigOperators.Group.Finset
 
 -/
 
-/-- The type specifing whether an operator is a creation or annihilation operator. -/
+/-- The type `CreateAnnihilate` is the type containing two elements `create` and `annihilate`.
+  This type is used to specify if an operator is a creation or annihilation operator
+  or the sum thereof or intergral thereover etc. -/
 inductive CreateAnnihilate where
   | create : CreateAnnihilate
   | annihilate : CreateAnnihilate

HepLean/PerturbationTheory/FieldOpAlgebra/Basic.lean

@@ -41,10 +41,7 @@ def fieldOpIdealSet : Set (FieldOpFreeAlgebra 𝓕) :=
 - `[ofCrAnOpF φa, ofCrAnOpF φa']ₛca` for `φa` and `φa'` annihilation operators. I.e two
   annihilation operators always super-commute.
 - `[ofCrAnOpF φ, ofCrAnOpF φ']ₛca` for `φ` and `φ'` field operators with different statistics.
-  I.e. Fermions super-commute with bosons.
-The algebra `𝓕.FieldOpAlgebra` is the most general (in the correct sense) algebra
-satisfying these properties.
--/
+  I.e. Fermions super-commute with bosons. -/
 abbrev FieldOpAlgebra : Type := (TwoSidedIdeal.span 𝓕.fieldOpIdealSet).ringCon.Quotient
 
 namespace FieldOpAlgebra
@@ -58,7 +55,23 @@ lemma equiv_iff_sub_mem_ideal (x y : FieldOpFreeAlgebra 𝓕) :
   rw [← TwoSidedIdeal.rel_iff]
   rfl
 
-/-- The projection of `FieldOpFreeAlgebra` down to `FieldOpAlgebra` as an algebra map. -/
+lemma equiv_iff_exists_add (x y : FieldOpFreeAlgebra 𝓕) :
+    x ≈ y ↔ ∃ a, x = y + a ∧ a ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet := by
+  apply Iff.intro
+  · intro h
+    rw [equiv_iff_sub_mem_ideal] at h
+    use x - y
+    simp [h]
+  · intro h
+    obtain ⟨a, rfl, ha⟩ := h
+    rw [equiv_iff_sub_mem_ideal]
+    simp [ha]
+
+/-- For a field specification `𝓕`, the projection
+
+`𝓕.FieldOpFreeAlgebra →ₐ[ℂ] FieldOpAlgebra 𝓕`
+
+taking each element of `𝓕.FieldOpFreeAlgebra` to its equivalence class in `FieldOpAlgebra 𝓕`. -/
 def ι : FieldOpFreeAlgebra 𝓕 →ₐ[ℂ] FieldOpAlgebra 𝓕 where
   toFun := (TwoSidedIdeal.span 𝓕.fieldOpIdealSet).ringCon.mk'
   map_one' := by rfl
@@ -444,12 +457,14 @@ lemma ι_eq_zero_iff_ι_bosonicProjF_fermonicProj_zero (x : FieldOpFreeAlgebra
 
 -/
 
-/-- An element of `FieldOpAlgebra` from a `FieldOp`. -/
+/-- For a field specification `𝓕` and an element `φ` of `𝓕.FieldOp`, the element of
+  `𝓕.FieldOpAlgebra` given by `ι (ofFieldOpF φ)`. -/
 def ofFieldOp (φ : 𝓕.FieldOp) : 𝓕.FieldOpAlgebra := ι (ofFieldOpF φ)
 
 lemma ofFieldOp_eq_ι_ofFieldOpF (φ : 𝓕.FieldOp) : ofFieldOp φ = ι (ofFieldOpF φ) := rfl
 
-/-- An element of `FieldOpAlgebra` from a list of `FieldOp`. -/
+/-- For a field specification `𝓕` and a list `φs` of `𝓕.FieldOp`, the element of
+  `𝓕.FieldOpAlgebra` given by `ι (ofFieldOpListF φ)`. -/
 def ofFieldOpList (φs : List 𝓕.FieldOp) : 𝓕.FieldOpAlgebra := ι (ofFieldOpListF φs)
 
 lemma ofFieldOpList_eq_ι_ofFieldOpListF (φs : List 𝓕.FieldOp) :
@@ -472,82 +487,99 @@ lemma ofFieldOpList_singleton (φ : 𝓕.FieldOp) :
     ofFieldOpList [φ] = ofFieldOp φ := by
   simp only [ofFieldOpList, ofFieldOp, ofFieldOpListF_singleton]
 
-/-- An element of `FieldOpAlgebra` from a `CrAnFieldOp`. -/
-def ofCrAnFieldOp (φ : 𝓕.CrAnFieldOp) : 𝓕.FieldOpAlgebra := ι (ofCrAnOpF φ)
+/-- For a field specification `𝓕` and an element `φ` of `𝓕.CrAnFieldOp`, the element of
+  `𝓕.FieldOpAlgebra` given by `ι (ofCrAnOpF φ)`. -/
+def ofCrAnOp (φ : 𝓕.CrAnFieldOp) : 𝓕.FieldOpAlgebra := ι (ofCrAnOpF φ)
 
-lemma ofCrAnFieldOp_eq_ι_ofCrAnOpF (φ : 𝓕.CrAnFieldOp) :
-    ofCrAnFieldOp φ = ι (ofCrAnOpF φ) := rfl
+lemma ofCrAnOp_eq_ι_ofCrAnOpF (φ : 𝓕.CrAnFieldOp) :
+    ofCrAnOp φ = ι (ofCrAnOpF φ) := rfl
 
 lemma ofFieldOp_eq_sum (φ : 𝓕.FieldOp) :
-    ofFieldOp φ = (∑ i : 𝓕.fieldOpToCrAnType φ, ofCrAnFieldOp ⟨φ, i⟩) := by
+    ofFieldOp φ = (∑ i : 𝓕.fieldOpToCrAnType φ, ofCrAnOp ⟨φ, i⟩) := by
   rw [ofFieldOp, ofFieldOpF]
   simp only [map_sum]
   rfl
 
-/-- An element of `FieldOpAlgebra` from a list of `CrAnFieldOp`. -/
-def ofCrAnFieldOpList (φs : List 𝓕.CrAnFieldOp) : 𝓕.FieldOpAlgebra := ι (ofCrAnListF φs)
+/-- For a field specification `𝓕` and a list `φs` of `𝓕.CrAnFieldOp`, the element of
+  `𝓕.FieldOpAlgebra` given by `ι (ofCrAnListF φ)`. -/
+def ofCrAnList (φs : List 𝓕.CrAnFieldOp) : 𝓕.FieldOpAlgebra := ι (ofCrAnListF φs)
 
-lemma ofCrAnFieldOpList_eq_ι_ofCrAnListF (φs : List 𝓕.CrAnFieldOp) :
-    ofCrAnFieldOpList φs = ι (ofCrAnListF φs) := rfl
+lemma ofCrAnList_eq_ι_ofCrAnListF (φs : List 𝓕.CrAnFieldOp) :
+    ofCrAnList φs = ι (ofCrAnListF φs) := rfl
 
-lemma ofCrAnFieldOpList_append (φs ψs : List 𝓕.CrAnFieldOp) :
-    ofCrAnFieldOpList (φs ++ ψs) = ofCrAnFieldOpList φs * ofCrAnFieldOpList ψs := by
-  simp only [ofCrAnFieldOpList]
+lemma ofCrAnList_append (φs ψs : List 𝓕.CrAnFieldOp) :
+    ofCrAnList (φs ++ ψs) = ofCrAnList φs * ofCrAnList ψs := by
+  simp only [ofCrAnList]
   rw [ofCrAnListF_append]
   simp
 
-lemma ofCrAnFieldOpList_singleton (φ : 𝓕.CrAnFieldOp) :
-    ofCrAnFieldOpList [φ] = ofCrAnFieldOp φ := by
-  simp only [ofCrAnFieldOpList, ofCrAnFieldOp, ofCrAnListF_singleton]
+lemma ofCrAnList_singleton (φ : 𝓕.CrAnFieldOp) :
+    ofCrAnList [φ] = ofCrAnOp φ := by
+  simp only [ofCrAnList, ofCrAnOp, ofCrAnListF_singleton]
 
 lemma ofFieldOpList_eq_sum (φs : List 𝓕.FieldOp) :
-    ofFieldOpList φs = ∑ s : CrAnSection φs, ofCrAnFieldOpList s.1 := by
+    ofFieldOpList φs = ∑ s : CrAnSection φs, ofCrAnList s.1 := by
   rw [ofFieldOpList, ofFieldOpListF_sum]
   simp only [map_sum]
   rfl
 
-/-- The annihilation part of a state. -/
+remark notation_drop := "In doc-strings we will often drop explicit applications of `ofCrAnOp`,
+`ofCrAnList`, `ofFieldOp`, and `ofFieldOpList`"
+
+/-- For a field specification `𝓕`, and an element `φ` of `𝓕.FieldOp`, the
+  annihilation part of `𝓕.FieldOp` as an element of `𝓕.FieldOpAlgebra`.
+  If `φ` is an incoming asymptotic state this is zero by definition, otherwise
+  it is of the form `ofCrAnOp _`. -/
 def anPart (φ : 𝓕.FieldOp) : 𝓕.FieldOpAlgebra := ι (anPartF φ)
 
 lemma anPart_eq_ι_anPartF (φ : 𝓕.FieldOp) : anPart φ = ι (anPartF φ) := rfl
 
 @[simp]
-lemma anPart_negAsymp (φ : 𝓕.Fields × Lorentz.Contr 4) :
+lemma anPart_negAsymp (φ : (Σ f, 𝓕.AsymptoticLabel f) × (Fin 3 → ℝ)) :
     anPart (FieldOp.inAsymp φ) = 0 := by
   simp [anPart, anPartF]
 
 @[simp]
-lemma anPart_position (φ : 𝓕.Fields × SpaceTime) :
+lemma anPart_position (φ : (Σ f, 𝓕.PositionLabel f) × SpaceTime) :
     anPart (FieldOp.position φ) =
-    ofCrAnFieldOp ⟨FieldOp.position φ, CreateAnnihilate.annihilate⟩ := by
-  simp [anPart, ofCrAnFieldOp]
+    ofCrAnOp ⟨FieldOp.position φ, CreateAnnihilate.annihilate⟩ := by
+  simp [anPart, ofCrAnOp]
 
 @[simp]
-lemma anPart_posAsymp (φ : 𝓕.Fields × Lorentz.Contr 4) :
-    anPart (FieldOp.outAsymp φ) = ofCrAnFieldOp ⟨FieldOp.outAsymp φ, ()⟩ := by
-  simp [anPart, ofCrAnFieldOp]
+lemma anPart_posAsymp (φ : (Σ f, 𝓕.AsymptoticLabel f) × (Fin 3 → ℝ)) :
+    anPart (FieldOp.outAsymp φ) = ofCrAnOp ⟨FieldOp.outAsymp φ, ()⟩ := by
+  simp [anPart, ofCrAnOp]
 
-/-- The creation part of a state. -/
+/-- For a field specification `𝓕`, and an element `φ` of `𝓕.FieldOp`, the
+  creation part of `𝓕.FieldOp` as an element of `𝓕.FieldOpAlgebra`.
+  If `φ` is an outgoing asymptotic state this is zero by definition, otherwise
+  it is of the form `ofCrAnOp _`. -/
 def crPart (φ : 𝓕.FieldOp) : 𝓕.FieldOpAlgebra := ι (crPartF φ)
 
 lemma crPart_eq_ι_crPartF (φ : 𝓕.FieldOp) : crPart φ = ι (crPartF φ) := rfl
 
 @[simp]
-lemma crPart_negAsymp (φ : 𝓕.Fields × Lorentz.Contr 4) :
-    crPart (FieldOp.inAsymp φ) = ofCrAnFieldOp ⟨FieldOp.inAsymp φ, ()⟩ := by
-  simp [crPart, ofCrAnFieldOp]
+lemma crPart_negAsymp (φ : (Σ f, 𝓕.AsymptoticLabel f) × (Fin 3 → ℝ)) :
+    crPart (FieldOp.inAsymp φ) = ofCrAnOp ⟨FieldOp.inAsymp φ, ()⟩ := by
+  simp [crPart, ofCrAnOp]
 
 @[simp]
-lemma crPart_position (φ : 𝓕.Fields × SpaceTime) :
+lemma crPart_position (φ : (Σ f, 𝓕.PositionLabel f) × SpaceTime) :
     crPart (FieldOp.position φ) =
-    ofCrAnFieldOp ⟨FieldOp.position φ, CreateAnnihilate.create⟩ := by
-  simp [crPart, ofCrAnFieldOp]
+    ofCrAnOp ⟨FieldOp.position φ, CreateAnnihilate.create⟩ := by
+  simp [crPart, ofCrAnOp]
 
 @[simp]
-lemma crPart_posAsymp (φ : 𝓕.Fields × Lorentz.Contr 4) :
+lemma crPart_posAsymp (φ : (Σ f, 𝓕.AsymptoticLabel f) × (Fin 3 → ℝ)) :
     crPart (FieldOp.outAsymp φ) = 0 := by
   simp [crPart]
 
+/-- For field specification `𝓕`, and an element `φ` of `𝓕.FieldOp` the following relation holds:
+
+`ofFieldOp φ = crPart φ + anPart φ`
+
+That is, every field operator splits into its creation part plus its annihilation part.
+-/
 lemma ofFieldOp_eq_crPart_add_anPart (φ : 𝓕.FieldOp) :
     ofFieldOp φ = crPart φ + anPart φ := by
   rw [ofFieldOp, crPart, anPart, ofFieldOpF_eq_crPartF_add_anPartF]

HepLean/PerturbationTheory/FieldOpAlgebra/Grading.lean

@@ -20,14 +20,14 @@ variable {𝓕 : FieldSpecification}
 
 /-- The submodule of `𝓕.FieldOpAlgebra` spanned by lists of field statistic `f`. -/
 def statSubmodule (f : FieldStatistic) : Submodule ℂ 𝓕.FieldOpAlgebra :=
-  Submodule.span ℂ {a | ∃ φs, a = ofCrAnFieldOpList φs ∧ (𝓕 |>ₛ φs) = f}
+  Submodule.span ℂ {a | ∃ φs, a = ofCrAnList φs ∧ (𝓕 |>ₛ φs) = f}
 
-lemma ofCrAnFieldOpList_mem_statSubmodule_of_eq (φs : List 𝓕.CrAnFieldOp) (f : FieldStatistic)
-    (h : (𝓕 |>ₛ φs) = f) : ofCrAnFieldOpList φs ∈ statSubmodule f :=
+lemma ofCrAnList_mem_statSubmodule_of_eq (φs : List 𝓕.CrAnFieldOp) (f : FieldStatistic)
+    (h : (𝓕 |>ₛ φs) = f) : ofCrAnList φs ∈ statSubmodule f :=
   Submodule.mem_span.mpr fun _ a => a ⟨φs, ⟨rfl, h⟩⟩
 
-lemma ofCrAnFieldOpList_mem_statSubmodule (φs : List 𝓕.CrAnFieldOp) :
-    ofCrAnFieldOpList φs ∈ statSubmodule (𝓕 |>ₛ φs) :=
+lemma ofCrAnList_mem_statSubmodule (φs : List 𝓕.CrAnFieldOp) :
+    ofCrAnList φs ∈ statSubmodule (𝓕 |>ₛ φs) :=
   Submodule.mem_span.mpr fun _ a => a ⟨φs, ⟨rfl, rfl⟩⟩
 
 lemma mem_bosonic_of_mem_free_bosonic (a : 𝓕.FieldOpFreeAlgebra)
@@ -40,7 +40,7 @@ lemma mem_bosonic_of_mem_free_bosonic (a : 𝓕.FieldOpFreeAlgebra)
     simp only [Set.mem_setOf_eq] at hx
     obtain ⟨φs, rfl, h⟩ := hx
     simp [p]
-    apply ofCrAnFieldOpList_mem_statSubmodule_of_eq
+    apply ofCrAnList_mem_statSubmodule_of_eq
     exact h
   · simp only [map_zero, p]
     exact Submodule.zero_mem (statSubmodule bosonic)
@@ -61,7 +61,7 @@ lemma mem_fermionic_of_mem_free_fermionic (a : 𝓕.FieldOpFreeAlgebra)
     simp only [Set.mem_setOf_eq] at hx
     obtain ⟨φs, rfl, h⟩ := hx
     simp [p]
-    apply ofCrAnFieldOpList_mem_statSubmodule_of_eq
+    apply ofCrAnList_mem_statSubmodule_of_eq
     exact h
   · simp only [map_zero, p]
     exact Submodule.zero_mem (statSubmodule fermionic)
@@ -204,7 +204,7 @@ lemma bosonicProj_mem_bosonic (a : 𝓕.FieldOpAlgebra) (ha : a ∈ statSubmodul
     simp only [p]
     apply Subtype.eq
     simp only
-    rw [ofCrAnFieldOpList]
+    rw [ofCrAnList]
     rw [bosonicProj_eq_bosonicProjFree]
     rw [bosonicProjFree_eq_ι_bosonicProjF]
     rw [bosonicProjF_of_mem_bosonic]
@@ -227,7 +227,7 @@ lemma fermionicProj_mem_fermionic (a : 𝓕.FieldOpAlgebra) (ha : a ∈ statSubm
     simp only [p]
     apply Subtype.eq
     simp only
-    rw [ofCrAnFieldOpList]
+    rw [ofCrAnList]
     rw [fermionicProj_eq_fermionicProjFree]
     rw [fermionicProjFree_eq_ι_fermionicProjF]
     rw [fermionicProjF_of_mem_fermionic]
@@ -384,15 +384,16 @@ lemma directSum_eq_bosonic_plus_fermionic
     abel
 
 /-- For a field statistic `𝓕`, the algebra `𝓕.FieldOpAlgebra` is graded by `FieldStatistic`.
-  Those `ofCrAnFieldOpList φs` for which `φs` has `bosonic` statistics span one part of the grading,
-  whilst those where `φs` has `fermionic` statistics span the other part of the grading. -/
+  Those `ofCrAnList φs` for which `φs` has an overall `bosonic` statistic span `bosonic`
+  submodule, whilst those `ofCrAnList φs` for which `φs` has an overall `fermionic` statistic span
+  the `fermionic` submodule. -/
 instance fieldOpAlgebraGrade : GradedAlgebra (A := 𝓕.FieldOpAlgebra) statSubmodule where
   one_mem := by
     simp only [statSubmodule]
     refine Submodule.mem_span.mpr fun p a => a ?_
     simp only [Set.mem_setOf_eq]
     use []
-    simp only [ofCrAnFieldOpList, ofCrAnListF_nil, map_one, ofList_empty, true_and]
+    simp only [ofCrAnList, ofCrAnListF_nil, map_one, ofList_empty, true_and]
     rfl
   mul_mem f1 f2 a1 a2 h1 h2 := by
     let p (a2 : 𝓕.FieldOpAlgebra) (hx : a2 ∈ statSubmodule f2) : Prop :=
@@ -404,13 +405,13 @@ instance fieldOpAlgebraGrade : GradedAlgebra (A := 𝓕.FieldOpAlgebra) statSubm
       obtain ⟨φs, rfl, h⟩ := hx
       simp only [p]
       let p (a1 : 𝓕.FieldOpAlgebra) (hx : a1 ∈ statSubmodule f1) : Prop :=
-        a1 * ofCrAnFieldOpList φs ∈ statSubmodule (f1 + f2)
+        a1 * ofCrAnList φs ∈ statSubmodule (f1 + f2)
       change p a1 h1
       apply Submodule.span_induction (p := p)
       · intro y hy
         obtain ⟨φs', rfl, h'⟩ := hy
         simp only [p]
-        rw [← ofCrAnFieldOpList_append]
+        rw [← ofCrAnList_append]
         refine Submodule.mem_span.mpr fun p a => a ?_
         simp only [Set.mem_setOf_eq]
         use φs' ++ φs

HepLean/PerturbationTheory/FieldOpAlgebra/NormalOrder/Basic.lean

@@ -219,7 +219,14 @@ lemma ι_normalOrderF_eq_of_equiv (a b : 𝓕.FieldOpFreeAlgebra) (h : a ≈ b)
   simp only [LinearMap.mem_ker, ← map_sub]
   exact ι_normalOrderF_zero_of_mem_ideal (a - b) h
 
-/-- Normal ordering on `FieldOpAlgebra`. -/
+/-- For a field specification `𝓕`, `normalOrder` is the linera map
+
+  `FieldOpAlgebra 𝓕 →ₗ[ℂ] FieldOpAlgebra 𝓕`
+
+  defined as the decent of `ι ∘ₗ normalOrderF` from `FieldOpFreeAlgebra 𝓕` to `FieldOpAlgebra 𝓕`.
+  This decent exists because `ι ∘ₗ normalOrderF` is well-defined on equivalence classes.
+
+  The notation `𝓝(a)` is used for `normalOrder a`.  -/
 noncomputable def normalOrder : FieldOpAlgebra 𝓕 →ₗ[ℂ] FieldOpAlgebra 𝓕 where
   toFun := Quotient.lift (ι.toLinearMap ∘ₗ normalOrderF) ι_normalOrderF_eq_of_equiv
   map_add' x y := by

HepLean/PerturbationTheory/FieldOpAlgebra/NormalOrder/Lemmas.lean

@@ -27,16 +27,16 @@ variable {𝓕 : FieldSpecification}
 lemma normalOrder_eq_ι_normalOrderF (a : 𝓕.FieldOpFreeAlgebra) :
     𝓝(ι a) = ι 𝓝ᶠ(a) := rfl
 
-lemma normalOrder_ofCrAnFieldOpList (φs : List 𝓕.CrAnFieldOp) :
-    𝓝(ofCrAnFieldOpList φs) = normalOrderSign φs • ofCrAnFieldOpList (normalOrderList φs) := by
-  rw [ofCrAnFieldOpList, normalOrder_eq_ι_normalOrderF, normalOrderF_ofCrAnListF]
+lemma normalOrder_ofCrAnList (φs : List 𝓕.CrAnFieldOp) :
+    𝓝(ofCrAnList φs) = normalOrderSign φs • ofCrAnList (normalOrderList φs) := by
+  rw [ofCrAnList, normalOrder_eq_ι_normalOrderF, normalOrderF_ofCrAnListF]
   rfl
 
 @[simp]
 lemma normalOrder_one_eq_one : normalOrder (𝓕 := 𝓕) 1 = 1 := by
-  have h1 : 1 = ofCrAnFieldOpList (𝓕 := 𝓕) [] := by simp [ofCrAnFieldOpList]
+  have h1 : 1 = ofCrAnList (𝓕 := 𝓕) [] := by simp [ofCrAnList]
   rw [h1]
-  rw [normalOrder_ofCrAnFieldOpList]
+  rw [normalOrder_ofCrAnList]
   simp
 
 @[simp]
@@ -48,14 +48,14 @@ lemma normalOrder_ofFieldOpList_nil : normalOrder (𝓕 := 𝓕) (ofFieldOpList
   simp
 
 @[simp]
-lemma normalOrder_ofCrAnFieldOpList_nil : normalOrder (𝓕 := 𝓕) (ofCrAnFieldOpList []) = 1 := by
-  rw [normalOrder_ofCrAnFieldOpList]
+lemma normalOrder_ofCrAnList_nil : normalOrder (𝓕 := 𝓕) (ofCrAnList []) = 1 := by
+  rw [normalOrder_ofCrAnList]
   simp only [normalOrderSign_nil, normalOrderList_nil, one_smul]
   rfl
 
-lemma ofCrAnFieldOpList_eq_normalOrder (φs : List 𝓕.CrAnFieldOp) :
-    ofCrAnFieldOpList (normalOrderList φs) = normalOrderSign φs • 𝓝(ofCrAnFieldOpList φs) := by
-  rw [normalOrder_ofCrAnFieldOpList, smul_smul, normalOrderSign, Wick.koszulSign_mul_self,
+lemma ofCrAnList_eq_normalOrder (φs : List 𝓕.CrAnFieldOp) :
+    ofCrAnList (normalOrderList φs) = normalOrderSign φs • 𝓝(ofCrAnList φs) := by
+  rw [normalOrder_ofCrAnList, smul_smul, normalOrderSign, Wick.koszulSign_mul_self,
     one_smul]
 
 lemma normalOrder_normalOrder_mid (a b c : 𝓕.FieldOpAlgebra) :
@@ -165,16 +165,16 @@ lemma normalOrder_ofFieldOp_ofFieldOp_swap (φ φ' : 𝓕.FieldOp) :
   rw [ofFieldOp_mul_ofFieldOp_eq_superCommute]
   simp
 
-lemma normalOrder_ofCrAnFieldOp_ofCrAnFieldOpList (φ : 𝓕.CrAnFieldOp)
-    (φs : List 𝓕.CrAnFieldOp) : 𝓝(ofCrAnFieldOp φ * ofCrAnFieldOpList φs) =
-    𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φs) • 𝓝(ofCrAnFieldOpList φs * ofCrAnFieldOp φ) := by
-  rw [← ofCrAnFieldOpList_singleton, ofCrAnFieldOpList_mul_ofCrAnFieldOpList_eq_superCommute]
+lemma normalOrder_ofCrAnOp_ofCrAnList (φ : 𝓕.CrAnFieldOp)
+    (φs : List 𝓕.CrAnFieldOp) : 𝓝(ofCrAnOp φ * ofCrAnList φs) =
+    𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φs) • 𝓝(ofCrAnList φs * ofCrAnOp φ) := by
+  rw [← ofCrAnList_singleton, ofCrAnList_mul_ofCrAnList_eq_superCommute]
   simp
 
-lemma normalOrder_ofCrAnFieldOp_ofFieldOpList_swap (φ : 𝓕.CrAnFieldOp) (φ' : List 𝓕.FieldOp) :
-    𝓝(ofCrAnFieldOp φ * ofFieldOpList φ') = 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') •
-    𝓝(ofFieldOpList φ' * ofCrAnFieldOp φ) := by
-  rw [← ofCrAnFieldOpList_singleton, ofCrAnFieldOpList_mul_ofFieldOpList_eq_superCommute]
+lemma normalOrder_ofCrAnOp_ofFieldOpList_swap (φ : 𝓕.CrAnFieldOp) (φ' : List 𝓕.FieldOp) :
+    𝓝(ofCrAnOp φ * ofFieldOpList φ') = 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') •
+    𝓝(ofFieldOpList φ' * ofCrAnOp φ) := by
+  rw [← ofCrAnList_singleton, ofCrAnList_mul_ofFieldOpList_eq_superCommute]
   simp
 
 lemma normalOrder_anPart_ofFieldOpList_swap (φ : 𝓕.FieldOp) (φ' : List 𝓕.FieldOp) :
@@ -184,11 +184,11 @@ lemma normalOrder_anPart_ofFieldOpList_swap (φ : 𝓕.FieldOp) (φ' : List 𝓕
     simp
   | .position φ =>
     simp only [anPart_position, instCommGroup.eq_1]
-    rw [normalOrder_ofCrAnFieldOp_ofFieldOpList_swap]
+    rw [normalOrder_ofCrAnOp_ofFieldOpList_swap]
     rfl
   | .outAsymp φ =>
     simp only [anPart_posAsymp, instCommGroup.eq_1]
-    rw [normalOrder_ofCrAnFieldOp_ofFieldOpList_swap]
+    rw [normalOrder_ofCrAnOp_ofFieldOpList_swap]
     rfl
 
 lemma normalOrder_ofFieldOpList_anPart_swap (φ : 𝓕.FieldOp) (φ' : List 𝓕.FieldOp) :
@@ -217,22 +217,32 @@ lemma anPart_mul_normalOrder_ofFieldOpList_eq_superCommute (φ : 𝓕.FieldOp)
 -/
 
 /--
-The proof of this result ultimetly depends on
-- `superCommuteF_ofCrAnListF_ofFieldOpListF_eq_sum`
-- `normalOrderSign_eraseIdx`
+For a field specification `𝓕`, an element `φ` of `𝓕.CrAnFieldOp`, a list `φs` of `𝓕.CrAnFieldOp`,
+  the following relation holds
+
+`[φ, 𝓝(φ₀…φₙ)]ₛ = ∑ i, 𝓢(φ, φ₀…φᵢ₋₁) • [φ, φᵢ]ₛ * 𝓝(φ₀…φᵢ₋₁φᵢ₊₁…φₙ)`.
+
+The proof of this result ultimetly goes as follows
+- The definition of `normalOrder` is used to rewrite `𝓝(φ₀…φₙ)` as a scalar multiple of
+  a `ofCrAnList φsn` where `φsn` is the normal ordering of `φ₀…φₙ`.
+- `superCommuteF_ofCrAnListF_ofCrAnListF_eq_sum` is used to rewrite the super commutator of `φ`
+  (considered as a list with one lement) with
+  `ofCrAnList φsn` as a sum of supercommutors, one for each element of `φsn`.
+- The fact that super-commutors are in the center of `𝓕.FieldOpAlgebra` is used to rearange terms.
+- Properties of ordered lists, and `normalOrderSign_eraseIdx` is then used to complete the proof.
 -/
-lemma ofCrAnFieldOp_superCommute_normalOrder_ofCrAnFieldOpList_sum (φ : 𝓕.CrAnFieldOp)
-    (φs : List 𝓕.CrAnFieldOp) : [ofCrAnFieldOp φ, 𝓝(ofCrAnFieldOpList φs)]ₛ = ∑ n : Fin φs.length,
-    𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ (φs.take n)) • [ofCrAnFieldOp φ, ofCrAnFieldOp φs[n]]ₛ
-    * 𝓝(ofCrAnFieldOpList (φs.eraseIdx n)) := by
-  rw [normalOrder_ofCrAnFieldOpList, map_smul]
-  rw [superCommute_ofCrAnFieldOp_ofCrAnFieldOpList_eq_sum, Finset.smul_sum,
+lemma ofCrAnOp_superCommute_normalOrder_ofCrAnList_sum (φ : 𝓕.CrAnFieldOp)
+    (φs : List 𝓕.CrAnFieldOp) : [ofCrAnOp φ, 𝓝(ofCrAnList φs)]ₛ = ∑ n : Fin φs.length,
+    𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ (φs.take n)) • [ofCrAnOp φ, ofCrAnOp φs[n]]ₛ
+    * 𝓝(ofCrAnList (φs.eraseIdx n)) := by
+  rw [normalOrder_ofCrAnList, map_smul]
+  rw [superCommute_ofCrAnOp_ofCrAnList_eq_sum, Finset.smul_sum,
     sum_normalOrderList_length]
   congr
   funext n
   simp only [instCommGroup.eq_1, List.get_eq_getElem, normalOrderList_get_normalOrderEquiv,
     normalOrderList_eraseIdx_normalOrderEquiv, Algebra.smul_mul_assoc, Fin.getElem_fin]
-  rw [ofCrAnFieldOpList_eq_normalOrder, mul_smul_comm, smul_smul, smul_smul]
+  rw [ofCrAnList_eq_normalOrder, mul_smul_comm, smul_smul, smul_smul]
   by_cases hs : (𝓕 |>ₛ φ) = (𝓕 |>ₛ φs[n])
   · congr
     erw [normalOrderSign_eraseIdx, ← hs]
@@ -247,14 +257,14 @@ lemma ofCrAnFieldOp_superCommute_normalOrder_ofCrAnFieldOpList_sum (φ : 𝓕.Cr
   · erw [superCommute_diff_statistic hs]
     simp
 
-lemma ofCrAnFieldOp_superCommute_normalOrder_ofFieldOpList_sum (φ : 𝓕.CrAnFieldOp)
+lemma ofCrAnOp_superCommute_normalOrder_ofFieldOpList_sum (φ : 𝓕.CrAnFieldOp)
     (φs : List 𝓕.FieldOp) :
-    [ofCrAnFieldOp φ, 𝓝(ofFieldOpList φs)]ₛ = ∑ n : Fin φs.length, 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ (φs.take n)) •
-    [ofCrAnFieldOp φ, ofFieldOp φs[n]]ₛ * 𝓝(ofFieldOpList (φs.eraseIdx n)) := by
+    [ofCrAnOp φ, 𝓝(ofFieldOpList φs)]ₛ = ∑ n : Fin φs.length, 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ (φs.take n)) •
+    [ofCrAnOp φ, ofFieldOp φs[n]]ₛ * 𝓝(ofFieldOpList (φs.eraseIdx n)) := by
   conv_lhs =>
     rw [ofFieldOpList_eq_sum, map_sum, map_sum]
     enter [2, s]
-    rw [ofCrAnFieldOp_superCommute_normalOrder_ofCrAnFieldOpList_sum, CrAnSection.sum_over_length]
+    rw [ofCrAnOp_superCommute_normalOrder_ofCrAnList_sum, CrAnSection.sum_over_length]
     enter [2, n]
     rw [CrAnSection.take_statistics_eq_take_state_statistics, smul_mul_assoc]
   rw [Finset.sum_comm]
@@ -282,13 +292,13 @@ lemma anPart_superCommute_normalOrder_ofFieldOpList_sum (φ : 𝓕.FieldOp) (φs
     simp
   | .position φ =>
     simp only [anPart_position, instCommGroup.eq_1, Fin.getElem_fin, Algebra.smul_mul_assoc]
-    rw [ofCrAnFieldOp_superCommute_normalOrder_ofFieldOpList_sum]
+    rw [ofCrAnOp_superCommute_normalOrder_ofFieldOpList_sum]
     simp only [instCommGroup.eq_1, crAnStatistics, Function.comp_apply, crAnFieldOpToFieldOp_prod,
       Fin.getElem_fin, Algebra.smul_mul_assoc]
     rfl
   | .outAsymp φ =>
     simp only [anPart_posAsymp, instCommGroup.eq_1, Fin.getElem_fin, Algebra.smul_mul_assoc]
-    rw [ofCrAnFieldOp_superCommute_normalOrder_ofFieldOpList_sum]
+    rw [ofCrAnOp_superCommute_normalOrder_ofFieldOpList_sum]
     simp only [instCommGroup.eq_1, crAnStatistics, Function.comp_apply, crAnFieldOpToFieldOp_prod,
       Fin.getElem_fin, Algebra.smul_mul_assoc]
     rfl
@@ -332,11 +342,18 @@ noncomputable def contractStateAtIndex (φ : 𝓕.FieldOp) (φs : List 𝓕.Fiel
   | some n => 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ (φs.take n)) • [anPart φ, ofFieldOp φs[n]]ₛ
 
 /--
-For a field specification `𝓕`, the following relation holds in the algebra `𝓕.FieldOpAlgebra`,
+For a field specification `𝓕`, a `φ` in `𝓕.FieldOp` and a list `φs` of `𝓕.FieldOp`
+the following relation holds in the algebra `𝓕.FieldOpAlgebra`,
 `φ * 𝓝(φ₀φ₁…φₙ) = 𝓝(φφ₀φ₁…φₙ) + ∑ i, (𝓢(φ,φ₀φ₁…φᵢ₋₁) • [anPartF φ, φᵢ]ₛ) * 𝓝(φ₀φ₁…φᵢ₋₁φᵢ₊₁…φₙ)`.
 
-The proof of this ultimently depends on :
-- `ofCrAnFieldOp_superCommute_normalOrder_ofCrAnFieldOpList_sum`
+The proof of ultimetly goes as follows:
+- `ofFieldOp_eq_crPart_add_anPart` is used to split `φ` into its creation and annihilation parts.
+- The fact that `crPart φ *  𝓝(φ₀φ₁…φₙ) = 𝓝(crPart φ * φ₀φ₁…φₙ)` is used.
+- The fact that `anPart φ * 𝓝(φ₀φ₁…φₙ)` is
+  `𝓢(φ, φ₀φ₁…φₙ) 𝓝(φ₀φ₁…φₙ) * anPart φ + [anPart φ, 𝓝(φ₀φ₁…φₙ)]` is used
+- The fact that `𝓢(φ, φ₀φ₁…φₙ) 𝓝(φ₀φ₁…φₙ) * anPart φ = 𝓝(anPart φ * φ₀φ₁…φₙ)`
+- The result `ofCrAnOp_superCommute_normalOrder_ofCrAnList_sum` is used
+  to expand `[anPart φ, 𝓝(φ₀φ₁…φₙ)]` as a sum.
 -/
 lemma ofFieldOp_mul_normalOrder_ofFieldOpList_eq_sum (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) :
     ofFieldOp φ * 𝓝(ofFieldOpList φs) =

HepLean/PerturbationTheory/FieldOpAlgebra/StaticWickTerm.lean

@@ -29,7 +29,7 @@ def staticWickTerm {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length
 
 /-- The static Wick term for the empty contraction of the empty list is `1`. -/
 @[simp]
-lemma staticWickTerm_empty_nil  :
+lemma staticWickTerm_empty_nil :
     staticWickTerm (empty (n := ([] : List 𝓕.FieldOp).length)) = 1 := by
   rw [staticWickTerm, uncontractedListGet, nil_zero_uncontractedList]
   simp [sign, empty, staticContract]
@@ -51,7 +51,7 @@ lemma staticWickTerm_insert_zero_none (φ : 𝓕.FieldOp) (φs : List 𝓕.Field
   simp only [staticContract_insert_none, insertAndContract_uncontractedList_none_zero,
     Algebra.smul_mul_assoc]
 
-/-- Let `φsΛ` be a Wick contraction for `φs = φ₀φ₁…φₙ`.  Then`(φsΛ ↩Λ φ 0 (some k)).wickTerm`
+/-- Let `φsΛ` be a Wick contraction for `φs = φ₀φ₁…φₙ`. Then`(φsΛ ↩Λ φ 0 (some k)).wickTerm`
 is equal the product of
 - the sign `𝓢(φ, φ₀…φᵢ₋₁) `
 - the sign `φsΛ.sign`
@@ -62,7 +62,7 @@ is equal the product of
 
 The proof of this result relies on
 - `staticContract_insert_some_of_lt` to rewrite static
- contractions.
+  contractions.
 - `normalOrder_uncontracted_some` to rewrite normal orderings.
 - `sign_insert_some_zero` to rewrite signs.
 -/
@@ -105,14 +105,13 @@ lemma staticWickTerm_insert_zero_some (φ : 𝓕.FieldOp) (φs : List 𝓕.Field
       rw [h1]
       simp
 
-
 /--
-Let `φsΛ` be a Wick contraction for `φs = φ₀φ₁…φₙ`.  Then
+Let `φsΛ` be a Wick contraction for `φs = φ₀φ₁…φₙ`. Then
 `φ * φsΛ.staticWickTerm = ∑ k, (φsΛ ↩Λ φ i k).wickTerm`
 where the sum is over all `k` in `Option φsΛ.uncontracted` (so either `none` or `some k`).
 
 The proof of proceeds as follows:
-- `ofFieldOp_mul_normalOrder_ofFieldOpList_eq_sum` is used to expand  `φ 𝓝([φsΛ]ᵘᶜ)` as
+- `ofFieldOp_mul_normalOrder_ofFieldOpList_eq_sum` is used to expand `φ 𝓝([φsΛ]ᵘᶜ)` as
   a sum over `k` in `Option φsΛ.uncontracted` of terms involving `[φ, φs[k]]` etc.
 - Then `staticWickTerm_insert_zero_none` and `staticWickTerm_insert_zero_some` are
   used to equate terms.

HepLean/PerturbationTheory/FieldOpAlgebra/StaticWickTheorem.lean

@@ -10,8 +10,6 @@ import HepLean.PerturbationTheory.FieldOpAlgebra.StaticWickTerm
 
 -/
 
-
-
 namespace FieldSpecification
 variable {𝓕 : FieldSpecification}
 open FieldOpFreeAlgebra

HepLean/PerturbationTheory/FieldOpAlgebra/SuperCommute.lean

@@ -88,7 +88,16 @@ lemma superCommuteRight_eq_of_equiv (a1 a2 : 𝓕.FieldOpFreeAlgebra) (h : a1
   simp only [add_sub_cancel]
   simp
 
-/-- The super commutor on the `FieldOpAlgebra`. -/
+/-- For a field specification `𝓕`, `superCommute` is the linear map
+  `FieldOpAlgebra 𝓕 →ₗ[ℂ] FieldOpAlgebra 𝓕 →ₗ[ℂ] FieldOpAlgebra 𝓕`
+  defined as the decent of `ι ∘ superCommuteF` in both arguments.
+  In particular for `φs` and `φs'` lists of `𝓕.CrAnFieldOp` in `FieldOpAlgebra 𝓕` the following
+  relation holds:
+
+  `superCommute φs φs' = φs * φs' - 𝓢(φs, φs') • φs' * φs`
+
+  The notation `[a, b]ₛ` is used for `superCommute a b`.
+  -/
 noncomputable def superCommute : FieldOpAlgebra 𝓕 →ₗ[ℂ]
     FieldOpAlgebra 𝓕 →ₗ[ℂ] FieldOpAlgebra 𝓕 where
   toFun := Quotient.lift superCommuteRight superCommuteRight_eq_of_equiv
@@ -131,23 +140,23 @@ lemma superCommute_eq_ι_superCommuteF (a b : 𝓕.FieldOpFreeAlgebra) :
 
 lemma superCommute_create_create {φ φ' : 𝓕.CrAnFieldOp}
     (h : 𝓕 |>ᶜ φ = .create) (h' : 𝓕 |>ᶜ φ' = .create) :
-    [ofCrAnFieldOp φ, ofCrAnFieldOp φ']ₛ = 0 := by
-  rw [ofCrAnFieldOp, ofCrAnFieldOp]
+    [ofCrAnOp φ, ofCrAnOp φ']ₛ = 0 := by
+  rw [ofCrAnOp, ofCrAnOp]
   rw [superCommute_eq_ι_superCommuteF, ι_superCommuteF_of_create_create _ _ h h']
 
 lemma superCommute_annihilate_annihilate {φ φ' : 𝓕.CrAnFieldOp}
     (h : 𝓕 |>ᶜ φ = .annihilate) (h' : 𝓕 |>ᶜ φ' = .annihilate) :
-    [ofCrAnFieldOp φ, ofCrAnFieldOp φ']ₛ = 0 := by
-  rw [ofCrAnFieldOp, ofCrAnFieldOp]
+    [ofCrAnOp φ, ofCrAnOp φ']ₛ = 0 := by
+  rw [ofCrAnOp, ofCrAnOp]
   rw [superCommute_eq_ι_superCommuteF, ι_superCommuteF_of_annihilate_annihilate _ _ h h']
 
 lemma superCommute_diff_statistic {φ φ' : 𝓕.CrAnFieldOp} (h : (𝓕 |>ₛ φ) ≠ 𝓕 |>ₛ φ') :
-    [ofCrAnFieldOp φ, ofCrAnFieldOp φ']ₛ = 0 := by
-  rw [ofCrAnFieldOp, ofCrAnFieldOp]
+    [ofCrAnOp φ, ofCrAnOp φ']ₛ = 0 := by
+  rw [ofCrAnOp, ofCrAnOp]
   rw [superCommute_eq_ι_superCommuteF, ι_superCommuteF_of_diff_statistic h]
 
-lemma superCommute_ofCrAnFieldOp_ofFieldOp_diff_stat_zero (φ : 𝓕.CrAnFieldOp) (ψ : 𝓕.FieldOp)
-    (h : (𝓕 |>ₛ φ) ≠ (𝓕 |>ₛ ψ)) : [ofCrAnFieldOp φ, ofFieldOp ψ]ₛ = 0 := by
+lemma superCommute_ofCrAnOp_ofFieldOp_diff_stat_zero (φ : 𝓕.CrAnFieldOp) (ψ : 𝓕.FieldOp)
+    (h : (𝓕 |>ₛ φ) ≠ (𝓕 |>ₛ ψ)) : [ofCrAnOp φ, ofFieldOp ψ]ₛ = 0 := by
   rw [ofFieldOp_eq_sum, map_sum]
   rw [Finset.sum_eq_zero]
   intro x hx
@@ -161,37 +170,37 @@ lemma superCommute_anPart_ofFieldOpF_diff_grade_zero (φ ψ : 𝓕.FieldOp)
     simp
   | FieldOp.position φ =>
     simp only [anPartF_position]
-    apply superCommute_ofCrAnFieldOp_ofFieldOp_diff_stat_zero _ _ _
+    apply superCommute_ofCrAnOp_ofFieldOp_diff_stat_zero _ _ _
     simpa [crAnStatistics] using h
   | FieldOp.outAsymp _ =>
     simp only [anPartF_posAsymp]
-    apply superCommute_ofCrAnFieldOp_ofFieldOp_diff_stat_zero _ _
+    apply superCommute_ofCrAnOp_ofFieldOp_diff_stat_zero _ _
     simpa [crAnStatistics] using h
 
-lemma superCommute_ofCrAnFieldOp_ofCrAnFieldOp_mem_center (φ φ' : 𝓕.CrAnFieldOp) :
-    [ofCrAnFieldOp φ, ofCrAnFieldOp φ']ₛ ∈ Subalgebra.center ℂ (FieldOpAlgebra 𝓕) := by
-  rw [ofCrAnFieldOp, ofCrAnFieldOp, superCommute_eq_ι_superCommuteF]
+lemma superCommute_ofCrAnOp_ofCrAnOp_mem_center (φ φ' : 𝓕.CrAnFieldOp) :
+    [ofCrAnOp φ, ofCrAnOp φ']ₛ ∈ Subalgebra.center ℂ (FieldOpAlgebra 𝓕) := by
+  rw [ofCrAnOp, ofCrAnOp, superCommute_eq_ι_superCommuteF]
   exact ι_superCommuteF_ofCrAnOpF_ofCrAnOpF_mem_center φ φ'
 
-lemma superCommute_ofCrAnFieldOp_ofCrAnFieldOp_commute (φ φ' : 𝓕.CrAnFieldOp)
+lemma superCommute_ofCrAnOp_ofCrAnOp_commute (φ φ' : 𝓕.CrAnFieldOp)
     (a : FieldOpAlgebra 𝓕) :
-    a * [ofCrAnFieldOp φ, ofCrAnFieldOp φ']ₛ = [ofCrAnFieldOp φ, ofCrAnFieldOp φ']ₛ * a := by
-  have h1 := superCommute_ofCrAnFieldOp_ofCrAnFieldOp_mem_center φ φ'
+    a * [ofCrAnOp φ, ofCrAnOp φ']ₛ = [ofCrAnOp φ, ofCrAnOp φ']ₛ * a := by
+  have h1 := superCommute_ofCrAnOp_ofCrAnOp_mem_center φ φ'
   rw [@Subalgebra.mem_center_iff] at h1
   exact h1 a
 
-lemma superCommute_ofCrAnFieldOp_ofFieldOp_mem_center (φ : 𝓕.CrAnFieldOp) (φ' : 𝓕.FieldOp) :
-    [ofCrAnFieldOp φ, ofFieldOp φ']ₛ ∈ Subalgebra.center ℂ (FieldOpAlgebra 𝓕) := by
+lemma superCommute_ofCrAnOp_ofFieldOp_mem_center (φ : 𝓕.CrAnFieldOp) (φ' : 𝓕.FieldOp) :
+    [ofCrAnOp φ, ofFieldOp φ']ₛ ∈ Subalgebra.center ℂ (FieldOpAlgebra 𝓕) := by
   rw [ofFieldOp_eq_sum]
   simp only [map_sum]
   refine Subalgebra.sum_mem (Subalgebra.center ℂ 𝓕.FieldOpAlgebra) ?_
   intro x hx
-  exact superCommute_ofCrAnFieldOp_ofCrAnFieldOp_mem_center φ ⟨φ', x⟩
+  exact superCommute_ofCrAnOp_ofCrAnOp_mem_center φ ⟨φ', x⟩
 
-lemma superCommute_ofCrAnFieldOp_ofFieldOp_commute (φ : 𝓕.CrAnFieldOp) (φ' : 𝓕.FieldOp)
-    (a : FieldOpAlgebra 𝓕) : a * [ofCrAnFieldOp φ, ofFieldOp φ']ₛ =
-    [ofCrAnFieldOp φ, ofFieldOp φ']ₛ * a := by
-  have h1 := superCommute_ofCrAnFieldOp_ofFieldOp_mem_center φ φ'
+lemma superCommute_ofCrAnOp_ofFieldOp_commute (φ : 𝓕.CrAnFieldOp) (φ' : 𝓕.FieldOp)
+    (a : FieldOpAlgebra 𝓕) : a * [ofCrAnOp φ, ofFieldOp φ']ₛ =
+    [ofCrAnOp φ, ofFieldOp φ']ₛ * a := by
+  have h1 := superCommute_ofCrAnOp_ofFieldOp_mem_center φ φ'
   rw [@Subalgebra.mem_center_iff] at h1
   exact h1 a
 
@@ -202,9 +211,9 @@ lemma superCommute_anPart_ofFieldOp_mem_center (φ φ' : 𝓕.FieldOp) :
     simp only [anPart_negAsymp, map_zero, LinearMap.zero_apply]
     exact Subalgebra.zero_mem (Subalgebra.center ℂ _)
   | FieldOp.position φ =>
-    exact superCommute_ofCrAnFieldOp_ofFieldOp_mem_center _ _
+    exact superCommute_ofCrAnOp_ofFieldOp_mem_center _ _
   | FieldOp.outAsymp _ =>
-    exact superCommute_ofCrAnFieldOp_ofFieldOp_mem_center _ _
+    exact superCommute_ofCrAnOp_ofFieldOp_mem_center _ _
 
 /-!
 
@@ -212,25 +221,25 @@ lemma superCommute_anPart_ofFieldOp_mem_center (φ φ' : 𝓕.FieldOp) :
 
 -/
 
-lemma superCommute_ofCrAnFieldOpList_ofCrAnFieldOpList (φs φs' : List 𝓕.CrAnFieldOp) :
-    [ofCrAnFieldOpList φs, ofCrAnFieldOpList φs']ₛ =
-    ofCrAnFieldOpList (φs ++ φs') - 𝓢(𝓕 |>ₛ φs, 𝓕 |>ₛ φs') • ofCrAnFieldOpList (φs' ++ φs) := by
-  rw [ofCrAnFieldOpList_eq_ι_ofCrAnListF, ofCrAnFieldOpList_eq_ι_ofCrAnListF]
+lemma superCommute_ofCrAnList_ofCrAnList (φs φs' : List 𝓕.CrAnFieldOp) :
+    [ofCrAnList φs, ofCrAnList φs']ₛ =
+    ofCrAnList (φs ++ φs') - 𝓢(𝓕 |>ₛ φs, 𝓕 |>ₛ φs') • ofCrAnList (φs' ++ φs) := by
+  rw [ofCrAnList_eq_ι_ofCrAnListF, ofCrAnList_eq_ι_ofCrAnListF]
   rw [superCommute_eq_ι_superCommuteF, superCommuteF_ofCrAnListF_ofCrAnListF]
   rfl
 
-lemma superCommute_ofCrAnFieldOp_ofCrAnFieldOp (φ φ' : 𝓕.CrAnFieldOp) :
-    [ofCrAnFieldOp φ, ofCrAnFieldOp φ']ₛ = ofCrAnFieldOp φ * ofCrAnFieldOp φ' -
-    𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') • ofCrAnFieldOp φ' * ofCrAnFieldOp φ := by
-  rw [ofCrAnFieldOp, ofCrAnFieldOp]
+lemma superCommute_ofCrAnOp_ofCrAnOp (φ φ' : 𝓕.CrAnFieldOp) :
+    [ofCrAnOp φ, ofCrAnOp φ']ₛ = ofCrAnOp φ * ofCrAnOp φ' -
+    𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ') • ofCrAnOp φ' * ofCrAnOp φ := by
+  rw [ofCrAnOp, ofCrAnOp]
   rw [superCommute_eq_ι_superCommuteF, superCommuteF_ofCrAnOpF_ofCrAnOpF]
   rfl
 
-lemma superCommute_ofCrAnFieldOpList_ofFieldOpList (φcas : List 𝓕.CrAnFieldOp)
+lemma superCommute_ofCrAnList_ofFieldOpList (φcas : List 𝓕.CrAnFieldOp)
     (φs : List 𝓕.FieldOp) :
-    [ofCrAnFieldOpList φcas, ofFieldOpList φs]ₛ = ofCrAnFieldOpList φcas * ofFieldOpList φs -
-    𝓢(𝓕 |>ₛ φcas, 𝓕 |>ₛ φs) • ofFieldOpList φs * ofCrAnFieldOpList φcas := by
-  rw [ofCrAnFieldOpList, ofFieldOpList]
+    [ofCrAnList φcas, ofFieldOpList φs]ₛ = ofCrAnList φcas * ofFieldOpList φs -
+    𝓢(𝓕 |>ₛ φcas, 𝓕 |>ₛ φs) • ofFieldOpList φs * ofCrAnList φcas := by
+  rw [ofCrAnList, ofFieldOpList]
   rw [superCommute_eq_ι_superCommuteF, superCommuteF_ofCrAnListF_ofFieldOpFsList]
   rfl
 
@@ -362,18 +371,18 @@ multiplication with a sign plus the super commutor.
 
 -/
 
-lemma ofCrAnFieldOpList_mul_ofCrAnFieldOpList_eq_superCommute (φs φs' : List 𝓕.CrAnFieldOp) :
-    ofCrAnFieldOpList φs * ofCrAnFieldOpList φs' =
-    𝓢(𝓕 |>ₛ φs, 𝓕 |>ₛ φs') • ofCrAnFieldOpList φs' * ofCrAnFieldOpList φs
-    + [ofCrAnFieldOpList φs, ofCrAnFieldOpList φs']ₛ := by
-  rw [superCommute_ofCrAnFieldOpList_ofCrAnFieldOpList]
-  simp [ofCrAnFieldOpList_append]
+lemma ofCrAnList_mul_ofCrAnList_eq_superCommute (φs φs' : List 𝓕.CrAnFieldOp) :
+    ofCrAnList φs * ofCrAnList φs' =
+    𝓢(𝓕 |>ₛ φs, 𝓕 |>ₛ φs') • ofCrAnList φs' * ofCrAnList φs
+    + [ofCrAnList φs, ofCrAnList φs']ₛ := by
+  rw [superCommute_ofCrAnList_ofCrAnList]
+  simp [ofCrAnList_append]
 
-lemma ofCrAnFieldOp_mul_ofCrAnFieldOpList_eq_superCommute (φ : 𝓕.CrAnFieldOp)
-    (φs' : List 𝓕.CrAnFieldOp) : ofCrAnFieldOp φ * ofCrAnFieldOpList φs' =
-    𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φs') • ofCrAnFieldOpList φs' * ofCrAnFieldOp φ
-    + [ofCrAnFieldOp φ, ofCrAnFieldOpList φs']ₛ := by
-  rw [← ofCrAnFieldOpList_singleton, ofCrAnFieldOpList_mul_ofCrAnFieldOpList_eq_superCommute]
+lemma ofCrAnOp_mul_ofCrAnList_eq_superCommute (φ : 𝓕.CrAnFieldOp)
+    (φs' : List 𝓕.CrAnFieldOp) : ofCrAnOp φ * ofCrAnList φs' =
+    𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φs') • ofCrAnList φs' * ofCrAnOp φ
+    + [ofCrAnOp φ, ofCrAnList φs']ₛ := by
+  rw [← ofCrAnList_singleton, ofCrAnList_mul_ofCrAnList_eq_superCommute]
   simp
 
 lemma ofFieldOpList_mul_ofFieldOpList_eq_superCommute (φs φs' : List 𝓕.FieldOp) :
@@ -402,11 +411,11 @@ lemma ofFieldOpList_mul_ofFieldOp_eq_superCommute (φs : List 𝓕.FieldOp) (φ
   rw [superCommute_ofFieldOpList_ofFieldOp]
   simp
 
-lemma ofCrAnFieldOpList_mul_ofFieldOpList_eq_superCommute (φs : List 𝓕.CrAnFieldOp)
-    (φs' : List 𝓕.FieldOp) : ofCrAnFieldOpList φs * ofFieldOpList φs' =
-    𝓢(𝓕 |>ₛ φs, 𝓕 |>ₛ φs') • ofFieldOpList φs' * ofCrAnFieldOpList φs
-    + [ofCrAnFieldOpList φs, ofFieldOpList φs']ₛ := by
-  rw [superCommute_ofCrAnFieldOpList_ofFieldOpList]
+lemma ofCrAnList_mul_ofFieldOpList_eq_superCommute (φs : List 𝓕.CrAnFieldOp)
+    (φs' : List 𝓕.FieldOp) : ofCrAnList φs * ofFieldOpList φs' =
+    𝓢(𝓕 |>ₛ φs, 𝓕 |>ₛ φs') • ofFieldOpList φs' * ofCrAnList φs
+    + [ofCrAnList φs, ofFieldOpList φs']ₛ := by
+  rw [superCommute_ofCrAnList_ofFieldOpList]
   simp
 
 lemma crPart_mul_anPart_eq_superCommute (φ φ' : 𝓕.FieldOp) :
@@ -441,17 +450,17 @@ lemma anPart_mul_anPart_swap (φ φ' : 𝓕.FieldOp) :
 
 -/
 
-lemma superCommute_ofCrAnFieldOpList_ofCrAnFieldOpList_symm (φs φs' : List 𝓕.CrAnFieldOp) :
-    [ofCrAnFieldOpList φs, ofCrAnFieldOpList φs']ₛ =
-    (- 𝓢(𝓕 |>ₛ φs, 𝓕 |>ₛ φs')) • [ofCrAnFieldOpList φs', ofCrAnFieldOpList φs]ₛ := by
-  rw [ofCrAnFieldOpList, ofCrAnFieldOpList, superCommute_eq_ι_superCommuteF,
+lemma superCommute_ofCrAnList_ofCrAnList_symm (φs φs' : List 𝓕.CrAnFieldOp) :
+    [ofCrAnList φs, ofCrAnList φs']ₛ =
+    (- 𝓢(𝓕 |>ₛ φs, 𝓕 |>ₛ φs')) • [ofCrAnList φs', ofCrAnList φs]ₛ := by
+  rw [ofCrAnList, ofCrAnList, superCommute_eq_ι_superCommuteF,
     superCommuteF_ofCrAnListF_ofCrAnListF_symm]
   rfl
 
-lemma superCommute_ofCrAnFieldOp_ofCrAnFieldOp_symm (φ φ' : 𝓕.CrAnFieldOp) :
-    [ofCrAnFieldOp φ, ofCrAnFieldOp φ']ₛ =
-    (- 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ')) • [ofCrAnFieldOp φ', ofCrAnFieldOp φ]ₛ := by
-  rw [ofCrAnFieldOp, ofCrAnFieldOp, superCommute_eq_ι_superCommuteF,
+lemma superCommute_ofCrAnOp_ofCrAnOp_symm (φ φ' : 𝓕.CrAnFieldOp) :
+    [ofCrAnOp φ, ofCrAnOp φ']ₛ =
+    (- 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φ')) • [ofCrAnOp φ', ofCrAnOp φ]ₛ := by
+  rw [ofCrAnOp, ofCrAnOp, superCommute_eq_ι_superCommuteF,
     superCommuteF_ofCrAnOpF_ofCrAnOpF_symm]
   rfl
 
@@ -461,54 +470,54 @@ lemma superCommute_ofCrAnFieldOp_ofCrAnFieldOp_symm (φ φ' : 𝓕.CrAnFieldOp)
 
 -/
 
-lemma superCommute_ofCrAnFieldOpList_ofCrAnFieldOpList_eq_sum (φs φs' : List 𝓕.CrAnFieldOp) :
-    [ofCrAnFieldOpList φs, ofCrAnFieldOpList φs']ₛ =
+lemma superCommute_ofCrAnList_ofCrAnList_eq_sum (φs φs' : List 𝓕.CrAnFieldOp) :
+    [ofCrAnList φs, ofCrAnList φs']ₛ =
     ∑ (n : Fin φs'.length), 𝓢(𝓕 |>ₛ φs, 𝓕 |>ₛ φs'.take n) •
-    ofCrAnFieldOpList (φs'.take n) * [ofCrAnFieldOpList φs, ofCrAnFieldOp (φs'.get n)]ₛ *
-    ofCrAnFieldOpList (φs'.drop (n + 1)) := by
+    ofCrAnList (φs'.take n) * [ofCrAnList φs, ofCrAnOp (φs'.get n)]ₛ *
+    ofCrAnList (φs'.drop (n + 1)) := by
   conv_lhs =>
-    rw [ofCrAnFieldOpList, ofCrAnFieldOpList, superCommute_eq_ι_superCommuteF,
+    rw [ofCrAnList, ofCrAnList, superCommute_eq_ι_superCommuteF,
       superCommuteF_ofCrAnListF_ofCrAnListF_eq_sum]
   rw [map_sum]
   rfl
 
-lemma superCommute_ofCrAnFieldOp_ofCrAnFieldOpList_eq_sum (φ : 𝓕.CrAnFieldOp)
-    (φs' : List 𝓕.CrAnFieldOp) : [ofCrAnFieldOp φ, ofCrAnFieldOpList φs']ₛ =
+lemma superCommute_ofCrAnOp_ofCrAnList_eq_sum (φ : 𝓕.CrAnFieldOp)
+    (φs' : List 𝓕.CrAnFieldOp) : [ofCrAnOp φ, ofCrAnList φs']ₛ =
     ∑ (n : Fin φs'.length), 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φs'.take n) •
-    [ofCrAnFieldOp φ, ofCrAnFieldOp (φs'.get n)]ₛ * ofCrAnFieldOpList (φs'.eraseIdx n) := by
+    [ofCrAnOp φ, ofCrAnOp (φs'.get n)]ₛ * ofCrAnList (φs'.eraseIdx n) := by
   conv_lhs =>
-    rw [← ofCrAnFieldOpList_singleton, superCommute_ofCrAnFieldOpList_ofCrAnFieldOpList_eq_sum]
+    rw [← ofCrAnList_singleton, superCommute_ofCrAnList_ofCrAnList_eq_sum]
   congr
   funext n
   simp only [instCommGroup.eq_1, ofList_singleton, List.get_eq_getElem, Algebra.smul_mul_assoc]
   congr 1
-  rw [ofCrAnFieldOpList_singleton, superCommute_ofCrAnFieldOp_ofCrAnFieldOp_commute]
-  rw [mul_assoc, ← ofCrAnFieldOpList_append]
+  rw [ofCrAnList_singleton, superCommute_ofCrAnOp_ofCrAnOp_commute]
+  rw [mul_assoc, ← ofCrAnList_append]
   congr
   exact Eq.symm (List.eraseIdx_eq_take_drop_succ φs' ↑n)
 
-lemma superCommute_ofCrAnFieldOpList_ofFieldOpList_eq_sum (φs : List 𝓕.CrAnFieldOp)
-    (φs' : List 𝓕.FieldOp) : [ofCrAnFieldOpList φs, ofFieldOpList φs']ₛ =
+lemma superCommute_ofCrAnList_ofFieldOpList_eq_sum (φs : List 𝓕.CrAnFieldOp)
+    (φs' : List 𝓕.FieldOp) : [ofCrAnList φs, ofFieldOpList φs']ₛ =
     ∑ (n : Fin φs'.length), 𝓢(𝓕 |>ₛ φs, 𝓕 |>ₛ φs'.take n) •
-    ofFieldOpList (φs'.take n) * [ofCrAnFieldOpList φs, ofFieldOp (φs'.get n)]ₛ *
+    ofFieldOpList (φs'.take n) * [ofCrAnList φs, ofFieldOp (φs'.get n)]ₛ *
     ofFieldOpList (φs'.drop (n + 1)) := by
   conv_lhs =>
-    rw [ofCrAnFieldOpList, ofFieldOpList, superCommute_eq_ι_superCommuteF,
+    rw [ofCrAnList, ofFieldOpList, superCommute_eq_ι_superCommuteF,
       superCommuteF_ofCrAnListF_ofFieldOpListF_eq_sum]
   rw [map_sum]
   rfl
 
-lemma superCommute_ofCrAnFieldOp_ofFieldOpList_eq_sum (φ : 𝓕.CrAnFieldOp) (φs' : List 𝓕.FieldOp) :
-    [ofCrAnFieldOp φ, ofFieldOpList φs']ₛ =
+lemma superCommute_ofCrAnOp_ofFieldOpList_eq_sum (φ : 𝓕.CrAnFieldOp) (φs' : List 𝓕.FieldOp) :
+    [ofCrAnOp φ, ofFieldOpList φs']ₛ =
     ∑ (n : Fin φs'.length), 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φs'.take n) •
-    [ofCrAnFieldOp φ, ofFieldOp (φs'.get n)]ₛ * ofFieldOpList (φs'.eraseIdx n) := by
+    [ofCrAnOp φ, ofFieldOp (φs'.get n)]ₛ * ofFieldOpList (φs'.eraseIdx n) := by
   conv_lhs =>
-    rw [← ofCrAnFieldOpList_singleton, superCommute_ofCrAnFieldOpList_ofFieldOpList_eq_sum]
+    rw [← ofCrAnList_singleton, superCommute_ofCrAnList_ofFieldOpList_eq_sum]
   congr
   funext n
   simp only [instCommGroup.eq_1, ofList_singleton, List.get_eq_getElem, Algebra.smul_mul_assoc]
   congr 1
-  rw [ofCrAnFieldOpList_singleton, superCommute_ofCrAnFieldOp_ofFieldOp_commute]
+  rw [ofCrAnList_singleton, superCommute_ofCrAnOp_ofFieldOp_commute]
   rw [mul_assoc, ← ofFieldOpList_append]
   congr
   exact Eq.symm (List.eraseIdx_eq_take_drop_succ φs' ↑n)

HepLean/PerturbationTheory/FieldOpAlgebra/TimeOrder.lean

@@ -367,7 +367,14 @@ lemma ι_timeOrderF_eq_of_equiv (a b : 𝓕.FieldOpFreeAlgebra) (h : a ≈ b) :
   simp only [LinearMap.mem_ker, ← map_sub]
   exact ι_timeOrderF_zero_of_mem_ideal (a - b) h
 
-/-- Time ordering on `FieldOpAlgebra`. -/
+/-- For a field specification `𝓕`, `timeOrder` is the linear map
+
+`FieldOpAlgebra 𝓕 →ₗ[ℂ] FieldOpAlgebra 𝓕`
+
+defined as the decent of `ι ∘ₗ timeOrderF` from `FieldOpFreeAlgebra 𝓕` to `FieldOpAlgebra 𝓕`.
+This decent exists because `ι ∘ₗ timeOrderF` is well-defined on equivalence classes.
+
+The notation `𝓣(a)` is used for `timeOrder a`. -/
 noncomputable def timeOrder : FieldOpAlgebra 𝓕 →ₗ[ℂ] FieldOpAlgebra 𝓕 where
   toFun := Quotient.lift (ι.toLinearMap ∘ₗ timeOrderF) ι_timeOrderF_eq_of_equiv
   map_add' x y := by
@@ -423,8 +430,11 @@ lemma timeOrder_ofFieldOpList_singleton (φ : 𝓕.FieldOp) :
     𝓣(ofFieldOpList [φ]) = ofFieldOpList [φ] := by
   rw [ofFieldOpList, timeOrder_eq_ι_timeOrderF, timeOrderF_ofFieldOpListF_singleton]
 
-/-- The time order of a list `𝓣(φ₀…φₙ)` is equal to
-`𝓢(φᵢ,φ₀…φᵢ₋₁) • φᵢ * 𝓣(φ₀…φᵢ₋₁φᵢ₊₁φₙ)` where `φᵢ` is the maximal time field in `φ₀…φₙ`-/
+/-- For a field specification `𝓕`, the time order operator acting on a
+  list of `𝓕.FieldOp`, `𝓣(φ₀…φₙ)`, is equal to
+  `𝓢(φᵢ,φ₀…φᵢ₋₁) • φᵢ * 𝓣(φ₀…φᵢ₋₁φᵢ₊₁φₙ)` where `φᵢ` is the maximal time field in `φ₀…φₙ`.
+
+  The proof of this result ultimitley relies on basic properties of ordering and signs. -/
 lemma timeOrder_eq_maxTimeField_mul_finset (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) :
     𝓣(ofFieldOpList (φ :: φs)) = 𝓢(𝓕 |>ₛ maxTimeField φ φs, 𝓕 |>ₛ ⟨(eraseMaxTimeField φ φs).get,
       (Finset.univ.filter (fun x =>
@@ -435,9 +445,9 @@ lemma timeOrder_eq_maxTimeField_mul_finset (φ : 𝓕.FieldOp) (φs : List 𝓕.
 
 lemma timeOrder_superCommute_eq_time_mid {φ ψ : 𝓕.CrAnFieldOp}
     (hφψ : crAnTimeOrderRel φ ψ) (hψφ : crAnTimeOrderRel ψ φ) (a b : 𝓕.FieldOpAlgebra) :
-    𝓣(a * [ofCrAnFieldOp φ, ofCrAnFieldOp ψ]ₛ * b) =
-    [ofCrAnFieldOp φ, ofCrAnFieldOp ψ]ₛ * 𝓣(a * b) := by
-  rw [ofCrAnFieldOp, ofCrAnFieldOp]
+    𝓣(a * [ofCrAnOp φ, ofCrAnOp ψ]ₛ * b) =
+    [ofCrAnOp φ, ofCrAnOp ψ]ₛ * 𝓣(a * b) := by
+  rw [ofCrAnOp, ofCrAnOp]
   rw [superCommute_eq_ι_superCommuteF]
   obtain ⟨a, rfl⟩ := ι_surjective a
   obtain ⟨b, rfl⟩ := ι_surjective b
@@ -449,17 +459,17 @@ lemma timeOrder_superCommute_eq_time_mid {φ ψ : 𝓕.CrAnFieldOp}
 
 lemma timeOrder_superCommute_eq_time_left {φ ψ : 𝓕.CrAnFieldOp}
     (hφψ : crAnTimeOrderRel φ ψ) (hψφ : crAnTimeOrderRel ψ φ) (b : 𝓕.FieldOpAlgebra) :
-    𝓣([ofCrAnFieldOp φ, ofCrAnFieldOp ψ]ₛ * b) =
-    [ofCrAnFieldOp φ, ofCrAnFieldOp ψ]ₛ * 𝓣(b) := by
-  trans 𝓣(1 * [ofCrAnFieldOp φ, ofCrAnFieldOp ψ]ₛ * b)
+    𝓣([ofCrAnOp φ, ofCrAnOp ψ]ₛ * b) =
+    [ofCrAnOp φ, ofCrAnOp ψ]ₛ * 𝓣(b) := by
+  trans 𝓣(1 * [ofCrAnOp φ, ofCrAnOp ψ]ₛ * b)
   simp only [one_mul]
   rw [timeOrder_superCommute_eq_time_mid hφψ hψφ]
   simp
 
 lemma timeOrder_superCommute_neq_time {φ ψ : 𝓕.CrAnFieldOp}
     (hφψ : ¬ (crAnTimeOrderRel φ ψ ∧ crAnTimeOrderRel ψ φ)) :
-    𝓣([ofCrAnFieldOp φ, ofCrAnFieldOp ψ]ₛ) = 0 := by
-  rw [ofCrAnFieldOp, ofCrAnFieldOp]
+    𝓣([ofCrAnOp φ, ofCrAnOp ψ]ₛ) = 0 := by
+  rw [ofCrAnOp, ofCrAnOp]
   rw [superCommute_eq_ι_superCommuteF]
   rw [timeOrder_eq_ι_timeOrderF]
   trans ι (timeOrderF (1 * (superCommuteF (ofCrAnOpF φ)) (ofCrAnOpF ψ) * 1))

HepLean/PerturbationTheory/FieldOpAlgebra/Universality.lean

@@ -0,0 +1,98 @@
+/-
+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.FieldOpAlgebra.Basic
+/-!
+
+# Universality properties of FieldOpAlgebra
+
+-/
+
+namespace FieldSpecification
+open FieldOpFreeAlgebra
+open HepLean.List
+open FieldStatistic
+
+namespace FieldOpAlgebra
+variable {𝓕 : FieldSpecification}
+
+/-- For a field specification, `𝓕`, given an algebra `A` and a function `f : 𝓕.CrAnFieldOp → A`
+  such that the lift of `f` to `FreeAlgebra.lift ℂ f : FreeAlgebra ℂ 𝓕.CrAnFieldOp → A` is
+  zero on the ideal defining `𝓕.FieldOpAlgebra`, the corresponding map `𝓕.FieldOpAlgebra → A`.
+-/
+def universalLiftMap {A : Type} [Semiring A] [Algebra ℂ A] (f : 𝓕.CrAnFieldOp → A)
+    (h1 : ∀ a ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet, FreeAlgebra.lift ℂ f a = 0) :
+    FieldOpAlgebra 𝓕 → A :=
+  Quotient.lift (FreeAlgebra.lift ℂ f) (by
+    intro a b h
+    rw [equiv_iff_exists_add] at h
+    obtain ⟨a, rfl, ha⟩ := h
+    simp only [map_add]
+    rw [h1 a ha]
+    simp)
+
+@[simp]
+lemma universalLiftMap_ι {A : Type} [Semiring A] [Algebra ℂ A] (f : 𝓕.CrAnFieldOp → A)
+    (h1 : ∀ a ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet, FreeAlgebra.lift ℂ f a = 0) :
+    universalLiftMap f h1 (ι a) = FreeAlgebra.lift ℂ f a := by rfl
+
+/-- For a field specification, `𝓕`, given an algebra `A` and a function `f : 𝓕.CrAnFieldOp → A`
+  such that the lift of `f` to `FreeAlgebra.lift ℂ f : FreeAlgebra ℂ 𝓕.CrAnFieldOp → A` is
+  zero on the ideal defining `𝓕.FieldOpAlgebra`, the corresponding algebra map
+  `𝓕.FieldOpAlgebra → A`.
+-/
+def universalLift {A : Type} [Semiring A] [Algebra ℂ A] (f : 𝓕.CrAnFieldOp → A)
+    (h1 : ∀ a ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet, FreeAlgebra.lift ℂ f a = 0) :
+    FieldOpAlgebra 𝓕 →ₐ[ℂ] A where
+  toFun := universalLiftMap f h1
+  map_one' := by
+    rw [show 1 = ι (𝓕 := 𝓕) 1 from rfl, universalLiftMap_ι]
+    simp
+  map_mul' x y := by
+    obtain ⟨x, rfl⟩ := ι_surjective x
+    obtain ⟨y, rfl⟩ := ι_surjective y
+    simp [← map_mul]
+  map_zero' := by
+    simp only
+    rw [show 0 = ι (𝓕 := 𝓕) 0 from rfl, universalLiftMap_ι]
+    simp
+  map_add' x y := by
+    obtain ⟨x, rfl⟩ := ι_surjective x
+    obtain ⟨y, rfl⟩ := ι_surjective y
+    simp [← map_add]
+  commutes' r := by
+    simp only
+    rw [Algebra.algebraMap_eq_smul_one r]
+    rw [show r • 1 = ι (𝓕 := 𝓕) (r • 1) from rfl, universalLiftMap_ι]
+    simp only [map_smul, map_one]
+    exact Eq.symm (Algebra.algebraMap_eq_smul_one r)
+
+@[simp]
+lemma universalLift_ι {A : Type} [Semiring A] [Algebra ℂ A] (f : 𝓕.CrAnFieldOp → A)
+    (h1 : ∀ a ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet, FreeAlgebra.lift ℂ f a = 0) :
+    universalLift f h1 (ι a) = FreeAlgebra.lift ℂ f a := by rfl
+
+/--
+For a field specification, `𝓕`, the algebra `𝓕.FieldOpAlgebra` satifies the following universal
+property. Let `f : 𝓕.CrAnFieldOp → A` be a function and `g : 𝓕.FieldOpFreeAlgebra →ₐ[ℂ] A`
+the universal lift of that function associated with the free algebra `𝓕.FieldOpFreeAlgebra`.
+If `g` is zero on the ideal defining `𝓕.FieldOpAlgebra`, then there is a unique
+algebra map `g' : FieldOpAlgebra 𝓕 →ₐ[ℂ] A` such that `g' ∘ ι = g`.
+-/
+lemma universality {A : Type} [Semiring A] [Algebra ℂ A] (f : 𝓕.CrAnFieldOp → A)
+    (h1 : ∀ a ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet, FreeAlgebra.lift ℂ f a = 0) :
+    ∃! g : FieldOpAlgebra 𝓕 →ₐ[ℂ] A, g ∘ ι = FreeAlgebra.lift ℂ f := by
+  use universalLift f h1
+  simp only
+  apply And.intro
+  · ext a
+    simp
+  · intro g hg
+    ext a
+    obtain ⟨a, rfl⟩ := ι_surjective a
+    simpa using congrFun hg a
+
+end FieldOpAlgebra
+end FieldSpecification

HepLean/PerturbationTheory/FieldOpAlgebra/WickTerm.lean

@@ -31,7 +31,7 @@ def wickTerm {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) :
 
 /-- The Wick term for the empty contraction of the empty list is `1`. -/
 @[simp]
-lemma wickTerm_empty_nil  :
+lemma wickTerm_empty_nil :
     wickTerm (empty (n := ([] : List 𝓕.FieldOp).length)) = 1 := by
   rw [wickTerm]
   simp [sign_empty]
@@ -52,7 +52,7 @@ lemma wickTerm_insert_none (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
     • (φsΛ.sign • φsΛ.timeContract * 𝓝(ofFieldOpList (φ :: [φsΛ]ᵘᶜ))) := by
   rw [wickTerm]
   by_cases hg : GradingCompliant φs φsΛ
-  · rw [normalOrder_uncontracted_none, sign_insert_none  _ _ _ _ hg]
+  · rw [normalOrder_uncontracted_none, sign_insert_none _ _ _ _ hg]
     simp only [Nat.succ_eq_add_one, timeContract_insert_none, instCommGroup.eq_1,
       Algebra.mul_smul_comm, Algebra.smul_mul_assoc, smul_smul]
     congr 1
@@ -99,8 +99,8 @@ is equal the product of
 
 The proof of this result relies on
 - `timeContract_insert_some_of_not_lt`
- and `timeContract_insert_some_of_lt` to rewrite time
- contractions.
+  and `timeContract_insert_some_of_lt` to rewrite time
+  contractions.
 - `normalOrder_uncontracted_some` to rewrite normal orderings.
 - `sign_insert_some_of_not_lt` and `sign_insert_some_of_lt` to rewrite signs.
 -/
@@ -173,7 +173,7 @@ all files in `φ₀…φᵢ₋₁` have time strictly less then `φ`. Then
 where the sum is over all `k` in `Option φsΛ.uncontracted` (so either `none` or `some k`).
 
 The proof of proceeds as follows:
-- `ofFieldOp_mul_normalOrder_ofFieldOpList_eq_sum` is used to expand  `φ 𝓝([φsΛ]ᵘᶜ)` as
+- `ofFieldOp_mul_normalOrder_ofFieldOpList_eq_sum` is used to expand `φ 𝓝([φsΛ]ᵘᶜ)` as
   a sum over `k` in `Option φsΛ.uncontracted` of terms involving `[φ, φs[k]]` etc.
 - Then `wickTerm_insert_none` and `wickTerm_insert_some` are used to equate terms.
 -/

HepLean/PerturbationTheory/FieldOpAlgebra/WicksTheoremNormal.lean

@@ -169,11 +169,11 @@ lemma wicks_theorem_normal_order_empty : 𝓣(𝓝(ofFieldOpList [])) =
   simp only [Finset.univ_unique, PUnit.default_eq_unit, List.length_nil, Equiv.coe_fn_symm_mk,
     sign_empty, timeContract_empty, OneMemClass.coe_one, one_smul, uncontractedListGet_empty,
     one_mul, Finset.sum_const, Finset.card_singleton, e2]
-  have h1' : ofFieldOpList (𝓕 := 𝓕) [] = ofCrAnFieldOpList [] := by rfl
+  have h1' : ofFieldOpList (𝓕 := 𝓕) [] = ofCrAnList [] := by rfl
   rw [h1']
-  rw [normalOrder_ofCrAnFieldOpList]
+  rw [normalOrder_ofCrAnList]
   simp only [normalOrderSign_nil, normalOrderList_nil, one_smul]
-  rw [ofCrAnFieldOpList, timeOrder_eq_ι_timeOrderF]
+  rw [ofCrAnList, timeOrder_eq_ι_timeOrderF]
   rw [timeOrderF_ofCrAnListF]
   simp
 

HepLean/PerturbationTheory/FieldOpFreeAlgebra/Basic.lean

@@ -35,11 +35,7 @@ namespace FieldSpecification
 variable {𝓕 : FieldSpecification}
 
 /-- For a field specification `𝓕`, the algebra `𝓕.FieldOpFreeAlgebra` is
-  the free algebra generated by creation and annihilation parts of field operators defined in
-  `𝓕.CrAnFieldOp`.
-  It represents the algebra containing all possible products and linear combinations
-  of creation and annihilation parts of field operators, without imposing any conditions.
--/
+  the free algebra generated by `𝓕.CrAnFieldOp`. -/
 abbrev FieldOpFreeAlgebra (𝓕 : FieldSpecification) : Type := FreeAlgebra ℂ 𝓕.CrAnFieldOp
 
 namespace FieldOpFreeAlgebra
@@ -55,6 +51,25 @@ remark naming_convention := "
 def ofCrAnOpF (φ : 𝓕.CrAnFieldOp) : FieldOpFreeAlgebra 𝓕 :=
   FreeAlgebra.ι ℂ φ
 
+/--
+The algebra `𝓕.FieldOpFreeAlgebra` satisfies the universal property that for any other algebra
+  `A` (e.g. the operator algebra of the theory) with a map `f : 𝓕.CrAnFieldOp → A` (e.g.
+  the inclusion of the creation and annihilation parts of field operators into the
+  operator algebra) there is a unqiue algebra map `g : 𝓕.FieldOpFreeAlgebra → A`
+  such that `g ∘ ofCrAnOpF = f`.
+
+  The unique `g` is given by `FreeAlgebra.lift ℂ f`.
+-/
+lemma universality {A : Type} [Semiring A] [Algebra ℂ A] (f : 𝓕.CrAnFieldOp → A) :
+    ∃! g : FieldOpFreeAlgebra 𝓕 →ₐ[ℂ] A, g ∘ ofCrAnOpF = f := by
+  use FreeAlgebra.lift ℂ f
+  apply And.intro
+  · funext x
+    simp [ofCrAnOpF]
+  · intro g hg
+    ext x
+    simpa using congrFun hg x
+
 /-- For a field specification `𝓕`, `ofCrAnListF φs` of `𝓕.FieldOpFreeAlgebra` formed by a
   list `φs` of `𝓕.CrAnFieldOp`. For example for the list `[φ₁ᶜ, φ₂ᵃ, φ₃ᶜ]` we schematically
   get `φ₁ᶜφ₂ᵃφ₃ᶜ`. The set of all `ofCrAnListF φs` forms a basis of `FieldOpFreeAlgebra 𝓕`. -/
@@ -75,16 +90,21 @@ lemma ofCrAnListF_singleton (φ : 𝓕.CrAnFieldOp) :
 
 /-- For a field specification `𝓕`, the element of `𝓕.FieldOpFreeAlgebra` formed by a
   `𝓕.FieldOp` by summing over the creation and annihilation components of `𝓕.FieldOp`.
-  For example for `φ₁` an incoming asymptotic field operator we get `φ₁ᶜ`, and for `φ₁` a
-  position field operator we get `φ₁ᶜ + φ₁ᵃ`. -/
+  For example for `φ₁` an incoming asymptotic field operator we get
+  `ofCrAnOpF φ₁ᶜ`, and for `φ₁` a
+  position field operator we get `ofCrAnOpF φ₁ᶜ + ofCrAnOpF φ₁ᵃ`. -/
 def ofFieldOpF (φ : 𝓕.FieldOp) : FieldOpFreeAlgebra 𝓕 :=
   ∑ (i : 𝓕.fieldOpToCrAnType φ), ofCrAnOpF ⟨φ, i⟩
 
 /-- For a field specification `𝓕`, the element of `𝓕.FieldOpFreeAlgebra` formed by a
   list of `𝓕.FieldOp` by summing over the creation and annihilation components.
-  For example, `φ₁` and `φ₂` position states `[φ1, φ2]` gets sent to `(φ1ᶜ+ φ1ᵃ) * (φ2ᶜ+ φ2ᵃ)`. -/
+  For example, `φ₁` and `φ₂` position states `[φ1, φ2]` gets sent to
+  `(ofCrAnOpF φ1ᶜ + ofCrAnOpF φ1ᵃ) * (ofCrAnOpF φ2ᶜ + ofCrAnOpF φ2ᵃ)`. -/
 def ofFieldOpListF (φs : List 𝓕.FieldOp) : FieldOpFreeAlgebra 𝓕 := (List.map ofFieldOpF φs).prod
 
+remark notation_drop := "In doc-strings we will often drop explicit applications of `ofCrAnOpF`,
+`ofCrAnListF`, `ofFieldOpF`, and `ofFieldOpListF`"
+
 /-- Coercion from `List 𝓕.FieldOp` to `FieldOpFreeAlgebra 𝓕` through `ofFieldOpListF`. -/
 instance : Coe (List 𝓕.FieldOp) (FieldOpFreeAlgebra 𝓕) := ⟨ofFieldOpListF⟩
 
@@ -131,18 +151,18 @@ def crPartF : 𝓕.FieldOp → 𝓕.FieldOpFreeAlgebra := fun φ =>
   | FieldOp.outAsymp _ => 0
 
 @[simp]
-lemma crPartF_negAsymp (φ : 𝓕.Fields × Lorentz.Contr 4) :
+lemma crPartF_negAsymp (φ : (Σ f, 𝓕.AsymptoticLabel f) × (Fin 3 → ℝ)) :
     crPartF (FieldOp.inAsymp φ) = ofCrAnOpF ⟨FieldOp.inAsymp φ, ()⟩ := by
   simp [crPartF]
 
 @[simp]
-lemma crPartF_position (φ : 𝓕.Fields × SpaceTime) :
+lemma crPartF_position (φ : (Σ f, 𝓕.PositionLabel f) × SpaceTime) :
     crPartF (FieldOp.position φ) =
     ofCrAnOpF ⟨FieldOp.position φ, CreateAnnihilate.create⟩ := by
   simp [crPartF]
 
 @[simp]
-lemma crPartF_posAsymp (φ : 𝓕.Fields × Lorentz.Contr 4) :
+lemma crPartF_posAsymp (φ : (Σ f, 𝓕.AsymptoticLabel f) × (Fin 3 → ℝ)) :
     crPartF (FieldOp.outAsymp φ) = 0 := by
   simp [crPartF]
 
@@ -156,18 +176,18 @@ def anPartF : 𝓕.FieldOp → 𝓕.FieldOpFreeAlgebra := fun φ =>
   | FieldOp.outAsymp φ => ofCrAnOpF ⟨FieldOp.outAsymp φ, ()⟩
 
 @[simp]
-lemma anPartF_negAsymp (φ : 𝓕.Fields × Lorentz.Contr 4) :
+lemma anPartF_negAsymp (φ : (Σ f, 𝓕.AsymptoticLabel f) × (Fin 3 → ℝ)) :
     anPartF (FieldOp.inAsymp φ) = 0 := by
   simp [anPartF]
 
 @[simp]
-lemma anPartF_position (φ : 𝓕.Fields × SpaceTime) :
+lemma anPartF_position (φ : (Σ f, 𝓕.PositionLabel f) × SpaceTime) :
     anPartF (FieldOp.position φ) =
     ofCrAnOpF ⟨FieldOp.position φ, CreateAnnihilate.annihilate⟩ := by
   simp [anPartF]
 
 @[simp]
-lemma anPartF_posAsymp (φ : 𝓕.Fields × Lorentz.Contr 4) :
+lemma anPartF_posAsymp (φ : (Σ f, 𝓕.AsymptoticLabel f) × (Fin 3 → ℝ)) :
     anPartF (FieldOp.outAsymp φ) = ofCrAnOpF ⟨FieldOp.outAsymp φ, ()⟩ := by
   simp [anPartF]
 

HepLean/PerturbationTheory/FieldOpFreeAlgebra/Grading.lean

@@ -236,9 +236,10 @@ lemma directSum_eq_bosonic_plus_fermionic
     conv_lhs => rw [hx, hy]
     abel
 
-/-- For a field statistic `𝓕`, the algebra `𝓕.FieldOpFreeAlgebra` is graded by `FieldStatistic`.
-  Those `ofCrAnListF φs` for which `φs` has `bosonic` statistics form one part of the grading,
-  whilst those where `φs` has `fermionic` statistics form the other part of the grading. -/
+/-- For a field specification `𝓕`, the algebra `𝓕.FieldOpFreeAlgebra` is graded by `FieldStatistic`.
+  Those `ofCrAnListF φs` for which `φs` has an overall `bosonic` statistic span `bosonic`
+  submodule, whilst those `ofCrAnListF φs` for which `φs` has an overall `fermionic` statistic span
+  the `fermionic` submodule. -/
 instance fieldOpFreeAlgebraGrade :
     GradedAlgebra (A := 𝓕.FieldOpFreeAlgebra) statisticSubmodule where
   one_mem := by

HepLean/PerturbationTheory/FieldOpFreeAlgebra/NormalOrder.lean

@@ -27,11 +27,12 @@ namespace FieldOpFreeAlgebra
 
 noncomputable section
 
-/-- The linear map on the free creation and annihlation
-  algebra defined as the map taking
-  a list of CrAnFieldOp to the normal-ordered list of states multiplied by
-  the sign corresponding to the number of fermionic-fermionic
-  exchanges done in ordering. -/
+/-- For a field specification `𝓕`, `normalOrderF` is the linera map
+  `FieldOpFreeAlgebra 𝓕 →ₗ[ℂ] FieldOpFreeAlgebra 𝓕`
+  defined by its action on the basis `ofCrAnListF φs`, taking `ofCrAnListF φs` to
+  `normalOrderSign φs • ofCrAnListF (normalOrderList φs)`.
+
+  The notation `𝓝ᶠ(a)` is used for `normalOrderF a`. -/
 def normalOrderF : FieldOpFreeAlgebra 𝓕 →ₗ[ℂ] FieldOpFreeAlgebra 𝓕 :=
   Basis.constr ofCrAnListFBasis ℂ fun φs =>
   normalOrderSign φs • ofCrAnListF (normalOrderList φs)

HepLean/PerturbationTheory/FieldOpFreeAlgebra/SuperCommute.lean

@@ -24,10 +24,11 @@ namespace FieldOpFreeAlgebra
 open FieldStatistic
 
 /-- For a field specification `𝓕`, the super commutator `superCommuteF` is defined as the linear
-  map `𝓕.FieldOpFreeAlgebra →ₗ[ℂ] 𝓕.FieldOpFreeAlgebra →ₗ[ℂ] 𝓕.FieldOpFreeAlgebra` such that
-  `superCommuteF (φ₀ᶜ…φₙᵃ) (φ₀'ᶜ…φₙ'ᶜ)` is equal to
-  `φ₀ᶜ…φₙᵃ * φ₀'ᶜ…φₙ'ᶜ - 𝓢(φ₀ᶜ…φₙᵃ, φ₀'ᶜ…φₙ'ᶜ) φ₀'ᶜ…φₙ'ᶜ * φ₀ᶜ…φₙᵃ`.
-  The notation `[a, b]ₛca` is used for this super commutator. -/
+  map `𝓕.FieldOpFreeAlgebra →ₗ[ℂ] 𝓕.FieldOpFreeAlgebra →ₗ[ℂ] 𝓕.FieldOpFreeAlgebra`
+  which on the lists `φs` and `φs'` of `𝓕.CrAnFieldOp` gives
+  `superCommuteF φs φs' = φs * φs' - 𝓢(φs, φs') • φs' * φs`.
+
+  The notation `[a, b]ₛca` can be used for `superCommuteF a b`. -/
 noncomputable def superCommuteF : 𝓕.FieldOpFreeAlgebra →ₗ[ℂ] 𝓕.FieldOpFreeAlgebra →ₗ[ℂ]
     𝓕.FieldOpFreeAlgebra :=
   Basis.constr ofCrAnListFBasis ℂ fun φs =>
@@ -404,9 +405,12 @@ lemma superCommuteF_ofCrAnListF_ofFieldOpListF_cons (φ : 𝓕.FieldOp) (φs : L
   simp [mul_comm]
 
 /--
-Within the creation and annihilation algebra, we have that
-`[φᶜᵃs, φᶜᵃ₀ … φᶜᵃₙ]ₛca = ∑ i, sᵢ • φᶜᵃs₀ … φᶜᵃᵢ₋₁ * [φᶜᵃs, φᶜᵃᵢ]ₛca * φᶜᵃᵢ₊₁ … φᶜᵃₙ`
-where `sᵢ` is the exchange sign for `φᶜᵃs` and `φᶜᵃs₀ … φᶜᵃᵢ₋₁`.
+For a field specification `𝓕`, and to lists `φs = φ₀…φₙ` and `φs'` of `𝓕.CrAnFieldOp`
+the following super commutation relation holds:
+
+`[φs', φ₀…φₙ]ₛca = ∑ i, 𝓢(φs', φ₀…φᵢ₋₁) • φ₀…φᵢ₋₁ * [φs', φᵢ]ₛca * φᵢ₊₁ … φₙ`
+
+The proof of this relation is via induction on the length of `φs`.
 -/
 lemma superCommuteF_ofCrAnListF_ofCrAnListF_eq_sum (φs : List 𝓕.CrAnFieldOp) :
     (φs' : List 𝓕.CrAnFieldOp) → [ofCrAnListF φs, ofCrAnListF φs']ₛca =

HepLean/PerturbationTheory/FieldOpFreeAlgebra/TimeOrder.lean

@@ -26,9 +26,12 @@ open HepLean.List
 
 -/
 
-/-- Time ordering for the `FieldOpFreeAlgebra` defined by taking
+/-- For a field specification `𝓕`, `timeOrderF` is the linear map
+  `FieldOpFreeAlgebra 𝓕 →ₗ[ℂ] FieldOpFreeAlgebra 𝓕`
+  defined by its action on the basis `ofCrAnListF φs`, taking
   `ofCrAnListF φs` to `crAnTimeOrderSign φs • ofCrAnListF (crAnTimeOrderList φs)`.
-  The notation `𝓣ᶠ(a)` is used for the time-ordering of `a : FieldOpFreeAlgebra`. -/
+
+  The notation `𝓣ᶠ(a)` is used for `timeOrderF a` -/
 def timeOrderF : FieldOpFreeAlgebra 𝓕 →ₗ[ℂ] FieldOpFreeAlgebra 𝓕 :=
   Basis.constr ofCrAnListFBasis ℂ fun φs =>
   crAnTimeOrderSign φs • ofCrAnListF (crAnTimeOrderList φs)

HepLean/PerturbationTheory/FieldSpecification/Basic.lean

@@ -23,62 +23,103 @@ From each field we can create three different types of `FieldOp`.
 
 These states carry the same field statistic as the field they are derived from.
 
+## Some references
+
+- https://particle.physics.ucdavis.edu/modernsusy/slides/slideimages/spinorfeynrules.pdf
+
 -/
 
-remark fieldSpecification_intro := "The raw ingredients of a field theory are:
-  - The specification of the fields.
-  - Whether each field is a boson or a fermion.
-  - Vertices present in the Lagrangian.
-  - The coefficent of each vertex.
-
-  We call the first two of these ingredients the `FieldSpecification` of the theory. "
-
-/-- A field specification is a type, `Fields`, elements of which are fields
-  present in a theory, and a map `statistics` from `Fields` to `FieldStatistic` which
-  identifies each field as a boson or a fermion. -/
+/--
+The structure `FieldSpecification` is defined to have the following content:
+  - A type `Field` whose elements are the constituent fields of the theory.
+  - For every field `f` in `Field`, a type `PositionLabel f` whose elements label the different
+    position operators associated with the field `f`. For example,
+    - For `f` a *real-scalar field*, `PositionLabel f` will have a unique element.
+    - For `f` a *complex-scalar field*, `PositionLabel f` will have two elements, one for the field
+      operator and one for its conjugate.
+    - For `f` a *Dirac fermion*, `PositionLabel f` will have eight elements, one for each Lorentz
+      index of the field and its conjugate.
+    - For `f` a *Weyl fermion*, `PositionLabel f` will have four elements, one for each Lorentz
+      index of the field and its conjugate.
+  - For every field `f` in `Field`, a type `AsymptoticLabel f` whose elements label the different
+    asymptotic based field operators associated with the field `f`. For example,
+    - For `f` a *real-scalar field*, `AsymptoticLabel f` will have a unique element.
+    - For `f` a *complex-scalar field*, `AsymptoticLabel f` will have two elements, one for the
+      field operator and one for its conjugate.
+    - For `f` a *Dirac fermion*, `AsymptoticLabel f` will have four elements, two for each spin.
+    - For `f` a *Weyl fermion*, `AsymptoticLabel f` will have two elements, one for each spin.
+  - For each field `f` in `Field`, a field statistic `statistic f` which classifying `f` as either
+    `bosonic` or `fermionic`.
+-/
 structure FieldSpecification where
-  /-- The type of fields. This also includes anti-states. -/
-  Fields : Type
-  /-- The specification if a field is bosonic or fermionic. -/
-  statistics : Fields → FieldStatistic
+  /-- A type whose elements are the constituent fields of the theory. -/
+  Field : Type
+  /-- For every field `f` in `Field`, the type `PositionLabel f` has elements that label the
+    different position operators associated with the field `f`. -/
+  PositionLabel : Field → Type
+  /-- For every field `f` in `Field`, the type `AsymptoticLabel f` has elements that label
+    the different asymptotic based field operators associated with the field `f`. -/
+  AsymptoticLabel : Field → Type
+  /-- For every field `f` in `Field`, the field statistic `statistic f` classifies `f` as either
+    `bosonic` or `fermionic`. -/
+  statistic : Field → FieldStatistic
 
 namespace FieldSpecification
 variable (𝓕 : FieldSpecification)
 
 /-- For a field specification `𝓕`, the type `𝓕.FieldOp` is defined such that every element of
   `FieldOp` corresponds either to:
-- an incoming asymptotic field operator `.inAsymp` specified by a field and a `4`-momentum.
-- an position operator `.position` specified by a field and a point in spacetime.
-- an outgoing asymptotic field operator `.outAsymp` specified by a field and a `4`-momentum.
+- an incoming asymptotic field operator `.inAsymp` which is specified by
+  a field `f` in `𝓕.Field`, an element of `AsymptoticLabel f` (which specifies exactly
+  which asymptotic field operator associated with `f`) and a `3`-momentum.
+- an position operator `.position` which is specified by
+  a field `f` in `𝓕.Field`, an element of `PositionLabel f` (which specifies exactly
+  which position field operator associated with `f`) and a element of `SpaceTime`.
+- an outgoing asymptotic field operator `.outAsymp` which is specified by
+  a field `f` in `𝓕.Field`, an element of `AsymptoticLabel f` (which specifies exactly
+  which asymptotic field operator associated with `f`) and a `3`-momentum.
+
+Note the use of `3`-momentum here rather then `4`-momentum. This is because the asymptotic states
+have on-shell momenta.
 -/
 inductive FieldOp (𝓕 : FieldSpecification) where
-  | inAsymp : 𝓕.Fields × Lorentz.Contr 4 → 𝓕.FieldOp
-  | position : 𝓕.Fields × SpaceTime → 𝓕.FieldOp
-  | outAsymp : 𝓕.Fields × Lorentz.Contr 4 → 𝓕.FieldOp
-
-/-- Taking a field operator to its underlying field. -/
-def fieldOpToField : 𝓕.FieldOp → 𝓕.Fields
-  | FieldOp.inAsymp φ => φ.1
-  | FieldOp.position φ => φ.1
-  | FieldOp.outAsymp φ => φ.1
+  | inAsymp : (Σ f, 𝓕.AsymptoticLabel f) × (Fin 3 → ℝ) → 𝓕.FieldOp
+  | position : (Σ f, 𝓕.PositionLabel f) × SpaceTime → 𝓕.FieldOp
+  | outAsymp : (Σ f, 𝓕.AsymptoticLabel f) × (Fin 3 → ℝ) → 𝓕.FieldOp
 
 /-- The bool on `FieldOp` which is true only for position field operator. -/
 def statesIsPosition : 𝓕.FieldOp → Bool
   | FieldOp.position _ => true
   | _ => false
 
-/-- The statistics associated to a field operator. -/
-def statesStatistic : 𝓕.FieldOp → FieldStatistic := 𝓕.statistics ∘ 𝓕.fieldOpToField
+/-- For a field specification `𝓕`, `𝓕.fieldOpToField` is defined to take field operators
+  to their underlying field. -/
+def fieldOpToField : 𝓕.FieldOp → 𝓕.Field
+  | FieldOp.inAsymp (f, _) => f.1
+  | FieldOp.position (f, _) => f.1
+  | FieldOp.outAsymp (f, _) => f.1
 
-/-- The field statistics associated with a field operator. -/
-scoped[FieldSpecification] notation 𝓕 "|>ₛ" φ => statesStatistic 𝓕 φ
+/-- For a field specification `𝓕`, and an element `φ` of `𝓕.FieldOp`.
+  The field statistic `fieldOpStatistic φ` is defined to be the statistic associated with
+  the field underlying `φ`.
 
-/-- The field statistics associated with a list field operators. -/
+  The following notation is used in relation to `fieldOpStatistic`:
+- For `φ` an element of `𝓕.FieldOp`, `𝓕 |>ₛ φ` is `fieldOpStatistic φ`.
+- For `φs` a list of `𝓕.FieldOp`, `𝓕 |>ₛ φs` is the product of `fieldOpStatistic φ` over
+  the list `φs`.
+- For a function `f : Fin n → 𝓕.FieldOp` and a finset `a` of `Fin n`, `𝓕 |>ₛ ⟨f, a⟩` is the
+  product of `fieldOpStatistic (f i)` for all `i ∈ a`. -/
+def fieldOpStatistic : 𝓕.FieldOp → FieldStatistic := 𝓕.statistic ∘ 𝓕.fieldOpToField
+
+@[inherit_doc fieldOpStatistic]
+scoped[FieldSpecification] notation 𝓕 "|>ₛ" φ => fieldOpStatistic 𝓕 φ
+
+@[inherit_doc fieldOpStatistic]
 scoped[FieldSpecification] notation 𝓕 "|>ₛ" φ => FieldStatistic.ofList
-    (statesStatistic 𝓕) φ
+    (fieldOpStatistic 𝓕) φ
 
-/-- The field statistic associated with a finite set-/
+@[inherit_doc fieldOpStatistic]
 scoped[FieldSpecification] notation 𝓕 "|>ₛ" "⟨" f ","a "⟩"=> FieldStatistic.ofFinset
-    (statesStatistic 𝓕) f a
+    (fieldOpStatistic 𝓕) f a
 
 end FieldSpecification

HepLean/PerturbationTheory/FieldSpecification/CrAnFieldOp.lean

@@ -63,14 +63,15 @@ def fieldOpToCreateAnnihilateTypeCongr : {i j : 𝓕.FieldOp} → i = j →
   | _, _, rfl => Equiv.refl _
 
 /--
-For a field specification `𝓕`, the type `𝓕.CrAnFieldOp` is defined such that every element
-corresponds to
-- an incoming asymptotic field operator `.inAsymp` and the unique element of `Unit`,
-  corresponding to the statement that an `inAsymp` state is a creation operator.
-- a position operator `.position` and an element of `CreateAnnihilate`,
-  corresponding to either the creation part or the annihilation part of a position operator.
-- an outgoing asymptotic field operator `.outAsymp` and the unique element of `Unit`,
-  corresponding to the statement that an `outAsymp` state is an annihilation operator.
+For a field specification `𝓕`, elements in `𝓕.CrAnFieldOp`, the type
+of creation and annihilation field operators, corresponds to
+- an incoming asymptotic field operator `.inAsymp` in `𝓕.FieldOp`.
+- a position operator `.position` in `𝓕.FieldOp` and an element of
+  `CreateAnnihilate` specifying the creation or annihilation part of that position operator.
+- an outgoing asymptotic field operator `.outAsymp` in `𝓕.FieldOp`.
+
+Note that the incoming and outgoing asymptotic field operators are implicitly creation and
+annihilation operators respectively.
 -/
 def CrAnFieldOp : Type := Σ (s : 𝓕.FieldOp), 𝓕.fieldOpToCrAnType s
 
@@ -89,15 +90,23 @@ def crAnFieldOpToCreateAnnihilate : 𝓕.CrAnFieldOp → CreateAnnihilate
   | ⟨FieldOp.position _, CreateAnnihilate.annihilate⟩ => CreateAnnihilate.annihilate
   | ⟨FieldOp.outAsymp _, _⟩ => CreateAnnihilate.annihilate
 
-/-- Takes a `CrAnFieldOp` state to its corresponding fields statistic (bosonic or fermionic). -/
-def crAnStatistics : 𝓕.CrAnFieldOp → FieldStatistic :=
-  𝓕.statesStatistic ∘ 𝓕.crAnFieldOpToFieldOp
+/-- For a field specification `𝓕`, and an element `φ` in `𝓕.CrAnFieldOp`, the field
+  statistic `crAnStatistics φ` is defined to be the statistic associated with the field `𝓕.Field`
+  (or equivalently `𝓕.FieldOp`) underlying `φ`.
 
-/-- The field statistic of a `CrAnFieldOp`. -/
+  The following notation is used in relation to `crAnStatistics`:
+  - For `φ` an element of `𝓕.CrAnFieldOp`, `𝓕 |>ₛ φ` is `crAnStatistics φ`.
+  - For `φs` a list of `𝓕.CrAnFieldOp`, `𝓕 |>ₛ φs` is the product of `crAnStatistics φ` over
+    the list `φs`.
+-/
+def crAnStatistics : 𝓕.CrAnFieldOp → FieldStatistic :=
+  𝓕.fieldOpStatistic ∘ 𝓕.crAnFieldOpToFieldOp
+
+@[inherit_doc crAnStatistics]
 scoped[FieldSpecification] notation 𝓕 "|>ₛ" φ =>
     (crAnStatistics 𝓕) φ
 
-/-- The field statistic of a list of `CrAnFieldOp`s. -/
+@[inherit_doc crAnStatistics]
 scoped[FieldSpecification] notation 𝓕 "|>ₛ" φ => FieldStatistic.ofList
     (crAnStatistics 𝓕) φ
 
@@ -106,4 +115,18 @@ scoped[FieldSpecification] notation 𝓕 "|>ₛ" φ => FieldStatistic.ofList
 scoped[FieldSpecification] infixl:80 "|>ᶜ" =>
     crAnFieldOpToCreateAnnihilate
 
+remark notation_remark := "When working with a field specification `𝓕` we will use
+some notation within doc-strings and in code. The main notation used is:
+- In doc-strings when field statistics occur in exchange signs we may drop the `𝓕 |>ₛ _`.
+- In doc-strings we will often write lists of `FieldOp` or `CrAnFieldOp` `φs` as e.g. `φ₀…φₙ`,
+  which should be interpreted within the context in which it appears.
+- In doc-strings we may use e.g. `φᶜ` to indicate the creation part of an operator and
+  `φᵃ` to indicate the annihilation part of an operator.
+
+Some examples:
+- `𝓢(φ, φs)` corresponds to `𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φs)`
+- `φ₀…φᵢ₋₁φᵢ₊₁…φₙ` corresponds to a (given) list `φs = φ₀…φₙ` with the element at the `i`th position
+  removed.
+"
+
 end FieldSpecification

HepLean/PerturbationTheory/FieldSpecification/Examples.lean

@@ -1,40 +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.Basic
-/-!
-
-# Specific examples of field specifications
-
--/
-
-namespace FieldSpecification
-variable (𝓕 : FieldSpecification)
-
-/-- The Field specification corresponding to a single bosonic field.
-  The type of fields is the unit type, and the statistic of the unique element of the unit
-  type is bosonic. -/
-def singleBoson : FieldSpecification where
-  Fields := Unit
-  statistics := fun _ => FieldStatistic.bosonic
-
-/-- The Field specification corresponding to a single fermionic field.
-  The type of fields is the unit type, and the statistic of the unique element of the unit
-  type is fermionic. -/
-def singleFermion : FieldSpecification where
-  Fields := Unit
-  statistics := fun _ => FieldStatistic.fermionic
-
-/-- The Field specification corresponding to two bosonic fields and two fermionic fields.
-  The type of fields is `Fin 2 ⊕ Fin 2`, and the statistic of the two `.inl` (left) elements
-  is bosonic and the statistic of the two `.inr` (right) elements is fermionic. -/
-def doubleBosonDoubleFermion : FieldSpecification where
-  Fields := Fin 2 ⊕ Fin 2
-  statistics := fun b =>
-    match b with
-    | Sum.inl _ => FieldStatistic.bosonic
-    | Sum.inr _ => FieldStatistic.fermionic
-
-end FieldSpecification

HepLean/PerturbationTheory/FieldSpecification/NormalOrder.lean

@@ -14,13 +14,14 @@ import HepLean.PerturbationTheory.Koszul.KoszulSign
 namespace FieldSpecification
 variable {𝓕 : FieldSpecification}
 
-/-- The normal ordering relation on creation and annihlation operators.
-  For a list of creation and annihlation states, this relation is designed
-  to move all creation states to the left, and all annihlation operators to the right.
-  We have that `normalOrderRel φ1 φ2` is true if
-  - `φ1` is a creation operator
-  or
-  - `φ2` is an annihlate operator. -/
+/-- For a field specification `𝓕`, `𝓕.normalOrderRel` is a relation on `𝓕.CrAnFieldOp`
+  representing normal ordering. It is defined such that `𝓕.normalOrderRel φ₀ φ₁`
+  is true if one of the following is true
+  - `φ₀` is a creation operator
+  - `φ₁` is an annihilation.
+
+  Thus, colloquially `𝓕.normalOrderRel φ₀ φ₁` says the creation operators are 'less then'
+  annihilation operators. -/
 def normalOrderRel : 𝓕.CrAnFieldOp → 𝓕.CrAnFieldOp → Prop :=
   fun a b => CreateAnnihilate.normalOrder (𝓕 |>ᶜ a) (𝓕 |>ᶜ b)
 
@@ -42,9 +43,9 @@ instance (φ φ' : 𝓕.CrAnFieldOp) : Decidable (normalOrderRel φ φ') :=
 
 -/
 
-/-- The sign associated with putting a list of creation and annihlation states into normal order
-  (with the creation operators on the left).
-  We pick up a minus sign for every fermion paired crossed. -/
+/-- For a field speciication `𝓕`, and a list `φs` of `𝓕.CrAnFieldOp`, `𝓕.normalOrderSign φs` is the
+  sign corresponding to the number of `fermionic`-`fermionic` exchanges undertaken to normal-order
+  `φs` using the insertion sort algorithm. -/
 def normalOrderSign (φs : List 𝓕.CrAnFieldOp) : ℂ :=
   Wick.koszulSign 𝓕.crAnStatistics 𝓕.normalOrderRel φs
 
@@ -221,9 +222,12 @@ open FieldStatistic
 
 -/
 
-/-- The normal ordering of a list of creation and annihilation states.
-  To give some schematic. For example:
-  - `normalOrderList [φ1c, φ1a, φ2c, φ2a] = [φ1c, φ2c, φ1a, φ2a]`
+/-- For a field specification `𝓕`, and a list `φs` of `𝓕.CrAnFieldOp`,
+  `𝓕.normalOrderList φs` is the list `φs` normal-ordered using ther
+  insertion sort algorithm. It puts creation operators on the left and annihilation operators on
+  the right. For example:
+
+  `𝓕.normalOrderList [φ1c, φ1a, φ2c, φ2a] = [φ1c, φ2c, φ1a, φ2a]`
 -/
 def normalOrderList (φs : List 𝓕.CrAnFieldOp) : List 𝓕.CrAnFieldOp :=
   List.insertionSort 𝓕.normalOrderRel φs
@@ -339,10 +343,17 @@ lemma normalOrderList_eraseIdx_normalOrderEquiv {φs : List 𝓕.CrAnFieldOp} (n
   simp only [normalOrderList, normalOrderEquiv]
   rw [HepLean.List.eraseIdx_insertionSort_fin]
 
-lemma normalOrderSign_eraseIdx (φs : List 𝓕.CrAnFieldOp) (n : Fin φs.length) :
-    normalOrderSign (φs.eraseIdx n) = normalOrderSign φs *
-    𝓢(𝓕 |>ₛ (φs.get n), 𝓕 |>ₛ (φs.take n)) *
-    𝓢(𝓕 |>ₛ (φs.get n), 𝓕 |>ₛ ((normalOrderList φs).take (normalOrderEquiv n))) := by
+/-- For a field specification `𝓕`, a list `φs = φ₀…φₙ` of `𝓕.CrAnFieldOp` and an `i < φs.length`,
+  the following relation holds
+  `normalOrderSign (φ₀…φᵢ₋₁φᵢ₊₁…φₙ)` is equal to the product of
+  - `normalOrderSign φ₀…φₙ`,
+  - `𝓢(φᵢ, φ₀…φᵢ₋₁)` i.e. the sign needed to remove `φᵢ` from  `φ₀…φₙ`,
+  - `𝓢(φᵢ, _)` where `_` is the list of elements appearing before `φᵢ` after normal ordering. I.e.
+    the sign needed to insert `φᵢ` back into the normal-ordered list at the correct place. -/
+lemma normalOrderSign_eraseIdx (φs : List 𝓕.CrAnFieldOp) (i : Fin φs.length) :
+    normalOrderSign (φs.eraseIdx i) = normalOrderSign φs *
+    𝓢(𝓕 |>ₛ (φs.get i), 𝓕 |>ₛ (φs.take i)) *
+    𝓢(𝓕 |>ₛ (φs.get i), 𝓕 |>ₛ ((normalOrderList φs).take (normalOrderEquiv i))) := by
   rw [normalOrderSign, Wick.koszulSign_eraseIdx, ← normalOrderSign]
   rfl
 

HepLean/PerturbationTheory/FieldSpecification/TimeOrder.lean

@@ -126,7 +126,7 @@ lemma timeOrder_maxTimeField (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
   the state of greatest time to the left).
   We pick up a minus sign for every fermion paired crossed. -/
 def timeOrderSign (φs : List 𝓕.FieldOp) : ℂ :=
-  Wick.koszulSign 𝓕.statesStatistic 𝓕.timeOrderRel φs
+  Wick.koszulSign 𝓕.fieldOpStatistic 𝓕.timeOrderRel φs
 
 @[simp]
 lemma timeOrderSign_nil : timeOrderSign (𝓕 := 𝓕) [] = 1 := by
@@ -191,7 +191,17 @@ lemma timeOrderList_eq_maxTimeField_timeOrderList (φ : 𝓕.FieldOp) (φs : Lis
 
 -/
 
-/-- The time ordering relation on CrAnFieldOp. -/
+/-- For a field specification `𝓕`, `𝓕.crAnTimeOrderRel` is a relation on
+  `𝓕.CrAnFieldOp` representing time ordering.
+  It is defined as such that `𝓕.crAnTimeOrderRel φ₀ φ₁` is true if and only if one of the following
+  holds
+- `φ₀` is an *outgoing* asymptotic operator
+- `φ₁` is an *incoming* asymptotic field operator
+- `φ₀` and `φ₁` are both position field operators where
+  the `SpaceTime` point of `φ₀` has a time *greater* then or equal to that of `φ₁`.
+
+Thus, colloquially `𝓕.crAnTimeOrderRel φ₀ φ₁` if `φ₀` has time *greater* then or equal to `φ₁`.
+-/
 def crAnTimeOrderRel (a b : 𝓕.CrAnFieldOp) : Prop := 𝓕.timeOrderRel a.1 b.1
 
 /-- The relation `crAnTimeOrderRel` is decidable, but not computablly so due to
@@ -211,9 +221,10 @@ instance : IsTrans 𝓕.CrAnFieldOp 𝓕.crAnTimeOrderRel where
 lemma crAnTimeOrderRel_refl (φ : 𝓕.CrAnFieldOp) : crAnTimeOrderRel φ φ := by
   exact (IsTotal.to_isRefl (r := 𝓕.crAnTimeOrderRel)).refl φ
 
-/-- The sign associated with putting a list of `CrAnFieldOp` into time order (with
-  the state of greatest time to the left).
-  We pick up a minus sign for every fermion paired crossed. -/
+/-- For a field specification `𝓕`, and a list `φs` of `𝓕.CrAnFieldOp`,
+  `𝓕.crAnTimeOrderSign φs` is the sign corresponding to the number of `ferimionic`-`fermionic`
+  exchanges undertaken to time-order (i.e. order with respect to `𝓕.crAnTimeOrderRel`) `φs` using
+  the insertion sort algorithm. -/
 def crAnTimeOrderSign (φs : List 𝓕.CrAnFieldOp) : ℂ :=
   Wick.koszulSign 𝓕.crAnStatistics 𝓕.crAnTimeOrderRel φs
 
@@ -239,7 +250,8 @@ lemma crAnTimeOrderSign_swap_eq_time {φ ψ : 𝓕.CrAnFieldOp}
     crAnTimeOrderSign (φs ++ φ :: ψ :: φs') = crAnTimeOrderSign (φs ++ ψ :: φ :: φs') := by
   exact Wick.koszulSign_swap_eq_rel _ _ h1 h2 _ _
 
-/-- Sort a list of `CrAnFieldOp` based on `crAnTimeOrderRel`. -/
+/-- For a field specification `𝓕`, and a list `φs` of `𝓕.CrAnFieldOp`,
+  `𝓕.crAnTimeOrderList φs` is the list `φs` time-ordered using the insertion sort algorithm. -/
 def crAnTimeOrderList (φs : List 𝓕.CrAnFieldOp) : List 𝓕.CrAnFieldOp :=
   List.insertionSort 𝓕.crAnTimeOrderRel φs
 
@@ -347,7 +359,7 @@ lemma crAnTimeOrderList_swap_eq_time {φ ψ : 𝓕.CrAnFieldOp}
 lemma koszulSignInsert_crAnTimeOrderRel_crAnSection {φ : 𝓕.FieldOp} {ψ : 𝓕.CrAnFieldOp}
     (h : ψ.1 = φ) : {φs : List 𝓕.FieldOp} → (ψs : CrAnSection φs) →
     Wick.koszulSignInsert 𝓕.crAnStatistics 𝓕.crAnTimeOrderRel ψ ψs.1 =
-    Wick.koszulSignInsert 𝓕.statesStatistic 𝓕.timeOrderRel φ φs
+    Wick.koszulSignInsert 𝓕.fieldOpStatistic 𝓕.timeOrderRel φ φs
   | [], ⟨[], h⟩ => by
     simp [Wick.koszulSignInsert]
   | φ' :: φs, ⟨ψ' :: ψs, h1⟩ => by

HepLean/PerturbationTheory/FieldStatistics/Basic.lean

@@ -26,8 +26,13 @@ namespace FieldStatistic
 
 variable {𝓕 : Type}
 
-/-- Field statistics form a commuative group isomorphic to `ℤ₂` in which `bosonic` is the identity
-  and `fermionic` is the non-trivial element. -/
+/-- The type `FieldStatistic` carries an instance of a commuative group in which
+- `bosonic * bosonic = bosonic`
+- `bosonic * fermionic = fermionic`
+- `fermionic * bosonic = fermionic`
+- `fermionic * fermionic = bosonic`
+
+This group is isomorphic to `ℤ₂`. -/
 @[simp]
 instance : CommGroup FieldStatistic where
   one := bosonic

HepLean/PerturbationTheory/FieldStatistics/ExchangeSign.lean

@@ -24,11 +24,12 @@ namespace FieldStatistic
 
 variable {𝓕 : Type}
 
-/-- The exchange sign is the group homomorphism `FieldStatistic →* FieldStatistic →* ℂ`,
-  which on two field statistics `a` and `b` is defined to be
-  `-1` if both `a` and `b` are `fermionic` and `1` otherwise.
-  It corresponds to the sign that one picks up when swapping fields `φ₁φ₂ → φ₂φ₁` with
-  `φ₁` and `φ₂` of statistics `a` and `b` respectively.
+/-- The exchange sign, `exchangeSign`, is defined as the group homomorphism
+  `FieldStatistic →* FieldStatistic →* ℂ`,
+  for which `exchangeSign a b` is `-1` if both `a` and `b` are `fermionic` and `1` otherwise.
+  The exchange sign is sign one picks up on exchanging an operator or field `φ₁` of statistic `a`
+  with one `φ₂` of statistic `b`, i.e. `φ₁φ₂ → φ₂φ₁`.
+
   The notation `𝓢(a, b)` is used for the exchange sign of `a` and `b`. -/
 def exchangeSign : FieldStatistic →* FieldStatistic →* ℂ where
   toFun a :=

HepLean/PerturbationTheory/WickContraction/InsertAndContract.lean

@@ -32,7 +32,7 @@ open HepLean.Fin
   elements and contracting `φ` optionally with `j`.
 
   The notation `φsΛ ↩Λ φ i j` is used to denote `φsΛ.insertAndContract φ i j`. Thus,
-  `φsΛ ↩Λ φ i none` indicates the case when we insert `φ` into `φs` but do not contract it.  -/
+  `φsΛ ↩Λ φ i none` indicates the case when we insert `φ` into `φs` but do not contract it. -/
 def insertAndContract {φs : List 𝓕.FieldOp} (φ : 𝓕.FieldOp) (φsΛ : WickContraction φs.length)
     (i : Fin φs.length.succ) (j : Option φsΛ.uncontracted) :
     WickContraction (φs.insertIdx i φ).length :=

HepLean/PerturbationTheory/WickContraction/Sign/InsertSome.lean

@@ -856,7 +856,7 @@ lemma signInsertSome_mul_filter_contracted_of_not_lt (φ : 𝓕.FieldOp) (φs :
 
 /--
 For `k < i`, the sign of `φsΛ ↩Λ φ i (some k)` is equal to the product of
-- the sign associated with moving `φ` through the `φsΛ`-uncontracted  fields in `φ₀…φₖ`,
+- the sign associated with moving `φ` through the `φsΛ`-uncontracted fields in `φ₀…φₖ`,
 - the sign associated with moving `φ` through the fields in `φ₀…φᵢ₋₁`,
 - the sign of `φsΛ`.
 
@@ -877,10 +877,9 @@ lemma sign_insert_some_of_lt (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
   rw [mul_comm, ← mul_assoc]
   simp
 
-
 /--
 For `i ≤ k`, the sign of `φsΛ ↩Λ φ i (some k)` is equal to the product of
-- the sign associated with moving `φ` through the `φsΛ`-uncontracted  fields in `φ₀…φₖ₋₁`,
+- the sign associated with moving `φ` through the `φsΛ`-uncontracted fields in `φ₀…φₖ₋₁`,
 - the sign associated with moving `φ` through the fields in `φ₀…φᵢ₋₁`,
 - the sign of `φsΛ`.
 
@@ -903,13 +902,12 @@ lemma sign_insert_some_of_not_lt (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
 
 lemma sign_insert_some_zero (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
     (φsΛ : WickContraction φs.length) (k : φsΛ.uncontracted)
-    (hn : GradingCompliant φs φsΛ ∧ (𝓕|>ₛφ) = 𝓕|>ₛφs[k.1]):
-    (φsΛ ↩Λ φ 0 k).sign =  𝓢(𝓕|>ₛφ, 𝓕 |>ₛ ⟨φs.get, (φsΛ.uncontracted.filter (fun x => x < ↑k))⟩) *
+    (hn : GradingCompliant φs φsΛ ∧ (𝓕|>ₛφ) = 𝓕|>ₛφs[k.1]) :
+    (φsΛ ↩Λ φ 0 k).sign = 𝓢(𝓕|>ₛφ, 𝓕 |>ₛ ⟨φs.get, (φsΛ.uncontracted.filter (fun x => x < ↑k))⟩) *
     φsΛ.sign := by
   rw [sign_insert_some_of_not_lt]
   · simp
   · simp
   · exact hn
 
-
 end WickContraction

HepLean/PerturbationTheory/WickContraction/Sign/Join.lean

@@ -162,7 +162,7 @@ lemma join_singleton_left_signFinset_eq_filter {φs : List 𝓕.FieldOp}
     left
     rw [join_singleton_signFinset_eq_filter]
   rw [mul_comm]
-  exact (ofFinset_filter_mul_neg 𝓕.statesStatistic _ _ _).symm
+  exact (ofFinset_filter_mul_neg 𝓕.fieldOpStatistic _ _ _).symm
 
 /-- The difference in sign between `φsucΛ.sign` and the direct contribution of `φsucΛ` to
   `(join (singleton h) φsucΛ)`. -/
@@ -418,7 +418,7 @@ lemma join_sign_induction {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs
     exact join_uncontractedListGet (singleton hij) φsucΛ'
 
 /-- Let `φsΛ` be a grading compliant Wick contraction for `φs` and
-  `φsucΛ` a Wick contraction for `[φsΛ]ᵘᶜ`. Then  `(join φsΛ φsucΛ).sign = φsΛ.sign * φsucΛ.sign`.
+  `φsucΛ` a Wick contraction for `[φsΛ]ᵘᶜ`. Then `(join φsΛ φsucΛ).sign = φsΛ.sign * φsucΛ.sign`.
 
   This lemma manifests the fact that it does not matter which order contracted pairs are brought
   together when defining the sign of a contraction. -/

HepLean/PerturbationTheory/WickContraction/StaticContract.lean

@@ -85,7 +85,7 @@ lemma staticContract_insert_some_of_lt
     · simp
     simp only [smul_smul]
     congr 1
-    have h1 : ofList 𝓕.statesStatistic (List.take (↑(φsΛ.uncontractedIndexEquiv.symm k))
+    have h1 : ofList 𝓕.fieldOpStatistic (List.take (↑(φsΛ.uncontractedIndexEquiv.symm k))
         (List.map φs.get φsΛ.uncontractedList))
         = (𝓕 |>ₛ ⟨φs.get, (Finset.filter (fun x => x < k) φsΛ.uncontracted)⟩) := by
       simp only [ofFinset]

HepLean/PerturbationTheory/WickContraction/TimeContract.lean

@@ -97,7 +97,7 @@ lemma timeContract_insert_some_of_lt
     · simp
     simp only [smul_smul]
     congr 1
-    have h1 : ofList 𝓕.statesStatistic (List.take (↑(φsΛ.uncontractedIndexEquiv.symm k))
+    have h1 : ofList 𝓕.fieldOpStatistic (List.take (↑(φsΛ.uncontractedIndexEquiv.symm k))
         (List.map φs.get φsΛ.uncontractedList))
         = (𝓕 |>ₛ ⟨φs.get, (Finset.filter (fun x => x < k) φsΛ.uncontracted)⟩) := by
       simp only [ofFinset]
@@ -128,7 +128,7 @@ lemma timeContract_insert_some_of_not_lt
   rw [timeContract_of_not_timeOrderRel, timeContract_of_timeOrderRel]
   simp only [instCommGroup.eq_1, Algebra.smul_mul_assoc, smul_smul]
   congr
-  have h1 : ofList 𝓕.statesStatistic (List.take (↑(φsΛ.uncontractedIndexEquiv.symm k))
+  have h1 : ofList 𝓕.fieldOpStatistic (List.take (↑(φsΛ.uncontractedIndexEquiv.symm k))
       (List.map φs.get φsΛ.uncontractedList))
       = (𝓕 |>ₛ ⟨φs.get, (Finset.filter (fun x => x < k) φsΛ.uncontracted)⟩) := by
     simp only [ofFinset]

docs/CuratedNotes/PerturbationTheory.html

@@ -65,7 +65,9 @@ layout: default
   {% if entry.type == "name" %}
 
   <div style="background-color: #f5f5f5; padding: 10px; border-radius: 4px;">
-    <p> <a href = "{{ entry.link }}" style="font-weight: bold; color: #2c5282;">{{ entry.name }}</a>: {{ entry.docString | markdownify}}</p>
+    <p> <a href = "{{ entry.link }}" style="font-weight: bold; color: #2c5282;">{{ entry.name }}</a>:
+      {% if entry.status == "incomplete" %}🚧{% endif %}
+      {{ entry.docString | markdownify}}</p>
     <details class="code-block-container">
     <summary>Show Lean code:</summary>
     <pre style="background: none; margin: 0;"><code class="language-lean">{{ entry.declString }}</code></pre>

scripts/MetaPrograms/notes.lean

@@ -7,6 +7,7 @@ import HepLean.Meta.Basic
 import HepLean.Meta.Remark.Properties
 import HepLean.Meta.Notes.ToHTML
 import Mathlib.Lean.CoreM
+import HepLean
 /-!
 
 # Extracting notes from Lean files
@@ -15,21 +16,31 @@ import Mathlib.Lean.CoreM
 
 open Lean System Meta HepLean
 
+inductive NameStatus
+  | complete : NameStatus
+  | incomplete : NameStatus
+
+instance : ToString NameStatus where
+  toString
+    | NameStatus.complete => "complete"
+    | NameStatus.incomplete => "incomplete"
+
 inductive NotePart
   | h1 : String → NotePart
   | h2 : String → NotePart
   | p : String → NotePart
-  | name : Name → NotePart
+  | name : Name → NameStatus → NotePart
   | warning : String → NotePart
 
 structure DeclInfo where
   line : Nat
   fileName : Name
   name : Name
+  status : NameStatus
   declString : String
   docString : String
 
-def DeclInfo.ofName (n : Name) : MetaM DeclInfo := do
+def DeclInfo.ofName (n : Name) (ns : NameStatus): MetaM DeclInfo := do
   let line ← Name.lineNumber n
   let fileName ← Name.fileName n
   let declString ← Name.getDeclString n
@@ -38,6 +49,7 @@ def DeclInfo.ofName (n : Name) : MetaM DeclInfo := do
     line := line,
     fileName := fileName,
     name := n,
+    status := ns,
     declString := declString,
     docString := docString}
 
@@ -50,6 +62,7 @@ def DeclInfo.toYML (d : DeclInfo) : MetaM String := do
     name: {d.name}
     line: {d.line}
     fileName: {d.fileName}
+    status: \"{d.status}\"
     link: \"{link}\"
     docString: |
       {docStringIndent}
@@ -79,7 +92,7 @@ def NotePart.toYMLM : ((List String) × Nat × Nat) →  NotePart → MetaM ((Li
   - type: warning
     content: \"{s}\""
     return ⟨x.1 ++ [newString], x.2⟩
-  | x, NotePart.name n => do
+  | x, NotePart.name n s => do
   match (← RemarkInfo.IsRemark n) with
   | true =>
     let remarkInfo ← RemarkInfo.getRemarkInfo n
@@ -89,12 +102,13 @@ def NotePart.toYMLM : ((List String) × Nat × Nat) →  NotePart → MetaM ((Li
     let newString := s!"
   - type: remark
     name: \"{shortName}\"
+    status : \"{s}\"
     link: \"{Name.toGitHubLink remarkInfo.fileName remarkInfo.line}\"
     content: |
       {contentIndent}"
     return ⟨x.1 ++ [newString], x.2⟩
   | false =>
-  let newString ← (← DeclInfo.ofName n).toYML
+  let newString ← (← DeclInfo.ofName n s).toYML
   return ⟨x.1 ++ [newString], x.2⟩
 
 structure Note where
@@ -120,98 +134,114 @@ def perturbationTheory : Note where
     .warning "This note is a work in progress and is not finished. Use with caution.
       (5th Feb 2025)",
     .h1 "Introduction",
-    .name `FieldSpecification.wicks_theorem_context,
+    .name `FieldSpecification.wicks_theorem_context .incomplete,
     .p "In this note we walk through the important parts of the proof of Wick's theorem
       for both fermions and bosons,
       as it appears in HepLean. We start with some basic definitions.",
     .h1 "Field operators",
     .h2 "Field statistics",
-    .name `FieldStatistic,
-    .name `FieldStatistic.instCommGroup,
-    .name `FieldStatistic.exchangeSign,
+    .name ``FieldStatistic .complete,
+    .name ``FieldStatistic.instCommGroup .complete,
+    .name ``FieldStatistic.exchangeSign .complete,
     .h2 "Field specifications",
-    .name `fieldSpecification_intro,
-    .name `FieldSpecification,
+    .name ``FieldSpecification .complete,
     .h2 "Field operators",
-    .name `FieldSpecification.FieldOp,
-    .name `FieldSpecification.CrAnFieldOp,
+    .name ``FieldSpecification.FieldOp .complete,
+    .name ``FieldSpecification.fieldOpStatistic .complete,
+    .name ``CreateAnnihilate .complete,
+    .name ``FieldSpecification.CrAnFieldOp .complete,
+    .name ``FieldSpecification.crAnStatistics .complete,
+    .name `FieldSpecification.notation_remark .complete,
     .h2 "Field-operator free algebra",
-    .name `FieldSpecification.FieldOpFreeAlgebra,
-    .name `FieldSpecification.FieldOpFreeAlgebra.naming_convention,
-    .name `FieldSpecification.FieldOpFreeAlgebra.ofCrAnOpF,
-    .name `FieldSpecification.FieldOpFreeAlgebra.ofCrAnListF,
-    .name `FieldSpecification.FieldOpFreeAlgebra.ofFieldOpF,
-    .name `FieldSpecification.FieldOpFreeAlgebra.ofFieldOpListF,
-    .name `FieldSpecification.FieldOpFreeAlgebra.fieldOpFreeAlgebraGrade,
-    .name `FieldSpecification.FieldOpFreeAlgebra.superCommuteF,
-    .name `FieldSpecification.FieldOpFreeAlgebra.superCommuteF_ofCrAnListF_ofFieldOpListF_eq_sum,
+    .name ``FieldSpecification.FieldOpFreeAlgebra .complete,
+    .name `FieldSpecification.FieldOpFreeAlgebra.naming_convention .complete,
+    .name ``FieldSpecification.FieldOpFreeAlgebra.ofCrAnOpF .complete,
+    .name ``FieldSpecification.FieldOpFreeAlgebra.universality .complete,
+    .name ``FieldSpecification.FieldOpFreeAlgebra.ofCrAnListF .complete,
+    .name ``FieldSpecification.FieldOpFreeAlgebra.ofFieldOpF .complete,
+    .name ``FieldSpecification.FieldOpFreeAlgebra.ofFieldOpListF .complete,
+    .name `FieldSpecification.FieldOpFreeAlgebra.notation_drop .complete,
+    .name ``FieldSpecification.FieldOpFreeAlgebra.fieldOpFreeAlgebraGrade .complete,
+    .name ``FieldSpecification.FieldOpFreeAlgebra.superCommuteF .complete,
+    .name ``FieldSpecification.FieldOpFreeAlgebra.superCommuteF_ofCrAnListF_ofCrAnListF_eq_sum .complete,
     .h2 "Field-operator algebra",
-    .name `FieldSpecification.FieldOpAlgebra,
-    .name `FieldSpecification.FieldOpAlgebra.fieldOpAlgebraGrade,
-    .name `FieldSpecification.FieldOpAlgebra.superCommute,
+    .name ``FieldSpecification.FieldOpAlgebra .complete,
+    .name ``FieldSpecification.FieldOpAlgebra.ι .complete,
+    .name ``FieldSpecification.FieldOpAlgebra.universality .complete,
+    .name ``FieldSpecification.FieldOpAlgebra.ofCrAnOp .complete,
+    .name ``FieldSpecification.FieldOpAlgebra.ofCrAnList .complete,
+    .name ``FieldSpecification.FieldOpAlgebra.ofFieldOp .complete,
+    .name ``FieldSpecification.FieldOpAlgebra.ofCrAnList .complete,
+    .name `FieldSpecification.FieldOpAlgebra.notation_drop .complete,
+    .name ``FieldSpecification.FieldOpAlgebra.anPart .complete,
+    .name ``FieldSpecification.FieldOpAlgebra.crPart .complete,
+    .name ``FieldSpecification.FieldOpAlgebra.ofFieldOp_eq_crPart_add_anPart .complete,
+    .name ``FieldSpecification.FieldOpAlgebra.fieldOpAlgebraGrade .complete,
+    .name ``FieldSpecification.FieldOpAlgebra.superCommute .complete,
     .h1 "Time ordering",
-    .name `FieldSpecification.crAnTimeOrderRel,
-    .name `FieldSpecification.crAnTimeOrderSign,
-    .name `FieldSpecification.FieldOpFreeAlgebra.timeOrderF,
-    .name `FieldSpecification.FieldOpAlgebra.timeOrder,
-    .name `FieldSpecification.FieldOpAlgebra.timeOrder_eq_maxTimeField_mul_finset,
+    .name ``FieldSpecification.crAnTimeOrderRel .complete,
+    .name ``FieldSpecification.crAnTimeOrderList .complete,
+    .name ``FieldSpecification.crAnTimeOrderSign .complete,
+    .name ``FieldSpecification.FieldOpFreeAlgebra.timeOrderF .complete,
+    .name ``FieldSpecification.FieldOpAlgebra.timeOrder .complete,
+    .name ``FieldSpecification.FieldOpAlgebra.timeOrder_eq_maxTimeField_mul_finset .complete,
     .h1 "Normal ordering",
-    .name `FieldSpecification.normalOrderRel,
-    .name `FieldSpecification.normalOrderSign,
-    .name `FieldSpecification.FieldOpFreeAlgebra.normalOrderF,
-    .name `FieldSpecification.FieldOpAlgebra.normalOrder,
-    .h2 "Some lemmas",
-    .name `FieldSpecification.normalOrderSign_eraseIdx,
-    .name `FieldSpecification.FieldOpAlgebra.ofCrAnFieldOp_superCommute_normalOrder_ofCrAnFieldOpList_sum,
-    .name `FieldSpecification.FieldOpAlgebra.ofFieldOp_mul_normalOrder_ofFieldOpList_eq_sum,
+    .name ``FieldSpecification.normalOrderRel .complete,
+    .name ``FieldSpecification.normalOrderList .complete,
+    .name ``FieldSpecification.normalOrderSign .complete,
+    .name ``FieldSpecification.normalOrderSign_eraseIdx .complete,
+    .name ``FieldSpecification.FieldOpFreeAlgebra.normalOrderF .complete,
+    .name ``FieldSpecification.FieldOpAlgebra.normalOrder .complete,
+    .name ``FieldSpecification.FieldOpAlgebra.ofCrAnOp_superCommute_normalOrder_ofCrAnList_sum .complete,
+    .name ``FieldSpecification.FieldOpAlgebra.ofFieldOp_mul_normalOrder_ofFieldOpList_eq_sum .complete,
     .h1 "Wick Contractions",
     .h2 "Definition",
-    .name `WickContraction,
-    .name `WickContraction.GradingCompliant,
+    .name ``WickContraction .incomplete,
+    .name ``WickContraction.GradingCompliant .incomplete,
     .h2 "Aside: Cardinality",
-    .name `WickContraction.card_eq_cardFun,
+    .name ``WickContraction.card_eq_cardFun .incomplete,
     .h2 "Constructors",
     .p "There are a number of ways to construct a Wick contraction from
       other Wick contractions or single contractions.",
-    .name `WickContraction.insertAndContract,
-    .name `WickContraction.join,
+    .name ``WickContraction.insertAndContract .incomplete,
+    .name ``WickContraction.join .incomplete,
     .h2 "Sign",
-    .name `WickContraction.sign,
-    .name `WickContraction.join_sign,
-    .name `WickContraction.sign_insert_none,
-    .name `WickContraction.sign_insert_none_zero,
-    .name `WickContraction.sign_insert_some_of_not_lt,
-    .name `WickContraction.sign_insert_some_of_lt,
-    .name `WickContraction.sign_insert_some_zero,
+    .name ``WickContraction.sign .incomplete,
+    .name ``WickContraction.join_sign .incomplete,
+    .name ``WickContraction.sign_insert_none .incomplete,
+    .name ``WickContraction.sign_insert_none_zero .incomplete,
+    .name ``WickContraction.sign_insert_some_of_not_lt .incomplete,
+    .name ``WickContraction.sign_insert_some_of_lt .incomplete,
+    .name ``WickContraction.sign_insert_some_zero .incomplete,
     .h2 "Normal order",
-    .name `FieldSpecification.FieldOpAlgebra.normalOrder_uncontracted_none,
-    .name `FieldSpecification.FieldOpAlgebra.normalOrder_uncontracted_some,
+    .name ``FieldSpecification.FieldOpAlgebra.normalOrder_uncontracted_none .incomplete,
+    .name ``FieldSpecification.FieldOpAlgebra.normalOrder_uncontracted_some .incomplete,
     .h1 "Static contractions",
-    .name `WickContraction.staticContract,
-    .name `WickContraction.staticContract_insert_some_of_lt,
-    .name `WickContraction.staticContract_insert_none,
+    .name ``WickContraction.staticContract .incomplete,
+    .name ``WickContraction.staticContract_insert_some_of_lt .incomplete,
+    .name ``WickContraction.staticContract_insert_none .incomplete,
     .h1 "Time contractions",
-    .name `FieldSpecification.FieldOpAlgebra.timeContract,
-    .name `WickContraction.timeContract,
-    .name `WickContraction.timeContract_insert_none,
-    .name `WickContraction.timeContract_insert_some_of_not_lt,
-    .name `WickContraction.timeContract_insert_some_of_lt,
+    .name ``FieldSpecification.FieldOpAlgebra.timeContract .incomplete,
+    .name ``WickContraction.timeContract .incomplete,
+    .name ``WickContraction.timeContract_insert_none .incomplete,
+    .name ``WickContraction.timeContract_insert_some_of_not_lt .incomplete,
+    .name ``WickContraction.timeContract_insert_some_of_lt .incomplete,
     .h1 "Wick terms",
-    .name `WickContraction.wickTerm,
-    .name `WickContraction.wickTerm_empty_nil,
-    .name `WickContraction.wickTerm_insert_none,
-    .name `WickContraction.wickTerm_insert_some,
-    .name `WickContraction.mul_wickTerm_eq_sum,
+    .name ``WickContraction.wickTerm .incomplete,
+    .name ``WickContraction.wickTerm_empty_nil .incomplete,
+    .name ``WickContraction.wickTerm_insert_none .incomplete,
+    .name ``WickContraction.wickTerm_insert_some .incomplete,
+    .name ``WickContraction.mul_wickTerm_eq_sum .incomplete,
     .h1 "Static wick terms",
-    .name `WickContraction.staticWickTerm,
-    .name `WickContraction.staticWickTerm_empty_nil,
-    .name `WickContraction.staticWickTerm_insert_zero_none,
-    .name `WickContraction.staticWickTerm_insert_zero_some,
-    .name `WickContraction.mul_staticWickTerm_eq_sum,
+    .name ``WickContraction.staticWickTerm .incomplete,
+    .name ``WickContraction.staticWickTerm_empty_nil .incomplete,
+    .name ``WickContraction.staticWickTerm_insert_zero_none .incomplete,
+    .name ``WickContraction.staticWickTerm_insert_zero_some .incomplete,
+    .name ``WickContraction.mul_staticWickTerm_eq_sum .incomplete,
     .h1 "The three Wick's theorems",
-    .name `FieldSpecification.wicks_theorem,
-    .name `FieldSpecification.FieldOpAlgebra.static_wick_theorem,
-    .name `FieldSpecification.FieldOpAlgebra.wicks_theorem_normal_order
+    .name ``FieldSpecification.wicks_theorem .incomplete,
+    .name ``FieldSpecification.FieldOpAlgebra.static_wick_theorem .incomplete,
+    .name ``FieldSpecification.FieldOpAlgebra.wicks_theorem_normal_order .incomplete
     ]
 
 unsafe def main (_ : List String) : IO UInt32 := do