docs: Field specification docs

HepLean/PerturbationTheory/CreateAnnihilate.lean

@@ -10,7 +10,9 @@ import Mathlib.Algebra.BigOperators.Group.Finset
 
 -/
 
-/-- The type specifing whether an operator is a creation or annihilation operator. -/
+/-- The type `CreateAnnihilate` is the type containing two elements `create` and `annihilate`.
+  This type is used to specify if an operator is a creation or annihilation operator
+  or the sum thereof or intergral thereover etc. -/
 inductive CreateAnnihilate where
   | create : CreateAnnihilate
   | annihilate : CreateAnnihilate

HepLean/PerturbationTheory/FieldOpAlgebra/Basic.lean

@@ -512,18 +512,18 @@ def anPart (φ : 𝓕.FieldOp) : 𝓕.FieldOpAlgebra := ι (anPartF φ)
 lemma anPart_eq_ι_anPartF (φ : 𝓕.FieldOp) : anPart φ = ι (anPartF φ) := rfl
 
 @[simp]
-lemma anPart_negAsymp (φ : 𝓕.asymptoticDOF × (Fin 3 → ℝ)) :
+lemma anPart_negAsymp (φ : (Σ f, 𝓕.AsymptoticLabel f) × (Fin 3 → ℝ)) :
     anPart (FieldOp.inAsymp φ) = 0 := by
   simp [anPart, anPartF]
 
 @[simp]
-lemma anPart_position (φ : 𝓕.positionDOF × SpaceTime) :
+lemma anPart_position (φ : (Σ f, 𝓕.PositionLabel f) × SpaceTime) :
     anPart (FieldOp.position φ) =
     ofCrAnFieldOp ⟨FieldOp.position φ, CreateAnnihilate.annihilate⟩ := by
   simp [anPart, ofCrAnFieldOp]
 
 @[simp]
-lemma anPart_posAsymp (φ : 𝓕.asymptoticDOF × (Fin 3 → ℝ)) :
+lemma anPart_posAsymp (φ : (Σ f, 𝓕.AsymptoticLabel f) × (Fin 3 → ℝ)) :
     anPart (FieldOp.outAsymp φ) = ofCrAnFieldOp ⟨FieldOp.outAsymp φ, ()⟩ := by
   simp [anPart, ofCrAnFieldOp]
 
@@ -533,18 +533,18 @@ def crPart (φ : 𝓕.FieldOp) : 𝓕.FieldOpAlgebra := ι (crPartF φ)
 lemma crPart_eq_ι_crPartF (φ : 𝓕.FieldOp) : crPart φ = ι (crPartF φ) := rfl
 
 @[simp]
-lemma crPart_negAsymp (φ : 𝓕.asymptoticDOF × (Fin 3 → ℝ)) :
+lemma crPart_negAsymp (φ : (Σ f, 𝓕.AsymptoticLabel f) × (Fin 3 → ℝ)) :
     crPart (FieldOp.inAsymp φ) = ofCrAnFieldOp ⟨FieldOp.inAsymp φ, ()⟩ := by
   simp [crPart, ofCrAnFieldOp]
 
 @[simp]
-lemma crPart_position (φ : 𝓕.positionDOF × SpaceTime) :
+lemma crPart_position (φ : (Σ f, 𝓕.PositionLabel f) × SpaceTime) :
     crPart (FieldOp.position φ) =
     ofCrAnFieldOp ⟨FieldOp.position φ, CreateAnnihilate.create⟩ := by
   simp [crPart, ofCrAnFieldOp]
 
 @[simp]
-lemma crPart_posAsymp (φ : 𝓕.asymptoticDOF × (Fin 3 → ℝ)) :
+lemma crPart_posAsymp (φ : (Σ f, 𝓕.AsymptoticLabel f) × (Fin 3 → ℝ)) :
     crPart (FieldOp.outAsymp φ) = 0 := by
   simp [crPart]
 

HepLean/PerturbationTheory/FieldOpFreeAlgebra/Basic.lean

@@ -131,18 +131,18 @@ def crPartF : 𝓕.FieldOp → 𝓕.FieldOpFreeAlgebra := fun φ =>
   | FieldOp.outAsymp _ => 0
 
 @[simp]
-lemma crPartF_negAsymp (φ : 𝓕.asymptoticDOF × (Fin 3 → ℝ)) :
+lemma crPartF_negAsymp (φ : (Σ f, 𝓕.AsymptoticLabel f) × (Fin 3 → ℝ)) :
     crPartF (FieldOp.inAsymp φ) = ofCrAnOpF ⟨FieldOp.inAsymp φ, ()⟩ := by
   simp [crPartF]
 
 @[simp]
-lemma crPartF_position (φ : 𝓕.positionDOF × SpaceTime) :
+lemma crPartF_position (φ : (Σ f, 𝓕.PositionLabel f) × SpaceTime) :
     crPartF (FieldOp.position φ) =
     ofCrAnOpF ⟨FieldOp.position φ, CreateAnnihilate.create⟩ := by
   simp [crPartF]
 
 @[simp]
-lemma crPartF_posAsymp (φ : 𝓕.asymptoticDOF × (Fin 3 → ℝ)) :
+lemma crPartF_posAsymp (φ : (Σ f, 𝓕.AsymptoticLabel f) × (Fin 3 → ℝ)) :
     crPartF (FieldOp.outAsymp φ) = 0 := by
   simp [crPartF]
 
