diff --git a/HepLean/Lorentz/Group/Proper.lean b/HepLean/Lorentz/Group/Proper.lean
index 4273cae..9e9deb6 100644
--- a/HepLean/Lorentz/Group/Proper.lean
+++ b/HepLean/Lorentz/Group/Proper.lean
@@ -189,7 +189,7 @@ lemma IsProper_iff (Λ : LorentzGroup d) : IsProper Λ ↔ detRep Λ = 1 := by
 lemma id_IsProper : @IsProper d 1 := by
   simp [IsProper]
 
-/-- If two Lorentz transformations are in the same connected componenet, and one is proper then
+/-- If two Lorentz transformations are in the same connected component, and one is proper then
   the other is also proper. -/
 lemma isProper_on_connected_component {Λ Λ' : LorentzGroup d} (h : Λ' ∈ connectedComponent Λ) :
     IsProper Λ ↔ IsProper Λ' := by
diff --git a/HepLean/Lorentz/MinkowskiMatrix.lean b/HepLean/Lorentz/MinkowskiMatrix.lean
index 14f015d..9d5741b 100644
--- a/HepLean/Lorentz/MinkowskiMatrix.lean
+++ b/HepLean/Lorentz/MinkowskiMatrix.lean
@@ -155,7 +155,7 @@ lemma det_dual : (dual Λ).det = Λ.det := by
   norm_cast
   simp
 
-/-- Expansion of the components of the Minkowski dual interms of the components
+/-- Expansion of the components of the Minkowski dual in terms of the components
   of the original matrix. -/
 lemma dual_apply (μ ν : Fin 1 ⊕ Fin d) :
     dual Λ μ ν = η μ μ * Λ ν μ * η ν ν := by
diff --git a/HepLean/PerturbationTheory/CreateAnnihilate.lean b/HepLean/PerturbationTheory/CreateAnnihilate.lean
index 0ab5d9a..895fefa 100644
--- a/HepLean/PerturbationTheory/CreateAnnihilate.lean
+++ b/HepLean/PerturbationTheory/CreateAnnihilate.lean
@@ -11,7 +11,7 @@ import Mathlib.Algebra.BigOperators.Group.Finset
 -/
 
 /-- 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
+  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
diff --git a/HepLean/PerturbationTheory/FeynmanDiagrams/Momentum.lean b/HepLean/PerturbationTheory/FeynmanDiagrams/Momentum.lean
index 9c908fc..794e7a3 100644
--- a/HepLean/PerturbationTheory/FeynmanDiagrams/Momentum.lean
+++ b/HepLean/PerturbationTheory/FeynmanDiagrams/Momentum.lean
@@ -48,7 +48,7 @@ We define the direct sum of the edge and vertex momentum spaces.
   Corresponding to that spanned by its momentum. -/
 def HalfEdgeMomenta : Type := F.𝓱𝓔 → ℝ
 
-/-- The half momenta carries the structure of an addative commutative group. -/
+/-- The half momenta carries the structure of an additive commutative group. -/
 instance : AddCommGroup F.HalfEdgeMomenta := Pi.addCommGroup
 
 /-- The half momenta carries the structure of a module over `ℝ`. Defined via its target. -/
@@ -83,7 +83,7 @@ def euclidInner : F.HalfEdgeMomenta →ₗ[ℝ] F.HalfEdgeMomenta →ₗ[ℝ] 
   Corresponding to that spanned by its total outflowing momentum. -/
 def EdgeMomenta : Type := F.𝓔 → ℝ
 
-/-- The edge momenta form an addative commuative group. -/
+/-- The edge momenta form an additive commuative group. -/
 instance : AddCommGroup F.EdgeMomenta := Pi.addCommGroup
 
 /-- The edge momenta form a module over `ℝ`. -/
@@ -93,7 +93,7 @@ instance : Module ℝ F.EdgeMomenta := Pi.module _ _ _
   Corresponding to that spanned by its total inflowing momentum. -/
 def VertexMomenta : Type := F.𝓥 → ℝ
 
-/-- The vertex momenta carries the structure of an addative commuative group. -/
+/-- The vertex momenta carries the structure of an additive commuative group. -/
 instance : AddCommGroup F.VertexMomenta := Pi.addCommGroup
 
 /-- The vertex momenta carries the structure of a module over `ℝ`. -/
@@ -106,7 +106,7 @@ def EdgeVertexMomentaMap : Fin 2 → Type := fun i =>
   | 1 => F.VertexMomenta
 
 /-- The target of the map `EdgeVertexMomentaMap` is either the type of edge momenta
-  or vertex momenta and thus carries the structure of an addative commuative group. -/
+  or vertex momenta and thus carries the structure of an additive commuative group. -/
 instance (i : Fin 2) : AddCommGroup (EdgeVertexMomentaMap F i) :=
   match i with
   | 0 => instAddCommGroupEdgeMomenta F
@@ -122,7 +122,7 @@ instance (i : Fin 2) : Module ℝ (EdgeVertexMomentaMap F i) :=
 /-- The direct sum of `EdgeMomenta` and `VertexMomenta`. -/
 def EdgeVertexMomenta : Type := DirectSum (Fin 2) (EdgeVertexMomentaMap F)
 
-/-- The structure of a addative commutative group on `EdgeVertexMomenta` for a
+/-- The structure of a additive commutative group on `EdgeVertexMomenta` for a
   Feynman diagram `F`. -/
 instance : AddCommGroup F.EdgeVertexMomenta := DirectSum.instAddCommGroup _
 
