refactor: Note

HepLean/PerturbationTheory/FieldOpAlgebra/WicksTheorem.lean

@@ -342,11 +342,19 @@ lemma wicks_theorem_congr {φs φs' : List 𝓕.FieldOp} (h : φs = φs') :
   simp
 
 remark wicks_theorem_context := "
-  Wick's theorem is one of the most important results in perturbative quantum field theory.
-  It expresses a time-ordered product of fields as a sum of terms consisting of
-  time-contractions of pairs of fields multiplied by the normal-ordered product of
-  the remaining fields. Wick's theorem is also the precursor to the diagrammatic
-  approach to quantum field theory called Feynman diagrams."
+  In perturbation 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.
+  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.
+
+  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 for time-ordered products of bosonic and fermionic fields.
   The time ordered product `T(φ₀φ₁…φₙ)` is equal to the sum of terms,

HepLean/PerturbationTheory/FieldOpFreeAlgebra/Basic.lean

@@ -35,7 +35,7 @@ namespace FieldSpecification
 variable {𝓕 : FieldSpecification}
 
 /-- For a field specification `𝓕`, the algebra `𝓕.FieldOpFreeAlgebra` is
-  the algebra generated by creation and annihilation parts of field operators defined in
+  the free algebra generated by creation and annihilation parts of field operators defined in
   `𝓕.CrAnFieldOp`.
   It represents the algebra containing all possible products and linear combinations
   of creation and annihilation parts of field operators, without imposing any conditions.
@@ -44,6 +44,12 @@ abbrev FieldOpFreeAlgebra (𝓕 : FieldSpecification) : Type := FreeAlgebra ℂ
 
 namespace FieldOpFreeAlgebra
 
+remark naming_convention := "
+  For mathematicial objects defined in relation to `FieldOpFreeAlgebra` we will often postfix
+  their names with an `F` to indicate that they are related to the free algebra.
+  This is to avoid confusion when working within the context of `FieldOpAlgebra` which is defined
+  as a quotient of `FieldOpFreeAlgebra`."
+
 /-- Maps a creation and annihlation state to the creation and annihlation free-algebra. -/
 def ofCrAnOpF (φ : 𝓕.CrAnFieldOp) : FieldOpFreeAlgebra 𝓕 :=
   FreeAlgebra.ι ℂ φ

HepLean/PerturbationTheory/FieldStatistics/Basic.lean

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

HepLean/PerturbationTheory/WickContraction/Card.lean

@@ -236,6 +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. -/
 theorem card_eq_cardFun : (n : ℕ) → Fintype.card (WickContraction n) = cardFun n
   | 0 => by decide
   | 1 => by decide

scripts/MetaPrograms/notes.lean

@@ -125,28 +125,18 @@ def perturbationTheory : Note where
       as it appears in HepLean. We start with some basic definitions.",
     .h1 "Field operators",
     .h2 "Field statistics",
-    .p "A quantum field can either be a bosonic or fermionic. This information is
-      contained in the inductive type `FieldStatistic`. This is defined as follows:",
     .name `FieldStatistic,
-    .p "Field statistics form a commuative group isomorphic to ℤ₂, with
-      the bosonic element of `FieldStatistic` being the identity element.",
-    .p "Most of our use of field statistics will come by comparing two field statistics
-      and picking up a minus sign when they are both fermionic. This concept is
-      made precise using the notion of an exchange sign, defined as:",
+    .name `FieldStatistic.instCommGroup,
     .name `FieldStatistic.exchangeSign,
-    .p "We use the notation `𝓢(a,b)` as shorthand for the exchange sign of `a` and `b`.",
     .h2 "Field specifications",
     .name `fieldSpecification_intro,
     .name `FieldSpecification,
-    .p "Some examples of `FieldSpecification`s are given below:",
-    .name `FieldSpecification.singleBoson,
-    .name `FieldSpecification.singleFermion,
-    .name `FieldSpecification.doubleBosonDoubleFermion,
     .h2 "Field operators",
     .name `FieldSpecification.FieldOp,
     .name `FieldSpecification.CrAnFieldOp,
     .h2 "Field-operator free algebra",
     .name `FieldSpecification.FieldOpFreeAlgebra,
+    .name `FieldSpecification.FieldOpFreeAlgebra.naming_convention,
     .name `FieldSpecification.FieldOpFreeAlgebra.superCommuteF,
     .h2 "Field-operator algebra",
     .name `FieldSpecification.FieldOpAlgebra,