@@ -156,18 +156,18 @@ def anPartF : 𝓕.FieldOp → 𝓕.FieldOpFreeAlgebra := fun φ =>
   | FieldOp.outAsymp φ => ofCrAnOpF ⟨FieldOp.outAsymp φ, ()⟩
 
 @[simp]
-lemma anPartF_negAsymp (φ : 𝓕.asymptoticDOF × (Fin 3 → ℝ)) :
+lemma anPartF_negAsymp (φ : (Σ f, 𝓕.AsymptoticLabel f) × (Fin 3 → ℝ)) :
     anPartF (FieldOp.inAsymp φ) = 0 := by
   simp [anPartF]
 
 @[simp]
-lemma anPartF_position (φ : 𝓕.positionDOF × SpaceTime) :
+lemma anPartF_position (φ : (Σ f, 𝓕.PositionLabel f) × SpaceTime) :
     anPartF (FieldOp.position φ) =
     ofCrAnOpF ⟨FieldOp.position φ, CreateAnnihilate.annihilate⟩ := by
   simp [anPartF]
 
 @[simp]
-lemma anPartF_posAsymp (φ : 𝓕.asymptoticDOF × (Fin 3 → ℝ)) :
+lemma anPartF_posAsymp (φ : (Σ f, 𝓕.AsymptoticLabel f) × (Fin 3 → ℝ)) :
     anPartF (FieldOp.outAsymp φ) = ofCrAnOpF ⟨FieldOp.outAsymp φ, ()⟩ := by
   simp [anPartF]
 

HepLean/PerturbationTheory/FieldSpecification/Basic.lean

@@ -29,50 +29,63 @@ These states carry the same field statistic as the field they are derived from.
 
 -/
 
-/-- A field specification is defined as a structure containing the basic data needed to write down
+/--
-  position and asymptotic field operators for a theory. It contains:
+The structure `FieldSpecification` is defined to have the following content:
-  - A type `positionDOF` containing the degree-of-freedom in position-based field
+  - A type `Field` whose elements are the constituent fields of the theory.
-  operators (excluding space-time position). Thus a sutible (but not unique) choice
+  - For every field `f` in `Field`, a type `PositionLabel f` whose elements label the different
-    - Real-scalar fields correspond to a single element of `positionDOF`.
+    position operators associated with the field `f`. For example,
-    - Complex-scalar fields correspond to two elements of `positionDOF`, one for the field and one
+    - For `f` a *real-scalar field*, `PositionLabel f` will have a unique element.
-      for its conjugate.
+    - For `f` a *complex-scalar field*, `PositionLabel f` will have two elements, one for the field
-    - Dirac fermions correspond to eight elements of `positionDOF`. One for each Lorentz index of
+      operator and one for its conjugate.
-      the field and its conjugate. (These are not all independent)
+    - For `f` a *Dirac fermion*, `PositionLabel f` will have eight elements, one for each Lorentz
-    - Weyl fermions correspond to four elements of `positionDOF`. One for each Lorentz index of the
+      index of the field and its conjugate.
-      field. (These are not all independent)
+    - For `f` a *Weyl fermion*, `PositionLabel f` will have four elements, one for each Lorentz
-  - A type `asymptoticDOF` containing the degree-of-freedom in asymptotic field operators. Thus a
+      index of the field and its conjugate.
-    sutible (but not unique) choice is
+  - For every field `f` in `Field`, a type `AsymptoticLabel f` whose elements label the different
-    - Real-scalar fields correspond to a single element of `asymptoticDOF`.
+    asymptotic based field operators associated with the field `f`. For example,
-    - Complex-scalar fields correspond to two elements of `asymptoticDOF`, one for the field and one
+    - For `f` a *real-scalar field*, `AsymptoticLabel f` will have a unique element.
-      for its conjugate.
+    - For `f` a *complex-scalar field*, `AsymptoticLabel f` will have two elements, one for the
-    - Dirac fermions correspond to four elements of `asymptoticDOF`, two for each type of spin.
+      field operator and one for its conjugate.
-    - Weyl fermions correspond to two elements of `asymptoticDOF`, one for each spin.
+    - For `f` a *Dirac fermion*, `AsymptoticLabel f` will have four elements, two for each spin.
-  - A specification `statisticsPos` on a `positionDOF` is Fermionic or Bosonic.
+    - For `f` a *Weyl fermion*, `AsymptoticLabel f` will have two elements, one for each spin.
-  - A specification `statisticsAsym` on a `asymptoticDOF` is Fermionic or Bosonic.
+  - For each field `f` in `Field`, a field statistic `statistic f` which classifying `f` as either
+    `bosonic` or `fermionic`.
 -/
 structure FieldSpecification where
-  /-- Degrees of freedom for position based field operators. -/
+  /-- A type whose elements are the constituent fields of the theory. -/
-  positionDOF : Type
+  Field : Type
-  /-- Degrees of freedom for asymptotic based field operators. -/
+  /-- For every field `f` in `Field`, the type `PositionLabel f` has elements that label the
-  asymptoticDOF : Type
+    different position operators associated with the field `f`. -/
-  /-- The specification if the `positionDOF` are Fermionic or Bosonic. -/
+  PositionLabel : Field → Type
-  statisticsPos : positionDOF → FieldStatistic
+  /-- For every field `f` in `Field`, the type `AsymptoticLabel f` has elements that label
-  /-- The specification if the `asymptoticDOF` are Fermionic or Bosonic. -/
+    the different asymptotic based field operators associated with the field `f`. -/
-  statisticsAsym : asymptoticDOF → FieldStatistic
+  AsymptoticLabel : Field → Type
+  /-- For every field `f` in `Field`, the field statistic `statistic f` classifies `f` as either
+    `bosonic` or `fermionic`. -/
+  statistic : Field → FieldStatistic
 
 namespace FieldSpecification
 variable (𝓕 : FieldSpecification)
 
 /-- For a field specification `𝓕`, the type `𝓕.FieldOp` is defined such that every element of
   `FieldOp` corresponds either to:
-- an incoming asymptotic field operator `.inAsymp` specified by a field and a `3`-momentum.
+- an incoming asymptotic field operator `.inAsymp` which is specified by
-- an position operator `.position` specified by a field and a point in spacetime.
+  a field `f` in `𝓕.Field`, an element of `AsymptoticLabel f` (which specifies exactly
-- an outgoing asymptotic field operator `.outAsymp` specified by a field and a `3`-momentum.
+  which asymptotic field operator associated with `f`) and a `3`-momentum.
+- an position operator `.position` which is specified by
+  a field `f` in `𝓕.Field`, an element of `PositionLabel f` (which specifies exactly
+  which position field operator associated with `f`) and a element of `SpaceTime`.
+- an outgoing asymptotic field operator `.outAsymp` which is specified by
+  a field `f` in `𝓕.Field`, an element of `AsymptoticLabel f` (which specifies exactly
+  which asymptotic field operator associated with `f`) and a `3`-momentum.
+
+Note the use of `3`-momentum here rather then `4`-momentum. This is because the asymptotic states
+have on-shell momenta.
 -/
 inductive FieldOp (𝓕 : FieldSpecification) where
-  | inAsymp : 𝓕.asymptoticDOF × (Fin 3 → ℝ) → 𝓕.FieldOp
+  | inAsymp : (Σ f, 𝓕.AsymptoticLabel f) × (Fin 3 → ℝ) → 𝓕.FieldOp
-  | position : 𝓕.positionDOF × SpaceTime → 𝓕.FieldOp
+  | position : (Σ f, 𝓕.PositionLabel f) × SpaceTime → 𝓕.FieldOp
-  | outAsymp : 𝓕.asymptoticDOF × (Fin 3 → ℝ) → 𝓕.FieldOp
+  | outAsymp : (Σ f, 𝓕.AsymptoticLabel f) × (Fin 3 → ℝ) → 𝓕.FieldOp
 
 
 /-- The bool on `FieldOp` which is true only for position field operator. -/
@@ -80,22 +93,34 @@ def statesIsPosition : 𝓕.FieldOp → Bool
   | FieldOp.position _ => true
   | _ => false
 
-/-- The statistics associated to a field operator. -/
+/-- For a field specification `𝓕`, `𝓕.fieldOpToField` is defined to take field operators
-def statesStatistic : 𝓕.FieldOp → FieldStatistic := fun f =>
+  to their underlying field. -/
-  match f with
+def fieldOpToField : 𝓕.FieldOp → 𝓕.Field
-  | FieldOp.inAsymp (a, _) => 𝓕.statisticsAsym a
+  | FieldOp.inAsymp (f, _) => f.1
-  | FieldOp.position (a, _) => 𝓕.statisticsPos a
+  | FieldOp.position (f, _) => f.1
-  | FieldOp.outAsymp (a, _) => 𝓕.statisticsAsym a
+  | FieldOp.outAsymp (f, _) => f.1
 
-/-- The field statistics associated with a field operator. -/
+/-- For a field specification `𝓕`, and an element `φ` of `𝓕.FieldOp`.
-scoped[FieldSpecification] notation 𝓕 "|>ₛ" φ => statesStatistic 𝓕 φ
+  The field statistic `fieldOpStatistic φ` is defined to be the statistic associated with
+  the field underlying `φ`.
 
-/-- The field statistics associated with a list field operators. -/
+  The following notation is used in relation to `fieldOpStatistic`:
+- For `φ` an element of  `𝓕.FieldOp`, `𝓕 |>ₛ φ` is `fieldOpStatistic φ`.
+- For `φs` a list of  `𝓕.FieldOp`, `𝓕 |>ₛ φs` is the product of `fieldOpStatistic φ` over
+  the list `φs`.
+- For a function `f : Fin n → 𝓕.FieldOp`  and a finset `a` of `Fin n`, `𝓕 |>ₛ ⟨f, a⟩` is the
+  product of `fieldOpStatistic (f i)` for all `i ∈ a`. -/
+def fieldOpStatistic : 𝓕.FieldOp → FieldStatistic :=  𝓕.statistic ∘ 𝓕.fieldOpToField
+
+@[inherit_doc fieldOpStatistic]
+scoped[FieldSpecification] notation 𝓕 "|>ₛ" φ => fieldOpStatistic 𝓕 φ
+
+@[inherit_doc fieldOpStatistic]
 scoped[FieldSpecification] notation 𝓕 "|>ₛ" φ => FieldStatistic.ofList
-    (statesStatistic 𝓕) φ
+    (fieldOpStatistic 𝓕) φ
 
-/-- The field statistic associated with a finite set-/
+@[inherit_doc fieldOpStatistic]
 scoped[FieldSpecification] notation 𝓕 "|>ₛ" "⟨" f ","a "⟩"=> FieldStatistic.ofFinset
-    (statesStatistic 𝓕) f a
+    (fieldOpStatistic 𝓕) f a
 
 end FieldSpecification

HepLean/PerturbationTheory/FieldSpecification/CrAnFieldOp.lean