diff --git a/HepLean/PerturbationTheory/FieldOpAlgebra/Basic.lean b/HepLean/PerturbationTheory/FieldOpAlgebra/Basic.lean
index 7f36022..77f0554 100644
--- a/HepLean/PerturbationTheory/FieldOpAlgebra/Basic.lean
+++ b/HepLean/PerturbationTheory/FieldOpAlgebra/Basic.lean
@@ -33,15 +33,18 @@ def fieldOpIdealSet : Set (FieldOpFreeAlgebra 𝓕) :=
       x = [ofCrAnOpF φ, ofCrAnOpF φ']ₛca)}
 
 /-- For a field specification `𝓕`, the algebra `𝓕.FieldOpAlgebra` is defined as the quotient
-  of the free algebra `𝓕.FieldOpFreeAlgebra` by the ideal generated by elements of the form
-- `[ofCrAnOpF φ1, [ofCrAnOpF φ2, ofCrAnOpF φ3]ₛca]ₛca`, which (with the other conditions)
-  gives us that super-commutors are in the center.
-- `[ofCrAnOpF φc, ofCrAnOpF φc']ₛca` for `φc` and `φc'` creation operators. I.e two creation
-  operators always super-commute.
-- `[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. -/
+  of the free algebra `𝓕.FieldOpFreeAlgebra` by the ideal generated by
+- `[ofCrAnOpF φc, ofCrAnOpF φc']ₛca` for `φc` and `φc'` field creation operators.
+  This corresponds to the condition that two creation operators always super-commute.
+- `[ofCrAnOpF φa, ofCrAnOpF φa']ₛca` for `φa` and `φa'` field annihilation operators.
+  This corresponds to the condition that two annihilation operators always super-commute.
+- `[ofCrAnOpF φ, ofCrAnOpF φ']ₛca` for `φ` and `φ'` operators with different statistics.
+  This corresponds to the condition that two operators with different statistics always
+  super-commute. In otherwords, fermions and bosons always super-commute.
+- `[ofCrAnOpF φ1, [ofCrAnOpF φ2, ofCrAnOpF φ3]ₛca]ₛca`. This corresponds to the condition,
+  when combined with the conditions above, that the super-commutor is in the center of the
+  of the algebra.
+-/
 abbrev FieldOpAlgebra : Type := (TwoSidedIdeal.span 𝓕.fieldOpIdealSet).ringCon.Quotient
 
 namespace FieldOpAlgebra
@@ -457,13 +460,15 @@ lemma ι_eq_zero_iff_ι_bosonicProjF_fermonicProj_zero (x : FieldOpFreeAlgebra 
 
 -/
 
-/-- For a field specification `𝓕` and an element `φ` of `𝓕.FieldOp`, the element of
+/-- For a field specification `𝓕` and an element `φ` of `𝓕.FieldOp`,
+  `ofFieldOp φ` is defined as the element of
   `𝓕.FieldOpAlgebra` given by `ι (ofFieldOpF φ)`. -/
 def ofFieldOp (φ : 𝓕.FieldOp) : 𝓕.FieldOpAlgebra := ι (ofFieldOpF φ)
 
 lemma ofFieldOp_eq_ι_ofFieldOpF (φ : 𝓕.FieldOp) : ofFieldOp φ = ι (ofFieldOpF φ) := rfl
 
-/-- For a field specification `𝓕` and a list `φs` of `𝓕.FieldOp`, the element of
+/-- For a field specification `𝓕` and a list `φs` of `𝓕.FieldOp`,
+  `ofFieldOpList φs` is defined as the element of
   `𝓕.FieldOpAlgebra` given by `ι (ofFieldOpListF φ)`. -/
 def ofFieldOpList (φs : List 𝓕.FieldOp) : 𝓕.FieldOpAlgebra := ι (ofFieldOpListF φs)
 
@@ -487,7 +492,8 @@ lemma ofFieldOpList_singleton (φ : 𝓕.FieldOp) :
     ofFieldOpList [φ] = ofFieldOp φ := by
   simp only [ofFieldOpList, ofFieldOp, ofFieldOpListF_singleton]
 
-/-- For a field specification `𝓕` and an element `φ` of `𝓕.CrAnFieldOp`, the element of
+/-- For a field specification `𝓕` and an element `φ` of `𝓕.CrAnFieldOp`,
+  `ofCrAnOp φ` is defined as the element of
   `𝓕.FieldOpAlgebra` given by `ι (ofCrAnOpF φ)`. -/
 def ofCrAnOp (φ : 𝓕.CrAnFieldOp) : 𝓕.FieldOpAlgebra := ι (ofCrAnOpF φ)
 
@@ -500,7 +506,8 @@ lemma ofFieldOp_eq_sum (φ : 𝓕.FieldOp) :
   simp only [map_sum]
   rfl
 
-/-- For a field specification `𝓕` and a list `φs` of `𝓕.CrAnFieldOp`, the element of
+/-- For a field specification `𝓕` and a list `φs` of `𝓕.CrAnFieldOp`,
+  `ofCrAnList φs` is defined as the element of
   `𝓕.FieldOpAlgebra` given by `ι (ofCrAnListF φ)`. -/
 def ofCrAnList (φs : List 𝓕.CrAnFieldOp) : 𝓕.FieldOpAlgebra := ι (ofCrAnListF φs)
 
@@ -528,8 +535,10 @@ remark notation_drop := "In doc-strings we will often drop explicit applications
 
 /-- 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 _`. -/
+  Thus for `φ`
+- an incoming asymptotic state this is `0`.
+- a position based state this is `ofCrAnOp ⟨φ, .create⟩`.
+- an outgoing asymptotic state this is `ofCrAnOp ⟨φ, ()⟩`. -/
 def anPart (φ : 𝓕.FieldOp) : 𝓕.FieldOpAlgebra := ι (anPartF φ)
 
 lemma anPart_eq_ι_anPartF (φ : 𝓕.FieldOp) : anPart φ = ι (anPartF φ) := rfl
@@ -552,8 +561,10 @@ lemma anPart_posAsymp (φ : (Σ f, 𝓕.AsymptoticLabel f) × (Fin 3 → ℝ)) :
 
 /-- 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 _`. -/
+  Thus for `φ`
+- an incoming asymptotic state this is `ofCrAnOp ⟨φ, ()⟩`.
+- a position based state this is `ofCrAnOp ⟨φ, .create⟩`.
+- an outgoing asymptotic state this is `0`. -/
 def crPart (φ : 𝓕.FieldOp) : 𝓕.FieldOpAlgebra := ι (crPartF φ)
 
 lemma crPart_eq_ι_crPartF (φ : 𝓕.FieldOp) : crPart φ = ι (crPartF φ) := rfl
diff --git a/HepLean/PerturbationTheory/FieldOpAlgebra/Grading.lean b/HepLean/PerturbationTheory/FieldOpAlgebra/Grading.lean
index 44d581c..926465d 100644
--- a/HepLean/PerturbationTheory/FieldOpAlgebra/Grading.lean
+++ b/HepLean/PerturbationTheory/FieldOpAlgebra/Grading.lean
@@ -384,9 +384,10 @@ lemma directSum_eq_bosonic_plus_fermionic
     abel
 
 /-- For a field statistic `𝓕`, the algebra `𝓕.FieldOpAlgebra` is graded by `FieldStatistic`.
-  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. -/
+  Those `ofCrAnList φs` for which `φs` has an overall `bosonic` statistic
+  (i.e. `𝓕 |>ₛ φs = bosonic`) span `bosonic`
+  submodule, whilst those `ofCrAnList φs` for which `φs` has an overall `fermionic` statistic
+  (i.e. `𝓕 |>ₛ φs = fermionic`) span the `fermionic` submodule. -/
 instance fieldOpAlgebraGrade : GradedAlgebra (A := 𝓕.FieldOpAlgebra) statSubmodule where
   one_mem := by
     simp only [statSubmodule]
diff --git a/HepLean/PerturbationTheory/FieldOpAlgebra/NormalOrder/Basic.lean b/HepLean/PerturbationTheory/FieldOpAlgebra/NormalOrder/Basic.lean
index 1e33184..7b7fbf9 100644
--- a/HepLean/PerturbationTheory/FieldOpAlgebra/NormalOrder/Basic.lean
+++ b/HepLean/PerturbationTheory/FieldOpAlgebra/NormalOrder/Basic.lean
@@ -223,10 +223,11 @@ lemma ι_normalOrderF_eq_of_equiv (a b : 𝓕.FieldOpFreeAlgebra) (h : a ≈ b)
 
   `FieldOpAlgebra 𝓕 →ₗ[ℂ] FieldOpAlgebra 𝓕`
 
-  defined as the decent of `ι ∘ₗ normalOrderF` from `FieldOpFreeAlgebra 𝓕` to `FieldOpAlgebra 𝓕`.
+  defined as the decent of `ι ∘ₗ normalOrderF : FieldOpFreeAlgebra 𝓕 →ₗ[ℂ] FieldOpAlgebra 𝓕`
+  from `FieldOpFreeAlgebra 𝓕` to `FieldOpAlgebra 𝓕`.
   This decent exists because `ι ∘ₗ normalOrderF` is well-defined on equivalence classes.
 
-  The notation `𝓝(a)` is used for `normalOrder a`. -/
+  The notation `𝓝(a)` is used for `normalOrder a` for `a` an element of `FieldOpAlgebra 𝓕`. -/
 noncomputable def normalOrder : FieldOpAlgebra 𝓕 →ₗ[ℂ] FieldOpAlgebra 𝓕 where
   toFun := Quotient.lift (ι.toLinearMap ∘ₗ normalOrderF) ι_normalOrderF_eq_of_equiv
   map_add' x y := by
diff --git a/HepLean/PerturbationTheory/FieldOpAlgebra/NormalOrder/Lemmas.lean b/HepLean/PerturbationTheory/FieldOpAlgebra/NormalOrder/Lemmas.lean
index 9e3bbd8..f1da540 100644
--- a/HepLean/PerturbationTheory/FieldOpAlgebra/NormalOrder/Lemmas.lean
+++ b/HepLean/PerturbationTheory/FieldOpAlgebra/NormalOrder/Lemmas.lean
@@ -231,7 +231,7 @@ The proof of this result ultimately goes as follows
   (considered as a list with one element) 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  rearrange terms.
-- Properties of ordered lists, and `normalOrderSign_eraseIdx` is then used to complete the proof.
+- Properties of ordered lists, and `normalOrderSign_eraseIdx` are then used to complete the proof.
 -/
 lemma ofCrAnOp_superCommute_normalOrder_ofCrAnList_sum (φ : 𝓕.CrAnFieldOp)
     (φs : List 𝓕.CrAnFieldOp) : [ofCrAnOp φ, 𝓝(ofCrAnList φs)]ₛ = ∑ n : Fin φs.length,
diff --git a/HepLean/PerturbationTheory/FieldOpAlgebra/NormalOrder/WickContractions.lean b/HepLean/PerturbationTheory/FieldOpAlgebra/NormalOrder/WickContractions.lean
index 3013fe1..d6f531c 100644
--- a/HepLean/PerturbationTheory/FieldOpAlgebra/NormalOrder/WickContractions.lean
+++ b/HepLean/PerturbationTheory/FieldOpAlgebra/NormalOrder/WickContractions.lean
@@ -26,7 +26,7 @@ variable {𝓕 : FieldSpecification}
 -/
 
 /-- For a list `φs = φ₀…φₙ` of `𝓕.FieldOp`, a Wick contraction `φsΛ` of `φs`, an element `φ` of
-  `𝓕.FieldOp`, and a `i ≤ φs.length` the following relation holds
+  `𝓕.FieldOp`, and a `i ≤ φs.length`, then the following relation holds:
 
   `𝓝([φsΛ ↩Λ φ i none]ᵘᶜ) = s • 𝓝(φ :: [φsΛ]ᵘᶜ)`
 
@@ -101,7 +101,7 @@ lemma normalOrder_uncontracted_none (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp
 /--
   For a list `φs = φ₀…φₙ` of `𝓕.FieldOp`, a Wick contraction `φsΛ` of `φs`, an element `φ` of
   `𝓕.FieldOp`, a `i ≤ φs.length` and a `k` in `φsΛ.uncontracted`, then
-  `𝓝([φsΛ ↩Λ φ i (some k)]ᵘᶜ)` is equal to the normal ordering of `[φsΛ]ᵘᶜ` with the `FieldOp`
+  `𝓝([φsΛ ↩Λ φ i (some k)]ᵘᶜ)` is equal to the normal ordering of `[φsΛ]ᵘᶜ` with the `𝓕.FieldOp`
   corresponding to `k` removed.
 
   The proof of this result ultimately a consequence of definitions.
diff --git a/HepLean/PerturbationTheory/FieldOpAlgebra/StaticWickTerm.lean b/HepLean/PerturbationTheory/FieldOpAlgebra/StaticWickTerm.lean
index 83ea0c5..abf040c 100644
--- a/HepLean/PerturbationTheory/FieldOpAlgebra/StaticWickTerm.lean
+++ b/HepLean/PerturbationTheory/FieldOpAlgebra/StaticWickTerm.lean
@@ -68,7 +68,7 @@ lemma staticWickTerm_insert_zero_none (φ : 𝓕.FieldOp) (φs : List 𝓕.Field
   uncontracted fields in `φ₀…φₖ₋₁`
 - the normal ordering `𝓝([φsΛ]ᵘᶜ.erase (uncontractedFieldOpEquiv φs φsΛ k))`.
 
-The proof of this result ultimitley relies on
+The proof of this result ultimately relies on
 - `staticContract_insert_some` to rewrite static contractions.
 - `normalOrder_uncontracted_some` to rewrite normal orderings.
 - `sign_insert_some_zero` to rewrite signs.
diff --git a/HepLean/PerturbationTheory/FieldOpAlgebra/TimeOrder.lean b/HepLean/PerturbationTheory/FieldOpAlgebra/TimeOrder.lean
index f28070d..a5ab710 100644
--- a/HepLean/PerturbationTheory/FieldOpAlgebra/TimeOrder.lean
+++ b/HepLean/PerturbationTheory/FieldOpAlgebra/TimeOrder.lean
@@ -371,7 +371,8 @@ lemma ι_timeOrderF_eq_of_equiv (a b : 𝓕.FieldOpFreeAlgebra) (h : a ≈ b) :
 
 `FieldOpAlgebra 𝓕 →ₗ[ℂ] FieldOpAlgebra 𝓕`
 
-defined as the decent of `ι ∘ₗ timeOrderF` from `FieldOpFreeAlgebra 𝓕` to `FieldOpAlgebra 𝓕`.
+defined as the decent of `ι ∘ₗ timeOrderF : FieldOpFreeAlgebra 𝓕 →ₗ[ℂ] FieldOpAlgebra 𝓕` from
+`FieldOpFreeAlgebra 𝓕` to `FieldOpAlgebra 𝓕`.
 This decent exists because `ι ∘ₗ timeOrderF` is well-defined on equivalence classes.
 
 The notation `𝓣(a)` is used for `timeOrder a`. -/
diff --git a/HepLean/PerturbationTheory/FieldOpAlgebra/Universality.lean b/HepLean/PerturbationTheory/FieldOpAlgebra/Universality.lean
index ca5eb42..bfe617f 100644
--- a/HepLean/PerturbationTheory/FieldOpAlgebra/Universality.lean
+++ b/HepLean/PerturbationTheory/FieldOpAlgebra/Universality.lean
@@ -78,8 +78,9 @@ lemma universalLift_ι {A : Type} [Semiring A] [Algebra ℂ A] (f : 𝓕.CrAnFie
 For a field specification, `𝓕`, the algebra `𝓕.FieldOpAlgebra` satisfies 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`.
+If `g` is zero on the ideal defining `𝓕.FieldOpAlgebra`, then there exists
+algebra map `g' : FieldOpAlgebra 𝓕 →ₐ[ℂ] A` such that `g' ∘ ι = g`, and furthermore this
+algebra map is unique.
 -/
 lemma universality {A : Type} [Semiring A] [Algebra ℂ A] (f : 𝓕.CrAnFieldOp → A)
     (h1 : ∀ a ∈ TwoSidedIdeal.span 𝓕.fieldOpIdealSet, FreeAlgebra.lift ℂ f a = 0) :
diff --git a/HepLean/PerturbationTheory/FieldOpAlgebra/WicksTheorem.lean b/HepLean/PerturbationTheory/FieldOpAlgebra/WicksTheorem.lean
index 2f4e6ba..e6df34c 100644
--- a/HepLean/PerturbationTheory/FieldOpAlgebra/WicksTheorem.lean
+++ b/HepLean/PerturbationTheory/FieldOpAlgebra/WicksTheorem.lean
@@ -47,13 +47,13 @@ lemma wicks_theorem_congr {φs φs' : List 𝓕.FieldOp} (h : φs = φs') :
   rfl
 
 remark wicks_theorem_context := "
-  In perturbation quantum field theory, Wick's theorem allows
+  In perturbative quantum field theory, Wick's theorem allows
   us to expand expectation values of time-ordered products of fields in terms of normal-orders
   and time contractions.
   The theorem is used to simplify the calculation of scattering amplitudes, and is the precurser
   to Feynman diagrams.
 
-  There is are actually three different versions of Wick's theorem used.
+  There are actually three different versions of Wick's theorem used.
   The static version, the time-dependent version, and the normal-ordered time-dependent version.
   HepLean contains a formalization of all three of these theorems in complete generality for
   mixtures of bosonic and fermionic fields.
diff --git a/HepLean/PerturbationTheory/FieldOpFreeAlgebra/Basic.lean b/HepLean/PerturbationTheory/FieldOpFreeAlgebra/Basic.lean
index ff292f8..8e93545 100644
--- a/HepLean/PerturbationTheory/FieldOpFreeAlgebra/Basic.lean
+++ b/HepLean/PerturbationTheory/FieldOpFreeAlgebra/Basic.lean
@@ -41,13 +41,14 @@ abbrev FieldOpFreeAlgebra (𝓕 : FieldSpecification) : Type := FreeAlgebra ℂ
 namespace FieldOpFreeAlgebra
 
 remark naming_convention := "
-  For mathematicial objects defined in relation to `FieldOpFreeAlgebra` we will often postfix
-  their names with an `F` to indicate that they are related to the free algebra.
+  For mathematicial objects defined in relation to `FieldOpFreeAlgebra` the postfix `F`
+  may be given to
+  their names to indicate that they are related to the free algebra.
   This is to avoid confusion when working within the context of `FieldOpAlgebra` which is defined
   as a quotient of `FieldOpFreeAlgebra`."
 
-/-- For a field specification `𝓕`, the element of `𝓕.FieldOpFreeAlgebra` formed by a
-  single `𝓕.CrAnFieldOp`. -/
+/-- For a field specification `𝓕`, and a element `φ` of `𝓕.CrAnFieldOp`,
+  `ofCrAnOpF φ` is defined as the element of `𝓕.FieldOpFreeAlgebra` formed by `φ`. -/
 def ofCrAnOpF (φ : 𝓕.CrAnFieldOp) : FieldOpFreeAlgebra 𝓕 :=
   FreeAlgebra.ι ℂ φ
 
@@ -70,9 +71,11 @@ lemma universality {A : Type} [Semiring A] [Algebra ℂ A] (f : 𝓕.CrAnFieldOp
     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 𝓕`. -/
+/-- For a field specification `𝓕`, and a list `φs` of `𝓕.CrAnFieldOp`,
+ `ofCrAnListF φs` is defined as the element of `𝓕.FieldOpFreeAlgebra`
+  obtained by the product of `ofCrAnListF φ` for each `φ` in `φs`.
+  For example `ofCrAnListF [φ₁, φ₂, φ₃] = ofCrAnOpF φ₁ * ofCrAnOpF φ₂ * ofCrAnOpF φ₃`.
+  The set of all `ofCrAnListF φs` forms a basis of `FieldOpFreeAlgebra 𝓕`. -/
 def ofCrAnListF (φs : List 𝓕.CrAnFieldOp) : FieldOpFreeAlgebra 𝓕 := (List.map ofCrAnOpF φs).prod
 
 @[simp]
@@ -88,22 +91,25 @@ lemma ofCrAnListF_append (φs φs' : List 𝓕.CrAnFieldOp) :
 lemma ofCrAnListF_singleton (φ : 𝓕.CrAnFieldOp) :
     ofCrAnListF [φ] = ofCrAnOpF φ := by simp [ofCrAnListF]
 
-/-- 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
-  `ofCrAnOpF φ₁ᶜ`, and for `φ₁` a
-  position field operator we get `ofCrAnOpF φ₁ᶜ + ofCrAnOpF φ₁ᵃ`. -/
+/-- For a field specification `𝓕`, and an element `φ` of  `𝓕.FieldOp`,
+  `ofFieldOpF φ` is the element of `𝓕.FieldOpFreeAlgebra` formed  by summing over
+  `ofCrAnOpF` of the
+  creation and annihilation parts of `φ`.
+
+  For example for `φ` an incoming asymptotic field operator we get
+  `ofCrAnOpF ⟨φ, ()⟩`, and for `φ` a
+  position field operator we get `ofCrAnOpF ⟨φ, .create⟩ + ofCrAnOpF ⟨φ, .annihilate⟩`. -/
 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
-  `(ofCrAnOpF φ1ᶜ + ofCrAnOpF φ1ᵃ) * (ofCrAnOpF φ2ᶜ + ofCrAnOpF φ2ᵃ)`. -/
+/-- For a field specification `𝓕`, and a list `φs` of `𝓕.FieldOp`,
+  `𝓕.ofFieldOpListF φs` is defined as the element of `𝓕.FieldOpFreeAlgebra`
+  obtained by the product of `ofFieldOpF φ` for each `φ` in `φs`.
+  For example `ofFieldOpListF [φ₁, φ₂, φ₃] = ofFieldOpF φ₁ * ofFieldOpF φ₂ * ofFieldOpF φ₃`. -/
 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`"
+remark notation_drop := "In doc-strings explicit applications of `ofCrAnOpF`,
+`ofCrAnListF`, `ofFieldOpF`, and `ofFieldOpListF` will often be dropped."
 
 /-- Coercion from `List 𝓕.FieldOp` to `FieldOpFreeAlgebra 𝓕` through `ofFieldOpListF`. -/
 instance : Coe (List 𝓕.FieldOp) (FieldOpFreeAlgebra 𝓕) := ⟨ofFieldOpListF⟩
diff --git a/HepLean/PerturbationTheory/FieldOpFreeAlgebra/Grading.lean b/HepLean/PerturbationTheory/FieldOpFreeAlgebra/Grading.lean
index 3c3bb4c..cc14a7b 100644
--- a/HepLean/PerturbationTheory/FieldOpFreeAlgebra/Grading.lean
+++ b/HepLean/PerturbationTheory/FieldOpFreeAlgebra/Grading.lean
@@ -237,8 +237,10 @@ lemma directSum_eq_bosonic_plus_fermionic
     abel
 
 /-- 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
+  Those `ofCrAnListF φs` for which `φs` has an overall `bosonic` statistic
+  (i.e. `𝓕 |>ₛ φs = bosonic`) span `bosonic`
+  submodule, whilst those `ofCrAnListF φs` for which `φs` has an overall `fermionic` statistic
+  (i.e. `𝓕 |>ₛ φs = fermionic`) span
   the `fermionic` submodule. -/
 instance fieldOpFreeAlgebraGrade :
     GradedAlgebra (A := 𝓕.FieldOpFreeAlgebra) statisticSubmodule where
diff --git a/HepLean/PerturbationTheory/FieldOpFreeAlgebra/NormalOrder.lean b/HepLean/PerturbationTheory/FieldOpFreeAlgebra/NormalOrder.lean
index c3da7f4..a2ddbb0 100644
--- a/HepLean/PerturbationTheory/FieldOpFreeAlgebra/NormalOrder.lean
+++ b/HepLean/PerturbationTheory/FieldOpFreeAlgebra/NormalOrder.lean
@@ -31,8 +31,11 @@ noncomputable section
   `FieldOpFreeAlgebra 𝓕 →ₗ[ℂ] FieldOpFreeAlgebra 𝓕`
   defined by its action on the basis `ofCrAnListF φs`, taking `ofCrAnListF φs` to
   `normalOrderSign φs • ofCrAnListF (normalOrderList φs)`.
+  That is, `normalOrderF` normal-orders the field operators and multiplies by the sign of the
+  normal order.
 
-  The notation `𝓝ᶠ(a)` is used for `normalOrderF a`. -/
+  The notation `𝓝ᶠ(a)` is used for `normalOrderF a` for `a` an element of
+  `FieldOpFreeAlgebra 𝓕`. -/
 def normalOrderF : FieldOpFreeAlgebra 𝓕 →ₗ[ℂ] FieldOpFreeAlgebra 𝓕 :=
   Basis.constr ofCrAnListFBasis ℂ fun φs =>
   normalOrderSign φs • ofCrAnListF (normalOrderList φs)
diff --git a/HepLean/PerturbationTheory/FieldOpFreeAlgebra/SuperCommute.lean b/HepLean/PerturbationTheory/FieldOpFreeAlgebra/SuperCommute.lean
index 3936096..ba365d2 100644
--- a/HepLean/PerturbationTheory/FieldOpFreeAlgebra/SuperCommute.lean
+++ b/HepLean/PerturbationTheory/FieldOpFreeAlgebra/SuperCommute.lean
@@ -405,7 +405,7 @@ lemma superCommuteF_ofCrAnListF_ofFieldOpListF_cons (φ : 𝓕.FieldOp) (φs : L
   simp [mul_comm]
 
 /--
-For a field specification `𝓕`, and to lists `φs = φ₀…φₙ` and `φs'` of `𝓕.CrAnFieldOp`
+For a field specification `𝓕`, and two lists `φs = φ₀…φₙ` and `φs'` of `𝓕.CrAnFieldOp`
 the following super commutation relation holds:
 
 `[φs', φ₀…φₙ]ₛca = ∑ i, 𝓢(φs', φ₀…φᵢ₋₁) • φ₀…φᵢ₋₁ * [φs', φᵢ]ₛca * φᵢ₊₁ … φₙ`
diff --git a/HepLean/PerturbationTheory/FieldOpFreeAlgebra/TimeOrder.lean b/HepLean/PerturbationTheory/FieldOpFreeAlgebra/TimeOrder.lean
index 75ef74d..ae1f4d0 100644
--- a/HepLean/PerturbationTheory/FieldOpFreeAlgebra/TimeOrder.lean
+++ b/HepLean/PerturbationTheory/FieldOpFreeAlgebra/TimeOrder.lean
@@ -30,6 +30,8 @@ open HepLean.List
   `FieldOpFreeAlgebra 𝓕 →ₗ[ℂ] FieldOpFreeAlgebra 𝓕`
   defined by its action on the basis `ofCrAnListF φs`, taking
   `ofCrAnListF φs` to `crAnTimeOrderSign φs • ofCrAnListF (crAnTimeOrderList φs)`.
+  That is, `timeOrderF` time-orders the field operators and multiplies by the sign of the
+  time order.
 
   The notation `𝓣ᶠ(a)` is used for `timeOrderF a` -/
 def timeOrderF : FieldOpFreeAlgebra 𝓕 →ₗ[ℂ] FieldOpFreeAlgebra 𝓕 :=
diff --git a/HepLean/PerturbationTheory/FieldSpecification/Basic.lean b/HepLean/PerturbationTheory/FieldSpecification/Basic.lean
index 03bd3b8..bd4e315 100644
--- a/HepLean/PerturbationTheory/FieldSpecification/Basic.lean
+++ b/HepLean/PerturbationTheory/FieldSpecification/Basic.lean
@@ -42,13 +42,15 @@ The structure `FieldSpecification` is defined to have the following content:
     - 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,
+    types of incoming asymptotic field operators associated with the
+    field `f` (this is also matches the types of outgoing asymptotic field operators).
+    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
+  - For each field `f` in `Field`, a field statistic `statistic f` which classifies `f` as either
     `bosonic` or `fermionic`.
 -/
 structure FieldSpecification where
@@ -67,20 +69,30 @@ structure FieldSpecification where
 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` 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.
+/-- For a field specification `𝓕`, the inductive type `𝓕.FieldOp` is defined
+  to contain the following elements:
+- for every `f` in `𝓕.Field`, element of `e` of `AsymptoticLabel f` and `3`-momentum `p`, an
+  element labelled `inAsymp f e p` corresponding to an incoming asymptotic field operator
+  of the field `f`, of label `e` (e.g. specifying the spin), and momentum `p`.
+- for every `f` in `𝓕.Field`, element of `e` of `PositionLabel f` and space-time position `x`, an
+  element labelled `position f e x` corresponding to a position field operator of the field `f`,
+  of label `e` (e.g. specifying the Lorentz index), and position `x`.
+- for every `f` in `𝓕.Field`, element of `e` of `AsymptoticLabel f` and `3`-momentum `p`, an
+  element labelled `outAsymp f e p` corresponding to an outgoing asymptotic field operator of the
+  field `f`, of label `e` (e.g. specifying the spin), and momentum `p`.
 
-Note the use of `3`-momentum here rather then `4`-momentum. This is because the asymptotic states
-have on-shell momenta.
+As some intuition, if `f` corresponds to a Weyl-fermion field, then
+- For `inAsymp f e p`, `e` would correspond to a spin `s`, and `inAsymp f e p` would, once
+  represented in the operator algebra,
+  be proportional to the creation operator `a(p, s)`.
+- `position f e x`, `e` would correspond to a Lorentz index `α`, and `position f e x` would,
+  once represented in the operator algebra, be proportional to the operator
+  `∑ s, ∫ d^3p/(…) (x_α(p,s)  a(p, s) e^{-i p x} + y_α(p,s) a^†(p, s) e^{-i p x})`.
+- `outAsymp f e p`, `e` would corresond to a spin `s`, and `outAsymp f e p` would,
+  once represented in the operator algebra, be proportional to the
+  annihilation operator `a^†(p, s)`.
+
+This type contains all operators which are related to a field.
 -/
 inductive FieldOp (𝓕 : FieldSpecification) where
   | inAsymp : (Σ f, 𝓕.AsymptoticLabel f) × (Fin 3 → ℝ) → 𝓕.FieldOp
diff --git a/HepLean/PerturbationTheory/FieldSpecification/CrAnFieldOp.lean b/HepLean/PerturbationTheory/FieldSpecification/CrAnFieldOp.lean
index 2d56cf3..89aa9c0 100644
--- a/HepLean/PerturbationTheory/FieldSpecification/CrAnFieldOp.lean
+++ b/HepLean/PerturbationTheory/FieldSpecification/CrAnFieldOp.lean
@@ -63,15 +63,31 @@ def fieldOpToCreateAnnihilateTypeCongr : {i j : 𝓕.FieldOp} → i = j →
   | _, _, rfl => Equiv.refl _
 
 /--
-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`.
+For a field specification `𝓕`, the (sigma) type `𝓕.CrAnFieldOp`
+corresponds to the type of creation and annihilation parts of field operators.
+It formally defined to consist of the following elements:
+- for each in incoming asymptotic field operator `φ` in `𝓕.FieldOp` an element
+  written as `⟨φ, ()⟩` in `𝓕.CrAnFieldOp`, corresponding to the creation part of `φ`.
+  Here `φ` has no annihilation part. (Here `()` is the unique element of `Unit`.)
+- for each position field operator `φ` in `𝓕.FieldOp` an element of `𝓕.CrAnFieldOp`
+  written as `⟨φ, .create⟩`, corresponding to the creation part of `φ`.
+- for each position field operator `φ` in `𝓕.FieldOp` an element of `𝓕.CrAnFieldOp`
+  written as `⟨φ, .annihilate⟩`, corresponding to the annihilation part of `φ`.
+- for each out outgoing asymptotic field operator `φ` in `𝓕.FieldOp` an element
+  written as `⟨φ, ()⟩` in `𝓕.CrAnFieldOp`, corresponding to the annihilation part of `φ`.
+  Here `φ` has no creation part. (Here `()` is the unique element of `Unit`.)
+
+As some intuition, if `f` corresponds to a Weyl-fermion field, it would contribute
+  the following elements to `𝓕.CrAnFieldOp`
+- an element corresponding to incoming asymptotic operators for each spin `s`: `a(p, s)`.
+- an element corresponding to the creation parts of position operators for each each Lorentz
+  index `α`:
+  `∑ s, ∫ d^3p/(…) (x_α(p,s)  a(p, s) e^{-i p x})`.
+- an element corresponding to anihilation parts of position operator,
+  for each each Lorentz index `α`:
+  `∑ s, ∫ d^3p/(…) (y_α(p,s) a^†(p, s) e^{-i p x})`.
+- an element corresponding to outgoing asymptotic operators for each spin `s`: `a^†(p, s)`.
 
-Note that the incoming and outgoing asymptotic field operators are implicitly creation and
-annihilation operators respectively.
 -/
 def CrAnFieldOp : Type := Σ (s : 𝓕.FieldOp), 𝓕.fieldOpToCrAnType s
 
@@ -82,8 +98,13 @@ def crAnFieldOpToFieldOp : 𝓕.CrAnFieldOp → 𝓕.FieldOp := Sigma.fst
 lemma crAnFieldOpToFieldOp_prod (s : 𝓕.FieldOp) (t : 𝓕.fieldOpToCrAnType s) :
     𝓕.crAnFieldOpToFieldOp ⟨s, t⟩ = s := rfl
 
-/-- The map from creation and annihilation states to the type `CreateAnnihilate`
-  specifying if a state is a creation or an annihilation state. -/
+/-- For a field specficiation `𝓕`, `𝓕.crAnFieldOpToCreateAnnihilate` is the map from
+  `𝓕.CrAnFieldOp` to `CreateAnnihilate` taking `φ` to `create` if
+- `φ` corresponds to an incoming asymptotic field operator or the creation part of a position based
+  field operator.
+
+otherwise it takes `φ` to `annihilate`.
+ -/
 def crAnFieldOpToCreateAnnihilate : 𝓕.CrAnFieldOp → CreateAnnihilate
   | ⟨FieldOp.inAsymp _, _⟩ => CreateAnnihilate.create
   | ⟨FieldOp.position _, CreateAnnihilate.create⟩ => CreateAnnihilate.create
@@ -92,7 +113,7 @@ def crAnFieldOpToCreateAnnihilate : 𝓕.CrAnFieldOp → CreateAnnihilate
 
 /-- 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 `𝓕.FieldOp`) underlying `φ`.
+  (or the `𝓕.FieldOp`) underlying `φ`.
 
   The following notation is used in relation to `crAnStatistics`:
   - For `φ` an element of `𝓕.CrAnFieldOp`, `𝓕 |>ₛ φ` is `crAnStatistics φ`.
@@ -115,18 +136,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. `φ₀…φₙ`,
+remark notation_remark := "When working with a field specification `𝓕` the
+following notation will be used within doc-strings:
+- when field statistics occur in exchange signs the `𝓕 |>ₛ _` may be dropped.
+- lists of `FieldOp` or `CrAnFieldOp` `φs` may be written as `φ₀…φₙ`,
   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
+- `φᶜ` may be used 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.
+Some examples of these notation-conventions are:
+- `𝓢(φ, φs)` which corresponds to `𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φs)`
+- `φ₀…φᵢ₋₁φᵢ₊₁…φₙ` which corresponds to a (given) list `φs = φ₀…φₙ` with the element at the
+  `i`th position removed.
 "
 
 end FieldSpecification
diff --git a/HepLean/PerturbationTheory/FieldSpecification/NormalOrder.lean b/HepLean/PerturbationTheory/FieldSpecification/NormalOrder.lean
index 17176b3..bae9058 100644
--- a/HepLean/PerturbationTheory/FieldSpecification/NormalOrder.lean
+++ b/HepLean/PerturbationTheory/FieldSpecification/NormalOrder.lean
@@ -17,8 +17,8 @@ variable {𝓕 : FieldSpecification}
 /-- 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.
+  - `φ₀` is a field creation operator
+  - `φ₁` is a field annihilation operator.
 
   Thus, colloquially `𝓕.normalOrderRel φ₀ φ₁` says the creation operators are 'less then'
   annihilation operators. -/
@@ -344,11 +344,12 @@ lemma normalOrderList_eraseIdx_normalOrderEquiv {φs : List 𝓕.CrAnFieldOp} (n
   rw [HepLean.List.eraseIdx_insertionSort_fin]
 
 /-- For a field specification `𝓕`, a list `φs = φ₀…φₙ` of `𝓕.CrAnFieldOp` and an `i < φs.length`,
-  the following relation holds
+  then
   `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.
+  - `𝓢(φᵢ, _)` 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 *
diff --git a/HepLean/PerturbationTheory/FieldSpecification/TimeOrder.lean b/HepLean/PerturbationTheory/FieldSpecification/TimeOrder.lean
index 1da3813..babe0ee 100644
--- a/HepLean/PerturbationTheory/FieldSpecification/TimeOrder.lean
+++ b/HepLean/PerturbationTheory/FieldSpecification/TimeOrder.lean
@@ -193,7 +193,7 @@ lemma timeOrderList_eq_maxTimeField_timeOrderList (φ : 𝓕.FieldOp) (φs : Lis
 
 /-- 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
+  It is defined 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
@@ -201,6 +201,8 @@ lemma timeOrderList_eq_maxTimeField_timeOrderList (φ : 𝓕.FieldOp) (φs : Lis
   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 `φ₁`.
+The use of *greater* then rather then *less* then is because on ordering lists of operators
+it is needed that the operator with the greatest time is to the left.
 -/
 def crAnTimeOrderRel (a b : 𝓕.CrAnFieldOp) : Prop := 𝓕.timeOrderRel a.1 b.1
 
diff --git a/HepLean/PerturbationTheory/FieldStatistics/ExchangeSign.lean b/HepLean/PerturbationTheory/FieldStatistics/ExchangeSign.lean
index 8b1b3cf..5fad4dd 100644
--- a/HepLean/PerturbationTheory/FieldStatistics/ExchangeSign.lean
+++ b/HepLean/PerturbationTheory/FieldStatistics/ExchangeSign.lean
@@ -27,8 +27,8 @@ variable {𝓕 : Type}
 /-- 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 exchange sign is the sign one picks up on exchanging an operator or field `φ₁` of statistic
+  `a` with an operator or field `φ₂` of statistic `b`, i.e. `φ₁φ₂ → φ₂φ₁`.
 
   The notation `𝓢(a, b)` is used for the exchange sign of `a` and `b`. -/
 def exchangeSign : FieldStatistic →* FieldStatistic →* ℂ where
diff --git a/HepLean/PerturbationTheory/WickContraction/Basic.lean b/HepLean/PerturbationTheory/WickContraction/Basic.lean
index 308a9b1..73aa956 100644
--- a/HepLean/PerturbationTheory/WickContraction/Basic.lean
+++ b/HepLean/PerturbationTheory/WickContraction/Basic.lean
@@ -19,20 +19,6 @@ contracting, a Wick contraction
 is a finite set of pairs of `Fin n` (numbers `0`, …, `n-1`), such that no
 element of `Fin n` occurs in more then one pair. The pairs are the positions of fields we
 'contract' together.
-
-For example for `n = 3` there are `4` Wick contractions:
-- `∅`, corresponding to the case where no fields are contracted.
-- `{{0, 1}}`, corresponding to the case where the field at position `0` and `1` are contracted.
-- `{{0, 2}}`, corresponding to the case where the field at position `0` and `2` are contracted.
-- `{{1, 2}}`, corresponding to the case where the field at position `1` and `2` are contracted.
-
-For `n=4` some possible Wick contractions are
-- `∅`, corresponding to the case where no fields are contracted.
-- `{{0, 1}, {2, 3}}`, corresponding to the case where the field at position `0` and `1` are
-  contracted and the field at position `2` and `3` are contracted.
-- `{{0, 2}, {1, 3}}`, corresponding to the case where the field at position `0` and `2` are
-  contracted and the field at position `1` and `3` are contracted.
-  etc.
 -/
 def WickContraction (n : ℕ) : Type :=
   {f : Finset ((Finset (Fin n))) // (∀ a ∈ f, a.card = 2) ∧
@@ -534,8 +520,8 @@ lemma prod_finset_eq_mul_fst_snd (c : WickContraction n) (a : c.1)
 /-- For a field specification `𝓕`, `φs` a list of `𝓕.FieldOp` and a Wick contraction
   `φsΛ` of `φs`, the Wick contraction `φsΛ` is said to be `GradingCompliant` if
   for every pair in `φsΛ` the contracted fields are either both `fermionic` or both `bosonic`.
-  I.e. in a `GradingCompliant` Wick contraction no contractions occur between `fermionic` and
-  `bosonic` fields. -/
+  In other words, in a `GradingCompliant` Wick contraction no contractions occur between
+  `fermionic` and `bosonic` fields. -/
 def GradingCompliant (φs : List 𝓕.FieldOp) (φsΛ : WickContraction φs.length) :=
   ∀ (a : φsΛ.1), (𝓕 |>ₛ φs[φsΛ.fstFieldOfContract a]) = (𝓕 |>ₛ φs[φsΛ.sndFieldOfContract a])
 
diff --git a/HepLean/PerturbationTheory/WickContraction/ExtractEquiv.lean b/HepLean/PerturbationTheory/WickContraction/ExtractEquiv.lean
index 6e17b3c..31c0989 100644
--- a/HepLean/PerturbationTheory/WickContraction/ExtractEquiv.lean
+++ b/HepLean/PerturbationTheory/WickContraction/ExtractEquiv.lean
@@ -107,4 +107,52 @@ lemma sum_extractEquiv_congr [AddCommMonoid M] {n m : ℕ} (i : Fin n) (f : Wick
   rw [Finset.sum_sigma']
   rfl
 
+/-- For `n = 3` there are `4` possible Wick contractions:
+
+- `∅`, corresponding to the case where no fields are contracted.
+- `{{0, 1}}`, corresponding to the case where the field at position `0` and `1` are contracted.
+- `{{0, 2}}`, corresponding to the case where the field at position `0` and `2` are contracted.
+- `{{1, 2}}`, corresponding to the case where the field at position `1` and `2` are contracted.
+
+The proof of this result uses the fact that Lean is an executable programming language
+and can calculate all Wick contractions for a given `n`. -/
+lemma mem_three (c : WickContraction 3) : c.1 ∈ ({∅, {{0, 1}}, {{0, 2}}, {{1, 2}}} :
+    Finset (Finset (Finset (Fin 3)))) := by
+  fin_cases c <;>
+    simp only [Fin.isValue, Nat.succ_eq_add_one, Nat.reduceAdd, Function.Embedding.coeFn_mk,
+      Finset.mem_insert, Finset.mem_singleton]
+  · exact Or.inl rfl
+  · exact Or.inr (Or.inl rfl)
+  · exact Or.inr (Or.inr (Or.inl rfl))
+  · exact Or.inr (Or.inr (Or.inr rfl))
+
+/-- For `n = 4` there are `10` possible Wick contractions including e.g.
+
+- `∅`, corresponding to the case where no fields are contracted.
+- `{{0, 1}, {2, 3}}`, corresponding to the case where the fields at position `0` and `1` are
+  contracted, and the fields at position `2` and `3` are contracted.
+- `{{0, 2}, {1, 3}}`, corresponding to the case where the fields at position `0` and `2` are
+  contracted, and the fields at position `1` and `3` are contracted.
+
+The proof of this result uses the fact that Lean is an executable programming language
+and can calculate all Wick contractions for a given `n`.
+-/
+lemma mem_four (c : WickContraction 4) : c.1 ∈ ({∅,
+    {{0, 1}}, {{0, 2}}, {{0, 3}}, {{1, 2}}, {{1, 3}}, {{2,3}},
+    {{0, 1}, {2, 3}}, {{0, 2}, {1, 3}}, {{0, 3}, {1, 2}}} :
+    Finset (Finset (Finset (Fin 4)))) := by
+  fin_cases c <;>
+    simp only [Fin.isValue, Nat.succ_eq_add_one, Nat.reduceAdd, Function.Embedding.coeFn_mk,
+      Finset.mem_insert, Finset.mem_singleton]
+  · exact Or.inl rfl -- ∅
+  · exact Or.inr (Or.inl rfl) -- {{0, 1}}
+  · exact Or.inr (Or.inr (Or.inl rfl)) -- {{0, 2}}
+  · exact Or.inr (Or.inr (Or.inr (Or.inl rfl))) -- {{0, 3}}
+  · exact Or.inr (Or.inr (Or.inr (Or.inr (Or.inl rfl)))) -- {{1, 2}}
+  · exact Or.inr (Or.inr (Or.inr (Or.inr (Or.inr (Or.inr (Or.inr (Or.inr (Or.inr rfl))))))))
+  · exact Or.inr (Or.inr (Or.inr (Or.inr (Or.inr (Or.inl rfl))))) -- {{1, 3}}
+  · exact Or.inr (Or.inr (Or.inr (Or.inr (Or.inr (Or.inr (Or.inr (Or.inr (Or.inl rfl))))))))
+  · exact Or.inr (Or.inr (Or.inr (Or.inr (Or.inr (Or.inr (Or.inl rfl)))))) -- {{2, 3 }}
+  · exact Or.inr (Or.inr (Or.inr (Or.inr (Or.inr (Or.inr (Or.inr (Or.inl rfl)))))))
+
 end WickContraction
diff --git a/HepLean/PerturbationTheory/WickContraction/InsertAndContract.lean b/HepLean/PerturbationTheory/WickContraction/InsertAndContract.lean
index 93d67b9..284cff2 100644
--- a/HepLean/PerturbationTheory/WickContraction/InsertAndContract.lean
+++ b/HepLean/PerturbationTheory/WickContraction/InsertAndContract.lean
@@ -25,7 +25,7 @@ open HepLean.Fin
 -/
 
 /-- Given a Wick contraction `φsΛ` for a list `φs` of `𝓕.FieldOp`,
-  a `𝓕.FieldOp` `φ`, an `i ≤ φs.length` and a `j` which is either `none` or
+  an element `φ` of `𝓕.FieldOp`, an `i ≤ φs.length` and a `j` which is either `none` or
   some element of `φsΛ.uncontracted`, the new Wick contraction
   `φsΛ.insertAndContract φ i j` is defined by inserting `φ` into `φs` after
   the first `i`-elements and moving the values representing the contracted pairs in `φsΛ`
@@ -35,6 +35,8 @@ open HepLean.Fin
 
   In other words, `φsΛ.insertAndContract φ i j` is formed by adding `φ` to `φs` at position `i`,
   and contracting `φ` with the field originally at position `j` if `j` is not none.
+  It is a Wick contraction of `φs.insertIdx φ i`, the list `φs` with `φ` inserted at
+  position `i`.
 
   The notation `φsΛ ↩Λ φ i j` is used to denote `φsΛ.insertAndContract φ i j`. -/
 def insertAndContract {φs : List 𝓕.FieldOp} (φ : 𝓕.FieldOp) (φsΛ : WickContraction φs.length)
@@ -285,11 +287,11 @@ lemma insert_fin_eq_self (φ : 𝓕.FieldOp) {φs : List 𝓕.FieldOp}
     rfl
 
 /-- For a list `φs` of `𝓕.FieldOp`, a Wick contraction `φsΛ` of `φs`, an element `φ` of
-  `𝓕.FieldOp`, a `i ≤ φs.length` a sum over
+  `𝓕.FieldOp` and a `i ≤ φs.length` then a sum over
   Wick contractions of `φs` with `φ` inserted at `i` is equal to the sum over Wick contractions
   `φsΛ` of just `φs` and the sum over optional uncontracted elements of the `φsΛ`.
 
-  I.e. `∑ (φsΛ : WickContraction (φs.insertIdx i φ).length), f φsΛ` is equal to
+  In other words, `∑ (φsΛ : WickContraction (φs.insertIdx i φ).length), f φsΛ` is equal to
   `∑ (φsΛ : WickContraction φs.length), ∑ (k : Option φsΛ.uncontracted), f (φsΛ ↩Λ φ i k) `.
   where `(φs.insertIdx i φ)` is `φs` with `φ` inserted at position `i`. -/
 lemma insertLift_sum (φ : 𝓕.FieldOp) {φs : List 𝓕.FieldOp}
diff --git a/HepLean/PerturbationTheory/WickContraction/Join.lean b/HepLean/PerturbationTheory/WickContraction/Join.lean
index ec1754d..994309b 100644
--- a/HepLean/PerturbationTheory/WickContraction/Join.lean
+++ b/HepLean/PerturbationTheory/WickContraction/Join.lean
@@ -25,7 +25,13 @@ open FieldOpAlgebra
 
 /-- Given a list `φs` of `𝓕.FieldOp`, a Wick contraction `φsΛ` of `φs` and a Wick contraction
   `φsucΛ` of `[φsΛ]ᵘᶜ`, `join φsΛ φsucΛ` is defined as the Wick contraction of `φs` consisting of
-  the contractions in `φsΛ` and those in `φsucΛ`. -/
+  the contractions in `φsΛ` and those in `φsucΛ`.
+
+  As an example, for `φs = [φ1, φ2, φ3, φ4]`,
+  `φsΛ = {{0, 1}}` corresponding to the contraction of `φ1` and `φ2` in `φs` and
+  `φsucΛ = {{0, 1}}`
+  corresponding to the contraction of `φ3` and `φ4` in `[φsΛ]ᵘᶜ = [φ3, φ4]`, then
+  `join φsΛ φsucΛ` is the contraction `{{0, 1}, {2, 3}}` of `φs`. -/
 def join {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length)
     (φsucΛ : WickContraction [φsΛ]ᵘᶜ.length) : WickContraction φs.length :=
   ⟨φsΛ.1 ∪ φsucΛ.1.map (Finset.mapEmbedding uncontractedListEmd).toEmbedding, by
diff --git a/HepLean/PerturbationTheory/WickContraction/Sign/Basic.lean b/HepLean/PerturbationTheory/WickContraction/Sign/Basic.lean
index 866a125..7638d3f 100644
--- a/HepLean/PerturbationTheory/WickContraction/Sign/Basic.lean
+++ b/HepLean/PerturbationTheory/WickContraction/Sign/Basic.lean
@@ -30,8 +30,9 @@ def signFinset (c : WickContraction n) (i1 i2 : Fin n) : Finset (Fin n) :=
 
 /-- For a list `φs` of `𝓕.FieldOp`, and a Wick contraction `φsΛ` of `φs`,
   the complex number `φsΛ.sign` is defined to be the sign (`1` or `-1`) corresponding
-  to the number of `fermionic`-`fermionic` exchanges that must done to put
-  contracted pairs with `φsΛ` next to one another, starting from the contracted pair
+  to the number of `fermionic`-`fermionic` exchanges that must be done to put
+  contracted pairs within `φsΛ` next to one another, starting recursively
+  from the contracted pair
   whose first element occurs at the left-most position. -/
 def sign (φs : List 𝓕.FieldOp) (φsΛ : WickContraction φs.length) : ℂ :=
   ∏ (a : φsΛ.1), 𝓢(𝓕 |>ₛ φs[φsΛ.sndFieldOfContract a],
diff --git a/HepLean/PerturbationTheory/WickContraction/Sign/InsertNone.lean b/HepLean/PerturbationTheory/WickContraction/Sign/InsertNone.lean
index 61dc471..11643f0 100644
--- a/HepLean/PerturbationTheory/WickContraction/Sign/InsertNone.lean
+++ b/HepLean/PerturbationTheory/WickContraction/Sign/InsertNone.lean
@@ -239,7 +239,7 @@ lemma signInsertNone_eq_filterset (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
   · exact hG
 
 /-- For a list `φs = φ₀…φₙ` of `𝓕.FieldOp`, a graded compliant Wick contraction `φsΛ` of `φs`,
-  an `i ≤ φs.length` and a `φ` in `𝓕.FieldOp`, the following relation holds
+  an `i ≤ φs.length`, and a `φ` in `𝓕.FieldOp`, then
   `(φsΛ ↩Λ φ i none).sign = s * φsΛ.sign`
   where `s` is the sign got by moving `φ` through the elements of `φ₀…φᵢ₋₁` which
   are contracted with some element.
@@ -255,7 +255,7 @@ lemma sign_insert_none (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
   exact hG
 
 /-- For a list `φs = φ₀…φₙ` of `𝓕.FieldOp`, a graded compliant Wick contraction `φsΛ` of `φs`,
-  and a `φ` in `𝓕.FieldOp`, the following relation holds `(φsΛ ↩Λ φ 0 none).sign = φsΛ.sign`.
+  and a `φ` in `𝓕.FieldOp`, then `(φsΛ ↩Λ φ 0 none).sign = φsΛ.sign`.
 
   This is a direct corollary of `sign_insert_none`. -/
 lemma sign_insert_none_zero (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
diff --git a/HepLean/PerturbationTheory/WickContraction/Sign/Join.lean b/HepLean/PerturbationTheory/WickContraction/Sign/Join.lean
index d58f5d6..1b2c689 100644
--- a/HepLean/PerturbationTheory/WickContraction/Sign/Join.lean
+++ b/HepLean/PerturbationTheory/WickContraction/Sign/Join.lean
@@ -422,7 +422,7 @@ lemma join_sign_induction {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs
   `(join φsΛ φsucΛ).sign = φsΛ.sign * φsucΛ.sign`.
 
   In `φsΛ.sign` the sign is determined by starting with the contracted pair
-  whose first element occurs at the left-most position. This lemma manifests that
+  whose first element occurs at the left-most position. This lemma manifests that this
   choice does not matter, and that contracted pairs can be brought together in any order. -/
 lemma join_sign {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length)
     (φsucΛ : WickContraction [φsΛ]ᵘᶜ.length) (hc : φsΛ.GradingCompliant) :
diff --git a/HepLean/PerturbationTheory/WickContraction/StaticContract.lean b/HepLean/PerturbationTheory/WickContraction/StaticContract.lean
index 0daeb10..e481b91 100644
--- a/HepLean/PerturbationTheory/WickContraction/StaticContract.lean
+++ b/HepLean/PerturbationTheory/WickContraction/StaticContract.lean
@@ -19,9 +19,9 @@ variable {n : ℕ} (c : WickContraction n)
 open HepLean.List
 open FieldOpAlgebra
 
-/-- For a list `φs` of `𝓕.FieldOp` and a Wick contraction `φsΛ` the
+/-- For a list `φs` of `𝓕.FieldOp` and a Wick contraction `φsΛ`, the
   element of the center of `𝓕.FieldOpAlgebra`, `φsΛ.staticContract` is defined as the product
-  of `[anPart φs[j], φs[k]]ₛ` over contracted pairs `{j, k}` (both indices of `φs`) in `φsΛ`
+  of `[anPart φs[j], φs[k]]ₛ` over contracted pairs `{j, k}` in `φsΛ`
   with `j < k`. -/
 noncomputable def staticContract {φs : List 𝓕.FieldOp}
     (φsΛ : WickContraction φs.length) :
@@ -31,7 +31,7 @@ noncomputable def staticContract {φs : List 𝓕.FieldOp}
       superCommute_anPart_ofFieldOp_mem_center _ _⟩
 
 /-- For a list `φs = φ₀…φₙ` of `𝓕.FieldOp`, a Wick contraction `φsΛ` of `φs`, an element `φ` of
-  `𝓕.FieldOp`, and a `i ≤ φs.length` the following relation holds
+  `𝓕.FieldOp`, and a `i ≤ φs.length`, then the following relation holds:
 
   `(φsΛ ↩Λ φ i none).staticContract = φsΛ.staticContract`
 
diff --git a/scripts/MetaPrograms/notes.lean b/scripts/MetaPrograms/notes.lean
index 43fea15..a3f5d48 100644
--- a/scripts/MetaPrograms/notes.lean
+++ b/scripts/MetaPrograms/notes.lean
@@ -143,10 +143,21 @@ def perturbationTheory : Note where
   parts := [
     .h1 "Introduction",
     .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,
+    .p "In this note we walk through the important parts of the proof of the three versions of
+      Wick's theorem for field operators containing carrying both fermionic and bosonic statitics,
       as it appears in HepLean. Not every lemma or definition is covered here.
       The aim is to give just enough that the story can be understood.",
+    .p "
+     Before proceeding with the steps in the proof, we review some basic terminology
+     related to Lean and type theory. The most important notion is that of a type.
+     We don't give any formal definition here, except to say that a type `T`, like a set, has
+     elements `x` which we say are of type `T` and write `x : T`. Examples of types include,
+     the type of natural numbers `ℕ`, the type of real numbers `ℝ`, the type of numbers
+     `0, …, n-1` denoted `Fin n`. Given two types `T` and `S`, we can form the product type `T × S`,
+     and the function type `T → S`.
+
+     Types form the foundation of Lean and the theory behind them will be used both explicitly and
+      implicitly throughout this note.",
     .h1 "Field operators",
     .h2 "Field statistics",
     .name ``FieldStatistic .complete,
@@ -159,6 +170,7 @@ def perturbationTheory : Note where
     .name ``FieldSpecification.fieldOpStatistic .complete,
     .name ``CreateAnnihilate .complete,
     .name ``FieldSpecification.CrAnFieldOp .complete,
+    .name ``FieldSpecification.crAnFieldOpToCreateAnnihilate .complete,
     .name ``FieldSpecification.crAnStatistics .complete,
     .name `FieldSpecification.notation_remark .complete,
     .h2 "Field-operator free algebra",
@@ -208,6 +220,8 @@ def perturbationTheory : Note where
     .h1 "Wick Contractions",
     .h2 "Definition",
     .name ``WickContraction .complete,
+    .name ``WickContraction.mem_three .complete,
+    .name ``WickContraction.mem_four .complete,
     .name `WickContraction.contraction_notation .complete,
     .name ``WickContraction.GradingCompliant .complete,
     .h2 "Aside: Cardinality",
@@ -235,7 +249,7 @@ def perturbationTheory : Note where
     .name ``WickContraction.staticContract .complete,
     .name ``WickContraction.staticContract_insert_none .complete,
     .name ``WickContraction.staticContract_insert_some .complete,
-    .h2 "Static wick terms",
+    .h2 "Static Wick terms",
     .name ``WickContraction.staticWickTerm .complete,
     .name ``WickContraction.staticWickTerm_empty_nil .complete,
     .name ``WickContraction.staticWickTerm_insert_zero_none .complete,