From 26d2c24c8309d9c145152c1b62f92c272c2e0581 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Sun, 9 Feb 2025 14:50:03 +0000
Subject: [PATCH 1/6] refactor: More spelling

---
 HepLean/FlavorPhysics/CKMMatrix/Relations.lean | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/HepLean/FlavorPhysics/CKMMatrix/Relations.lean b/HepLean/FlavorPhysics/CKMMatrix/Relations.lean
index 480dae4..8731be0 100644
--- a/HepLean/FlavorPhysics/CKMMatrix/Relations.lean
+++ b/HepLean/FlavorPhysics/CKMMatrix/Relations.lean
@@ -21,7 +21,7 @@ open ComplexConjugate
 
 section rows
 
-/-- The absolute value squared of any rwo of a CKM matrix is `1`, in terms of `Vabs`. -/
+/-- The absolute value squared of any row of a CKM matrix is `1`, in terms of `Vabs`. -/
 lemma VAbs_sum_sq_row_eq_one (V : Quotient CKMMatrixSetoid) (i : Fin 3) :
     (VAbs i 0 V) ^ 2 + (VAbs i 1 V) ^ 2 + (VAbs i 2 V) ^ 2 = 1 := by
   obtain ⟨V, hV⟩ := Quot.exists_rep V
@@ -36,31 +36,31 @@ lemma VAbs_sum_sq_row_eq_one (V : Quotient CKMMatrixSetoid) (i : Fin 3) :
   rw [← ofReal_inj]
   simpa using ht
 
-/-- The absolute value squared of the first rwo of a CKM matrix is `1`, in terms of `abs`. -/
+/-- The absolute value squared of the first row of a CKM matrix is `1`, in terms of `abs`. -/
 lemma fst_row_normalized_abs (V : CKMMatrix) : abs [V]ud ^ 2 + abs [V]us ^ 2 + abs [V]ub ^ 2 = 1 :=
   VAbs_sum_sq_row_eq_one ⟦V⟧ 0
 
-/-- The absolute value squared of the second rwo of a CKM matrix is `1`, in terms of `abs`. -/
+/-- The absolute value squared of the second row of a CKM matrix is `1`, in terms of `abs`. -/
 lemma snd_row_normalized_abs (V : CKMMatrix) : abs [V]cd ^ 2 + abs [V]cs ^ 2 + abs [V]cb ^ 2 = 1 :=
   VAbs_sum_sq_row_eq_one ⟦V⟧ 1
 
-/-- The absolute value squared of the third rwo of a CKM matrix is `1`, in terms of `abs`. -/
+/-- The absolute value squared of the third row of a CKM matrix is `1`, in terms of `abs`. -/
 lemma thd_row_normalized_abs (V : CKMMatrix) : abs [V]td ^ 2 + abs [V]ts ^ 2 + abs [V]tb ^ 2 = 1 :=
   VAbs_sum_sq_row_eq_one ⟦V⟧ 2
 
-/-- The absolute value squared of the first rwo of a CKM matrix is `1`, in terms of `nomSq`. -/
+/-- The absolute value squared of the first row of a CKM matrix is `1`, in terms of `nomSq`. -/
 lemma fst_row_normalized_normSq (V : CKMMatrix) :
     normSq [V]ud + normSq [V]us + normSq [V]ub = 1 := by
   repeat rw [← Complex.sq_abs]
   exact V.fst_row_normalized_abs
 
-/-- The absolute value squared of the second rwo of a CKM matrix is `1`, in terms of `nomSq`. -/
+/-- The absolute value squared of the second row of a CKM matrix is `1`, in terms of `nomSq`. -/
 lemma snd_row_normalized_normSq (V : CKMMatrix) :
     normSq [V]cd + normSq [V]cs + normSq [V]cb = 1 := by
   repeat rw [← Complex.sq_abs]
   exact V.snd_row_normalized_abs
 
-/-- The absolute value squared of the third rwo of a CKM matrix is `1`, in terms of `nomSq`. -/
+/-- The absolute value squared of the third row of a CKM matrix is `1`, in terms of `nomSq`. -/
 lemma thd_row_normalized_normSq (V : CKMMatrix) :
     normSq [V]td + normSq [V]ts + normSq [V]tb = 1 := by
   repeat rw [← Complex.sq_abs]

From 4096010e70e9ad9d7f4bc626af8352cdaca2b809 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Mon, 10 Feb 2025 10:21:57 +0000
Subject: [PATCH 2/6] doc: Edits to Wick theorem docs

---
 HepLean/Lorentz/Group/Proper.lean             |  2 +-
 HepLean/Lorentz/MinkowskiMatrix.lean          |  2 +-
 .../PerturbationTheory/CreateAnnihilate.lean  |  2 +-
 .../FeynmanDiagrams/Momentum.lean             | 10 +--
 .../FieldOpAlgebra/Basic.lean                 | 45 ++++++++------
 .../FieldOpAlgebra/Grading.lean               |  7 ++-
 .../FieldOpAlgebra/NormalOrder/Basic.lean     |  5 +-
 .../FieldOpAlgebra/NormalOrder/Lemmas.lean    |  2 +-
 .../NormalOrder/WickContractions.lean         |  4 +-
 .../FieldOpAlgebra/StaticWickTerm.lean        |  2 +-
 .../FieldOpAlgebra/TimeOrder.lean             |  3 +-
 .../FieldOpAlgebra/Universality.lean          |  5 +-
 .../FieldOpAlgebra/WicksTheorem.lean          |  4 +-
 .../FieldOpFreeAlgebra/Basic.lean             | 42 +++++++------
 .../FieldOpFreeAlgebra/Grading.lean           |  6 +-
 .../FieldOpFreeAlgebra/NormalOrder.lean       |  5 +-
 .../FieldOpFreeAlgebra/SuperCommute.lean      |  2 +-
 .../FieldOpFreeAlgebra/TimeOrder.lean         |  2 +
 .../FieldSpecification/Basic.lean             | 42 ++++++++-----
 .../FieldSpecification/CrAnFieldOp.lean       | 61 +++++++++++++------
 .../FieldSpecification/NormalOrder.lean       |  9 +--
 .../FieldSpecification/TimeOrder.lean         |  4 +-
 .../FieldStatistics/ExchangeSign.lean         |  4 +-
 .../WickContraction/Basic.lean                | 18 +-----
 .../WickContraction/ExtractEquiv.lean         | 48 +++++++++++++++
 .../WickContraction/InsertAndContract.lean    |  8 ++-
 .../WickContraction/Join.lean                 |  8 ++-
 .../WickContraction/Sign/Basic.lean           |  5 +-
 .../WickContraction/Sign/InsertNone.lean      |  4 +-
 .../WickContraction/Sign/Join.lean            |  2 +-
 .../WickContraction/StaticContract.lean       |  6 +-
 scripts/MetaPrograms/notes.lean               | 20 +++++-
 32 files changed, 255 insertions(+), 134 deletions(-)

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,

From b30a49d7db71c7bbff0664c49ea98bf2d7957de5 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Mon, 10 Feb 2025 10:40:07 +0000
Subject: [PATCH 3/6] refactor: More docs for Wick's theorems

---
 .../FieldOpAlgebra/StaticWickTerm.lean        |  8 +++---
 .../FieldOpAlgebra/StaticWickTheorem.lean     |  2 +-
 .../FieldOpAlgebra/TimeContraction.lean       |  2 +-
 .../FieldOpAlgebra/WickTerm.lean              | 19 ++++++-------
 .../FieldOpAlgebra/WicksTheorem.lean          |  4 +--
 .../FieldOpAlgebra/WicksTheoremNormal.lean    | 27 ++++++++++---------
 .../WickContraction/TimeCond.lean             |  6 ++---
 .../WickContraction/TimeContract.lean         |  8 +++---
 8 files changed, 38 insertions(+), 38 deletions(-)

diff --git a/HepLean/PerturbationTheory/FieldOpAlgebra/StaticWickTerm.lean b/HepLean/PerturbationTheory/FieldOpAlgebra/StaticWickTerm.lean
index abf040c..d4abf71 100644
--- a/HepLean/PerturbationTheory/FieldOpAlgebra/StaticWickTerm.lean
+++ b/HepLean/PerturbationTheory/FieldOpAlgebra/StaticWickTerm.lean
@@ -31,8 +31,8 @@ noncomputable section
 def staticWickTerm {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) : 𝓕.FieldOpAlgebra :=
   φsΛ.sign • φsΛ.staticContract * 𝓝(ofFieldOpList [φsΛ]ᵘᶜ)
 
-/-- For the empty list `[]` of `𝓕.FieldOp`, the `staticWickTerm` of the empty Wick contraction
-  `empty` of `[]` (its only Wick contraction) is `1`. -/
+/-- For the empty list `[]` of `𝓕.FieldOp`, the `staticWickTerm` of the Wick contraction
+  corresponding to the empty set `∅` (the only Wick contraction of `[]`) is `1`. -/
 @[simp]
 lemma staticWickTerm_empty_nil :
     staticWickTerm (empty (n := ([] : List 𝓕.FieldOp).length)) = 1 := by
