Docs: Documentation related to Wick contraction (#287)

* refactor: Fix field struct defn.

* rename: FieldStruct to FieldSpecification

* feat: Add examples of field specifications

* docs: Slight improvement of module docs

* refactor: Rename CreateAnnihilate

* docs: Algebras

* Update CrAnStates.lean

HepLean/PerturbationTheory/Algebras/StateAlgebra/Basic.lean

@@ -3,13 +3,19 @@ Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
-import HepLean.PerturbationTheory.FieldSpecification.CreateAnnihilate
+import HepLean.PerturbationTheory.FieldSpecification.CrAnStates
 /-!
 
 # State algebra
 
-We define the state algebra of a field structure to be the free algebra
-generated by the states.
+From the states associated with a field specification we can form a free algebra
+generated by these states. We call this the state algebra, or the state free-algebra.
+
+The state free-algebra has minimal assumptions, yet can be used to concretely define time-ordering.
+
+In
+`HepLean.PerturbationTheory.Algebras.CrAnAlgebra.Basic`
+we defined a related free-algebra generated by creation and annihilation states.
 
 -/
 

HepLean/PerturbationTheory/FieldSpecification/CrAnSection.lean

@@ -3,32 +3,28 @@ Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
-import HepLean.PerturbationTheory.FieldSpecification.CreateAnnihilate
+import HepLean.PerturbationTheory.FieldSpecification.CrAnStates
 /-!
 
 # Creation and annihlation sections
 
-This module defines creation and annihilation sections, which represent different ways to associate
-fields with creation or annihilation operators.
+In the module
+`HepLean.PerturbationTheory.FieldSpecification.Basic`
+we defined states for a field specification, and in the module
+`HepLean.PerturbationTheory.FieldStatistics.CrAnStates`
+we defined a refinement of states called `CrAnStates` which distinquishes between the
+creation and annihilation components of states.
+There exists, in particular, a map from `CrAnStates` to `States` called `crAnStatesToStates`.
 
-## Main definitions
+Given a list of `States`, `φs`, in this module we define a section of `φs` to be a list of
+`CrAnStates`, `ψs`, such that under the map `crAnStatesToStates`, `ψs` is mapped to `φs`.
+That is to say, the states underlying `ψs` are the states in `φs`.
+We denote these sections as `CrAnSection φs`.
 
-- `CrAnSection φs` : Represents sections in `𝓕.CrAnStates` over a list of states `φs`.
-  Given fields `φ₁...φₙ`, this captures all possible ways to assign each field as either a creation
-  or annihilation operator.
+Looking forward the main consequence of this definition is the lemma
+`FieldSpecification.CrAnAlgebra.ofStateList_sum`.
 
-- `head`, `tail` : Access the first element and remaining elements of a section
-
-- `cons` : Constructs a new section by prepending a creation/annihilation state
-
-- Various equivalences:
-  * `nilEquiv` : Empty sections
-  * `singletonEquiv` : Sections over single elements
-  * `consEquiv` : Separates head and tail
-  * `appendEquiv` : Splits sections at a given point
-
-All sections form finite types and support operations like taking/dropping elements and
-concatenation while preserving the relationship between states and their operator assignments.
+In this module we define various properties of `CrAnSection`.
 
 -/
 
@@ -41,8 +37,7 @@ variable {𝓕 : FieldSpecification}
   `φ₁⁰φ₂¹...φₙ⁰` `φ₁¹φ₂¹...φₙ⁰` etc. If some fields are exclusively creation or annhilation
   operators at this point (e.g. ansymptotic states) this is accounted for. -/
 def CrAnSection (φs : List 𝓕.States) : Type :=
-  {ψs : List 𝓕.CrAnStates //
-    List.map 𝓕.crAnStatesToStates ψs = φs}
+  {ψs : List 𝓕.CrAnStates // ψs.map 𝓕.crAnStatesToStates = φs}
   -- Π i, 𝓕.statesToCreateAnnihilateType (φs.get i)
 
 namespace CrAnSection

HepLean/PerturbationTheory/FieldSpecification/CrAnStates.lean

@@ -7,10 +7,30 @@ import HepLean.PerturbationTheory.FieldSpecification.Basic
 import HepLean.PerturbationTheory.CreateAnnihilate
 /-!
 
-# Creation and annihlation parts of fields
+# Creation and annihilation states
+
+Called `CrAnStates` for short here.
+
+Given a field specification, in addition to defining states
+(see: `HepLean.PerturbationTheory.FieldSpecification.Basic`),
+we can also define creation and annihilation states.
+These are similar to states but come with an additional specification of whether they correspond to
+creation or annihilation operators.
+
+In particular we have the following creation and annihilation states for each field:
+- Negative asymptotic states - with the implicit specification that it is a creation state.
+- Position states with a creation specification.
+- Position states with an annihilation specification.
+- Positive asymptotic states - with the implicit specification that it is an annihilation state.
+
+In this module in addition to defining `CrAnStates` we also define some maps:
+- The map `crAnStatesToStates` takes a `CrAnStates` to its state in `States`.
+- The map `crAnStatesToCreateAnnihilate` takes a `CrAnStates` to its corresponding
+`CreateAnnihilate` value.
+- The map `crAnStatistics` takes a `CrAnStates` to its corresponding `FieldStatistic`
+(bosonic or fermionic).
 
 -/
-
 namespace FieldSpecification
 variable (𝓕 : FieldSpecification)
 

HepLean/PerturbationTheory/FieldStatistics/ExchangeSign.lean

@@ -8,6 +8,16 @@ import HepLean.PerturbationTheory.FieldStatistics.Basic
 
 # Exchange sign for field statistics
 
+Suppose we have two fields `φ` and `ψ`, and the term `φψ`, if we swap them
+`ψφ`, we may pick up a sign. This sign is called the exchange sign.
+This sign is `-1` if both fields `ψ` and `φ` are fermionic and `1` otherwise.
+
+In this module we define the exchange sign for general field statistics,
+and prove some properties of it. Importantly:
+- It is symmetric `exchangeSign_symm`.
+- When multiplied with itself it is `1` `exchangeSign_mul_self`.
+- It is a cocycle `exchangeSign_cocycle`.
+
 -/
 
 namespace FieldStatistic
@@ -47,16 +57,17 @@ def exchangeSign : FieldStatistic →* FieldStatistic →* ℂ where
   Defined to be `-1` if both field statistics are `fermionic` and `1` otherwise. -/
 scoped[FieldStatistic] notation "𝓢(" a "," b ")" => exchangeSign a b
 
+/-- The exchange sign is symmetric. -/
+lemma exchangeSign_symm (a b : FieldStatistic) : 𝓢(a, b) = 𝓢(b, a) := by
+  fin_cases a <;> fin_cases b <;> rfl
+
 @[simp]
 lemma exchangeSign_bosonic (a : FieldStatistic) : 𝓢(a, bosonic) = 1 := by
   fin_cases a <;> rfl
 
 @[simp]
 lemma bosonic_exchangeSign (a : FieldStatistic) : 𝓢(bosonic, a) = 1 := by
-  fin_cases a <;> rfl
-
-lemma exchangeSign_symm (a b : FieldStatistic) : 𝓢(a, b) = 𝓢(b, a) := by
-  fin_cases a <;> fin_cases b <;> rfl
+  rw [exchangeSign_symm, exchangeSign_bosonic]
 
 lemma exchangeSign_eq_if (a b : FieldStatistic) :
     𝓢(a, b) = if a = fermionic ∧ b = fermionic then - 1 else 1 := by
@@ -75,6 +86,7 @@ lemma exchangeSign_ofList_cons (a : FieldStatistic)
     𝓢(a, ofList s (φ :: φs)) = 𝓢(a, s φ) * 𝓢(a, ofList s φs) := by
   rw [ofList_cons_eq_mul, map_mul]
 
+/-- The exchange sign is a cocycle. -/
 lemma exchangeSign_cocycle (a b c : FieldStatistic) :
     𝓢(a, b * c) * 𝓢(b, c) = 𝓢(a, b) * 𝓢(a * b, c) := by
   fin_cases a <;> fin_cases b <;> fin_cases c <;> simp