doc: Edits to Wick theorem docs

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

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

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

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 _
 

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
+  of the free algebra `𝓕.FieldOpFreeAlgebra` by the ideal generated by
-- `[ofCrAnOpF φ1, [ofCrAnOpF φ2, ofCrAnOpF φ3]ₛca]ₛca`, which (with the other conditions)
+- `[ofCrAnOpF φc, ofCrAnOpF φc']ₛca` for `φc` and `φc'` field creation operators.
-  gives us that super-commutors are in the center.
+  This corresponds to the condition that two creation operators always super-commute.
-- `[ofCrAnOpF φc, ofCrAnOpF φc']ₛca` for `φc` and `φc'` creation operators. I.e two creation
+- `[ofCrAnOpF φa, ofCrAnOpF φa']ₛca` for `φa` and `φa'` field annihilation operators.
-  operators always super-commute.
+  This corresponds to the condition that two annihilation operators always super-commute.
-- `[ofCrAnOpF φa, ofCrAnOpF φa']ₛca` for `φa` and `φa'` annihilation operators. I.e two
+- `[ofCrAnOpF φ, ofCrAnOpF φ']ₛca` for `φ` and `φ'` operators with different statistics.
-  annihilation operators always super-commute.
+  This corresponds to the condition that two operators with different statistics always
-- `[ofCrAnOpF φ, ofCrAnOpF φ']ₛca` for `φ` and `φ'` field operators with different statistics.
+  super-commute. In otherwords, fermions and bosons always super-commute.
-  I.e. Fermions super-commute with bosons. -/
+- `[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
+  Thus for `φ`
-  it is of the form `ofCrAnOp _`. -/
+- 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
+  Thus for `φ`
-  it is of the form `ofCrAnOp _`. -/
+- 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

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`
+  Those `ofCrAnList φs` for which `φs` has an overall `bosonic` statistic
-  submodule, whilst those `ofCrAnList φs` for which `φs` has an overall `fermionic` statistic span
+  (i.e. `𝓕 |>ₛ φs = bosonic`) span `bosonic`
-  the `fermionic` submodule. -/
+  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]

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

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,

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.

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.

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`. -/

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
+If `g` is zero on the ideal defining `𝓕.FieldOpAlgebra`, then there exists
-algebra map `g' : FieldOpAlgebra 𝓕 →ₐ[ℂ] A` such that `g' ∘ ι = g`.
+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) :

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.

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
+  For mathematicial objects defined in relation to `FieldOpFreeAlgebra` the postfix `F`
-  their names with an `F` to indicate that they are related to the free algebra.
+  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
+/-- For a field specification `𝓕`, and a element `φ` of `𝓕.CrAnFieldOp`,
-  single `𝓕.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
+/-- For a field specification `𝓕`, and a list `φs` of `𝓕.CrAnFieldOp`,
-  list `φs` of `𝓕.CrAnFieldOp`. For example for the list `[φ₁ᶜ, φ₂ᵃ, φ₃ᶜ]` we schematically
+ `ofCrAnListF φs` is defined as the element of `𝓕.FieldOpFreeAlgebra`
-  get `φ₁ᶜφ₂ᵃφ₃ᶜ`. The set of all `ofCrAnListF φs` forms a basis 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
+/-- For a field specification `𝓕`, and an element `φ` of  `𝓕.FieldOp`,
-  `𝓕.FieldOp` by summing over the creation and annihilation components of `𝓕.FieldOp`.
+  `ofFieldOpF φ` is the element of `𝓕.FieldOpFreeAlgebra` formed  by summing over
-  For example for `φ₁` an incoming asymptotic field operator we get
+  `ofCrAnOpF` of the
-  `ofCrAnOpF φ₁ᶜ`, and for `φ₁` a
+  creation and annihilation parts of `φ`.
-  position field operator we get `ofCrAnOpF φ₁ᶜ + ofCrAnOpF φ₁ᵃ`. -/
+
+  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
+/-- For a field specification `𝓕`, and a list `φs` of `𝓕.FieldOp`,
-  list of `𝓕.FieldOp` by summing over the creation and annihilation components.
+  `𝓕.ofFieldOpListF φs` is defined as the element of `𝓕.FieldOpFreeAlgebra`
-  For example, `φ₁` and `φ₂` position states `[φ1, φ2]` gets sent to
+  obtained by the product of `ofFieldOpF φ` for each `φ` in `φs`.
-  `(ofCrAnOpF φ1ᶜ + ofCrAnOpF φ1ᵃ) * (ofCrAnOpF φ2ᶜ + ofCrAnOpF φ2ᵃ)`. -/
+  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`,
+remark notation_drop := "In doc-strings explicit applications of `ofCrAnOpF`,
-`ofCrAnListF`, `ofFieldOpF`, and `ofFieldOpListF`"
+`ofCrAnListF`, `ofFieldOpF`, and `ofFieldOpListF` will often be dropped."
 
 /-- Coercion from `List 𝓕.FieldOp` to `FieldOpFreeAlgebra 𝓕` through `ofFieldOpListF`. -/
 instance : Coe (List 𝓕.FieldOp) (FieldOpFreeAlgebra 𝓕) := ⟨ofFieldOpListF⟩

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`
+  Those `ofCrAnListF φs` for which `φs` has an overall `bosonic` statistic
-  submodule, whilst those `ofCrAnListF φs` for which `φs` has an overall `fermionic` statistic span
+  (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

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)

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 * φᵢ₊₁ … φₙ`

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 𝓕 :=

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
+/-- For a field specification `𝓕`, the inductive type `𝓕.FieldOp` is defined
-  `FieldOp` corresponds either to:
+  to contain the following elements:
-- an incoming asymptotic field operator `.inAsymp` which is specified by
+- for every `f` in `𝓕.Field`, element of `e` of `AsymptoticLabel f` and `3`-momentum `p`, an
-  a field `f` in `𝓕.Field`, an element of `AsymptoticLabel f` (which specifies exactly
+  element labelled `inAsymp f e p` corresponding to an incoming asymptotic field operator
-  which asymptotic field operator associated with `f`) and a `3`-momentum.
+  of the field `f`, of label `e` (e.g. specifying the spin), and momentum `p`.
-- an position operator `.position` which is specified by
+- for every `f` in `𝓕.Field`, element of `e` of `PositionLabel f` and space-time position `x`, an
-  a field `f` in `𝓕.Field`, an element of `PositionLabel f` (which specifies exactly
+  element labelled `position f e x` corresponding to a position field operator of the field `f`,
-  which position field operator associated with `f`) and a element of `SpaceTime`.
+  of label `e` (e.g. specifying the Lorentz index), and position `x`.
-- an outgoing asymptotic field operator `.outAsymp` which is specified by
+- for every `f` in `𝓕.Field`, element of `e` of `AsymptoticLabel f` and `3`-momentum `p`, an
-  a field `f` in `𝓕.Field`, an element of `AsymptoticLabel f` (which specifies exactly
+  element labelled `outAsymp f e p` corresponding to an outgoing asymptotic field operator of the
-  which asymptotic field operator associated with `f`) and a `3`-momentum.
+  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
+As some intuition, if `f` corresponds to a Weyl-fermion field, then
-have on-shell momenta.
+- 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

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
+For a field specification `𝓕`, the (sigma) type `𝓕.CrAnFieldOp`
-of creation and annihilation field operators, corresponds to
+corresponds to the type of creation and annihilation parts of field operators.
-- an incoming asymptotic field operator `.inAsymp` in `𝓕.FieldOp`.
+It formally defined to consist of the following elements:
-- a position operator `.position` in `𝓕.FieldOp` and an element of
+- for each in incoming asymptotic field operator `φ` in `𝓕.FieldOp` an element
-  `CreateAnnihilate` specifying the creation or annihilation part of that position operator.
+  written as `⟨φ, ()⟩` in `𝓕.CrAnFieldOp`, corresponding to the creation part of `φ`.
-- an outgoing asymptotic field operator `.outAsymp` in `𝓕.FieldOp`.
+  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`
+/-- For a field specficiation `𝓕`, `𝓕.crAnFieldOpToCreateAnnihilate` is the map from
-  specifying if a state is a creation or an annihilation state. -/
+  `𝓕.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
+remark notation_remark := "When working with a field specification `𝓕` the
-some notation within doc-strings and in code. The main notation used is:
+following notation will be used within doc-strings:
-- In doc-strings when field statistics occur in exchange signs we may drop the `𝓕 |>ₛ _`.
+- when field statistics occur in exchange signs the `𝓕 |>ₛ _` may be dropped.
-- In doc-strings we will often write lists of `FieldOp` or `CrAnFieldOp` `φs` as e.g. `φ₀…φₙ`,
+- 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:
+Some examples of these notation-conventions are:
-- `𝓢(φ, φs)` corresponds to `𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φs)`
+- `𝓢(φ, φs)` which corresponds to `𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φs)`
-- `φ₀…φᵢ₋₁φᵢ₊₁…φₙ` corresponds to a (given) list `φs = φ₀…φₙ` with the element at the `i`th position
+- `φ₀…φᵢ₋₁φᵢ₊₁…φₙ` which corresponds to a (given) list `φs = φ₀…φₙ` with the element at the
-  removed.
+  `i`th position removed.
 "
 
 end FieldSpecification

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 a field creation operator
-  - `φ₁` is an annihilation.
+  - `φ₁` 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 *

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
 

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`
+  The exchange sign is the sign one picks up on exchanging an operator or field `φ₁` of statistic
-  with one `φ₂` of statistic `b`, i.e. `φ₁φ₂ → φ₂φ₁`.
+  `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

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
+  In other words, in a `GradingCompliant` Wick contraction no contractions occur between
-  `bosonic` fields. -/
+  `fermionic` and `bosonic` fields. -/
 def GradingCompliant (φs : List 𝓕.FieldOp) (φsΛ : WickContraction φs.length) :=
   ∀ (a : φsΛ.1), (𝓕 |>ₛ φs[φsΛ.fstFieldOfContract a]) = (𝓕 |>ₛ φs[φsΛ.sndFieldOfContract a])
 

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

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}

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

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
+  to the number of `fermionic`-`fermionic` exchanges that must be done to put
-  contracted pairs with `φsΛ` next to one another, starting from the contracted pair
+  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],

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)

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) :

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`
 

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
+    .p "In this note we walk through the important parts of the proof of the three versions of
-      for both fermions and bosons,
+      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,