@@ -63,14 +63,15 @@ def fieldOpToCreateAnnihilateTypeCongr : {i j : 𝓕.FieldOp} → i = j →
   | _, _, rfl => Equiv.refl _
 
 /--
-For a field specification `𝓕`, the type `𝓕.CrAnFieldOp` is defined such that every element
+For a field specification `𝓕`, elements in `𝓕.CrAnFieldOp`, the type
-corresponds to
+of creation and annihilation field operators, corresponds to
-- an incoming asymptotic field operator `.inAsymp` and the unique element of `Unit`,
+- an incoming asymptotic field operator `.inAsymp` in `𝓕.FieldOp`.
-  corresponding to the statement that an `inAsymp` state is a creation operator.
+- a position operator `.position` in `𝓕.FieldOp` and an element of
-- a position operator `.position` and an element of `CreateAnnihilate`,
+  `CreateAnnihilate` specifying the creation or annihilation part of that position operator.
-  corresponding to either the creation part or the annihilation part of a position operator.
+- an outgoing asymptotic field operator `.outAsymp` in `𝓕.FieldOp`.
-- an outgoing asymptotic field operator `.outAsymp` and the unique element of `Unit`,
+
-  corresponding to the statement that an `outAsymp` state is an annihilation operator.
+Note that the incoming and outgoing asymptotic field operators are implicitly creation and
+annihilation operators respectively.
 -/
 def CrAnFieldOp : Type := Σ (s : 𝓕.FieldOp), 𝓕.fieldOpToCrAnType s
 
@@ -89,15 +90,23 @@ def crAnFieldOpToCreateAnnihilate : 𝓕.CrAnFieldOp → CreateAnnihilate
   | ⟨FieldOp.position _, CreateAnnihilate.annihilate⟩ => CreateAnnihilate.annihilate
   | ⟨FieldOp.outAsymp _, _⟩ => CreateAnnihilate.annihilate
 
-/-- Takes a `CrAnFieldOp` state to its corresponding fields statistic (bosonic or fermionic). -/
+/-- For a field specification `𝓕`, and an element `φ` in `𝓕.CrAnFieldOp`, the field
-def crAnStatistics : 𝓕.CrAnFieldOp → FieldStatistic :=
+  statistic `crAnStatistics φ` is defined to be the statistic associated with the field `𝓕.Field`
-  𝓕.statesStatistic ∘ 𝓕.crAnFieldOpToFieldOp
+  (or equivalently `𝓕.FieldOp`) underlying `φ`.
 
-/-- The field statistic of a `CrAnFieldOp`. -/
+  The following notation is used in relation to `crAnStatistics`:
+  - For `φ` an element of  `𝓕.CrAnFieldOp`, `𝓕 |>ₛ φ` is `crAnStatistics φ`.
+  - For `φs` a list of  `𝓕.CrAnFieldOp`, `𝓕 |>ₛ φs` is the product of `crAnStatistics φ` over
+    the list `φs`.
+-/
+def crAnStatistics : 𝓕.CrAnFieldOp → FieldStatistic :=
+  𝓕.fieldOpStatistic ∘ 𝓕.crAnFieldOpToFieldOp
+
+@[inherit_doc crAnStatistics]
 scoped[FieldSpecification] notation 𝓕 "|>ₛ" φ =>
     (crAnStatistics 𝓕) φ
 
-/-- The field statistic of a list of `CrAnFieldOp`s. -/
+@[inherit_doc crAnStatistics]
 scoped[FieldSpecification] notation 𝓕 "|>ₛ" φ => FieldStatistic.ofList
     (crAnStatistics 𝓕) φ
 
@@ -108,8 +117,14 @@ scoped[FieldSpecification] infixl:80 "|>ᶜ" =>
 
 remark notation_remark := "When working with a field specification `𝓕` we will use
 some notation within doc-strings and in code. The main notation used is:
-- In docstrings when field statistics occur in exchange signs we may drop the `𝓕 |>ₛ`.
+- In doc-strings when field statistics occur in exchange signs we may drop the `𝓕 |>ₛ _`.
-- In docstrings we will often write lists of `FieldOp` or `CrAnFieldOp` `φs` as e.g. `φ₀…φₙ`,
+- In doc-strings we will often write lists of `FieldOp` or `CrAnFieldOp` `φs` as e.g. `φ₀…φₙ`,
-  which should be interpreted within the context in which it appears."
+  which should be interpreted within the context in which it appears.
+
+Some examples:
+- `𝓢(φ, φs)` corresponds to  `𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ φs)`
+- `φ₀…φᵢ₋₁φᵢ₊₁…φₙ` corresponds to a (given) list `φs = φ₀…φₙ` with the element at the `i`th position
+  removed.
+"
 
 end FieldSpecification

HepLean/PerturbationTheory/FieldSpecification/TimeOrder.lean

@@ -126,7 +126,7 @@ lemma timeOrder_maxTimeField (φ : 𝓕.FieldOp) (φs : List 𝓕.FieldOp)
   the state of greatest time to the left).
   We pick up a minus sign for every fermion paired crossed. -/
 def timeOrderSign (φs : List 𝓕.FieldOp) : ℂ :=
-  Wick.koszulSign 𝓕.statesStatistic 𝓕.timeOrderRel φs
+  Wick.koszulSign 𝓕.fieldOpStatistic 𝓕.timeOrderRel φs
 
 @[simp]
 lemma timeOrderSign_nil : timeOrderSign (𝓕 := 𝓕) [] = 1 := by