@@ -116,9 +116,9 @@ lemma staticWickTerm_insert_zero_some (φ : 𝓕.FieldOp) (φs : List 𝓕.Field
 For a list `φs = φ₀…φₙ` of `𝓕.FieldOp`, a Wick contraction `φsΛ` of `φs`, the following relation
 holds
 
-`φ * φsΛ.staticWickTerm = ∑ k, (φsΛ ↩Λ φ i k).wickTerm`
+`φ * φsΛ.staticWickTerm = ∑ k, (φsΛ ↩Λ φ 0 k).staticWickTerm`
 
-where the sum is over all `k` in `Option φsΛ.uncontracted` (so either `none` or `some k`).
+where the sum is over all `k` in `Option φsΛ.uncontracted`,  so `k` is either `none` or `some k`.
 
 The proof of proceeds as follows:
 - `ofFieldOp_mul_normalOrder_ofFieldOpList_eq_sum` is used to expand `φ 𝓝([φsΛ]ᵘᶜ)` as
diff --git a/HepLean/PerturbationTheory/FieldOpAlgebra/StaticWickTheorem.lean b/HepLean/PerturbationTheory/FieldOpAlgebra/StaticWickTheorem.lean
index a873b97..7b060b9 100644
--- a/HepLean/PerturbationTheory/FieldOpAlgebra/StaticWickTheorem.lean
+++ b/HepLean/PerturbationTheory/FieldOpAlgebra/StaticWickTheorem.lean
@@ -22,7 +22,7 @@ namespace FieldOpAlgebra
 /--
 For a list `φs` of `𝓕.FieldOp`, the static version of Wick's theorem states that
 
-`φs =∑ φsΛ, φsΛ.staticWickTerm`
+`φs = ∑ φsΛ, φsΛ.staticWickTerm`
 
 where the sum is over all Wick contraction `φsΛ`.
 
diff --git a/HepLean/PerturbationTheory/FieldOpAlgebra/TimeContraction.lean b/HepLean/PerturbationTheory/FieldOpAlgebra/TimeContraction.lean
index 5c76e62..0004319 100644
--- a/HepLean/PerturbationTheory/FieldOpAlgebra/TimeContraction.lean
+++ b/HepLean/PerturbationTheory/FieldOpAlgebra/TimeContraction.lean
@@ -24,7 +24,7 @@ namespace FieldOpAlgebra
 open FieldStatistic
 
 /-- For a field specification `𝓕`, and `φ` and `ψ` elements of `𝓕.FieldOp`, the element of
-  `𝓕.FieldOpAlgebra`, `timeContract φ ψ` is defined to be `𝓣(φψ)- 𝓝(φψ)`. -/
+  `𝓕.FieldOpAlgebra`, `timeContract φ ψ` is defined to be `𝓣(φψ) - 𝓝(φψ)`. -/
 def timeContract (φ ψ : 𝓕.FieldOp) : 𝓕.FieldOpAlgebra :=
     𝓣(ofFieldOp φ * ofFieldOp ψ) - 𝓝(ofFieldOp φ * ofFieldOp ψ)
 
diff --git a/HepLean/PerturbationTheory/FieldOpAlgebra/WickTerm.lean b/HepLean/PerturbationTheory/FieldOpAlgebra/WickTerm.lean
index 3f70846..cc3af9d 100644
--- a/HepLean/PerturbationTheory/FieldOpAlgebra/WickTerm.lean
+++ b/HepLean/PerturbationTheory/FieldOpAlgebra/WickTerm.lean
@@ -33,8 +33,8 @@ noncomputable section
 def wickTerm {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) : 𝓕.FieldOpAlgebra :=
   φsΛ.sign • φsΛ.timeContract * 𝓝(ofFieldOpList [φsΛ]ᵘᶜ)
 
-/-- For the empty list `[]` of `𝓕.FieldOp`, the `wickTerm` of the empty Wick contraction
-  `empty` of `[]` (its only Wick contraction) is `1`. -/
+/-- For the empty list `[]` of `𝓕.FieldOp`, the `wickTerm` of the Wick contraction
+  corresponding to the empty set `∅` (the only Wick contraction of `[]`) is `1`. -/
 @[simp]
 lemma wickTerm_empty_nil :
     wickTerm (empty (n := ([] : List 𝓕.FieldOp).length)) = 1 := by
@@ -95,9 +95,9 @@ lemma wickTerm_insert_none (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
 
 /-- For a list `φs = φ₀…φₙ` of `𝓕.FieldOp`, a Wick contraction `φsΛ` of `φs`, an element `φ` of
   `𝓕.FieldOp`, `i ≤ φs.length` and a `k` in `φsΛ.uncontracted`,
-  such that all `FieldOp` in `φ₀…φᵢ₋₁` have time strictly less then `φ` and
+  such that all `𝓕.FieldOp` in `φ₀…φᵢ₋₁` have time strictly less then `φ` and
   `φ` has a time greater then or equal to all `FieldOp` in `φ₀…φₙ`, then
-  `(φsΛ ↩Λ φ i (some k)).wickTerm`
+  `(φsΛ ↩Λ φ i (some k)).staticWickTerm`
 is equal the product of
 - the sign `𝓢(φ, φ₀…φᵢ₋₁) `
 - the sign `φsΛ.sign`
@@ -175,17 +175,18 @@ lemma wickTerm_insert_some (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
       exact hg'
 
 /--
-Let `φsΛ` be a Wick contraction for `φs = φ₀φ₁…φₙ`. Let `φ` be a field with time
-greater then or equal to all the `FieldOp` in `φs`. Let `i ≤ φs.length` be such that
-all `FieldOp` in `φ₀…φᵢ₋₁` have time strictly less then `φ`. Then
+For a list `φs = φ₀…φₙ` of `𝓕.FieldOp`, a Wick contraction `φsΛ` of `φs`, an element `φ` of
+  `𝓕.FieldOp`, and `i ≤ φs.length`
+  such that all `𝓕.FieldOp` in `φ₀…φᵢ₋₁` have time strictly less then `φ` and
+  `φ` has a time greater then or equal to all `FieldOp` in `φ₀…φₙ`, then
 
 `φ * φsΛ.wickTerm = 𝓢(φ, φ₀…φᵢ₋₁) • ∑ k, (φsΛ ↩Λ φ i k).wickTerm`
 
-where the sum is over all `k` in `Option φsΛ.uncontracted` (so either `none` or `some k`).
+where the sum is over all `k` in `Option φsΛ.uncontracted`, so `k` is either `none` or `some k`.
 
 The proof of proceeds as follows:
 - `ofFieldOp_mul_normalOrder_ofFieldOpList_eq_sum` is used to expand `φ 𝓝([φsΛ]ᵘᶜ)` as
-  a sum over `k` in `Option φsΛ.uncontracted` of terms involving `[anPart φ, φs[k]]ₛ`..
+  a sum over `k` in `Option φsΛ.uncontracted` of terms involving `[anPart φ, φs[k]]ₛ`.
 - Then `wickTerm_insert_none` and `wickTerm_insert_some` are used to equate terms.
 -/
 lemma mul_wickTerm_eq_sum (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp) (i : Fin φs.length.succ)
diff --git a/HepLean/PerturbationTheory/FieldOpAlgebra/WicksTheorem.lean b/HepLean/PerturbationTheory/FieldOpAlgebra/WicksTheorem.lean
index e6df34c..2ca9795 100644
--- a/HepLean/PerturbationTheory/FieldOpAlgebra/WicksTheorem.lean
+++ b/HepLean/PerturbationTheory/FieldOpAlgebra/WicksTheorem.lean
@@ -75,11 +75,11 @@ The inductive step works as follows:
 
 For the LHS:
 1. `timeOrder_eq_maxTimeField_mul_finset` is used to write
-  `𝓣(φ₀…φₙ)` as ` 𝓢(φᵢ,φ₀…φᵢ₋₁) • φᵢ * 𝓣(φ₀…φᵢ₋₁φᵢ₊₁φₙ)` where `φᵢ` is
+  `𝓣(φ₀…φₙ)` as `𝓢(φᵢ,φ₀…φᵢ₋₁) • φᵢ * 𝓣(φ₀…φᵢ₋₁φᵢ₊₁φₙ)` where `φᵢ` is
   the maximal time field in `φ₀…φₙ`
 2. The induction hypothesis is then used on `𝓣(φ₀…φᵢ₋₁φᵢ₊₁φₙ)` to expand it as a sum over
   Wick contractions of `φ₀…φᵢ₋₁φᵢ₊₁φₙ`.
-3. This gives terms of the form `φᵢ * φsΛ.timeContract` on which
+3. This gives terms of the form `φᵢ * φsΛ.wickTerm` on which
   `mul_wickTerm_eq_sum` is used where `φsΛ` is a Wick contraction of `φ₀…φᵢ₋₁φᵢ₊₁φ`,
   to rewrite terms as a sum over optional uncontracted elements of `φsΛ`
 
diff --git a/HepLean/PerturbationTheory/FieldOpAlgebra/WicksTheoremNormal.lean b/HepLean/PerturbationTheory/FieldOpAlgebra/WicksTheoremNormal.lean
index ac694dd..679abaf 100644
--- a/HepLean/PerturbationTheory/FieldOpAlgebra/WicksTheoremNormal.lean
+++ b/HepLean/PerturbationTheory/FieldOpAlgebra/WicksTheoremNormal.lean
@@ -31,9 +31,10 @@ This result follows from
 - `static_wick_theorem` to rewrite `𝓣(φs)` on the left hand side as a sum of
   `𝓣(φsΛ.staticWickTerm)`.
 - `EqTimeOnly.timeOrder_staticContract_of_not_mem` and `timeOrder_timeOrder_mid` to set to
-  zero those terms in which the contracted elements do not have equal time.
-- `staticContract_eq_timeContract_of_eqTimeOnly` to rewrite the static contract as a time contract
-  for those terms which have equal time.
+  those `𝓣(φsΛ.staticWickTerm)` for which `φsΛ` has a contracted pair which are not
+  equal time to zero.
+- `staticContract_eq_timeContract_of_eqTimeOnly` to rewrite the static contract
+  in the reminaing `𝓣(φsΛ.staticWickTerm)` as a time contract.
 - `timeOrder_timeContract_mul_of_eqTimeOnly_left` to move the time contracts out of the time
   ordering.
 -/
@@ -111,20 +112,20 @@ For a list `φs` of `𝓕.FieldOp`, then `𝓣(φs)` is equal to the sum of
 
 - `∑ φsΛ, φsΛ.wickTerm` where the sum is over all Wick contraction `φsΛ` which have
   no contractions of equal time.
-- `∑ φsΛ, sign φs ↑φsΛ • (φsΛ.1).timeContract ∑ φssucΛ, φssucΛ.wickTerm`, where
+- `∑ φsΛ, φsΛ.sign • φsΛ.timeContract  * (∑ φssucΛ, φssucΛ.wickTerm)`, where
   the first sum is over all Wick contraction `φsΛ` which only have equal time contractions
   and the second sum is over all Wick contraction `φssucΛ` of the uncontracted elements of `φsΛ`
   which do not have any equal time contractions.
 
-The proof of this result relies on `wicks_theorem` to rewrite `𝓣(φs)` as a sum over
-all Wick contractions.
-The sum over all Wick contractions is then split additively into two parts using based on having or
-not having equal time contractions.
-The sum over Wick contractions which do have equal time contractions is turned into two sums
-one over the Wick contractions which only have equal time contractions and the other over the
-uncontracted elements of the Wick contraction which do not have equal time contractions using
-`join`.
-The properties of `join_sign_timeContract` is then used to equate terms.
+The proof of proceeds as follows
+- `wicks_theorem` is used to rewrite `𝓣(φs)` as a sum over all Wick contractions.
+- The sum over all Wick contractions is then split additively into two parts using based on having
+  or not having an equal time contractions.
+- Using `join`, the sum `∑ φsΛ, _` over Wick contractions which do have equal time contractions
+  is split into two sums `∑ φsΛ, ∑ φsucΛ, _`, the first over non-zero elements
+  which only have equal time contractions and the second over Wick contractions `φsucΛ` of
+  `[φsΛ]ᵘᶜ` which do not have equal time contractions.
+- `join_sign_timeContract` is then used to equate terms.
 -/
 lemma timeOrder_haveEqTime_split (φs : List 𝓕.FieldOp) :
     𝓣(ofFieldOpList φs) = (∑ (φsΛ : {φsΛ : WickContraction φs.length // ¬ HaveEqTime φsΛ}),
diff --git a/HepLean/PerturbationTheory/WickContraction/TimeCond.lean b/HepLean/PerturbationTheory/WickContraction/TimeCond.lean
index 4cc6e70..cde0f93 100644
--- a/HepLean/PerturbationTheory/WickContraction/TimeCond.lean
+++ b/HepLean/PerturbationTheory/WickContraction/TimeCond.lean
@@ -97,7 +97,7 @@ lemma empty_mem {φs : List 𝓕.FieldOp} : empty (n := φs.length).EqTimeOnly :
   simp [empty]
 
 /-- Let `φs` be a list of `𝓕.FieldOp` and `φsΛ` a `WickContraction` of `φs` with
-  in which every contraction involves two `FieldOp`s that have the same time. Then
+  in which every contraction involves two `𝓕FieldOp`s that have the same time, then
   `φsΛ.staticContract = φsΛ.timeContract`. -/
 lemma staticContract_eq_timeContract_of_eqTimeOnly (h : φsΛ.EqTimeOnly) :
     φsΛ.staticContract = φsΛ.timeContract := by
@@ -194,7 +194,7 @@ lemma timeOrder_timeContract_mul_of_eqTimeOnly_mid {φs : List 𝓕.FieldOp}
   exact timeOrder_timeContract_mul_of_eqTimeOnly_mid_induction φsΛ hl a b φsΛ.1.card rfl
 
 /-- Let `φs` be a list of `𝓕.FieldOp`, `φsΛ` a `WickContraction` of `φs` with
-  in which every contraction involves two `FieldOp`s that have the same time and
+  in which every contraction involves two `𝓕.FieldOp`s that have the same time and
   `b` a general element in `𝓕.FieldOpAlgebra`. Then
   `𝓣(φsΛ.timeContract.1 * b) = φsΛ.timeContract.1 * 𝓣(b)`.
 
@@ -248,7 +248,7 @@ lemma timeOrder_timeContract_of_not_eqTimeOnly {φs : List 𝓕.FieldOp}
   simp_all
 
 /-- Let `φs` be a list of `𝓕.FieldOp` and `φsΛ` a `WickContraction` with
-  at least one contraction between `FieldOp` that do not have the same time. Then
+  at least one contraction between `𝓕.FieldOp` that do not have the same time. Then
   `𝓣(φsΛ.staticContract.1) = 0`. -/
 lemma timeOrder_staticContract_of_not_mem {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length)
     (hl : ¬ φsΛ.EqTimeOnly) : 𝓣(φsΛ.staticContract.1) = 0 := by
diff --git a/HepLean/PerturbationTheory/WickContraction/TimeContract.lean b/HepLean/PerturbationTheory/WickContraction/TimeContract.lean
index 559b286..80549d9 100644
--- a/HepLean/PerturbationTheory/WickContraction/TimeContract.lean
+++ b/HepLean/PerturbationTheory/WickContraction/TimeContract.lean
@@ -21,7 +21,7 @@ open FieldOpAlgebra
 
 /-- For a list `φs` of `𝓕.FieldOp` and a Wick contraction `φsΛ` the
   element of the center of `𝓕.FieldOpAlgebra`, `φsΛ.timeContract` is defined as the product
-  of `timeContract φs[j] φs[k]` over contracted pairs `{j, k}` (both indices of `φs`) in `φsΛ`
+  of `timeContract φs[j] φs[k]` over contracted pairs `{j, k}` in `φsΛ`
   with `j < k`. -/
 noncomputable def timeContract {φs : List 𝓕.FieldOp}
     (φsΛ : WickContraction φs.length) :
@@ -86,7 +86,7 @@ open FieldStatistic
   - `[anPart φ, φs[k]]ₛ`
   - `φsΛ.timeContract`
   - two copies of the exchange sign of `φ` with the uncontracted fields in `φ₀…φₖ₋₁`.
-    These two exchange signs cancle each other out but are included for convenience.
+    These two exchange signs cancel each other out but are included for convenience.
 
   The proof of this result ultimately a consequence of definitions and
   `timeContract_of_timeOrderRel`. -/
@@ -125,15 +125,13 @@ lemma timeContract_insert_some_of_lt
 
 /-- 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` such that `k < i`, with the
-  condition that `φs[k]` does not have has greater or equal time to `φ`, then
+  condition that `φs[k]` does not have time greater or equal to `φ`, then
   `(φsΛ ↩Λ φ i (some k)).timeContract` is equal to the product of
   - `[anPart φ, φs[k]]ₛ`
   - `φsΛ.timeContract`
   - the exchange sign of `φ` with the uncontracted fields in `φ₀…φₖ₋₁`.
   - the exchange sign of `φ` with the uncontracted fields in `φ₀…φₖ`.
 
-  Most of the contributes to the exchange signs cancle.
-
   The proof of this result ultimately a consequence of definitions and
   `timeContract_of_not_timeOrderRel_expand`. -/
 lemma timeContract_insert_some_of_not_lt

From dc5b63c4a758fee67372e8324db8aba25be1c8ac Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Mon, 10 Feb 2025 10:51:44 +0000
Subject: [PATCH 4/6] refactor: Spelling and typos

---
 HepLean/AnomalyCancellation/SM/Permutations.lean          | 4 ++--
 HepLean/BeyondTheStandardModel/GeorgiGlashow/Basic.lean   | 2 +-
 HepLean/BeyondTheStandardModel/PatiSalam/Basic.lean       | 2 +-
 HepLean/Lorentz/ComplexTensor/PauliMatrices/Basis.lean    | 2 +-
 HepLean/Lorentz/Group/Boosts.lean                         | 2 +-
 HepLean/Lorentz/Group/Orthochronous.lean                  | 2 +-
 HepLean/Lorentz/MinkowskiMatrix.lean                      | 2 +-
 HepLean/Lorentz/PauliMatrices/SelfAdjoint.lean            | 8 ++++----
 HepLean/Mathematics/List/InsertionSort.lean               | 2 +-
 HepLean/Meta/Remark/Properties.lean                       | 2 +-
 HepLean/PerturbationTheory/CreateAnnihilate.lean          | 2 +-
 HepLean/PerturbationTheory/FeynmanDiagrams/Momentum.lean  | 8 ++++----
 HepLean/PerturbationTheory/FieldOpAlgebra/Basic.lean      | 4 ++--
 .../FieldOpAlgebra/NormalOrder/Lemmas.lean                | 2 +-
 HepLean/PerturbationTheory/FieldOpAlgebra/WickTerm.lean   | 2 +-
 .../FieldOpAlgebra/WicksTheoremNormal.lean                | 2 +-
 HepLean/PerturbationTheory/FieldSpecification/Basic.lean  | 2 +-
 .../FieldSpecification/CrAnFieldOp.lean                   | 4 ++--
 .../FieldSpecification/CrAnSection.lean                   | 2 +-
 .../PerturbationTheory/FieldSpecification/TimeOrder.lean  | 6 +++---
 HepLean/PerturbationTheory/FieldStatistics/Basic.lean     | 2 +-
 .../PerturbationTheory/WickContraction/Sign/Basic.lean    | 2 +-
 HepLean/PerturbationTheory/WickContraction/TimeCond.lean  | 2 +-
 HepLean/StandardModel/HiggsBoson/GaugeAction.lean         | 4 ++--
 HepLean/Tensors/Tree/Elab.lean                            | 2 +-
 25 files changed, 37 insertions(+), 37 deletions(-)

diff --git a/HepLean/AnomalyCancellation/SM/Permutations.lean b/HepLean/AnomalyCancellation/SM/Permutations.lean
index b49700c..c712c80 100644
--- a/HepLean/AnomalyCancellation/SM/Permutations.lean
+++ b/HepLean/AnomalyCancellation/SM/Permutations.lean
@@ -63,7 +63,7 @@ def repCharges {n : ℕ} : Representation ℚ (PermGroup n) (SMCharges n).Charge
     erw [toSMSpecies_toSpecies_inv]
     rfl
 
-/-- The species chages of a set of charges acted on by a family permutation is the permutation
+/-- The species charges of a set of charges acted on by a family permutation is the permutation
   of those species charges with the corresponding part of the family permutation. -/
 lemma repCharges_toSpecies (f : PermGroup n) (S : (SMCharges n).Charges) (j : Fin 5) :
     toSpecies j (repCharges f S) = toSpecies j S ∘ f⁻¹ j := by
@@ -78,7 +78,7 @@ lemma toSpecies_sum_invariant (m : ℕ) (f : PermGroup n) (S : (SMCharges n).Cha
   exact Fintype.sum_equiv (f⁻¹ j) (fun x => ((fun a => a ^ m) ∘ (toSpecies j) S ∘ ⇑(f⁻¹ j)) x)
     (fun x => ((fun a => a ^ m) ∘ (toSpecies j) S) x) (congrFun rfl)
 
-/-- The gravitional anomaly equations is invariant under family permutations. -/
+/-- The gravitational anomaly equations is invariant under family permutations. -/
 lemma accGrav_invariant (f : PermGroup n) (S : (SMCharges n).Charges) :
     accGrav (repCharges f S) = accGrav S := accGrav_ext
   (by simpa using toSpecies_sum_invariant 1 f S)
diff --git a/HepLean/BeyondTheStandardModel/GeorgiGlashow/Basic.lean b/HepLean/BeyondTheStandardModel/GeorgiGlashow/Basic.lean
index 695ce7b..eb19e0f 100644
--- a/HepLean/BeyondTheStandardModel/GeorgiGlashow/Basic.lean
+++ b/HepLean/BeyondTheStandardModel/GeorgiGlashow/Basic.lean
@@ -38,7 +38,7 @@ informal_lemma inclSM_ker where
   deps := [``inclSM, ``StandardModel.gaugeGroupℤ₆SubGroup]
 
 /-- The group embedding from `StandardModel.GaugeGroupℤ₆` to `GaugeGroupI` induced by `inclSM` by
-quotienting by the kernal `inclSM_ker`.
+quotienting by the kernel `inclSM_ker`.
 -/
 informal_definition embedSMℤ₆ where
   deps := [``inclSM, ``StandardModel.GaugeGroupℤ₆, ``GaugeGroupI, ``inclSM_ker]
diff --git a/HepLean/BeyondTheStandardModel/PatiSalam/Basic.lean b/HepLean/BeyondTheStandardModel/PatiSalam/Basic.lean
index 6cb7c9e..34f59e5 100644
--- a/HepLean/BeyondTheStandardModel/PatiSalam/Basic.lean
+++ b/HepLean/BeyondTheStandardModel/PatiSalam/Basic.lean
@@ -43,7 +43,7 @@ informal_lemma inclSM_ker where
   deps := [``inclSM, ``StandardModel.gaugeGroupℤ₃SubGroup]
 
 /-- The group embedding from `StandardModel.GaugeGroupℤ₃` to `GaugeGroupI` induced by `inclSM` by
-quotienting by the kernal `inclSM_ker`.
+quotienting by the kernel `inclSM_ker`.
 -/
 informal_definition embedSMℤ₃ where
   deps := [``inclSM, ``StandardModel.GaugeGroupℤ₃, ``GaugeGroupI, ``inclSM_ker]
diff --git a/HepLean/Lorentz/ComplexTensor/PauliMatrices/Basis.lean b/HepLean/Lorentz/ComplexTensor/PauliMatrices/Basis.lean
index 84a73ed..47e1c38 100644
--- a/HepLean/Lorentz/ComplexTensor/PauliMatrices/Basis.lean
+++ b/HepLean/Lorentz/ComplexTensor/PauliMatrices/Basis.lean
@@ -216,7 +216,7 @@ lemma basis_contr_pauliMatrix_basis_tree_expand' {n : ℕ} {c : Fin n → comple
   rfl
 
 /-- The map to color which appears when contracting a basis vector with
-  puali matrices. -/
+  Pauli matrices. -/
 def pauliMatrixBasisProdMap
     {n : ℕ} {c : Fin n → complexLorentzTensor.C}
     (b : Π k, Fin (complexLorentzTensor.repDim (c k))) (i1 i2 i3 : Fin 4) :
diff --git a/HepLean/Lorentz/Group/Boosts.lean b/HepLean/Lorentz/Group/Boosts.lean
index 2e48e7d..a5ba0c5 100644
--- a/HepLean/Lorentz/Group/Boosts.lean
+++ b/HepLean/Lorentz/Group/Boosts.lean
@@ -43,7 +43,7 @@ def genBoostAux₁ (u v : FuturePointing d) : ContrMod d →ₗ[ℝ] ContrMod d
       smul_tmul, tmul_smul, map_smul, smul_eq_mul, RingHom.id_apply]
     rw [← mul_assoc, mul_comm 2 c, mul_assoc, mul_smul]
 
-/-- An auxiliary linear map used in the definition of a genearlised boost. -/
+/-- An auxiliary linear map used in the definition of a generalised boost. -/
 def genBoostAux₂ (u v : FuturePointing d) : ContrMod d →ₗ[ℝ] ContrMod d where
   toFun x := - (⟪x, u.1.1 + v.1.1⟫ₘ / (1 + ⟪u.1.1, v.1.1⟫ₘ)) • (u.1.1 + v.1.1)
   map_add' x y := by
diff --git a/HepLean/Lorentz/Group/Orthochronous.lean b/HepLean/Lorentz/Group/Orthochronous.lean
index 82dcf50..528a123 100644
--- a/HepLean/Lorentz/Group/Orthochronous.lean
+++ b/HepLean/Lorentz/Group/Orthochronous.lean
@@ -113,7 +113,7 @@ lemma orthchroMapReal_minus_one_or_one (Λ : LorentzGroup d) :
 
 local notation "ℤ₂" => Multiplicative (ZMod 2)
 
-/-- A continuous map from `lorentzGroup` to `ℤ₂` whose kernal are the Orthochronous elements. -/
+/-- A continuous map from `lorentzGroup` to `ℤ₂` whose kernel are the Orthochronous elements. -/
 def orthchroMap : C(LorentzGroup d, ℤ₂) :=
   ContinuousMap.comp coeForℤ₂ {
     toFun := fun Λ => ⟨orthchroMapReal Λ, orthchroMapReal_minus_one_or_one Λ⟩,
diff --git a/HepLean/Lorentz/MinkowskiMatrix.lean b/HepLean/Lorentz/MinkowskiMatrix.lean
index 9d5741b..24fea36 100644
--- a/HepLean/Lorentz/MinkowskiMatrix.lean
+++ b/HepLean/Lorentz/MinkowskiMatrix.lean
@@ -163,7 +163,7 @@ lemma dual_apply (μ ν : Fin 1 ⊕ Fin d) :
     diagonal_mul, transpose_apply, diagonal_apply_eq]
 
 /-- The components of the Minkowski dual of a matrix multiplied by the Minkowski matrix
-  in tems of the original matrix. -/
+  in terms of the original matrix. -/
 lemma dual_apply_minkowskiMatrix (μ ν : Fin 1 ⊕ Fin d) :
     dual Λ μ ν * η ν ν = η μ μ * Λ ν μ := by
   rw [dual_apply, mul_assoc]
diff --git a/HepLean/Lorentz/PauliMatrices/SelfAdjoint.lean b/HepLean/Lorentz/PauliMatrices/SelfAdjoint.lean
index 8bb7651..2028b8c 100644
--- a/HepLean/Lorentz/PauliMatrices/SelfAdjoint.lean
+++ b/HepLean/Lorentz/PauliMatrices/SelfAdjoint.lean
@@ -338,7 +338,7 @@ lemma σSAL_decomp (M : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)) :
     ring
 
 /-- The component of a self-adjoint matrix in the direction `σ0` under
-  the basis formed by the covaraiant Pauli matrices. -/
+  the basis formed by the covariant Pauli matrices. -/
 @[simp]
 lemma σSAL_repr_inl_0 (M : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)) :
     σSAL.repr M (Sum.inl 0) = 1 / 2 * Matrix.trace (σ0 * M.1) := by
@@ -355,7 +355,7 @@ lemma σSAL_repr_inl_0 (M : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)) :
   simp [σSAL]
 
 /-- The component of a self-adjoint matrix in the direction `-σ1` under
-  the basis formed by the covaraiant Pauli matrices. -/
+  the basis formed by the covariant Pauli matrices. -/
 @[simp]
 lemma σSAL_repr_inr_0 (M : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)) :
     σSAL.repr M (Sum.inr 0) = - 1 / 2 * Matrix.trace (σ1 * M.1) := by
@@ -372,7 +372,7 @@ lemma σSAL_repr_inr_0 (M : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)) :
   simp [σSAL]
 
 /-- The component of a self-adjoint matrix in the direction `-σ2` under
-  the basis formed by the covaraiant Pauli matrices. -/
+  the basis formed by the covariant Pauli matrices. -/
 @[simp]
 lemma σSAL_repr_inr_1 (M : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)) :
     σSAL.repr M (Sum.inr 1) = - 1 / 2 * Matrix.trace (σ2 * M.1) := by
@@ -389,7 +389,7 @@ lemma σSAL_repr_inr_1 (M : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)) :
   simp [σSAL]
 
 /-- The component of a self-adjoint matrix in the direction `-σ3` under
-  the basis formed by the covaraiant Pauli matrices. -/
+  the basis formed by the covariant Pauli matrices. -/
 @[simp]
 lemma σSAL_repr_inr_2 (M : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)) :
     σSAL.repr M (Sum.inr 2) = - 1 / 2 * Matrix.trace (σ3 * M.1) := by
diff --git a/HepLean/Mathematics/List/InsertionSort.lean b/HepLean/Mathematics/List/InsertionSort.lean
index 9957650..17f5cca 100644
--- a/HepLean/Mathematics/List/InsertionSort.lean
+++ b/HepLean/Mathematics/List/InsertionSort.lean
@@ -23,7 +23,7 @@ lemma insertionSortMin_lt_length_succ {α : Type} (r : α → α → Prop) [Deci
   rw [eraseIdx_length']
   simp
 
-/-- Given a list `i :: l` the left-most minimial position `a` of `i :: l` wrt `r`
+/-- Given a list `i :: l` the left-most minimal position `a` of `i :: l` wrt `r`
   as an element of `Fin (insertionSortDropMinPos r i l).length.succ`. -/
 def insertionSortMinPosFin {α : Type} (r : α → α → Prop) [DecidableRel r] (i : α) (l : List α) :
     Fin (insertionSortDropMinPos r i l).length.succ :=
diff --git a/HepLean/Meta/Remark/Properties.lean b/HepLean/Meta/Remark/Properties.lean
index 820843a..ba03f21 100644
--- a/HepLean/Meta/Remark/Properties.lean
+++ b/HepLean/Meta/Remark/Properties.lean
@@ -25,7 +25,7 @@ def RemarkInfo.toFullName (r : RemarkInfo) : Name :=
   else
     r.name
 
-/-- A Bool which is true if a name correponds to a remark. -/
+/-- A Bool which is true if a name corresponds to a remark. -/
 def RemarkInfo.IsRemark (n : Name) : m Bool := do
   let allRemarks ← allRemarkInfo
   let r := allRemarks.find? fun r => r.toFullName == n
diff --git a/HepLean/PerturbationTheory/CreateAnnihilate.lean b/HepLean/PerturbationTheory/CreateAnnihilate.lean
index 895fefa..cc397b1 100644
--- a/HepLean/PerturbationTheory/CreateAnnihilate.lean
+++ b/HepLean/PerturbationTheory/CreateAnnihilate.lean
@@ -12,7 +12,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
-  or the sum thereof or intergral thereover etc. -/
+  or the sum thereof or integral thereover etc. -/
 inductive CreateAnnihilate where
   | create : CreateAnnihilate
   | annihilate : CreateAnnihilate
diff --git a/HepLean/PerturbationTheory/FeynmanDiagrams/Momentum.lean b/HepLean/PerturbationTheory/FeynmanDiagrams/Momentum.lean
index 794e7a3..012b617 100644
--- a/HepLean/PerturbationTheory/FeynmanDiagrams/Momentum.lean
+++ b/HepLean/PerturbationTheory/FeynmanDiagrams/Momentum.lean
@@ -83,17 +83,17 @@ def euclidInner : F.HalfEdgeMomenta →ₗ[ℝ] F.HalfEdgeMomenta →ₗ[ℝ] 
   Corresponding to that spanned by its total outflowing momentum. -/
 def EdgeMomenta : Type := F.𝓔 → ℝ
 
-/-- The edge momenta form an additive commuative group. -/
+/-- The edge momenta form an additive commutative group. -/
 instance : AddCommGroup F.EdgeMomenta := Pi.addCommGroup
 
 /-- The edge momenta form a module over `ℝ`. -/
 instance : Module ℝ F.EdgeMomenta := Pi.module _ _ _
 
-/-- The type which associates to each ege a `1`-dimensional vector space.
+/-- The type which associates to each edge a `1`-dimensional vector space.
   Corresponding to that spanned by its total inflowing momentum. -/
 def VertexMomenta : Type := F.𝓥 → ℝ
 
-/-- The vertex momenta carries the structure of an additive commuative group. -/
+/-- The vertex momenta carries the structure of an additive commutative 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 additive commuative group. -/
+  or vertex momenta and thus carries the structure of an additive commutative group. -/
 instance (i : Fin 2) : AddCommGroup (EdgeVertexMomentaMap F i) :=
   match i with
   | 0 => instAddCommGroupEdgeMomenta F
diff --git a/HepLean/PerturbationTheory/FieldOpAlgebra/Basic.lean b/HepLean/PerturbationTheory/FieldOpAlgebra/Basic.lean
index 77f0554..a4bd1ef 100644
--- a/HepLean/PerturbationTheory/FieldOpAlgebra/Basic.lean
+++ b/HepLean/PerturbationTheory/FieldOpAlgebra/Basic.lean
@@ -40,7 +40,7 @@ def fieldOpIdealSet : Set (FieldOpFreeAlgebra 𝓕) :=
   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.
+  super-commute. In other words, 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.
@@ -218,7 +218,7 @@ lemma ι_superCommuteF_ofCrAnOpF_ofCrAnOpF_mem_center (φ ψ : 𝓕.CrAnFieldOp)
 
 /-!
 
-## The kernal of ι
+## The kernel of ι
 -/
 
 lemma ι_eq_zero_iff_mem_ideal (x : FieldOpFreeAlgebra 𝓕) :
diff --git a/HepLean/PerturbationTheory/FieldOpAlgebra/NormalOrder/Lemmas.lean b/HepLean/PerturbationTheory/FieldOpAlgebra/NormalOrder/Lemmas.lean
index f1da540..97ac79d 100644
--- a/HepLean/PerturbationTheory/FieldOpAlgebra/NormalOrder/Lemmas.lean
+++ b/HepLean/PerturbationTheory/FieldOpAlgebra/NormalOrder/Lemmas.lean
@@ -282,7 +282,7 @@ lemma ofCrAnOp_superCommute_normalOrder_ofFieldOpList_sum (φ : 𝓕.CrAnFieldOp
 
 /--
 The commutor of the annihilation part of a field operator with a normal ordered list of field
-operators can be decomponsed into the sum of the commutators of the annihilation part with each
+operators can be decomposed into the sum of the commutators of the annihilation part with each
 element of the list of field operators, i.e.
 `[anPart φ, 𝓝(φ₀…φₙ)]ₛ= ∑ i, 𝓢(φ, φ₀…φᵢ₋₁) • [anPart φ, φᵢ]ₛ * 𝓝(φ₀…φᵢ₋₁φᵢ₊₁…φₙ)`.
 -/
diff --git a/HepLean/PerturbationTheory/FieldOpAlgebra/WickTerm.lean b/HepLean/PerturbationTheory/FieldOpAlgebra/WickTerm.lean
index cc3af9d..200f7d9 100644
--- a/HepLean/PerturbationTheory/FieldOpAlgebra/WickTerm.lean
+++ b/HepLean/PerturbationTheory/FieldOpAlgebra/WickTerm.lean
@@ -104,7 +104,7 @@ is equal the product of
 - `φsΛ.timeContract`
 - `s • [anPart φ, ofFieldOp φs[k]]ₛ` where `s` is the sign associated with moving `φ` through
   uncontracted fields in `φ₀…φₖ₋₁`
-- the normal ordering `[φsΛ]ᵘᶜ` with the field corresonding to `k` removed.
+- the normal ordering `[φsΛ]ᵘᶜ` with the field corresponding to `k` removed.
 
 The proof of this result relies on
 - `timeContract_insert_some_of_not_lt`
diff --git a/HepLean/PerturbationTheory/FieldOpAlgebra/WicksTheoremNormal.lean b/HepLean/PerturbationTheory/FieldOpAlgebra/WicksTheoremNormal.lean
index 679abaf..b2132b7 100644
--- a/HepLean/PerturbationTheory/FieldOpAlgebra/WicksTheoremNormal.lean
+++ b/HepLean/PerturbationTheory/FieldOpAlgebra/WicksTheoremNormal.lean
@@ -34,7 +34,7 @@ This result follows from
   those `𝓣(φsΛ.staticWickTerm)` for which `φsΛ` has a contracted pair which are not
   equal time to zero.
 - `staticContract_eq_timeContract_of_eqTimeOnly` to rewrite the static contract
-  in the reminaing `𝓣(φsΛ.staticWickTerm)` as a time contract.
+  in the remaining `𝓣(φsΛ.staticWickTerm)` as a time contract.
 - `timeOrder_timeContract_mul_of_eqTimeOnly_left` to move the time contracts out of the time
   ordering.
 -/
diff --git a/HepLean/PerturbationTheory/FieldSpecification/Basic.lean b/HepLean/PerturbationTheory/FieldSpecification/Basic.lean
index bd4e315..cf59085 100644
--- a/HepLean/PerturbationTheory/FieldSpecification/Basic.lean
+++ b/HepLean/PerturbationTheory/FieldSpecification/Basic.lean
@@ -88,7 +88,7 @@ As some intuition, if `f` corresponds to a Weyl-fermion field, then
 - `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,
+- `outAsymp f e p`, `e` would correspond 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)`.
 
diff --git a/HepLean/PerturbationTheory/FieldSpecification/CrAnFieldOp.lean b/HepLean/PerturbationTheory/FieldSpecification/CrAnFieldOp.lean
index 89aa9c0..13141fd 100644
--- a/HepLean/PerturbationTheory/FieldSpecification/CrAnFieldOp.lean
+++ b/HepLean/PerturbationTheory/FieldSpecification/CrAnFieldOp.lean
@@ -83,7 +83,7 @@ As some intuition, if `f` corresponds to a Weyl-fermion field, it would contribu
 - 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,
+- an element corresponding to annihilation 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)`.
@@ -98,7 +98,7 @@ def crAnFieldOpToFieldOp : 𝓕.CrAnFieldOp → 𝓕.FieldOp := Sigma.fst
 lemma crAnFieldOpToFieldOp_prod (s : 𝓕.FieldOp) (t : 𝓕.fieldOpToCrAnType s) :
     𝓕.crAnFieldOpToFieldOp ⟨s, t⟩ = s := rfl
 
-/-- For a field specficiation `𝓕`, `𝓕.crAnFieldOpToCreateAnnihilate` is the map from
+/-- For a field specification `𝓕`, `𝓕.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.
diff --git a/HepLean/PerturbationTheory/FieldSpecification/CrAnSection.lean b/HepLean/PerturbationTheory/FieldSpecification/CrAnSection.lean
index 5b44b3c..6f355e4 100644
--- a/HepLean/PerturbationTheory/FieldSpecification/CrAnSection.lean
+++ b/HepLean/PerturbationTheory/FieldSpecification/CrAnSection.lean
@@ -126,7 +126,7 @@ def singletonEquiv {φ : 𝓕.FieldOp} : CrAnSection [φ] ≃
     simp only [head]
     rfl
 
-/-- An equivalence seperating the head of a creation and annihilation section
+/-- An equivalence separating the head of a creation and annihilation section
   from the tail. -/
 def consEquiv {φ : 𝓕.FieldOp} {φs : List 𝓕.FieldOp} : CrAnSection (φ :: φs) ≃
     𝓕.fieldOpToCrAnType φ × CrAnSection φs where
diff --git a/HepLean/PerturbationTheory/FieldSpecification/TimeOrder.lean b/HepLean/PerturbationTheory/FieldSpecification/TimeOrder.lean
index babe0ee..19da522 100644
--- a/HepLean/PerturbationTheory/FieldSpecification/TimeOrder.lean
+++ b/HepLean/PerturbationTheory/FieldSpecification/TimeOrder.lean
@@ -32,7 +32,7 @@ def timeOrderRel : 𝓕.FieldOp → 𝓕.FieldOp → Prop
   | FieldOp.inAsymp _, FieldOp.position _ => False
   | FieldOp.inAsymp _, FieldOp.inAsymp _ => True
 
-/-- The relation `timeOrderRel` is decidable, but not computablly so due to
+/-- The relation `timeOrderRel` is decidable, but not computable so due to
   `Real.decidableLE`. -/
 noncomputable instance : (φ φ' : 𝓕.FieldOp) → Decidable (timeOrderRel φ φ')
   | FieldOp.outAsymp _, _ => isTrue True.intro
@@ -206,7 +206,7 @@ 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
 
-/-- The relation `crAnTimeOrderRel` is decidable, but not computablly so due to
+/-- The relation `crAnTimeOrderRel` is decidable, but not computable so due to
   `Real.decidableLE`. -/
 noncomputable instance (φ φ' : 𝓕.CrAnFieldOp) : Decidable (crAnTimeOrderRel φ φ') :=
   inferInstanceAs (Decidable (𝓕.timeOrderRel φ.1 φ'.1))
@@ -508,7 +508,7 @@ lemma sum_crAnSections_timeOrder {φs : List 𝓕.FieldOp} [AddCommMonoid M]
 def normTimeOrderRel (a b : 𝓕.CrAnFieldOp) : Prop :=
   crAnTimeOrderRel a b ∧ (crAnTimeOrderRel b a → normalOrderRel a b)
 
-/-- The relation `normTimeOrderRel` is decidable, but not computablly so due to
+/-- The relation `normTimeOrderRel` is decidable, but not computable so due to
   `Real.decidableLE`. -/
 noncomputable instance (φ φ' : 𝓕.CrAnFieldOp) : Decidable (normTimeOrderRel φ φ') :=
   instDecidableAnd
diff --git a/HepLean/PerturbationTheory/FieldStatistics/Basic.lean b/HepLean/PerturbationTheory/FieldStatistics/Basic.lean
index 9639ade..10333ee 100644
--- a/HepLean/PerturbationTheory/FieldStatistics/Basic.lean
+++ b/HepLean/PerturbationTheory/FieldStatistics/Basic.lean
@@ -26,7 +26,7 @@ namespace FieldStatistic
 
 variable {𝓕 : Type}
 
-/-- The type `FieldStatistic` carries an instance of a commuative group in which
+/-- The type `FieldStatistic` carries an instance of a commutative group in which
 - `bosonic * bosonic = bosonic`
 - `bosonic * fermionic = fermionic`
 - `fermionic * bosonic = fermionic`
diff --git a/HepLean/PerturbationTheory/WickContraction/Sign/Basic.lean b/HepLean/PerturbationTheory/WickContraction/Sign/Basic.lean
index 7638d3f..07e4657 100644
--- a/HepLean/PerturbationTheory/WickContraction/Sign/Basic.lean
+++ b/HepLean/PerturbationTheory/WickContraction/Sign/Basic.lean
@@ -21,7 +21,7 @@ open FieldStatistic
 
 /-- Given a Wick contraction `c : WickContraction n` and `i1 i2 : Fin n` the finite set
   of elements of `Fin n` between `i1` and `i2` which are either uncontracted
-  or are contracted but are contracted with an element occuring after `i1`.
+  or are contracted but are contracted with an element occurring after `i1`.
   I.e. the elements of `Fin n` between `i1` and `i2` which are not contracted with before `i1`.
   One should assume `i1 < i2` otherwise this finite set is empty. -/
 def signFinset (c : WickContraction n) (i1 i2 : Fin n) : Finset (Fin n) :=
diff --git a/HepLean/PerturbationTheory/WickContraction/TimeCond.lean b/HepLean/PerturbationTheory/WickContraction/TimeCond.lean
index cde0f93..9ac387a 100644
--- a/HepLean/PerturbationTheory/WickContraction/TimeCond.lean
+++ b/HepLean/PerturbationTheory/WickContraction/TimeCond.lean
@@ -506,7 +506,7 @@ lemma hasEqTimeEquiv_ext_sigma {φs : List 𝓕.FieldOp} {x1 x2 :
     simp only [ne_eq, congr_refl] at h2
     simp [h2]
 
-/-- The equivalence which seperates a Wick contraction which has an equal time contraction
+/-- The equivalence which separates a Wick contraction which has an equal time contraction
 into a non-empty contraction only between equal-time fields and a Wick contraction which
 does not have equal time contractions. -/
 def hasEqTimeEquiv (φs : List 𝓕.FieldOp) :
diff --git a/HepLean/StandardModel/HiggsBoson/GaugeAction.lean b/HepLean/StandardModel/HiggsBoson/GaugeAction.lean
index 0c2a714..4bcd195 100644
--- a/HepLean/StandardModel/HiggsBoson/GaugeAction.lean
+++ b/HepLean/StandardModel/HiggsBoson/GaugeAction.lean
@@ -43,7 +43,7 @@ noncomputable def higgsRepUnitary : GaugeGroupI →* unitaryGroup (Fin 2) ℂ wh
     repeat rw [mul_assoc]
   map_one' := by simp
 
-/-- Using the orthonormal basis of `HiggsVec`, turns a `2×2`-matrix intoa a linear map
+/-- Using the orthonormal basis of `HiggsVec`, turns a `2×2`-matrix into a linear map
   of `HiggsVec`. -/
 noncomputable def matrixToLin : Matrix (Fin 2) (Fin 2) ℂ →* (HiggsVec →L[ℂ] HiggsVec) where
   toFun g := LinearMap.toContinuousLinearMap
@@ -220,7 +220,7 @@ informal_lemma guage_orbit where
   deps := [``rotate_fst_zero_snd_real]
 
 /-- The Higgs boson breaks electroweak symmetry down to the electromagnetic force, i.e., the
-stablity group of the action of `rep` on `![0, Complex.ofReal ‖φ‖]`, for non-zero `‖φ‖`, is the
+stability group of the action of `rep` on `![0, Complex.ofReal ‖φ‖]`, for non-zero `‖φ‖`, is the
 `SU(3) × U(1)` subgroup of `gaugeGroup := SU(3) × SU(2) × U(1)` with the embedding given by
 `(g, e^{i θ}) ↦ (g, diag (e ^ {3 * i θ}, e ^ {- 3 * i θ}), e^{i θ})`.
 -/
diff --git a/HepLean/Tensors/Tree/Elab.lean b/HepLean/Tensors/Tree/Elab.lean
index a93f997..d1c6130 100644
--- a/HepLean/Tensors/Tree/Elab.lean
+++ b/HepLean/Tensors/Tree/Elab.lean
@@ -77,7 +77,7 @@ syntax num : indexExpr
 /-- Notation to describe the jiggle of a tensor index. -/
 syntax "τ(" ident ")" : indexExpr
 
-/-- Bool which is ture if an index is a num. -/
+/-- Bool which is true if an index is a num. -/
 def indexExprIsNum (stx : Syntax) : Bool :=
   match stx with
   | `(indexExpr|$_:num) => true

From b4333f038aff74ea55e698cdaae06190f3353bdb Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Mon, 10 Feb 2025 10:59:09 +0000
Subject: [PATCH 5/6] refactor: More spellings

---
 HepLean/Lorentz/ComplexTensor/Metrics/Basis.lean       |  4 ++--
 HepLean/Lorentz/MinkowskiMatrix.lean                   |  2 +-
 HepLean/Lorentz/PauliMatrices/SelfAdjoint.lean         |  2 +-
 HepLean/Lorentz/RealVector/Basic.lean                  |  2 +-
 HepLean/Lorentz/RealVector/Modules.lean                |  2 +-
 HepLean/Mathematics/List.lean                          |  2 +-
 HepLean/PerturbationTheory/FieldOpAlgebra/Basic.lean   |  6 +++---
 .../FieldOpAlgebra/NormalOrder/Lemmas.lean             |  6 +++---
 .../FieldOpAlgebra/SuperCommute.lean                   |  6 +++---
 .../FieldOpFreeAlgebra/SuperCommute.lean               | 10 +++++-----
 10 files changed, 21 insertions(+), 21 deletions(-)

diff --git a/HepLean/Lorentz/ComplexTensor/Metrics/Basis.lean b/HepLean/Lorentz/ComplexTensor/Metrics/Basis.lean
index cbbf5a4..fc2f828 100644
--- a/HepLean/Lorentz/ComplexTensor/Metrics/Basis.lean
+++ b/HepLean/Lorentz/ComplexTensor/Metrics/Basis.lean
@@ -61,7 +61,7 @@ lemma coMetric_basis_expand_tree : {η' | μ ν}ᵀ.tensor =
     (smul (-1) (tensorNode (basisVector ![Color.down, Color.down] (fun _ => 3))))).tensor :=
   coMetric_basis_expand
 
-/-- The expansion of the Lorentz contrvariant metric in terms of basis vectors. -/
+/-- The expansion of the Lorentz contravariant metric in terms of basis vectors. -/
 lemma contrMatrix_basis_expand : {η | μ ν}ᵀ.tensor =
     basisVector ![Color.up, Color.up] (fun _ => 0)
     - basisVector ![Color.up, Color.up] (fun _ => 1)
@@ -87,7 +87,7 @@ lemma contrMatrix_basis_expand : {η | μ ν}ᵀ.tensor =
       simp only [Fin.isValue, Lorentz.complexContrBasisFin4, Basis.coe_reindex, Function.comp_apply]
       rfl
 
-/-- The expansion of the Lorentz contrvariant metric in terms of basis vectors as
+/-- The expansion of the Lorentz contravariant metric in terms of basis vectors as
   a structured tensor tree. -/
 lemma contrMatrix_basis_expand_tree : {η | μ ν}ᵀ.tensor =
     (TensorTree.add (tensorNode (basisVector ![Color.up, Color.up] (fun _ => 0))) <|
diff --git a/HepLean/Lorentz/MinkowskiMatrix.lean b/HepLean/Lorentz/MinkowskiMatrix.lean
index 24fea36..fbc57ae 100644
--- a/HepLean/Lorentz/MinkowskiMatrix.lean
+++ b/HepLean/Lorentz/MinkowskiMatrix.lean
@@ -118,7 +118,7 @@ def dual : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ := η * Λᵀ * η
 lemma dual_id : @dual d 1 = 1 := by
   simpa only [dual, transpose_one, mul_one] using minkowskiMatrix.sq
 
-/-- The Minkowski dual swaps multiplications (acts contrvariantly). -/
+/-- The Minkowski dual swaps multiplications (acts contravariantly). -/
 @[simp]
 lemma dual_mul : dual (Λ * Λ') = dual Λ' * dual Λ := by
   simp only [dual, transpose_mul]
diff --git a/HepLean/Lorentz/PauliMatrices/SelfAdjoint.lean b/HepLean/Lorentz/PauliMatrices/SelfAdjoint.lean
index 2028b8c..acf5c9d 100644
--- a/HepLean/Lorentz/PauliMatrices/SelfAdjoint.lean
+++ b/HepLean/Lorentz/PauliMatrices/SelfAdjoint.lean
@@ -405,7 +405,7 @@ lemma σSAL_repr_inr_2 (M : selfAdjoint (Matrix (Fin 2) (Fin 2) ℂ)) :
   linear_combination (norm := ring_nf) -h0
   simp only [σSAL, Basis.mk_repr, Fin.isValue, sub_self]
 
-/-- The relationship between the basis `σSA` of contrvariant Pauli-matrices and the basis
+/-- The relationship between the basis `σSA` of contravariant Pauli-matrices and the basis
   `σSAL` of covariant Pauli matrices is by multiplication by the Minkowski matrix. -/
 lemma σSA_minkowskiMetric_σSAL (i : Fin 1 ⊕ Fin 3) :
     σSA i = minkowskiMatrix i i • σSAL i := by
diff --git a/HepLean/Lorentz/RealVector/Basic.lean b/HepLean/Lorentz/RealVector/Basic.lean
index efc3717..3ab80f1 100644
--- a/HepLean/Lorentz/RealVector/Basic.lean
+++ b/HepLean/Lorentz/RealVector/Basic.lean
@@ -25,7 +25,7 @@ open minkowskiMatrix
   Lorentz vectors. In index notation these have an up index `ψⁱ`. -/
 def Contr (d : ℕ) : Rep ℝ (LorentzGroup d) := Rep.of ContrMod.rep
 
-/-- The representation of contrvariant Lorentz vectors forms a topological space, induced
+/-- The representation of contravariant Lorentz vectors forms a topological space, induced
   by its equivalence to `Fin 1 ⊕ Fin d → ℝ`. -/
 instance : TopologicalSpace (Contr d) := TopologicalSpace.induced
   ContrMod.toFin1dℝEquiv (Pi.topologicalSpace)
diff --git a/HepLean/Lorentz/RealVector/Modules.lean b/HepLean/Lorentz/RealVector/Modules.lean
index bc38c7c..b78c999 100644
--- a/HepLean/Lorentz/RealVector/Modules.lean
+++ b/HepLean/Lorentz/RealVector/Modules.lean
@@ -113,7 +113,7 @@ lemma stdBasis_apply (μ ν : Fin 1 ⊕ Fin d) : (stdBasis μ).val ν = if μ =
   refine ite_congr ?h₁ (congrFun rfl) (congrFun rfl)
   exact Eq.propIntro (fun a => id (Eq.symm a)) fun a => id (Eq.symm a)
 
-/-- Decomposition of a contrvariant Lorentz vector into the standard basis. -/
+/-- Decomposition of a contravariant Lorentz vector into the standard basis. -/
 lemma stdBasis_decomp (v : ContrMod d) : v = ∑ i, v.toFin1dℝ i • stdBasis i := by
   apply toFin1dℝEquiv.injective
   simp only [map_sum, _root_.map_smul]
diff --git a/HepLean/Mathematics/List.lean b/HepLean/Mathematics/List.lean
index b4cd91c..6cfa02c 100644
--- a/HepLean/Mathematics/List.lean
+++ b/HepLean/Mathematics/List.lean
@@ -755,7 +755,7 @@ lemma eraseIdx_insertionSort_fin {I : Type} (le1 : I → I → Prop) [DecidableR
     = List.insertionSort le1 (r.eraseIdx n) :=
   eraseIdx_insertionSort le1 n.val r (Fin.prop n)
 
-/-- Given a list `i :: l` the left-most minimial position `a` of `i :: l` wrt `r`.
+/-- Given a list `i :: l` the left-most minimal position `a` of `i :: l` wrt `r`.
   That is the first position
   of `l` such that for every element `(i :: l)[b]` before that position
   `r ((i :: l)[b]) ((i :: l)[a])` is not true. The use of `i :: l` here
diff --git a/HepLean/PerturbationTheory/FieldOpAlgebra/Basic.lean b/HepLean/PerturbationTheory/FieldOpAlgebra/Basic.lean
index a4bd1ef..7779877 100644
--- a/HepLean/PerturbationTheory/FieldOpAlgebra/Basic.lean
+++ b/HepLean/PerturbationTheory/FieldOpAlgebra/Basic.lean
@@ -19,8 +19,8 @@ open FieldStatistic
 
 variable (𝓕 : FieldSpecification)
 
-/-- The set contains the super-commutors equal to zero in the operator algebra.
-  This contains e.g. the super-commutor of two creation operators. -/
+/-- The set contains the super-commutators equal to zero in the operator algebra.
+  This contains e.g. the super-commutator of two creation operators. -/
 def fieldOpIdealSet : Set (FieldOpFreeAlgebra 𝓕) :=
   { x |
     (∃ (φ1 φ2 φ3 : 𝓕.CrAnFieldOp),
@@ -42,7 +42,7 @@ def fieldOpIdealSet : Set (FieldOpFreeAlgebra 𝓕) :=
   This corresponds to the condition that two operators with different statistics always
   super-commute. In other words, 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
+  when combined with the conditions above, that the super-commutator is in the center of the
   of the algebra.
 -/
 abbrev FieldOpAlgebra : Type := (TwoSidedIdeal.span 𝓕.fieldOpIdealSet).ringCon.Quotient
diff --git a/HepLean/PerturbationTheory/FieldOpAlgebra/NormalOrder/Lemmas.lean b/HepLean/PerturbationTheory/FieldOpAlgebra/NormalOrder/Lemmas.lean
index 97ac79d..e1e3f04 100644
--- a/HepLean/PerturbationTheory/FieldOpAlgebra/NormalOrder/Lemmas.lean
+++ b/HepLean/PerturbationTheory/FieldOpAlgebra/NormalOrder/Lemmas.lean
@@ -229,8 +229,8 @@ The proof of this result ultimately goes as follows
   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 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.
+  `ofCrAnList φsn` as a sum of super commutators, one for each element of `φsn`.
+- The fact that super-commutators are in the center of `𝓕.FieldOpAlgebra` is used to  rearrange terms.
 - Properties of ordered lists, and `normalOrderSign_eraseIdx` are then used to complete the proof.
 -/
 lemma ofCrAnOp_superCommute_normalOrder_ofCrAnList_sum (φ : 𝓕.CrAnFieldOp)
@@ -281,7 +281,7 @@ lemma ofCrAnOp_superCommute_normalOrder_ofFieldOpList_sum (φ : 𝓕.CrAnFieldOp
   rw [← Finset.sum_mul, ← map_sum, ← map_sum, ← ofFieldOp_eq_sum, ← ofFieldOpList_eq_sum]
 
 /--
-The commutor of the annihilation part of a field operator with a normal ordered list of field
+The commutator of the annihilation part of a field operator with a normal ordered list of field
 operators can be decomposed into the sum of the commutators of the annihilation part with each
 element of the list of field operators, i.e.
 `[anPart φ, 𝓝(φ₀…φₙ)]ₛ= ∑ i, 𝓢(φ, φ₀…φᵢ₋₁) • [anPart φ, φᵢ]ₛ * 𝓝(φ₀…φᵢ₋₁φᵢ₊₁…φₙ)`.
diff --git a/HepLean/PerturbationTheory/FieldOpAlgebra/SuperCommute.lean b/HepLean/PerturbationTheory/FieldOpAlgebra/SuperCommute.lean
index f37ea26..cce56cd 100644
--- a/HepLean/PerturbationTheory/FieldOpAlgebra/SuperCommute.lean
+++ b/HepLean/PerturbationTheory/FieldOpAlgebra/SuperCommute.lean
@@ -49,7 +49,7 @@ lemma ι_superCommuteF_eq_of_equiv_right (a b1 b2 : 𝓕.FieldOpFreeAlgebra) (h
   simp only [LinearMap.mem_ker, ← map_sub]
   exact ι_superCommuteF_right_zero_of_mem_ideal a (b1 - b2) h
 
-/-- The super commutor on the `FieldOpAlgebra` defined as a linear map `[a,_]ₛ`. -/
+/-- The super commutator on the `FieldOpAlgebra` defined as a linear map `[a,_]ₛ`. -/
 noncomputable def superCommuteRight (a : 𝓕.FieldOpFreeAlgebra) :
   FieldOpAlgebra 𝓕 →ₗ[ℂ] FieldOpAlgebra 𝓕 where
   toFun := Quotient.lift (ι.toLinearMap ∘ₗ superCommuteF a)
@@ -367,7 +367,7 @@ lemma superCommute_anPart_ofFieldOp (φ φ' : 𝓕.FieldOp) :
 ## Mul equal superCommute
 
 Lemmas which rewrite a multiplication of two elements of the algebra as their commuted
-multiplication with a sign plus the super commutor.
+multiplication with a sign plus the super commutator.
 
 -/
 
@@ -446,7 +446,7 @@ lemma anPart_mul_anPart_swap (φ φ' : 𝓕.FieldOp) :
 
 /-!
 
-## Symmetry of the super commutor.
+## Symmetry of the super commutator.
 
 -/
 
diff --git a/HepLean/PerturbationTheory/FieldOpFreeAlgebra/SuperCommute.lean b/HepLean/PerturbationTheory/FieldOpFreeAlgebra/SuperCommute.lean
index ba365d2..77046ea 100644
--- a/HepLean/PerturbationTheory/FieldOpFreeAlgebra/SuperCommute.lean
+++ b/HepLean/PerturbationTheory/FieldOpFreeAlgebra/SuperCommute.lean
@@ -17,7 +17,7 @@ namespace FieldOpFreeAlgebra
 
 /-!
 
-## The super commutor on the FieldOpFreeAlgebra.
+## The super commutator on the FieldOpFreeAlgebra.
 
 -/
 
@@ -40,7 +40,7 @@ scoped[FieldSpecification.FieldOpFreeAlgebra] notation "[" φs "," φs' "]ₛca"
 
 /-!
 
-## The super commutor of different types of elements
+## The super commutator of different types of elements
 
 -/
 
@@ -257,7 +257,7 @@ lemma superCommuteF_anPartF_ofFieldOpF (φ φ' : 𝓕.FieldOp) :
 ## Mul equal superCommuteF
 
 Lemmas which rewrite a multiplication of two elements of the algebra as their commuted
-multiplication with a sign plus the super commutor.
+multiplication with a sign plus the super commutator.
 
 -/
 lemma ofCrAnListF_mul_ofCrAnListF_eq_superCommuteF (φs φs' : List 𝓕.CrAnFieldOp) :
@@ -328,7 +328,7 @@ lemma ofCrAnListF_mul_ofFieldOpListF_eq_superCommuteF (φs : List 𝓕.CrAnField
 
 /-!
 
-## Symmetry of the super commutor.
+## Symmetry of the super commutator.
 
 -/
 
@@ -359,7 +359,7 @@ lemma superCommuteF_ofCrAnOpF_ofCrAnOpF_symm (φ φ' : 𝓕.CrAnFieldOp) :
 
 /-!
 
-## Splitting the super commutor on lists into sums.
+## Splitting the super commutator on lists into sums.
 
 -/
 

From 6519b9be36f181393d8ffff95b787d9f9f9db524 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Mon, 10 Feb 2025 11:05:03 +0000
Subject: [PATCH 6/6] refactor: Lint

---
 .../PerturbationTheory/FieldOpAlgebra/NormalOrder/Lemmas.lean  | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/HepLean/PerturbationTheory/FieldOpAlgebra/NormalOrder/Lemmas.lean b/HepLean/PerturbationTheory/FieldOpAlgebra/NormalOrder/Lemmas.lean
index e1e3f04..fd6cdb0 100644
--- a/HepLean/PerturbationTheory/FieldOpAlgebra/NormalOrder/Lemmas.lean
+++ b/HepLean/PerturbationTheory/FieldOpAlgebra/NormalOrder/Lemmas.lean
@@ -230,7 +230,8 @@ The proof of this result ultimately goes as follows
 - `superCommuteF_ofCrAnListF_ofCrAnListF_eq_sum` is used to rewrite the super commutator of `φ`
   (considered as a list with one element) with
   `ofCrAnList φsn` as a sum of super commutators, one for each element of `φsn`.
-- The fact that super-commutators are in the center of `𝓕.FieldOpAlgebra` is used to  rearrange terms.
+- The fact that super-commutators are in the center of `𝓕.FieldOpAlgebra` is used to  rearrange
+  terms.
 - Properties of ordered lists, and `normalOrderSign_eraseIdx` are then used to complete the proof.
 -/
 lemma ofCrAnOp_superCommute_normalOrder_ofCrAnList_sum (φ : 𝓕.CrAnFieldOp)