Merge pull request #320 from HEPLean/WickTheoremDoc

doc: Remaining docs for Wick's theorem

HepLean/PerturbationTheory/FieldOpAlgebra/NormalOrder/Basic.lean

@@ -226,7 +226,7 @@ lemma ι_normalOrderF_eq_of_equiv (a b : 𝓕.FieldOpFreeAlgebra) (h : a ≈ b)
   defined as the decent of `ι ∘ₗ normalOrderF` from `FieldOpFreeAlgebra 𝓕` to `FieldOpAlgebra 𝓕`.
   This decent exists because `ι ∘ₗ normalOrderF` is well-defined on equivalence classes.
 
-  The notation `𝓝(a)` is used for `normalOrder a`.  -/
+  The notation `𝓝(a)` is used for `normalOrder a`. -/
 noncomputable def normalOrder : FieldOpAlgebra 𝓕 →ₗ[ℂ] FieldOpAlgebra 𝓕 where
   toFun := Quotient.lift (ι.toLinearMap ∘ₗ normalOrderF) ι_normalOrderF_eq_of_equiv
   map_add' x y := by

HepLean/PerturbationTheory/FieldOpAlgebra/NormalOrder/Lemmas.lean

@@ -118,6 +118,8 @@ lemma crPart_mul_normalOrder (φ : 𝓕.FieldOp) (a : 𝓕.FieldOpAlgebra) :
 
 -/
 
+/-- For a field specfication `𝓕`, and `a` and `b` in `𝓕.FieldOpAlgebra` the normal ordering
+  of the super commutator of `a` and `b` vanishes. I.e. `𝓝([a,b]ₛ) = 0`. -/
 @[simp]
 lemma normalOrder_superCommute_eq_zero (a b : 𝓕.FieldOpAlgebra) :
     𝓝([a, b]ₛ) = 0 := by
@@ -226,7 +228,7 @@ The proof of this result ultimetly goes as follows
 - The definition of `normalOrder` is used to rewrite `𝓝(φ₀…φₙ)` as a scalar multiple of
   a `ofCrAnList φsn` where `φsn` is the normal ordering of `φ₀…φₙ`.
 - `superCommuteF_ofCrAnListF_ofCrAnListF_eq_sum` is used to rewrite the super commutator of `φ`