@@ -354,7 +354,7 @@ lemma crAnTimeOrderList_swap_eq_time {φ ψ : 𝓕.CrAnFieldOp}
 lemma koszulSignInsert_crAnTimeOrderRel_crAnSection {φ : 𝓕.FieldOp} {ψ : 𝓕.CrAnFieldOp}
     (h : ψ.1 = φ) : {φs : List 𝓕.FieldOp} → (ψs : CrAnSection φs) →
     Wick.koszulSignInsert 𝓕.crAnStatistics 𝓕.crAnTimeOrderRel ψ ψs.1 =
-    Wick.koszulSignInsert 𝓕.statesStatistic 𝓕.timeOrderRel φ φs
+    Wick.koszulSignInsert 𝓕.fieldOpStatistic 𝓕.timeOrderRel φ φs
   | [], ⟨[], h⟩ => by
     simp [Wick.koszulSignInsert]
   | φ' :: φs, ⟨ψ' :: ψs, h1⟩ => by

HepLean/PerturbationTheory/FieldStatistics/Basic.lean

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

HepLean/PerturbationTheory/FieldStatistics/ExchangeSign.lean

@@ -24,11 +24,12 @@ namespace FieldStatistic
 
 variable {𝓕 : Type}
 
-/-- The exchange sign is the group homomorphism `FieldStatistic →* FieldStatistic →* ℂ`,
+/-- The exchange sign, `exchangeSign`, is defined as the group homomorphism
-  which on two field statistics `a` and `b` is defined to be
+  `FieldStatistic →* FieldStatistic →* ℂ`,
-  `-1` if both `a` and `b` are `fermionic` and `1` otherwise.
+  for which `exchangeSign a b` is `-1` if both `a` and `b` are `fermionic` and `1` otherwise.
-  It corresponds to the sign that one picks up when swapping fields `φ₁φ₂ → φ₂φ₁` with
+  The exchange sign is sign one picks up on exchanging an operator or field `φ₁` of statistic `a`
-  `φ₁` and `φ₂` of statistics `a` and `b` respectively.
+  with one `φ₂` of statistic `b`, i.e. `φ₁φ₂ → φ₂φ₁`.
+
   The notation `𝓢(a, b)` is used for the exchange sign of `a` and `b`. -/
 def exchangeSign : FieldStatistic →* FieldStatistic →* ℂ where
   toFun a :=

HepLean/PerturbationTheory/WickContraction/Sign/Join.lean

@@ -162,7 +162,7 @@ lemma join_singleton_left_signFinset_eq_filter {φs : List 𝓕.FieldOp}
     left
     rw [join_singleton_signFinset_eq_filter]
   rw [mul_comm]
-  exact (ofFinset_filter_mul_neg 𝓕.statesStatistic _ _ _).symm
+  exact (ofFinset_filter_mul_neg 𝓕.fieldOpStatistic _ _ _).symm
 
 /-- The difference in sign between `φsucΛ.sign` and the direct contribution of `φsucΛ` to
   `(join (singleton h) φsucΛ)`. -/

HepLean/PerturbationTheory/WickContraction/StaticContract.lean

@@ -85,7 +85,7 @@ lemma staticContract_insert_some_of_lt
     · simp
     simp only [smul_smul]
     congr 1
-    have h1 : ofList 𝓕.statesStatistic (List.take (↑(φsΛ.uncontractedIndexEquiv.symm k))
+    have h1 : ofList 𝓕.fieldOpStatistic (List.take (↑(φsΛ.uncontractedIndexEquiv.symm k))
         (List.map φs.get φsΛ.uncontractedList))
         = (𝓕 |>ₛ ⟨φs.get, (Finset.filter (fun x => x < k) φsΛ.uncontracted)⟩) := by
       simp only [ofFinset]

HepLean/PerturbationTheory/WickContraction/TimeContract.lean

@@ -97,7 +97,7 @@ lemma timeContract_insert_some_of_lt
     · simp
     simp only [smul_smul]
     congr 1
-    have h1 : ofList 𝓕.statesStatistic (List.take (↑(φsΛ.uncontractedIndexEquiv.symm k))
+    have h1 : ofList 𝓕.fieldOpStatistic (List.take (↑(φsΛ.uncontractedIndexEquiv.symm k))
         (List.map φs.get φsΛ.uncontractedList))
         = (𝓕 |>ₛ ⟨φs.get, (Finset.filter (fun x => x < k) φsΛ.uncontracted)⟩) := by
       simp only [ofFinset]
@@ -128,7 +128,7 @@ lemma timeContract_insert_some_of_not_lt
   rw [timeContract_of_not_timeOrderRel, timeContract_of_timeOrderRel]
   simp only [instCommGroup.eq_1, Algebra.smul_mul_assoc, smul_smul]
   congr
-  have h1 : ofList 𝓕.statesStatistic (List.take (↑(φsΛ.uncontractedIndexEquiv.symm k))
+  have h1 : ofList 𝓕.fieldOpStatistic (List.take (↑(φsΛ.uncontractedIndexEquiv.symm k))
       (List.map φs.get φsΛ.uncontractedList))
       = (𝓕 |>ₛ ⟨φs.get, (Finset.filter (fun x => x < k) φsΛ.uncontracted)⟩) := by
     simp only [ofFinset]

docs/CuratedNotes/PerturbationTheory.html

@@ -65,7 +65,9 @@ layout: default
   {% if entry.type == "name" %}
 
   <div style="background-color: #f5f5f5; padding: 10px; border-radius: 4px;">
-    <p> <a href = "{{ entry.link }}" style="font-weight: bold; color: #2c5282;">{{ entry.name }}</a>: {{ entry.docString | markdownify}}</p>
+    <p> <a href = "{{ entry.link }}" style="font-weight: bold; color: #2c5282;">{{ entry.name }}</a>:
+      {% if entry.status == "incomplete" %}🚧{% endif %}
+      {{ entry.docString | markdownify}}</p>
     <details class="code-block-container">
     <summary>Show Lean code:</summary>
     <pre style="background: none; margin: 0;"><code class="language-lean">{{ entry.declString }}</code></pre>

scripts/MetaPrograms/notes.lean

@@ -7,6 +7,7 @@ import HepLean.Meta.Basic
 import HepLean.Meta.Remark.Properties
 import HepLean.Meta.Notes.ToHTML
 import Mathlib.Lean.CoreM
+import HepLean
 /-!
 
 # Extracting notes from Lean files
@@ -15,21 +16,31 @@ import Mathlib.Lean.CoreM
 
 open Lean System Meta HepLean
 
+inductive NameStatus
+  | complete : NameStatus
+  | incomplete : NameStatus
+
+instance : ToString NameStatus where
+  toString
+    | NameStatus.complete => "complete"
+    | NameStatus.incomplete => "incomplete"
+
 inductive NotePart
   | h1 : String → NotePart
   | h2 : String → NotePart
   | p : String → NotePart
-  | name : Name → NotePart
+  | name : Name → NameStatus → NotePart
   | warning : String → NotePart
 
 structure DeclInfo where
   line : Nat
   fileName : Name
   name : Name
+  status : NameStatus
   declString : String
   docString : String
 
-def DeclInfo.ofName (n : Name) : MetaM DeclInfo := do
+def DeclInfo.ofName (n : Name) (ns : NameStatus): MetaM DeclInfo := do
   let line ← Name.lineNumber n
   let fileName ← Name.fileName n
   let declString ← Name.getDeclString n
@@ -38,6 +49,7 @@ def DeclInfo.ofName (n : Name) : MetaM DeclInfo := do
     line := line,
     fileName := fileName,
     name := n,
+    status := ns,
     declString := declString,
     docString := docString}
 
@@ -50,6 +62,7 @@ def DeclInfo.toYML (d : DeclInfo) : MetaM String := do
     name: {d.name}
     line: {d.line}
     fileName: {d.fileName}
+    status: \"{d.status}\"
     link: \"{link}\"
     docString: |
       {docStringIndent}
@@ -79,7 +92,7 @@ def NotePart.toYMLM : ((List String) × Nat × Nat) →  NotePart → MetaM ((Li
   - type: warning
     content: \"{s}\""
     return ⟨x.1 ++ [newString], x.2⟩
-  | x, NotePart.name n => do
+  | x, NotePart.name n s => do
   match (← RemarkInfo.IsRemark n) with
   | true =>
     let remarkInfo ← RemarkInfo.getRemarkInfo n
@@ -89,12 +102,13 @@ def NotePart.toYMLM : ((List String) × Nat × Nat) →  NotePart → MetaM ((Li
     let newString := s!"
   - type: remark
     name: \"{shortName}\"
+    status : \"{s}\"
     link: \"{Name.toGitHubLink remarkInfo.fileName remarkInfo.line}\"
     content: |
       {contentIndent}"
     return ⟨x.1 ++ [newString], x.2⟩
   | false =>
-  let newString ← (← DeclInfo.ofName n).toYML
+  let newString ← (← DeclInfo.ofName n s).toYML
   return ⟨x.1 ++ [newString], x.2⟩
 
 structure Note where
@@ -120,104 +134,108 @@ def perturbationTheory : Note where
     .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,
+    .name `FieldSpecification.wicks_theorem_context .incomplete,
     .p "In this note we walk through the important parts of the proof of Wick's theorem
       for both fermions and bosons,
       as it appears in HepLean. We start with some basic definitions.",
     .h1 "Field operators",
     .h2 "Field statistics",
-    .name `FieldStatistic,
+    .name ``FieldStatistic .complete,
-    .name `FieldStatistic.instCommGroup,
+    .name ``FieldStatistic.instCommGroup .complete,
-    .name `FieldStatistic.exchangeSign,
+    .name ``FieldStatistic.exchangeSign .complete,
     .h2 "Field specifications",
-    .name `FieldSpecification,
+    .name ``FieldSpecification .complete,
     .h2 "Field operators",
-    .name `FieldSpecification.FieldOp,
+    .name ``FieldSpecification.FieldOp .complete,
-    .name `FieldSpecification.statesStatistic,
+    .name ``FieldSpecification.fieldOpStatistic .complete,
-    .name `FieldSpecification.CrAnFieldOp,
+    .name ``CreateAnnihilate .complete,
-    .name `FieldSpecification.crAnStatistics,
+    .name ``FieldSpecification.CrAnFieldOp .complete,
-    .name `FieldSpecification.notation_remark,
+    .name ``FieldSpecification.crAnStatistics .complete,
+    .name `FieldSpecification.notation_remark .complete,
     .h2 "Field-operator free algebra",
-    .name `FieldSpecification.FieldOpFreeAlgebra,
+    .name ``FieldSpecification.FieldOpFreeAlgebra .incomplete,
-    .name `FieldSpecification.FieldOpFreeAlgebra.naming_convention,
+    .name `FieldSpecification.FieldOpFreeAlgebra.naming_convention .incomplete,
-    .name `FieldSpecification.FieldOpFreeAlgebra.ofCrAnOpF,
+    .name ``FieldSpecification.FieldOpFreeAlgebra.ofCrAnOpF .incomplete,
-    .name `FieldSpecification.FieldOpFreeAlgebra.ofCrAnListF,
+    .name ``FieldSpecification.FieldOpFreeAlgebra.ofCrAnListF .incomplete,
-    .name `FieldSpecification.FieldOpFreeAlgebra.ofFieldOpF,
+    .name ``FieldSpecification.FieldOpFreeAlgebra.ofFieldOpF .incomplete,
-    .name `FieldSpecification.FieldOpFreeAlgebra.ofFieldOpListF,
+    .name ``FieldSpecification.FieldOpFreeAlgebra.ofFieldOpListF .incomplete,
-    .name `FieldSpecification.FieldOpFreeAlgebra.fieldOpFreeAlgebraGrade,
+    .name ``FieldSpecification.FieldOpFreeAlgebra.fieldOpFreeAlgebraGrade .incomplete,
-    .name `FieldSpecification.FieldOpFreeAlgebra.superCommuteF,
+    .name ``FieldSpecification.FieldOpFreeAlgebra.superCommuteF .incomplete,
-    .name `FieldSpecification.FieldOpFreeAlgebra.superCommuteF_ofCrAnListF_ofFieldOpListF_eq_sum,
+    .name ``FieldSpecification.FieldOpFreeAlgebra.superCommuteF_ofCrAnListF_ofFieldOpListF_eq_sum .incomplete,
     .h2 "Field-operator algebra",
-    .name `FieldSpecification.FieldOpAlgebra,
+    .name ``FieldSpecification.FieldOpAlgebra .incomplete,
-    .name `FieldSpecification.FieldOpAlgebra.ofCrAnFieldOp,
+    .name ``FieldSpecification.FieldOpAlgebra.ofCrAnFieldOp .incomplete,
-    .name `FieldSpecification.FieldOpAlgebra.ofCrAnFieldOpList,
+    .name ``FieldSpecification.FieldOpAlgebra.ofCrAnFieldOpList .incomplete,
-    .name `FieldSpecification.FieldOpAlgebra.ofFieldOp,
+    .name ``FieldSpecification.FieldOpAlgebra.ofFieldOp .incomplete,
-    .name `FieldSpecification.FieldOpAlgebra.ofCrAnFieldOpList,
+    .name ``FieldSpecification.FieldOpAlgebra.ofCrAnFieldOpList .incomplete,
-    .name `FieldSpecification.FieldOpAlgebra.fieldOpAlgebraGrade,
+    .name ``FieldSpecification.FieldOpAlgebra.anPart .incomplete,
-    .name `FieldSpecification.FieldOpAlgebra.superCommute,
+    .name ``FieldSpecification.FieldOpAlgebra.crPart .incomplete,
+    .name ``FieldSpecification.FieldOpAlgebra.ofFieldOp_eq_crPart_add_anPart .incomplete,
+    .name ``FieldSpecification.FieldOpAlgebra.fieldOpAlgebraGrade .incomplete,
+    .name ``FieldSpecification.FieldOpAlgebra.superCommute .incomplete,
     .h1 "Time ordering",
-    .name `FieldSpecification.crAnTimeOrderRel,
+    .name ``FieldSpecification.crAnTimeOrderRel .incomplete,
-    .name `FieldSpecification.crAnTimeOrderSign,
+    .name ``FieldSpecification.crAnTimeOrderSign .incomplete,
-    .name `FieldSpecification.FieldOpFreeAlgebra.timeOrderF,
+    .name ``FieldSpecification.FieldOpFreeAlgebra.timeOrderF .incomplete,
-    .name `FieldSpecification.FieldOpAlgebra.timeOrder,
+    .name ``FieldSpecification.FieldOpAlgebra.timeOrder .incomplete,
-    .name `FieldSpecification.FieldOpAlgebra.timeOrder_eq_maxTimeField_mul_finset,
+    .name ``FieldSpecification.FieldOpAlgebra.timeOrder_eq_maxTimeField_mul_finset .incomplete,
     .h1 "Normal ordering",
-    .name `FieldSpecification.normalOrderRel,
+    .name ``FieldSpecification.normalOrderRel .incomplete,
-    .name `FieldSpecification.normalOrderSign,
+    .name ``FieldSpecification.normalOrderSign .incomplete,
-    .name `FieldSpecification.FieldOpFreeAlgebra.normalOrderF,
+    .name ``FieldSpecification.FieldOpFreeAlgebra.normalOrderF .incomplete,
-    .name `FieldSpecification.FieldOpAlgebra.normalOrder,
+    .name ``FieldSpecification.FieldOpAlgebra.normalOrder .incomplete,
     .h2 "Some lemmas",
-    .name `FieldSpecification.normalOrderSign_eraseIdx,
+    .name ``FieldSpecification.normalOrderSign_eraseIdx .incomplete,
-    .name `FieldSpecification.FieldOpAlgebra.ofCrAnFieldOp_superCommute_normalOrder_ofCrAnFieldOpList_sum,
+    .name ``FieldSpecification.FieldOpAlgebra.ofCrAnFieldOp_superCommute_normalOrder_ofCrAnFieldOpList_sum .incomplete,
-    .name `FieldSpecification.FieldOpAlgebra.ofFieldOp_mul_normalOrder_ofFieldOpList_eq_sum,
+    .name ``FieldSpecification.FieldOpAlgebra.ofFieldOp_mul_normalOrder_ofFieldOpList_eq_sum .incomplete,
     .h1 "Wick Contractions",
     .h2 "Definition",
-    .name `WickContraction,
+    .name ``WickContraction .incomplete,
-    .name `WickContraction.GradingCompliant,
+    .name ``WickContraction.GradingCompliant .incomplete,
     .h2 "Aside: Cardinality",
-    .name `WickContraction.card_eq_cardFun,
+    .name ``WickContraction.card_eq_cardFun .incomplete,
     .h2 "Constructors",
     .p "There are a number of ways to construct a Wick contraction from
       other Wick contractions or single contractions.",
-    .name `WickContraction.insertAndContract,
+    .name ``WickContraction.insertAndContract .incomplete,
-    .name `WickContraction.join,
+    .name ``WickContraction.join .incomplete,
     .h2 "Sign",
-    .name `WickContraction.sign,
+    .name ``WickContraction.sign .incomplete,
-    .name `WickContraction.join_sign,
+    .name ``WickContraction.join_sign .incomplete,
-    .name `WickContraction.sign_insert_none,
+    .name ``WickContraction.sign_insert_none .incomplete,
-    .name `WickContraction.sign_insert_none_zero,
+    .name ``WickContraction.sign_insert_none_zero .incomplete,
-    .name `WickContraction.sign_insert_some_of_not_lt,
+    .name ``WickContraction.sign_insert_some_of_not_lt .incomplete,
-    .name `WickContraction.sign_insert_some_of_lt,
+    .name ``WickContraction.sign_insert_some_of_lt .incomplete,
-    .name `WickContraction.sign_insert_some_zero,
+    .name ``WickContraction.sign_insert_some_zero .incomplete,
     .h2 "Normal order",
-    .name `FieldSpecification.FieldOpAlgebra.normalOrder_uncontracted_none,
+    .name ``FieldSpecification.FieldOpAlgebra.normalOrder_uncontracted_none .incomplete,
-    .name `FieldSpecification.FieldOpAlgebra.normalOrder_uncontracted_some,
+    .name ``FieldSpecification.FieldOpAlgebra.normalOrder_uncontracted_some .incomplete,
     .h1 "Static contractions",
-    .name `WickContraction.staticContract,
+    .name ``WickContraction.staticContract .incomplete,
-    .name `WickContraction.staticContract_insert_some_of_lt,
+    .name ``WickContraction.staticContract_insert_some_of_lt .incomplete,
-    .name `WickContraction.staticContract_insert_none,
+    .name ``WickContraction.staticContract_insert_none .incomplete,
     .h1 "Time contractions",
-    .name `FieldSpecification.FieldOpAlgebra.timeContract,
+    .name ``FieldSpecification.FieldOpAlgebra.timeContract .incomplete,
-    .name `WickContraction.timeContract,
+    .name ``WickContraction.timeContract .incomplete,
-    .name `WickContraction.timeContract_insert_none,
+    .name ``WickContraction.timeContract_insert_none .incomplete,
-    .name `WickContraction.timeContract_insert_some_of_not_lt,
+    .name ``WickContraction.timeContract_insert_some_of_not_lt .incomplete,
-    .name `WickContraction.timeContract_insert_some_of_lt,
+    .name ``WickContraction.timeContract_insert_some_of_lt .incomplete,
     .h1 "Wick terms",
-    .name `WickContraction.wickTerm,
+    .name ``WickContraction.wickTerm .incomplete,
-    .name `WickContraction.wickTerm_empty_nil,
+    .name ``WickContraction.wickTerm_empty_nil .incomplete,
-    .name `WickContraction.wickTerm_insert_none,
+    .name ``WickContraction.wickTerm_insert_none .incomplete,
-    .name `WickContraction.wickTerm_insert_some,
+    .name ``WickContraction.wickTerm_insert_some .incomplete,
-    .name `WickContraction.mul_wickTerm_eq_sum,
+    .name ``WickContraction.mul_wickTerm_eq_sum .incomplete,
     .h1 "Static wick terms",
-    .name `WickContraction.staticWickTerm,
+    .name ``WickContraction.staticWickTerm .incomplete,
-    .name `WickContraction.staticWickTerm_empty_nil,
+    .name ``WickContraction.staticWickTerm_empty_nil .incomplete,
-    .name `WickContraction.staticWickTerm_insert_zero_none,
+    .name ``WickContraction.staticWickTerm_insert_zero_none .incomplete,
-    .name `WickContraction.staticWickTerm_insert_zero_some,
+    .name ``WickContraction.staticWickTerm_insert_zero_some .incomplete,
-    .name `WickContraction.mul_staticWickTerm_eq_sum,
+    .name ``WickContraction.mul_staticWickTerm_eq_sum .incomplete,
     .h1 "The three Wick's theorems",
-    .name `FieldSpecification.wicks_theorem,
+    .name ``FieldSpecification.wicks_theorem .incomplete,
-    .name `FieldSpecification.FieldOpAlgebra.static_wick_theorem,
+    .name ``FieldSpecification.FieldOpAlgebra.static_wick_theorem .incomplete,
-    .name `FieldSpecification.FieldOpAlgebra.wicks_theorem_normal_order
+    .name ``FieldSpecification.FieldOpAlgebra.wicks_theorem_normal_order .incomplete
     ]
 
 unsafe def main (_ : List String) : IO UInt32 := do