-  (considered as a list with one lement) with
+  (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 rearange terms.
 - Properties of ordered lists, and `normalOrderSign_eraseIdx` is then used to complete the proof.
@@ -344,11 +346,11 @@ noncomputable def contractStateAtIndex (φ : 𝓕.FieldOp) (φs : List 𝓕.Fiel
 /--
 For a field specification `𝓕`, a `φ` in `𝓕.FieldOp` and a list `φs` of `𝓕.FieldOp`
 the following relation holds in the algebra `𝓕.FieldOpAlgebra`,
-`φ * 𝓝(φ₀φ₁…φₙ) = 𝓝(φφ₀φ₁…φₙ) + ∑ i, (𝓢(φ,φ₀φ₁…φᵢ₋₁) • [anPartF φ, φᵢ]ₛ) * 𝓝(φ₀φ₁…φᵢ₋₁φᵢ₊₁…φₙ)`.
+`φ * 𝓝(φ₀φ₁…φₙ) = 𝓝(φφ₀φ₁…φₙ) + ∑ i, (𝓢(φ,φ₀φ₁…φᵢ₋₁) • [anPart φ, φᵢ]ₛ) * 𝓝(φ₀φ₁…φᵢ₋₁φᵢ₊₁…φₙ)`.
 
 The proof of ultimetly goes as follows:
 - `ofFieldOp_eq_crPart_add_anPart` is used to split `φ` into its creation and annihilation parts.
-- The fact that `crPart φ *  𝓝(φ₀φ₁…φₙ) = 𝓝(crPart φ * φ₀φ₁…φₙ)` is used.
+- The fact that `crPart φ * 𝓝(φ₀φ₁…φₙ) = 𝓝(crPart φ * φ₀φ₁…φₙ)` is used.
 - The fact that `anPart φ * 𝓝(φ₀φ₁…φₙ)` is
   `𝓢(φ, φ₀φ₁…φₙ) 𝓝(φ₀φ₁…φₙ) * anPart φ + [anPart φ, 𝓝(φ₀φ₁…φₙ)]` is used
 - The fact that `𝓢(φ, φ₀φ₁…φₙ) 𝓝(φ₀φ₁…φₙ) * anPart φ = 𝓝(anPart φ * φ₀φ₁…φₙ)`

HepLean/PerturbationTheory/FieldOpAlgebra/NormalOrder/WickContractions.lean

@@ -25,10 +25,14 @@ variable {𝓕 : FieldSpecification}
 
 -/
 
-/--
-Let `c` be a Wick Contraction for `φs := φ₀φ₁…φₙ`.
-We have (roughly) `𝓝ᶠ([φsΛ ↩Λ φ i none]ᵘᶜ) = s • 𝓝ᶠ(φ :: [φsΛ]ᵘᶜ)`
-Where `s` is the exchange sign for `φ` and the uncontracted fields in `φ₀φ₁…φᵢ₋₁`.
+/-- 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
+
+  `𝓝([φsΛ ↩Λ φ i none]ᵘᶜ) = s • 𝓝(φ :: [φsΛ]ᵘᶜ)`
+
+  where `s` is the exchange sign for `φ` and the uncontracted fields in `φ₀…φᵢ₋₁`.
+
+  The prove of this result ultimately a consequence of `normalOrder_superCommute_eq_zero`.
 -/
 lemma normalOrder_uncontracted_none (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
     (i : Fin φs.length.succ) (φsΛ : WickContraction φs.length) :
@@ -95,10 +99,12 @@ lemma normalOrder_uncontracted_none (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp
   rw [insertAndContract_uncontractedList_none_map]
 
 /--
-Let `c` be a Wick Contraction for `φ₀φ₁…φₙ`.
-We have (roughly) `N(c ↩Λ φ i k).uncontractedList`
-is equal to `N((c.uncontractedList).eraseIdx k')`
-where `k'` is the position in `c.uncontractedList` corresponding to `k`.
+  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`
+  corresponding to `k` removed.
+
+  The proof of this result ultimately a consequence of definitions.
 -/
 lemma normalOrder_uncontracted_some (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
     (i : Fin φs.length.succ) (φsΛ : WickContraction φs.length) (k : φsΛ.uncontracted) :

HepLean/PerturbationTheory/FieldOpAlgebra/StaticWickTerm.lean

@@ -22,12 +22,17 @@ open FieldOpAlgebra
 open FieldStatistic
 noncomputable section
 
-/-- For a Wick contraction `φsΛ`, we define `staticWickTerm φsΛ` to be the element of
-  `𝓕.FieldOpAlgebra` given by `φsΛ.sign • φsΛ.staticContract * 𝓝([φsΛ]ᵘᶜ)`. -/
+/-- For a list `φs` of `𝓕.FieldOp`, and a Wick contraction `φsΛ` of `φs`, the element
+  of `𝓕.FieldOpAlgebra`, `φsΛ.staticWickTerm` is defined as
+
+  `φsΛ.sign • φsΛ.staticContract * 𝓝([φsΛ]ᵘᶜ)`.
+
+  This is term which appears in the static version Wick's theorem. -/
 def staticWickTerm {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) : 𝓕.FieldOpAlgebra :=
   φsΛ.sign • φsΛ.staticContract * 𝓝(ofFieldOpList [φsΛ]ᵘᶜ)
 
-/-- The static Wick term for the empty contraction of the empty list is `1`. -/
+/-- For the empty list `[]` of `𝓕.FieldOp`, the `staticWickTerm` of the empty Wick contraction
+  `empty` of `[]` (its only Wick contraction) is `1`. -/
 @[simp]
 lemma staticWickTerm_empty_nil :
     staticWickTerm (empty (n := ([] : List 𝓕.FieldOp).length)) = 1 := by
@@ -35,7 +40,9 @@ lemma staticWickTerm_empty_nil :
   simp [sign, empty, staticContract]
 
 /--
-Let `φsΛ` be a Wick Contraction for `φs = φ₀φ₁…φₙ`. Then the following holds
+For a list `φs = φ₀…φₙ` of `𝓕.FieldOp`, a Wick contraction `φsΛ` of `φs`, and an element `φ` of
+  `𝓕.FieldOp`, the following relation holds
+
 `(φsΛ ↩Λ φ 0 none).staticWickTerm = φsΛ.sign • φsΛ.staticWickTerm * 𝓝(φ :: [φsΛ]ᵘᶜ)`
 
 The proof of this result relies on
@@ -51,8 +58,9 @@ lemma staticWickTerm_insert_zero_none (φ : 𝓕.FieldOp) (φs : List 𝓕.Field
   simp only [staticContract_insert_none, insertAndContract_uncontractedList_none_zero,
     Algebra.smul_mul_assoc]
 
-/-- Let `φsΛ` be a Wick contraction for `φs = φ₀φ₁…φₙ`. Then`(φsΛ ↩Λ φ 0 (some k)).wickTerm`
-is equal the product of
+/-- For a list `φs = φ₀…φₙ` of `𝓕.FieldOp`, a Wick contraction `φsΛ` of `φs`, an element `φ` of
+  `𝓕.FieldOp`, and a `k` in `φsΛ.uncontracted`, `(φsΛ ↩Λ φ 0 (some k)).wickTerm` is equal
+  to the product of
 - the sign `𝓢(φ, φ₀…φᵢ₋₁) `
 - the sign `φsΛ.sign`
 - `φsΛ.staticContract`
@@ -60,9 +68,8 @@ is equal the product of
   uncontracted fields in `φ₀…φₖ₋₁`
 - the normal ordering `𝓝([φsΛ]ᵘᶜ.erase (uncontractedFieldOpEquiv φs φsΛ k))`.
 
-The proof of this result relies on
-- `staticContract_insert_some_of_lt` to rewrite static
-  contractions.
+The proof of this result ultimitley relies on
+- `staticContract_insert_some` to rewrite static contractions.
 - `normalOrder_uncontracted_some` to rewrite normal orderings.
 - `sign_insert_some_zero` to rewrite signs.
 -/
@@ -106,13 +113,16 @@ lemma staticWickTerm_insert_zero_some (φ : 𝓕.FieldOp) (φs : List 𝓕.Field
       simp
 
 /--
-Let `φsΛ` be a Wick contraction for `φs = φ₀φ₁…φₙ`. Then
+For a list `φs = φ₀…φₙ` of `𝓕.FieldOp`, a Wick contraction `φsΛ` of `φs`, the following relation
+holds
+
 `φ * φsΛ.staticWickTerm = ∑ k, (φsΛ ↩Λ φ i k).wickTerm`
+
 where the sum is over all `k` in `Option φsΛ.uncontracted` (so either `none` or `some k`).
 
 The proof of proceeds as follows:
 - `ofFieldOp_mul_normalOrder_ofFieldOpList_eq_sum` is used to expand `φ 𝓝([φsΛ]ᵘᶜ)` as
-  a sum over `k` in `Option φsΛ.uncontracted` of terms involving `[φ, φs[k]]` etc.
+  a sum over `k` in `Option φsΛ.uncontracted` of terms involving `[anPart φ, φs[k]]ₛ`.
 - Then `staticWickTerm_insert_zero_none` and `staticWickTerm_insert_zero_some` are
   used to equate terms.
 -/

HepLean/PerturbationTheory/FieldOpAlgebra/StaticWickTheorem.lean

@@ -20,24 +20,41 @@ open FieldStatistic
 namespace FieldOpAlgebra
 
 /--
-The static Wicks theorem states that
-`φ₀…φₙ` is equal to
-`∑ φsΛ, φsΛ.1.sign • φsΛ.1.staticContract * 𝓝(ofFieldOpList [φsΛ.1]ᵘᶜ)`
-over all Wick contraction `φsΛ`.
-This is compared to the ordinary Wicks theorem in which `staticContract` is replaced with
-`timeContract`.
+For a list `φs` of `𝓕.FieldOp`, the static version of Wick's theorem states that
+
+`φs =∑ φsΛ, φsΛ.staticWickTerm`
+
+where the sum is over all Wick contraction `φsΛ`.
+
+The proof is via induction on `φs`.
+- The base case `φs = []` is handled by `staticWickTerm_empty_nil`.
 
-The proof is via induction on `φs`. The base case `φs = []` is handled by `static_wick_theorem_nil`.
 The inductive step works as follows:
-- The proof considers `φ₀…φₙ` as `φ₀(φ₁…φₙ)` and use the induction hypothesis on `φ₁…φₙ`.
-- It also uses `ofFieldOp_mul_normalOrder_ofFieldOpList_eq_sum`
+
+For the LHS:
+1. The proof considers `φ₀…φₙ` as `φ₀(φ₁…φₙ)` and use the induction hypothesis on `φ₁…φₙ`.
+2. This gives terms of the form `φ * φsΛ.staticWickTerm` on which
+  `mul_staticWickTerm_eq_sum` is used where `φsΛ` is a Wick contraction of `φ₁…φₙ`,
+  to rewrite terms as a sum over optional uncontracted elements of `φsΛ`
+
+On the LHS we now have a sum over Wick contractions `φsΛ` of `φ₁…φₙ` (from 1) and optional
+uncontracted elements of `φsΛ` (from 2)
+
+For the RHS:
+1. The sum over Wick contractions of `φ₀…φₙ` on the RHS
+  is split via `insertLift_sum` into a sum over Wick contractions `φsΛ` of `φ₁…φₙ` and
+  sum over optional uncontracted elements of `φsΛ`.
+
+Both side now are sums over the same thing and their terms equate by the nature of the
+lemmas used.
+
 -/
 theorem static_wick_theorem : (φs : List 𝓕.FieldOp) →
     ofFieldOpList φs = ∑ (φsΛ : WickContraction φs.length), φsΛ.staticWickTerm
   | [] => by
     simp only [ofFieldOpList, ofFieldOpListF_nil, map_one, List.length_nil]
     rw [sum_WickContraction_nil]
-    simp
+    rw [staticWickTerm_empty_nil]
   | φ :: φs => by
     rw [ofFieldOpList_cons, static_wick_theorem φs]
     rw [show (φ :: φs) = φs.insertIdx (⟨0, Nat.zero_lt_succ φs.length⟩ : Fin φs.length.succ) φ

HepLean/PerturbationTheory/FieldOpAlgebra/TimeContraction.lean

@@ -23,15 +23,18 @@ namespace FieldOpAlgebra
 
 open FieldStatistic
 
-/-- The time contraction of two FieldOp as an element of `𝓞.A` defined
-  as their time ordering in the state algebra minus their normal ordering in the
-  creation and annihlation algebra, both mapped to `𝓞.A`.. -/
+/-- For a field specification `𝓕`, and `φ` and `ψ` elements of `𝓕.FieldOp`, the element of
+  `𝓕.FieldOpAlgebra`, `timeContract φ ψ` is defined to be `𝓣(φψ)- 𝓝(φψ)`. -/
 def timeContract (φ ψ : 𝓕.FieldOp) : 𝓕.FieldOpAlgebra :=
     𝓣(ofFieldOp φ * ofFieldOp ψ) - 𝓝(ofFieldOp φ * ofFieldOp ψ)
 
 lemma timeContract_eq_smul (φ ψ : 𝓕.FieldOp) : timeContract φ ψ =
     𝓣(ofFieldOp φ * ofFieldOp ψ) + (-1 : ℂ) • 𝓝(ofFieldOp φ * ofFieldOp ψ) := by rfl
 
+/-- For a field specification `𝓕`, and `φ` and `ψ` elements of `𝓕.FieldOp`, if
+  `φ` and `ψ` are time-ordered then
+
+  `timeContract φ ψ = [anPart φ, ofFieldOp ψ]ₛ`. -/
 lemma timeContract_of_timeOrderRel (φ ψ : 𝓕.FieldOp) (h : timeOrderRel φ ψ) :
     timeContract φ ψ = [anPart φ, ofFieldOp ψ]ₛ := by
   conv_rhs =>
@@ -55,6 +58,10 @@ lemma timeContract_of_not_timeOrderRel (φ ψ : 𝓕.FieldOp) (h : ¬ timeOrderR
   simp only [instCommGroup.eq_1, map_smul, map_add, smul_add]
   rw [smul_smul, smul_smul, mul_comm]
 
+/-- For a field specification `𝓕`, and `φ` and `ψ` elements of `𝓕.FieldOp`, if
+  `φ` and `ψ` are not time-ordered then
+
+  `timeContract φ ψ = 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ψ) • [anPart ψ, ofFieldOp φ]ₛ`. -/
 lemma timeContract_of_not_timeOrderRel_expand (φ ψ : 𝓕.FieldOp) (h : ¬ timeOrderRel φ ψ) :
     timeContract φ ψ = 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ψ) • [anPart ψ, ofFieldOp φ]ₛ := by
   rw [timeContract_of_not_timeOrderRel _ _ h]
@@ -62,6 +69,8 @@ lemma timeContract_of_not_timeOrderRel_expand (φ ψ : 𝓕.FieldOp) (h : ¬ tim
   have h1 := IsTotal.total (r := 𝓕.timeOrderRel) φ ψ
   simp_all
 
+/-- For a field specification `𝓕`, and `φ` and `ψ` elements of `𝓕.FieldOp`, then
+  `timeContract φ ψ` is in the center of `𝓕.FieldOpAlgebra`. -/
 lemma timeContract_mem_center (φ ψ : 𝓕.FieldOp) :
     timeContract φ ψ ∈ Subalgebra.center ℂ 𝓕.FieldOpAlgebra := by
   by_cases h : timeOrderRel φ ψ

HepLean/PerturbationTheory/FieldOpAlgebra/TimeOrder.lean

@@ -496,6 +496,8 @@ lemma timeOrder_superCommute_anPart_ofFieldOp_neq_time {φ ψ : 𝓕.FieldOp}
     apply timeOrder_superCommute_neq_time
     simp_all [crAnTimeOrderRel]
 
+/-- For a field specification `𝓕`, and `a`, `b`, `c` in `𝓕.FieldOpAlgebra`, then
+  `𝓣(a * b * c) = 𝓣(a * 𝓣(b) * c)`. -/
 lemma timeOrder_timeOrder_mid (a b c : 𝓕.FieldOpAlgebra) :
     𝓣(a * b * c) = 𝓣(a * 𝓣(b) * c) := by
   obtain ⟨a, rfl⟩ := ι_surjective a

HepLean/PerturbationTheory/FieldOpAlgebra/WickTerm.lean

@@ -24,12 +24,17 @@ open FieldOpAlgebra
 open FieldStatistic
 noncomputable section
 
-/-- For a Wick contraction `φsΛ`, we define `wickTerm φsΛ` to be the element of `𝓕.FieldOpAlgebra`
-  given by `φsΛ.sign • φsΛ.timeContract * 𝓝([φsΛ]ᵘᶜ)`. -/
+/-- For a list `φs` of `𝓕.FieldOp`, and a Wick contraction `φsΛ` of `φs`, the element
+  of `𝓕.FieldOpAlgebra`, `φsΛ.wickTerm` is defined as
+
+  `φsΛ.sign • φsΛ.timeContract * 𝓝([φsΛ]ᵘᶜ)`.
+
+  This is term which appears in the Wick's theorem. -/
 def wickTerm {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) : 𝓕.FieldOpAlgebra :=
   φsΛ.sign • φsΛ.timeContract * 𝓝(ofFieldOpList [φsΛ]ᵘᶜ)
 
-/-- The Wick term for the empty contraction of the empty list is `1`. -/
+/-- For the empty list `[]` of `𝓕.FieldOp`, the `wickTerm` of the empty Wick contraction
+  `empty` of `[]` (its only Wick contraction) is `1`. -/
 @[simp]
 lemma wickTerm_empty_nil :
     wickTerm (empty (n := ([] : List 𝓕.FieldOp).length)) = 1 := by
@@ -37,7 +42,9 @@ lemma wickTerm_empty_nil :
   simp [sign_empty]
 
 /--
-Let `φsΛ` be a Wick Contraction for `φs = φ₀φ₁…φₙ`. Then the following holds
+For a list `φs = φ₀…φₙ` of `𝓕.FieldOp`, a Wick contraction `φsΛ` of `φs`, an element `φ` of
+  `𝓕.FieldOp`, and `i ≤ φs.length` the following relation holds
+
 `(φsΛ ↩Λ φ i none).wickTerm = 𝓢(φ, φ₀…φᵢ₋₁) φsΛ.sign • φsΛ.timeContract * 𝓝(φ :: [φsΛ]ᵘᶜ)`
 
 The proof of this result relies on
@@ -86,16 +93,18 @@ lemma wickTerm_insert_none (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
     simp only [ZeroMemClass.coe_zero, zero_mul, smul_zero]
     exact hg
 
-/-- Let `φsΛ` be a Wick contraction for `φs = φ₀φ₁…φₙ`. Let `φ` be a field with time
-greater then or equal to all the fields in `φs`. Let `i` be a in `Fin φs.length.succ` such that
-all files in `φ₀…φᵢ₋₁` have time strictly less then `φ`. Then`(φsΛ ↩Λ φ i (some k)).wickTerm`
+/-- 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
+  `φ` has a time greater then or equal to all `FieldOp` in `φ₀…φₙ`, then
+  `(φsΛ ↩Λ φ i (some k)).wickTerm`
 is equal the product of
 - the sign `𝓢(φ, φ₀…φᵢ₋₁) `
 - the sign `φsΛ.sign`
 - `φsΛ.timeContract`
 - `s • [anPart φ, ofFieldOp φs[k]]ₛ` where `s` is the sign associated with moving `φ` through
   uncontracted fields in `φ₀…φₖ₋₁`
-- the normal ordering `𝓝([φsΛ]ᵘᶜ.erase (uncontractedFieldOpEquiv φs φsΛ k))`.
+- the normal ordering `[φsΛ]ᵘᶜ` with the field corresonding to `k` removed.
 
 The proof of this result relies on
 - `timeContract_insert_some_of_not_lt`
@@ -167,14 +176,16 @@ lemma wickTerm_insert_some (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
 
 /--
 Let `φsΛ` be a Wick contraction for `φs = φ₀φ₁…φₙ`. Let `φ` be a field with time
-greater then or equal to all the fields in `φs`. Let `i` be a in `Fin φs.length.succ` such that
-all files in `φ₀…φᵢ₋₁` have time strictly less then `φ`. Then
+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
+
 `φ * φsΛ.wickTerm = 𝓢(φ, φ₀…φᵢ₋₁) • ∑ k, (φsΛ ↩Λ φ i k).wickTerm`
+
 where the sum is over all `k` in `Option φsΛ.uncontracted` (so either `none` or `some k`).
 
 The proof of proceeds as follows:
 - `ofFieldOp_mul_normalOrder_ofFieldOpList_eq_sum` is used to expand `φ 𝓝([φsΛ]ᵘᶜ)` as
-  a sum over `k` in `Option φsΛ.uncontracted` of terms involving `[φ, φs[k]]` etc.
+  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)

HepLean/PerturbationTheory/FieldOpAlgebra/WicksTheorem.lean

@@ -61,18 +61,38 @@ remark wicks_theorem_context := "
   The statement of these theorems for bosons is simplier then when fermions are involved, since
   one does not have to worry about the minus-signs picked up on exchanging fields."
 
-/-- Wick's theorem states that for a list of fields `φs = φ₀…φₙ`
-`𝓣(φs) = ∑ φsΛ, (φsΛ.sign • φsΛ.timeContract) * 𝓝([φsΛ]ᵘᶜ)`
-where the sum is over all Wick contractions `φsΛ` of `φs`.
+/--
+For a list `φs` of `𝓕.FieldOp`, Wick's theorem states that
+
+`𝓣(φs) = ∑ φsΛ, φsΛ.wickTerm`
+
+where the sum is over all Wick contraction `φsΛ`.
+
+The proof is via induction on `φs`.
+- The base case `φs = []` is handled by `wickTerm_empty_nil`.
 
-The proof is via induction on `φs`. The base case `φs = []` is handled by `wicks_theorem_nil`.
 The inductive step works as follows:
-- The lemma `timeOrder_eq_maxTimeField_mul_finset` is used to write
+
+For the LHS:
+1. `timeOrder_eq_maxTimeField_mul_finset` is used to write
   `𝓣(φ₀…φₙ)` as ` 𝓢(φᵢ,φ₀…φᵢ₋₁) • φᵢ * 𝓣(φ₀…φᵢ₋₁φᵢ₊₁φₙ)` where `φᵢ` is
-  the maximal time field in `φ₀…φₙ`.
-- The induction hypothesis is used to expand `𝓣(φ₀…φᵢ₋₁φᵢ₊₁φₙ)` as a sum over Wick contractions of
-  `φ₀…φᵢ₋₁φᵢ₊₁φₙ`.
-- Further the lemmas `wick_term_cons_eq_sum_wick_term` and `insertLift_sum` are used.
+  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
+  `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Λ`
+
+On the LHS we now have a sum over Wick contractions `φsΛ` of `φ₀…φᵢ₋₁φᵢ₊₁φ` (from 2) and optional
+uncontracted elements of `φsΛ` (from 3)
+
+For the RHS:
+1. The sum over Wick contractions of `φ₀…φₙ` on the RHS
+  is split via `insertLift_sum` into a sum over Wick contractions `φsΛ` of `φ₀…φᵢ₋₁φᵢ₊₁φ` and
+  sum over optional uncontracted elements of `φsΛ`.
+
+Both side now are sums over the same thing and their terms equate by the nature of the
+lemmas used.
 -/
 theorem wicks_theorem : (φs : List 𝓕.FieldOp) → 𝓣(ofFieldOpList φs) =
     ∑ (φsΛ : WickContraction φs.length), φsΛ.wickTerm
@@ -80,7 +100,7 @@ theorem wicks_theorem : (φs : List 𝓕.FieldOp) → 𝓣(ofFieldOpList φs) =
     rw [timeOrder_ofFieldOpList_nil]
     simp only [map_one, List.length_nil, Algebra.smul_mul_assoc]
     rw [sum_WickContraction_nil]
-    simp
+    simp only [wickTerm_empty_nil]
   | φ :: φs => by
     have ih := wicks_theorem (eraseMaxTimeField φ φs)
     conv_lhs => rw [timeOrder_eq_maxTimeField_mul_finset, ih, Finset.mul_sum]

HepLean/PerturbationTheory/FieldOpAlgebra/WicksTheoremNormal.lean

@@ -20,6 +20,23 @@ namespace FieldOpAlgebra
 open WickContraction
 open EqTimeOnly
 
+/--
+For a list `φs` of `𝓕.FieldOp`, then
+
+`𝓣(φs) = ∑ φsΛ, φsΛ.1.wickTerm • φsΛ.1.timeContract.1 * 𝓣(𝓝(ofFieldOpList [φsΛ.1]ᵘᶜ))`
+
+where the sum is over all Wick contraction `φsΛ` which only have equal time contractions.
+
+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.
+- `timeOrder_timeContract_mul_of_eqTimeOnly_left` to move the time contracts out of the time
+  ordering.
+-/
 lemma timeOrder_ofFieldOpList_eqTimeOnly (φs : List 𝓕.FieldOp) :
     𝓣(ofFieldOpList φs) = ∑ (φsΛ : {φsΛ // φsΛ.EqTimeOnly (φs := φs)}),
     φsΛ.1.sign • φsΛ.1.timeContract.1 * 𝓣(𝓝(ofFieldOpList [φsΛ.1]ᵘᶜ)) := by
@@ -45,7 +62,7 @@ lemma timeOrder_ofFieldOpList_eqTimeOnly (φs : List 𝓕.FieldOp) :
   exact x.2
 
 lemma timeOrder_ofFieldOpList_eq_eqTimeOnly_empty (φs : List 𝓕.FieldOp) :
-    timeOrder (ofFieldOpList φs) = 𝓣(𝓝(ofFieldOpList φs)) +
+    𝓣(ofFieldOpList φs) = 𝓣(𝓝(ofFieldOpList φs)) +
     ∑ (φsΛ : {φsΛ // φsΛ.EqTimeOnly (φs := φs) ∧ φsΛ ≠ empty}),
     φsΛ.1.sign • φsΛ.1.timeContract.1 * 𝓣(𝓝(ofFieldOpList [φsΛ.1]ᵘᶜ)) := by
   let e1 : {φsΛ : WickContraction φs.length // φsΛ.EqTimeOnly} ≃
@@ -71,6 +88,17 @@ lemma timeOrder_ofFieldOpList_eq_eqTimeOnly_empty (φs : List 𝓕.FieldOp) :
     rw [← e2.symm.sum_comp]
     rfl
 
+/--
+For a list `φs` of `𝓕.FieldOp`, then
+
+`𝓣(𝓝(φs)) = 𝓣(φs) - ∑ φsΛ, φsΛ.1.wickTerm • φsΛ.1.timeContract.1 * 𝓣(𝓝(ofFieldOpList [φsΛ.1]ᵘᶜ))`
+
+where the sum is over all *non-empty* Wick contraction `φsΛ` which only
+  have equal time contractions.
+
+This result follows directly from
+- `timeOrder_ofFieldOpList_eqTimeOnly`
+-/
 lemma normalOrder_timeOrder_ofFieldOpList_eq_eqTimeOnly_empty (φs : List 𝓕.FieldOp) :
     𝓣(𝓝(ofFieldOpList φs)) = 𝓣(ofFieldOpList φs) -
     ∑ (φsΛ : {φsΛ // φsΛ.EqTimeOnly (φs := φs) ∧ φsΛ ≠ empty}),
@@ -78,14 +106,32 @@ lemma normalOrder_timeOrder_ofFieldOpList_eq_eqTimeOnly_empty (φs : List 𝓕.F
   rw [timeOrder_ofFieldOpList_eq_eqTimeOnly_empty]
   simp
 
-lemma normalOrder_timeOrder_ofFieldOpList_eq_haveEqTime_sum_not_haveEqTime (φs : List 𝓕.FieldOp) :
-    𝓣(𝓝(ofFieldOpList φs)) = (∑ (φsΛ : {φsΛ : WickContraction φs.length // ¬ HaveEqTime φsΛ}),
+/--
+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
+  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.
+-/
+lemma timeOrder_haveEqTime_split (φs : List 𝓕.FieldOp) :
+    𝓣(ofFieldOpList φs) = (∑ (φsΛ : {φsΛ : WickContraction φs.length // ¬ HaveEqTime φsΛ}),
     φsΛ.1.sign • φsΛ.1.timeContract.1 * 𝓝(ofFieldOpList [φsΛ.1]ᵘᶜ))
-    + (∑ (φsΛ : {φsΛ : WickContraction φs.length // HaveEqTime φsΛ}),
-    φsΛ.1.sign • φsΛ.1.timeContract.1 * 𝓝(ofFieldOpList [φsΛ.1]ᵘᶜ))
-    - ∑ (φsΛ : {φsΛ // φsΛ.EqTimeOnly (φs := φs) ∧ φsΛ ≠ empty}),
-    φsΛ.1.sign • φsΛ.1.timeContract.1 * 𝓣(𝓝(ofFieldOpList [φsΛ.1]ᵘᶜ)) := by
-  rw [normalOrder_timeOrder_ofFieldOpList_eq_eqTimeOnly_empty]
+    + ∑ (φsΛ : {φsΛ // φsΛ.EqTimeOnly (φs := φs) ∧ φsΛ ≠ empty}), φsΛ.1.sign • φsΛ.1.timeContract *
+    (∑ φssucΛ : { φssucΛ : WickContraction [φsΛ.1]ᵘᶜ.length // ¬ φssucΛ.HaveEqTime },
+      φssucΛ.1.wickTerm) := by
   rw [wicks_theorem]
   simp only [wickTerm]
   let e1 : WickContraction φs.length ≃ {φsΛ // HaveEqTime φsΛ} ⊕ {φsΛ // ¬ HaveEqTime φsΛ} := by
@@ -94,17 +140,9 @@ lemma normalOrder_timeOrder_ofFieldOpList_eq_haveEqTime_sum_not_haveEqTime (φs
   simp only [Equiv.symm_symm, Algebra.smul_mul_assoc, Fintype.sum_sum_type,
     Equiv.sumCompl_apply_inl, Equiv.sumCompl_apply_inr, ne_eq, sub_left_inj, e1]
   rw [add_comm]
-
-lemma haveEqTime_wick_sum_eq_split (φs : List 𝓕.FieldOp) :
-    (∑ (φsΛ : {φsΛ : WickContraction φs.length // HaveEqTime φsΛ}),
-    φsΛ.1.sign • φsΛ.1.timeContract.1 * 𝓝(ofFieldOpList [φsΛ.1]ᵘᶜ)) =
-    ∑ (φsΛ : {φsΛ // φsΛ.EqTimeOnly (φs := φs) ∧ φsΛ ≠ empty}),
-      (sign φs ↑φsΛ • (φsΛ.1).timeContract *
-    ∑ φssucΛ : { φssucΛ : WickContraction [φsΛ.1]ᵘᶜ.length // ¬φssucΛ.HaveEqTime },
-      sign [φsΛ.1]ᵘᶜ φssucΛ •
-      (φssucΛ.1).timeContract * normalOrder (ofFieldOpList [φssucΛ.1]ᵘᶜ)) := by
+  congr 1
   let f : WickContraction φs.length → 𝓕.FieldOpAlgebra := fun φsΛ =>
-    φsΛ.sign • φsΛ.timeContract.1 * 𝓝(ofFieldOpList [φsΛ]ᵘᶜ)
+    φsΛ.sign • (φsΛ.timeContract.1 * 𝓝(ofFieldOpList [φsΛ]ᵘᶜ))
   change ∑ (φsΛ : {φsΛ : WickContraction φs.length // HaveEqTime φsΛ}), f φsΛ.1 = _
   rw [sum_haveEqTime]
   congr
@@ -112,12 +150,12 @@ lemma haveEqTime_wick_sum_eq_split (φs : List 𝓕.FieldOp) :
   simp only [f]
   conv_lhs =>
     enter [2, φsucΛ]
-    enter [1]
+    rw [← Algebra.smul_mul_assoc]
     rw [join_sign_timeContract φsΛ.1 φsucΛ.1]
   conv_lhs =>
     enter [2, φsucΛ]
     rw [mul_assoc]
-  rw [← Finset.mul_sum]
+  rw [← Finset.mul_sum, ← Algebra.smul_mul_assoc]
   congr
   funext φsΛ'
   simp only [ne_eq, Algebra.smul_mul_assoc]
@@ -125,17 +163,16 @@ lemma haveEqTime_wick_sum_eq_split (φs : List 𝓕.FieldOp) :
   rw [@join_uncontractedListGet]
 
 lemma normalOrder_timeOrder_ofFieldOpList_eq_not_haveEqTime_sub_inductive (φs : List 𝓕.FieldOp) :
-    𝓣(𝓝(ofFieldOpList φs)) = (∑ (φsΛ : {φsΛ : WickContraction φs.length // ¬ HaveEqTime φsΛ}),
-    φsΛ.1.sign • φsΛ.1.timeContract.1 * 𝓝(ofFieldOpList [φsΛ.1]ᵘᶜ))
+    𝓣(𝓝(ofFieldOpList φs)) =
+      (∑ (φsΛ : {φsΛ : WickContraction φs.length // ¬ HaveEqTime φsΛ}), φsΛ.1.wickTerm)
       + ∑ (φsΛ : {φsΛ // φsΛ.EqTimeOnly (φs := φs) ∧ φsΛ ≠ empty}),
         sign φs ↑φsΛ • (φsΛ.1).timeContract *
         (∑ φssucΛ : { φssucΛ : WickContraction [φsΛ.1]ᵘᶜ.length // ¬ φssucΛ.HaveEqTime },
-      sign [φsΛ.1]ᵘᶜ φssucΛ • (φssucΛ.1).timeContract * normalOrder (ofFieldOpList [φssucΛ.1]ᵘᶜ) -
-      𝓣(𝓝(ofFieldOpList [φsΛ.1]ᵘᶜ))) := by
-  rw [normalOrder_timeOrder_ofFieldOpList_eq_haveEqTime_sum_not_haveEqTime]
+        φssucΛ.1.wickTerm - 𝓣(𝓝(ofFieldOpList [φsΛ.1]ᵘᶜ))) := by
+  rw [normalOrder_timeOrder_ofFieldOpList_eq_eqTimeOnly_empty,
+    timeOrder_haveEqTime_split]
   rw [add_sub_assoc]
   congr 1
-  rw [haveEqTime_wick_sum_eq_split]
   simp only [ne_eq, Algebra.smul_mul_assoc]
   rw [← Finset.sum_sub_distrib]
   congr 1
@@ -177,19 +214,25 @@ lemma wicks_theorem_normal_order_empty : 𝓣(𝓝(ofFieldOpList [])) =
   rw [timeOrderF_ofCrAnListF]
   simp
 
-/--
-Wicks theorem for normal ordering followed by time-ordering, states that
-`𝓣(𝓝(φ₀…φₙ))` is equal to
-`∑ φsΛ, φsΛ.1.sign • φsΛ.1.timeContract.1 * 𝓝(ofFieldOpList [φsΛ.1]ᵘᶜ)`
-over those Wick contraction `φsΛ` which do not have any equal time contractions.
-This is compared to the ordinary Wicks theorem which sums over all Wick contractions.
+/--For a list `φs` of `𝓕.FieldOp`, the normal-ordered version of Wick's theorem states that
+
+`𝓣(𝓝(φs)) = ∑ φsΛ, φsΛ.wickTerm`
+
+where the sum is over all Wick contraction `φsΛ` in which no two contracted elements
+have the same time.
+
+The proof of proceeds by induction on `φs`, with the base case `[]` holding by following
+through definitions. and the inductive case holding as a result of
+- `timeOrder_haveEqTime_split`
+- `normalOrder_timeOrder_ofFieldOpList_eq_eqTimeOnly_empty`
+- and the induction hypothesis on `𝓣(𝓝([φsΛ.1]ᵘᶜ))` for contractions `φsΛ` of `φs` which only
+  have equal time contractions and are non-empty.
 -/
 theorem wicks_theorem_normal_order : (φs : List 𝓕.FieldOp) →
     𝓣(𝓝(ofFieldOpList φs)) =
     ∑ (φsΛ : {φsΛ : WickContraction φs.length // ¬ HaveEqTime φsΛ}), φsΛ.1.wickTerm
   | [] => wicks_theorem_normal_order_empty
   | φ :: φs => by
-    simp only [wickTerm]
     rw [normalOrder_timeOrder_ofFieldOpList_eq_not_haveEqTime_sub_inductive]
     simp only [Algebra.smul_mul_assoc, ne_eq, add_right_eq_self]
     apply Finset.sum_eq_zero

HepLean/PerturbationTheory/FieldSpecification/NormalOrder.lean

@@ -347,7 +347,7 @@ lemma normalOrderList_eraseIdx_normalOrderEquiv {φs : List 𝓕.CrAnFieldOp} (n
   the following relation holds
   `normalOrderSign (φ₀…φᵢ₋₁φᵢ₊₁…φₙ)` is equal to the product of
   - `normalOrderSign φ₀…φₙ`,
-  - `𝓢(φᵢ, φ₀…φᵢ₋₁)` i.e. the sign needed to remove `φᵢ` from  `φ₀…φₙ`,
+  - `𝓢(φᵢ, φ₀…φᵢ₋₁)` i.e. the sign needed to remove `φᵢ` from `φ₀…φₙ`,
   - `𝓢(φᵢ, _)` where `_` is the list of elements appearing before `φᵢ` after normal ordering. I.e.
     the sign needed to insert `φᵢ` back into the normal-ordered list at the correct place. -/
 lemma normalOrderSign_eraseIdx (φs : List 𝓕.CrAnFieldOp) (i : Fin φs.length) :

HepLean/PerturbationTheory/WickContraction/Basic.lean

@@ -14,13 +14,18 @@ open FieldSpecification
 variable {𝓕 : FieldSpecification}
 
 /--
-Given a natural number `n` corresponding to the number of fields, a Wick contraction
-is a finite set of pairs of `Fin n`, such that no element of `Fin n` occurs in more then one pair.
+Given a natural number `n`, which will correspond to the number of fields needing
+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
@@ -37,6 +42,12 @@ namespace WickContraction
 variable {n : ℕ} (c : WickContraction n)
 open HepLean.List
 
+remark contraction_notation := "Given a field specification `𝓕`, and a list `φs`
+  of `𝓕.FieldOp`, a Wick contraction of `φs` will mean a Wick contraction in
+  `WickContraction φs.length`. The notation `φsΛ` will be used for such contractions.
+  The terminology that `φsΛ` contracts pairs within of `φs` will also be used, even though
+  `φsΛ` is really contains positions of `φs`."
+
 /-- Wick contractions are decidable. -/
 instance : DecidableEq (WickContraction n) := Subtype.instDecidableEq
 
@@ -520,8 +531,11 @@ lemma prod_finset_eq_mul_fst_snd (c : WickContraction n) (a : c.1)
   rw [← (c.contractEquivFinTwo a).symm.prod_comp]
   simp [contractEquivFinTwo]
 
-/-- A Wick contraction associated with a list of states is said to be `GradingCompliant` if in any
-  contracted pair of states they are either both fermionic or both bosonic. -/
+/-- 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. -/
 def GradingCompliant (φs : List 𝓕.FieldOp) (φsΛ : WickContraction φs.length) :=
   ∀ (a : φsΛ.1), (𝓕 |>ₛ φs[φsΛ.fstFieldOfContract a]) = (𝓕 |>ₛ φs[φsΛ.sndFieldOfContract a])
 

HepLean/PerturbationTheory/WickContraction/Card.lean

@@ -236,9 +236,9 @@ def cardFun : ℕ → ℕ
   | 1 => 1
   | Nat.succ (Nat.succ n) => cardFun (Nat.succ n) + (n + 1) * cardFun n
 
-/-- The number of Wick contractions for `n : ℕ` fields, i.e. the cardinality of
-  `WickContraction n`, is equal to the terms in
-  Online Encyclopedia of Integer Sequences (OEIS) A000085. -/
+/-- The number of Wick contractions in `WickContraction n` is equal to the terms in
+  Online Encyclopedia of Integer Sequences (OEIS) A000085. That is:
+  1, 1, 2, 4, 10, 26, 76, 232, 764, 2620, 9496, ... -/
 theorem card_eq_cardFun : (n : ℕ) → Fintype.card (WickContraction n) = cardFun n
   | 0 => by decide
   | 1 => by decide

HepLean/PerturbationTheory/WickContraction/InsertAndContract.lean

@@ -24,15 +24,19 @@ open HepLean.Fin
 
 -/
 
-/-- Given a Wick contraction `φsΛ` associated to a list `φs`,
-    a position `i : Fin φs.lengthsucc`, an element `φ`, and an optional uncontracted element
-  `j : Option (φsΛ.uncontracted)` of `φsΛ`.
-  The Wick contraction `φsΛ.insertAndContract φ i j` is defined to be the Wick contraction
-  associated with `(φs.insertIdx i φ)` formed by 'inserting' `φ` into `φs` after the first `i`
-  elements and contracting `φ` optionally with `j`.
+/-- 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
+  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Λ`
+  accordingly.
+  If `j` is not `none`, but rather `some j`, to this contraction is added the contraction
+  of `φ` (at position `i`) with the new position of `j` after `φ` is added.
 
-  The notation `φsΛ ↩Λ φ i j` is used to denote `φsΛ.insertAndContract φ i j`. Thus,
-  `φsΛ ↩Λ φ i none` indicates the case when we insert `φ` into `φs` but do not contract it. -/
+  In other words, `φsΛ.insertAndContract φ i j` is formed by adding `φ` to `φs` at position `i`,
+  and contracting `φ` with the field orginally at position `j` if `j` is not none.
+
+  The notation `φsΛ ↩Λ φ i j` is used to denote `φsΛ.insertAndContract φ i j`. -/
 def insertAndContract {φs : List 𝓕.FieldOp} (φ : 𝓕.FieldOp) (φsΛ : WickContraction φs.length)
     (i : Fin φs.length.succ) (j : Option φsΛ.uncontracted) :
     WickContraction (φs.insertIdx i φ).length :=
@@ -280,6 +284,14 @@ lemma insert_fin_eq_self (φ : 𝓕.FieldOp) {φs : List 𝓕.FieldOp}
     use z
     rfl
 
+/-- For a list `φs` of `𝓕.FieldOp`, a Wick contraction `φsΛ` of `φs`, an element `φ` of
+  `𝓕.FieldOp`, a `i ≤ φs.length` 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
+  `∑ (φ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}
     (i : Fin φs.length.succ) [AddCommMonoid M] (f : WickContraction (φs.insertIdx i φ).length → M) :
     ∑ c, f c =

HepLean/PerturbationTheory/WickContraction/Join.lean

@@ -23,9 +23,9 @@ variable {n : ℕ} (c : WickContraction n)
 open HepLean.List
 open FieldOpAlgebra
 
-/-- Given a Wick contraction `φsΛ` on `φs` and a Wick contraction `φsucΛ` on the uncontracted fields
-within `φsΛ`, a Wick contraction on `φs`consisting of the contractins in `φsΛ` and
-the contractions in `φsucΛ`. -/
+/-- 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Λ`. -/
 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

@@ -28,10 +28,11 @@ def signFinset (c : WickContraction n) (i1 i2 : Fin n) : Finset (Fin n) :=
   Finset.univ.filter (fun i => i1 < i ∧ i < i2 ∧
   (c.getDual? i = none ∨ ∀ (h : (c.getDual? i).isSome), i1 < (c.getDual? i).get h))
 
-/-- Given a Wick contraction `φsΛ` associated with a list of states `φs`
-  the sign associated with `φsΛ` is the sign corresponding to the number
-  of fermionic-fermionic exchanges one must do to put elements in contracted pairs
-  of `φsΛ` next to each other. -/
+/-- 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
+  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],
     𝓕 |>ₛ ⟨φs.get, φsΛ.signFinset (φsΛ.fstFieldOfContract a) (φsΛ.sndFieldOfContract a)⟩)

HepLean/PerturbationTheory/WickContraction/Sign/InsertNone.lean

@@ -238,10 +238,14 @@ lemma signInsertNone_eq_filterset (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
     simp [h]
   · exact hG
 
-/-- For `φsΛ` a grading compliant Wick contraction, and `i : Fin φs.length.succ` we have
+/-- 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
   `(φsΛ ↩Λ φ i none).sign = s * φsΛ.sign`
   where `s` is the sign got by moving `φ` through the elements of `φ₀…φᵢ₋₁` which
-  are contracted. -/
+  are contracted with some element.
+
+  The proof of this result involves a careful consideration of the contributions of different
+  `FieldOp`s in `φs` to the sign of `φsΛ ↩Λ φ i none`. -/
 lemma sign_insert_none (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
     (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (hG : GradingCompliant φs φsΛ) :
     (φsΛ ↩Λ φ i none).sign = 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ⟨φs.get, Finset.univ.filter
@@ -250,6 +254,11 @@ lemma sign_insert_none (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
   rw [signInsertNone_eq_filterset]
   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`.
+
+  This is a direct corollary of `sign_insert_none`. -/
 lemma sign_insert_none_zero (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
     (φsΛ : WickContraction φs.length) : (φsΛ ↩Λ φ 0 none).sign = φsΛ.sign := by
   rw [sign_insert_none_eq_signInsertNone_mul_sign]

HepLean/PerturbationTheory/WickContraction/Sign/InsertSome.lean

@@ -855,13 +855,15 @@ lemma signInsertSome_mul_filter_contracted_of_not_lt (φ : 𝓕.FieldOp) (φs :
         exact fun h => lt_of_le_of_ne h (Fin.succAbove_ne i ((φsΛ.getDual? j).get hj))
 
 /--
-For `k < i`, the sign of `φsΛ ↩Λ φ i (some k)` is equal to the product of
-- the sign associated with moving `φ` through the `φsΛ`-uncontracted fields in `φ₀…φₖ`,
-- the sign associated with moving `φ` through the fields in `φ₀…φᵢ₋₁`,
+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`,
+the sign of `φsΛ ↩Λ φ i (some k)` is equal to the product of
+- the sign associated with moving `φ` through the `φsΛ`-uncontracted `FieldOp` in `φ₀…φₖ`,
+- the sign associated with moving `φ` through all `FieldOp` in `φ₀…φᵢ₋₁`,
 - the sign of `φsΛ`.
 
 The proof of this result involves a careful consideration of the contributions of different
-fields in `φs` to the sign of `φsΛ ↩Λ φ i (some k)`.
+`FieldOp` in `φs` to the sign of `φsΛ ↩Λ φ i (some k)`.
 -/
 lemma sign_insert_some_of_lt (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
     (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (k : φsΛ.uncontracted)
@@ -878,13 +880,15 @@ lemma sign_insert_some_of_lt (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
   simp
 
 /--
-For `i ≤ k`, the sign of `φsΛ ↩Λ φ i (some k)` is equal to the product of
-- the sign associated with moving `φ` through the `φsΛ`-uncontracted fields in `φ₀…φₖ₋₁`,
-- the sign associated with moving `φ` through the fields in `φ₀…φᵢ₋₁`,
+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 `i ≤ k`,
+the sign of `φsΛ ↩Λ φ i (some k)` is equal to the product of
+- the sign associated with moving `φ` through the `φsΛ`-uncontracted `FieldOp` in `φ₀…φₖ₋₁`,
+- the sign associated with moving `φ` through all the `FieldOp` in `φ₀…φᵢ₋₁`,
 - the sign of `φsΛ`.
 
 The proof of this result involves a careful consideration of the contributions of different
-fields in `φs` to the sign of `φsΛ ↩Λ φ i (some k)`.
+`FieldOp` in `φs` to the sign of `φsΛ ↩Λ φ i (some k)`.
 -/
 lemma sign_insert_some_of_not_lt (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
     (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (k : φsΛ.uncontracted)
@@ -900,6 +904,15 @@ lemma sign_insert_some_of_not_lt (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
   rw [mul_comm, ← mul_assoc]
   simp
 
+/--
+For a list `φs = φ₀…φₙ` of `𝓕.FieldOp`, a Wick contraction `φsΛ` of `φs`, an element `φ` of
+  `𝓕.FieldOp`, and a `k` in `φsΛ.uncontracted`,
+the sign of `φsΛ ↩Λ φ 0 (some k)` is equal to the product of
+- the sign associated with moving `φ` through the `φsΛ`-uncontracted `FieldOp` in `φ₀…φₖ₋₁`,
+- the sign of `φsΛ`.
+
+This is a direct corollary of `sign_insert_some_of_not_lt`.
+-/
 lemma sign_insert_some_zero (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
     (φsΛ : WickContraction φs.length) (k : φsΛ.uncontracted)
     (hn : GradingCompliant φs φsΛ ∧ (𝓕|>ₛφ) = 𝓕|>ₛφs[k.1]) :

HepLean/PerturbationTheory/WickContraction/Sign/Join.lean

@@ -417,16 +417,23 @@ lemma join_sign_induction {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs
     apply sign_congr
     exact join_uncontractedListGet (singleton hij) φsucΛ'
 
-/-- Let `φsΛ` be a grading compliant Wick contraction for `φs` and
-  `φsucΛ` a Wick contraction for `[φsΛ]ᵘᶜ`. Then `(join φsΛ φsucΛ).sign = φsΛ.sign * φsucΛ.sign`.
+/-- For a list `φs` of `𝓕.FieldOp`, a grading compliant Wick contraction `φsΛ` of `φs`,
+  and a Wick contraction `φsucΛ` of `[φsΛ]ᵘᶜ`, the following relation holds
+  `(join φsΛ φsucΛ).sign = φsΛ.sign * φsucΛ.sign`.
 
-  This lemma manifests the fact that it does not matter which order contracted pairs are brought
-  together when defining the sign of a contraction. -/
+  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
+  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) :
-    (join φsΛ φsucΛ).sign = φsΛ.sign * φsucΛ.sign := by
-  exact join_sign_induction φsΛ φsucΛ hc (φsΛ).1.card rfl
+    (join φsΛ φsucΛ).sign = φsΛ.sign * φsucΛ.sign :=
+  join_sign_induction φsΛ φsucΛ hc (φsΛ).1.card rfl
 
+/-- For a list `φs` of `𝓕.FieldOp`, a Wick contraction `φsΛ` of `φs`,
+  and a Wick contraction `φsucΛ` of `[φsΛ]ᵘᶜ`,
+  `(join φsΛ φsucΛ).sign • (join φsΛ φsucΛ).timeContract` is equal to the product of
+  - `φsΛ.sign • φsΛ.timeContract` and
+  - `φsucΛ.sign • φsucΛ.timeContract`. -/
 lemma join_sign_timeContract {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length)
     (φsucΛ : WickContraction [φsΛ]ᵘᶜ.length) :
     (join φsΛ φsucΛ).sign • (join φsΛ φsucΛ).timeContract.1 =

HepLean/PerturbationTheory/WickContraction/StaticContract.lean

@@ -18,9 +18,11 @@ namespace WickContraction
 variable {n : ℕ} (c : WickContraction n)
 open HepLean.List
 open FieldOpAlgebra
-/-- Given a Wick contraction `φsΛ` associated with a list `φs`, the
-  product of all time-contractions of pairs of contracted elements in `φs`,
-  as a member of the center of `𝓞.A`. -/
+
+/-- 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Λ`
+  with `j < k`. -/
 noncomputable def staticContract {φs : List 𝓕.FieldOp}
     (φsΛ : WickContraction φs.length) :
     Subalgebra.center ℂ 𝓕.FieldOpAlgebra :=
@@ -28,6 +30,13 @@ noncomputable def staticContract {φs : List 𝓕.FieldOp}
     ofFieldOp (φs.get (φsΛ.sndFieldOfContract a))]ₛ,
       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
+
+  `(φsΛ ↩Λ φ i none).staticContract = φsΛ.staticContract`
+
+  The prove of this result ultimately a consequence of definitions.
+-/
 @[simp]
 lemma staticContract_insert_none (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
     (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) :
@@ -37,15 +46,16 @@ lemma staticContract_insert_none (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
   ext a
   simp
 
-/-- For `φsΛ` a Wick contraction for `φs = φ₀…φₙ`, the time contraction
-  `(φsΛ ↩Λ φ i (some j)).timeContract 𝓞` is equal to the multiple of
-- the time contraction of `φ` with `φⱼ` if `i < i.succAbove j` else
-    `φⱼ` with `φ`.
-- `φsΛ.timeContract 𝓞`.
-This follows from the fact that `(φsΛ ↩Λ φ i (some j))` has one more contracted pair than `φsΛ`,
-corresponding to `φ` contracted with `φⱼ`. The order depends on whether we insert `φ` before
-or after `φⱼ`. -/
-lemma staticContract_insertAndContract_some
+/--
+  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)).staticContract` is equal to the product of
+  - `[anPart φ, φs[k]]ₛ` if `i ≤ k` or `[anPart φs[k], φ]ₛ` if `k < i`
+  - `φsΛ.staticContract`.
+
+  The proof of this result ultimately a consequence of definitions.
+-/
+lemma staticContract_insert_some
     (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
     (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (j : φsΛ.uncontracted) :
     (φsΛ ↩Λ φ i (some j)).staticContract =
@@ -74,7 +84,7 @@ lemma staticContract_insert_some_of_lt
     𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ⟨φs.get, (φsΛ.uncontracted.filter (fun x => x < k))⟩)
     • (contractStateAtIndex φ [φsΛ]ᵘᶜ ((uncontractedFieldOpEquiv φs φsΛ) (some k)) *
       φsΛ.staticContract) := by
-  rw [staticContract_insertAndContract_some]
+  rw [staticContract_insert_some]
   simp only [Nat.succ_eq_add_one, Fin.getElem_fin, ite_mul, instCommGroup.eq_1,
     contractStateAtIndex, uncontractedFieldOpEquiv, Equiv.optionCongr_apply,
     Equiv.coe_trans, Option.map_some', Function.comp_apply, finCongr_apply, Fin.coe_cast,

HepLean/PerturbationTheory/WickContraction/TimeCond.lean

@@ -96,6 +96,9 @@ lemma empty_mem {φs : List 𝓕.FieldOp} : empty (n := φs.length).EqTimeOnly :
   rw [eqTimeOnly_iff_forall_finset]
   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
+  `φsΛ.staticContract = φsΛ.timeContract`. -/
 lemma staticContract_eq_timeContract_of_eqTimeOnly (h : φsΛ.EqTimeOnly) :
     φsΛ.staticContract = φsΛ.timeContract := by
   simp only [staticContract, timeContract]
@@ -190,6 +193,12 @@ lemma timeOrder_timeContract_mul_of_eqTimeOnly_mid {φs : List 𝓕.FieldOp}
     𝓣(a * φsΛ.timeContract.1 * b) = φsΛ.timeContract.1 * 𝓣(a * b) := by
   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
+  `b` a general element in `𝓕.FieldOpAlgebra`. Then
+  `𝓣(φsΛ.timeContract.1 * b) = φsΛ.timeContract.1 * 𝓣(b)`.
+
+  This follows from properties of orderings and the ideal defining `𝓕.FieldOpAlgebra`. -/
 lemma timeOrder_timeContract_mul_of_eqTimeOnly_left {φs : List 𝓕.FieldOp}
     (φsΛ : WickContraction φs.length)
     (hl : φsΛ.EqTimeOnly) (b : 𝓕.FieldOpAlgebra) :
@@ -238,6 +247,9 @@ lemma timeOrder_timeContract_of_not_eqTimeOnly {φs : List 𝓕.FieldOp}
   intro h
   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
+  `𝓣(φ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
   obtain ⟨i, j, hij, φsucΛ, rfl, hr⟩ := exists_join_singleton_of_not_eqTimeOnly φsΛ hl

HepLean/PerturbationTheory/WickContraction/TimeContract.lean

@@ -18,9 +18,11 @@ namespace WickContraction
 variable {n : ℕ} (c : WickContraction n)
 open HepLean.List
 open FieldOpAlgebra
-/-- Given a Wick contraction `φsΛ` associated with a list `φs`, the
-  product of all time-contractions of pairs of contracted elements in `φs`,
-  as a member of the center of `𝓞.A`. -/
+
+/-- 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Λ`
+  with `j < k`. -/
 noncomputable def timeContract {φs : List 𝓕.FieldOp}
     (φsΛ : WickContraction φs.length) :
     Subalgebra.center ℂ 𝓕.FieldOpAlgebra :=
@@ -28,11 +30,12 @@ noncomputable def timeContract {φs : List 𝓕.FieldOp}
     (φs.get (φsΛ.fstFieldOfContract a)) (φs.get (φsΛ.sndFieldOfContract a)),
     timeContract_mem_center _ _⟩
 
-/-- For `φsΛ` a Wick contraction for `φs`, the time contraction `(φsΛ ↩Λ φ i none).timeContract 𝓞`
-  is equal to `φsΛ.timeContract 𝓞`.
+/-- 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
 
-This result follows from the fact that `timeContract` only depends on contracted pairs,
-and `(φsΛ ↩Λ φ i none)` has the 'same' contracted pairs as `φsΛ`. -/
+  `(φsΛ ↩Λ φ i none).timeContract = φsΛ.timeContract`
+
+  The prove of this result ultimately a consequence of definitions. -/
 @[simp]
 lemma timeContract_insert_none (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
     (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) :
@@ -42,14 +45,13 @@ lemma timeContract_insert_none (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
   ext a
   simp
 
-/-- For `φsΛ` a Wick contraction for `φs = φ₀…φₙ`, the time contraction
-  `(φsΛ ↩Λ φ i (some j)).timeContract 𝓞` is equal to the multiple of
-- the time contraction of `φ` with `φⱼ` if `i < i.succAbove j` else
-    `φⱼ` with `φ`.
-- `φsΛ.timeContract 𝓞`.
-This follows from the fact that `(φsΛ ↩Λ φ i (some j))` has one more contracted pair than `φsΛ`,
-corresponding to `φ` contracted with `φⱼ`. The order depends on whether we insert `φ` before
-or after `φⱼ`. -/
+/-- 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)).timeContract` is equal to the product of
+  - `timeContract φ φs[k]` if `i ≤ k` or `timeContract φs[k] φ` if `k < i`
+  - `φsΛ.timeContract`.
+
+  The proof of this result ultimately a consequence of definitions. -/
 lemma timeContract_insertAndContract_some
     (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
     (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (j : φsΛ.uncontracted) :
@@ -77,6 +79,17 @@ lemma timeContract_empty (φs : List 𝓕.FieldOp) :
 
 open FieldStatistic
 
+/-! 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 `i ≤ k`, with the
+  condition that `φ` has greater or equal time to `φs[k]`, then
+  `(φsΛ ↩Λ φ i (some k)).timeContract` is equal to the product of
+  - `[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.
+
+  The proof of this result ultimately a consequence of definitions and
+  `timeContract_of_timeOrderRel`. -/
 lemma timeContract_insert_some_of_lt
     (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
     (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (k : φsΛ.uncontracted)
@@ -110,6 +123,19 @@ lemma timeContract_insert_some_of_lt
     simp only [exchangeSign_mul_self]
     · exact ht
 
+/-! 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
+  `(φ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
     (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
     (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (k : φsΛ.uncontracted)

HepLean/PerturbationTheory/WickContraction/Uncontracted.lean

@@ -16,7 +16,8 @@ namespace WickContraction
 variable {n : ℕ} (c : WickContraction n)
 open HepLean.List
 
-/-- Given a Wick contraction, the finset of elements of `Fin n` which are not contracted. -/
+/-- For a Wick contraction `c`, `c.uncontracted` is defined as the finset of elements of `Fin n`
+  which are not in any contracted pair. -/
 def uncontracted : Finset (Fin n) := Finset.filter (fun i => c.getDual? i = none) (Finset.univ)
 
 lemma congr_uncontracted {n m : ℕ} (c : WickContraction n) (h : n = m) :

HepLean/PerturbationTheory/WickContraction/UncontractedList.lean

@@ -314,8 +314,11 @@ lemma take_uncontractedIndexEquiv_symm (k : c.uncontracted) :
 
 -/
 
-/-- Given a Wick Contraction `φsΛ` for a list of states `φs`. The list of uncontracted
-  states in `φs`. -/
+/-- Given a Wick Contraction `φsΛ` of a list `φs` of `𝓕.FieldOp`. The list
+  `φsΛ.uncontractedListGet` of `𝓕.FieldOp` is defined as the list `φs` with
+  all contracted positions removed, leaving the uncontracted `𝓕.FieldOp`.
+
+  The notation `[φsΛ]ᵘᶜ` is used for `φsΛ.uncontractedListGet`. -/
 def uncontractedListGet {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) :
     List 𝓕.FieldOp := φsΛ.uncontractedList.map φs.get
 

scripts/MetaPrograms/notes.lean

@@ -131,8 +131,6 @@ def perturbationTheory : Note where
   title := "Proof of Wick's theorem"
   curators := ["Joseph Tooby-Smith"]
   parts := [
-    .warning "This note is a work in progress and is not finished. Use with caution.
-      (5th Feb 2025)",
     .h1 "Introduction",
     .name `FieldSpecification.wicks_theorem_context .incomplete,
     .p "In this note we walk through the important parts of the proof of Wick's theorem
@@ -185,6 +183,7 @@ def perturbationTheory : Note where
     .name ``FieldSpecification.FieldOpFreeAlgebra.timeOrderF .complete,
     .name ``FieldSpecification.FieldOpAlgebra.timeOrder .complete,
     .name ``FieldSpecification.FieldOpAlgebra.timeOrder_eq_maxTimeField_mul_finset .complete,
+    .name ``FieldSpecification.FieldOpAlgebra.timeOrder_timeOrder_mid .complete,
     .h1 "Normal ordering",
     .name ``FieldSpecification.normalOrderRel .complete,
     .name ``FieldSpecification.normalOrderList .complete,
@@ -192,56 +191,74 @@ def perturbationTheory : Note where
     .name ``FieldSpecification.normalOrderSign_eraseIdx .complete,
     .name ``FieldSpecification.FieldOpFreeAlgebra.normalOrderF .complete,
     .name ``FieldSpecification.FieldOpAlgebra.normalOrder .complete,
+    .name ``FieldSpecification.FieldOpAlgebra.normalOrder_superCommute_eq_zero .complete,
     .name ``FieldSpecification.FieldOpAlgebra.ofCrAnOp_superCommute_normalOrder_ofCrAnList_sum .complete,
     .name ``FieldSpecification.FieldOpAlgebra.ofFieldOp_mul_normalOrder_ofFieldOpList_eq_sum .complete,
     .h1 "Wick Contractions",
     .h2 "Definition",
-    .name ``WickContraction .incomplete,
-    .name ``WickContraction.GradingCompliant .incomplete,
+    .name ``WickContraction .complete,
+    .name `WickContraction.contraction_notation .complete,
+    .name ``WickContraction.GradingCompliant .complete,
     .h2 "Aside: Cardinality",
-    .name ``WickContraction.card_eq_cardFun .incomplete,
+    .name ``WickContraction.card_eq_cardFun .complete,
+    .h2 "Uncontracted elements",
+    .name ``WickContraction.uncontracted .complete,
+    .name ``WickContraction.uncontractedListGet .complete,
     .h2 "Constructors",
-    .p "There are a number of ways to construct a Wick contraction from
-      other Wick contractions or single contractions.",
-    .name ``WickContraction.insertAndContract .incomplete,
-    .name ``WickContraction.join .incomplete,
+    .name ``WickContraction.insertAndContract .complete,
+    .name ``WickContraction.insertLift_sum .complete,
+    .name ``WickContraction.join .complete,
     .h2 "Sign",
-    .name ``WickContraction.sign .incomplete,
-    .name ``WickContraction.join_sign .incomplete,
-    .name ``WickContraction.sign_insert_none .incomplete,
-    .name ``WickContraction.sign_insert_none_zero .incomplete,
-    .name ``WickContraction.sign_insert_some_of_not_lt .incomplete,
-    .name ``WickContraction.sign_insert_some_of_lt .incomplete,
-    .name ``WickContraction.sign_insert_some_zero .incomplete,
+    .name ``WickContraction.sign .complete,
+    .name ``WickContraction.join_sign .complete,
+    .name ``WickContraction.sign_insert_none .complete,
+    .name ``WickContraction.sign_insert_none_zero .complete,
+    .name ``WickContraction.sign_insert_some_of_not_lt .complete,
+    .name ``WickContraction.sign_insert_some_of_lt .complete,
+    .name ``WickContraction.sign_insert_some_zero .complete,
     .h2 "Normal order",
-    .name ``FieldSpecification.FieldOpAlgebra.normalOrder_uncontracted_none .incomplete,
-    .name ``FieldSpecification.FieldOpAlgebra.normalOrder_uncontracted_some .incomplete,
-    .h1 "Static contractions",
-    .name ``WickContraction.staticContract .incomplete,
-    .name ``WickContraction.staticContract_insert_some_of_lt .incomplete,
-    .name ``WickContraction.staticContract_insert_none .incomplete,
-    .h1 "Time contractions",
-    .name ``FieldSpecification.FieldOpAlgebra.timeContract .incomplete,
-    .name ``WickContraction.timeContract .incomplete,
-    .name ``WickContraction.timeContract_insert_none .incomplete,
-    .name ``WickContraction.timeContract_insert_some_of_not_lt .incomplete,
-    .name ``WickContraction.timeContract_insert_some_of_lt .incomplete,
-    .h1 "Wick terms",
-    .name ``WickContraction.wickTerm .incomplete,
-    .name ``WickContraction.wickTerm_empty_nil .incomplete,
-    .name ``WickContraction.wickTerm_insert_none .incomplete,
-    .name ``WickContraction.wickTerm_insert_some .incomplete,
-    .name ``WickContraction.mul_wickTerm_eq_sum .incomplete,
-    .h1 "Static wick terms",
-    .name ``WickContraction.staticWickTerm .incomplete,
-    .name ``WickContraction.staticWickTerm_empty_nil .incomplete,
-    .name ``WickContraction.staticWickTerm_insert_zero_none .incomplete,
-    .name ``WickContraction.staticWickTerm_insert_zero_some .incomplete,
-    .name ``WickContraction.mul_staticWickTerm_eq_sum .incomplete,
-    .h1 "The three Wick's theorems",
-    .name ``FieldSpecification.wicks_theorem .incomplete,
-    .name ``FieldSpecification.FieldOpAlgebra.static_wick_theorem .incomplete,
-    .name ``FieldSpecification.FieldOpAlgebra.wicks_theorem_normal_order .incomplete
+    .name ``FieldSpecification.FieldOpAlgebra.normalOrder_uncontracted_none .complete,
+    .name ``FieldSpecification.FieldOpAlgebra.normalOrder_uncontracted_some .complete,
+    .h1 "Static Wicks theorem",
+    .h2 "Static contractions",
+    .name ``WickContraction.staticContract .complete,
+    .name ``WickContraction.staticContract_insert_none .complete,
+    .name ``WickContraction.staticContract_insert_some .complete,
+    .h2 "Static wick terms",
+    .name ``WickContraction.staticWickTerm .complete,
+    .name ``WickContraction.staticWickTerm_empty_nil .complete,
+    .name ``WickContraction.staticWickTerm_insert_zero_none .complete,
+    .name ``WickContraction.staticWickTerm_insert_zero_some .complete,
+    .name ``WickContraction.mul_staticWickTerm_eq_sum .complete,
+    .h2 "The Static Wicks theorem",
+    .name ``FieldSpecification.FieldOpAlgebra.static_wick_theorem .complete,
+    .h1 "Wick's theorem",
+    .h2 "Time contractions",
+    .name ``FieldSpecification.FieldOpAlgebra.timeContract .complete,
+    .name ``FieldSpecification.FieldOpAlgebra.timeContract_of_timeOrderRel .complete,
+    .name ``FieldSpecification.FieldOpAlgebra.timeContract_of_not_timeOrderRel_expand .complete,
+    .name ``FieldSpecification.FieldOpAlgebra.timeContract_mem_center .complete,
+    .name ``WickContraction.timeContract .complete,
+    .name ``WickContraction.timeContract_insert_none .complete,
+    .name ``WickContraction.timeContract_insert_some_of_not_lt .complete,
+    .name ``WickContraction.timeContract_insert_some_of_lt .complete,
+    .name ``WickContraction.join_sign_timeContract .complete,
+    .h2 "Wick terms",
+    .name ``WickContraction.wickTerm .complete,
+    .name ``WickContraction.wickTerm_empty_nil .complete,
+    .name ``WickContraction.wickTerm_insert_none .complete,
+    .name ``WickContraction.wickTerm_insert_some .complete,
+    .name ``WickContraction.mul_wickTerm_eq_sum .complete,
+    .h2 "Wick's theorem",
+    .name ``FieldSpecification.wicks_theorem .complete,
+    .h1 "Normal-ordered Wick's theorem",
+    .name ``WickContraction.EqTimeOnly.timeOrder_staticContract_of_not_mem .complete,
+    .name ``WickContraction.EqTimeOnly.staticContract_eq_timeContract_of_eqTimeOnly .complete,
+    .name ``WickContraction.EqTimeOnly.timeOrder_timeContract_mul_of_eqTimeOnly_left .complete,
+    .name ``FieldSpecification.FieldOpAlgebra.timeOrder_ofFieldOpList_eqTimeOnly .complete,
+    .name ``FieldSpecification.FieldOpAlgebra.normalOrder_timeOrder_ofFieldOpList_eq_eqTimeOnly_empty .complete,
+    .name ``FieldSpecification.FieldOpAlgebra.timeOrder_haveEqTime_split .complete,
+    .name ``FieldSpecification.FieldOpAlgebra.wicks_theorem_normal_order .complete
     ]
 
 unsafe def main (_ : List String) : IO UInt32 := do