refactor: Some properties of field specifications (#285)

* refactor: Fix field struct defn.

* rename: FieldStruct to FieldSpecification

* feat: Add examples of field specifications

* docs: Slight improvement of module docs

HepLean/PerturbationTheory/Algebras/CrAnAlgebra/Basic.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
 import HepLean.PerturbationTheory.Algebras.StateAlgebra.Basic
-import HepLean.PerturbationTheory.FieldStruct.CrAnSection
+import HepLean.PerturbationTheory.FieldSpecification.CrAnSection
 /-!
 
 # Creation and annihlation free-algebra
@@ -31,15 +31,15 @@ super commutation relations between creation and annihilation operators.
 
 -/
 
-namespace FieldStruct
-variable {𝓕 : FieldStruct}
+namespace FieldSpecification
+variable {𝓕 : FieldSpecification}
 
 /-- The creation and annihlation free-algebra.
   The free algebra generated by `CrAnStates`,
   that is a position based states or assymptotic states with a specification of
   whether the state is a creation or annihlation state.
   As a module `CrAnAlgebra` is spanned by lists of `CrAnStates`. -/
-abbrev CrAnAlgebra (𝓕 : FieldStruct) : Type := FreeAlgebra ℂ 𝓕.CrAnStates
+abbrev CrAnAlgebra (𝓕 : FieldSpecification) : Type := FreeAlgebra ℂ 𝓕.CrAnStates
 
 namespace CrAnAlgebra
 
@@ -263,4 +263,4 @@ noncomputable def smulLinearMap (c : ℂ) : CrAnAlgebra 𝓕 →ₗ[ℂ] CrAnAlg
 
 end CrAnAlgebra
 
-end FieldStruct
+end FieldSpecification

HepLean/PerturbationTheory/Algebras/CrAnAlgebra/NormalOrder.lean

@@ -3,23 +3,18 @@ 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.FieldStruct.NormalOrder
+import HepLean.PerturbationTheory.FieldSpecification.NormalOrder
 import HepLean.PerturbationTheory.Algebras.CrAnAlgebra.SuperCommute
 import HepLean.PerturbationTheory.Koszul.KoszulSign
 /-!
 
-# Normal Ordering
+# Normal Ordering in the CrAnAlgebra
 
-The normal ordering puts all creation operators to the left and all annihilation operators to the
-right. It acts on `CrAnStates` and defines a linear map from the `CrAnAlgebra` to itself.
-
-The normal ordering satisfies a number of nice properties with relation to the operator
-algebra 𝓞.A.
 
 -/
 
-namespace FieldStruct
-variable {𝓕 : FieldStruct}
+namespace FieldSpecification
+variable {𝓕 : FieldSpecification}
 open FieldStatistic
 /-!
 
@@ -552,4 +547,4 @@ end
 
 end CrAnAlgebra
 
-end FieldStruct
+end FieldSpecification

HepLean/PerturbationTheory/Algebras/CrAnAlgebra/SuperCommute.lean

@@ -9,8 +9,8 @@ import HepLean.PerturbationTheory.Algebras.CrAnAlgebra.Basic
 # Super Commute
 -/
 
-namespace FieldStruct
-variable {𝓕 : FieldStruct}
+namespace FieldSpecification
+variable {𝓕 : FieldSpecification}
 
 namespace CrAnAlgebra
 
@@ -18,7 +18,7 @@ open StateAlgebra
 
 /-!
 
-## The super commutor on the creation and annihlation algebra.
+## The super commutor on the CrAnAlgebra.
 
 -/
 
@@ -35,7 +35,7 @@ noncomputable def superCommute : 𝓕.CrAnAlgebra →ₗ[ℂ] 𝓕.CrAnAlgebra
 /-- The super commutor on the creation and annihlation algebra. For two bosonic operators
   or a bosonic and fermionic operator this corresponds to the usual commutator
   whilst for two fermionic operators this corresponds to the anti-commutator. -/
-scoped[FieldStruct.CrAnAlgebra] notation "⟨" φs "," φs' "⟩ₛca" => superCommute φs φs'
+scoped[FieldSpecification.CrAnAlgebra] notation "⟨" φs "," φs' "⟩ₛca" => superCommute φs φs'
 
 lemma superCommute_ofCrAnList (φs φs' : List 𝓕.CrAnStates) : ⟨ofCrAnList φs, ofCrAnList φs'⟩ₛca =
     ofCrAnList (φs ++ φs') - 𝓢(𝓕 |>ₛ φs, 𝓕 |>ₛ φs') • ofCrAnList (φs' ++ φs) := by
@@ -421,4 +421,4 @@ lemma superCommute_ofCrAnList_ofStateList_eq_sum (φs : List 𝓕.CrAnStates) :
 
 end CrAnAlgebra
 
-end FieldStruct
+end FieldSpecification

HepLean/PerturbationTheory/Algebras/OperatorAlgebra/Basic.lean

@@ -10,8 +10,8 @@ import HepLean.PerturbationTheory.Algebras.CrAnAlgebra.SuperCommute
 
 -/
 
-namespace FieldStruct
-variable (𝓕 : FieldStruct)
+namespace FieldSpecification
+variable (𝓕 : FieldSpecification)
 open CrAnAlgebra
 
 /-- The structure of an algebra with properties necessary for that algebra
@@ -45,7 +45,7 @@ structure OperatorAlgebra where
 
 namespace OperatorAlgebra
 open FieldStatistic
-variable {𝓕 : FieldStruct} (𝓞 : 𝓕.OperatorAlgebra)
+variable {𝓕 : FieldSpecification} (𝓞 : 𝓕.OperatorAlgebra)
 
 /-- The algebra `𝓞.A` carries the instance of a semi-ring induced via `A_seimRing`. -/
 instance : Semiring 𝓞.A := 𝓞.A_semiRing
@@ -199,4 +199,4 @@ lemma crAnF_superCommute_ofCrAnState_ofStateList_eq_sum (φ : 𝓕.CrAnStates) (
     rw [← map_mul, ← ofStateList_append, ← List.eraseIdx_eq_take_drop_succ]
 
 end OperatorAlgebra
-end FieldStruct
+end FieldSpecification

HepLean/PerturbationTheory/Algebras/OperatorAlgebra/NormalOrder.lean

@@ -7,18 +7,12 @@ import HepLean.PerturbationTheory.Algebras.CrAnAlgebra.NormalOrder
 import HepLean.PerturbationTheory.Koszul.KoszulSign
 /-!
 
-# Normal Ordering
-
-The normal ordering puts all creation operators to the left and all annihilation operators to the
-right. It acts on `CrAnStates` and defines a linear map from the `CrAnAlgebra` to itself.
-
-The normal ordering satisfies a number of nice properties with relation to the operator
-algebra 𝓞.A.
+# Normal ordering of the operator algebra
 
 -/
 
-namespace FieldStruct
-variable {𝓕 : FieldStruct}
+namespace FieldSpecification
+variable {𝓕 : FieldSpecification}
 
 namespace OperatorAlgebra
 variable {𝓞 : OperatorAlgebra 𝓕}
@@ -383,4 +377,4 @@ lemma crAnF_ofState_normalOrder_insert (φ : 𝓕.States) (φs : List 𝓕.State
 
 end OperatorAlgebra
 
-end FieldStruct
+end FieldSpecification

HepLean/PerturbationTheory/Algebras/OperatorAlgebra/TimeContraction.lean

@@ -14,8 +14,8 @@ generated by the states.
 
 -/
 
-namespace FieldStruct
-variable {𝓕 : FieldStruct}
+namespace FieldSpecification
+variable {𝓕 : FieldSpecification}
 open CrAnAlgebra
 noncomputable section
 
@@ -89,4 +89,4 @@ lemma timeContract_zero_of_diff_grade (φ ψ : 𝓕.States) (h : (𝓕 |>ₛ φ)
 end OperatorAlgebra
 
 end
-end FieldStruct
+end FieldSpecification

HepLean/PerturbationTheory/Algebras/StateAlgebra/Basic.lean

@@ -3,7 +3,7 @@ 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.FieldStruct.CreateAnnihilate
+import HepLean.PerturbationTheory.FieldSpecification.CreateAnnihilate
 /-!
 
 # State algebra
@@ -13,14 +13,14 @@ generated by the states.
 
 -/
 
-namespace FieldStruct
-variable {𝓕 : FieldStruct}
+namespace FieldSpecification
+variable {𝓕 : FieldSpecification}
 
 /-- The state free-algebra.
   The free algebra generated by `States`,
   that is a position based states or assymptotic states.
   As a module `StateAlgebra` is spanned by lists of `States`. -/
-abbrev StateAlgebra (𝓕 : FieldStruct) : Type := FreeAlgebra ℂ 𝓕.States
+abbrev StateAlgebra (𝓕 : FieldSpecification) : Type := FreeAlgebra ℂ 𝓕.States
 
 namespace StateAlgebra
 
@@ -90,4 +90,4 @@ lemma superCommute_ofList (φs φs' : List 𝓕.States) : ⟨ofList φs, ofList
 
 end StateAlgebra
 
-end FieldStruct
+end FieldSpecification

HepLean/PerturbationTheory/Algebras/StateAlgebra/TimeOrder.lean

@@ -3,19 +3,16 @@ 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.FieldStruct.TimeOrder
+import HepLean.PerturbationTheory.FieldSpecification.TimeOrder
 import HepLean.PerturbationTheory.Koszul.KoszulSign
 /-!
 
-# State algebra
-
-We define the state algebra of a field structure to be the free algebra
-generated by the states.
+# Time ordering on the state algebra
 
 -/
 
-namespace FieldStruct
-variable {𝓕 : FieldStruct}
+namespace FieldSpecification
+variable {𝓕 : FieldSpecification}
 noncomputable section
 
 namespace StateAlgebra
@@ -80,4 +77,4 @@ lemma timeOrder_eq_maxTimeField_mul (φ : 𝓕.States) (φs : List 𝓕.States)
 
 end StateAlgebra
 end
-end FieldStruct
+end FieldSpecification

HepLean/PerturbationTheory/FieldSpecification/Basic.lean

@@ -9,20 +9,31 @@ import HepLean.SpaceTime.Basic
 import HepLean.PerturbationTheory.FieldStatistics.OfFinset
 /-!
 
-# Field structures
+# Field specification
+
+In this module is the definition of a field specification.
+A field specification is a structure consisting of a type of fields and a
+the field statistics of each field.
+
+From each field we can create three different types of `States`.
+- Negative asymptotic states.
+- Position states.
+- Positive asymptotic states.
+
+These states carry the same field statistic as the field they are derived from.
 
 -/
 
-/-- A field structure is a type of fields plus a specification of the
+/-- A field specification is a type of fields plus a specification of the
   statistics (fermionic or bosonic) of each field. -/
-structure FieldStruct where
+structure FieldSpecification where
   /-- The type of fields. This also includes anti-states. -/
   Fields : Type
   /-- The specification if a field is bosonic or fermionic. -/
   statistics : Fields → FieldStatistic
 
-namespace FieldStruct
-variable (𝓕 : FieldStruct)
+namespace FieldSpecification
+variable (𝓕 : FieldSpecification)
 
 /-- Negative asymptotic states are specified by a field and a momentum. -/
 def AsymptoticNegTime : Type := 𝓕.Fields × Lorentz.Contr 4
@@ -34,7 +45,7 @@ def AsymptoticPosTime : Type := 𝓕.Fields × Lorentz.Contr 4
 def PositionStates : Type := 𝓕.Fields × SpaceTime
 
 /-- The combination of asymptotic states and position states. -/
-inductive States (𝓕 : FieldStruct) where
+inductive States (𝓕 : FieldSpecification) where
   | negAsymp : 𝓕.AsymptoticNegTime → 𝓕.States
   | position : 𝓕.PositionStates → 𝓕.States
   | posAsymp : 𝓕.AsymptoticPosTime → 𝓕.States
@@ -49,14 +60,14 @@ def statesToField : 𝓕.States → 𝓕.Fields
 def statesStatistic : 𝓕.States → FieldStatistic := 𝓕.statistics ∘ 𝓕.statesToField
 
 /-- The field statistics associated with a state. -/
-scoped[FieldStruct] notation 𝓕 "|>ₛ" φ => statesStatistic 𝓕 φ
+scoped[FieldSpecification] notation 𝓕 "|>ₛ" φ => statesStatistic 𝓕 φ
 
 /-- The field statistics associated with a list states. -/
-scoped[FieldStruct] notation 𝓕 "|>ₛ" φ => FieldStatistic.ofList
+scoped[FieldSpecification] notation 𝓕 "|>ₛ" φ => FieldStatistic.ofList
     (statesStatistic 𝓕) φ
 
 /-- The field statistic associated with a finite set-/
-scoped[FieldStruct] notation 𝓕 "|>ₛ" "⟨" f ","a "⟩"=> FieldStatistic.ofFinset
+scoped[FieldSpecification] notation 𝓕 "|>ₛ" "⟨" f ","a "⟩"=> FieldStatistic.ofFinset
     (statesStatistic 𝓕) f a
 
-end FieldStruct
+end FieldSpecification

HepLean/PerturbationTheory/FieldSpecification/CrAnSection.lean

@@ -3,7 +3,7 @@ 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.FieldStruct.CreateAnnihilate
+import HepLean.PerturbationTheory.FieldSpecification.CreateAnnihilate
 /-!
 
 # Creation and annihlation sections
@@ -32,8 +32,8 @@ concatenation while preserving the relationship between states and their operato
 
 -/
 
-namespace FieldStruct
-variable {𝓕 : FieldStruct}
+namespace FieldSpecification
+variable {𝓕 : FieldSpecification}
 
 /-- The sections in `𝓕.CrAnStates` over a list `φs : List 𝓕.States`.
   In terms of physics, given some fields `φ₁...φₙ`, the different ways one can associate
@@ -47,7 +47,7 @@ def CrAnSection (φs : List 𝓕.States) : Type :=
 
 namespace CrAnSection
 open FieldStatistic
-variable {𝓕 : FieldStruct} {φs : List 𝓕.States}
+variable {𝓕 : FieldSpecification} {φs : List 𝓕.States}
 
 @[simp]
 lemma length_eq (ψs : CrAnSection φs) : ψs.1.length = φs.length := by
@@ -392,4 +392,4 @@ lemma sum_eraseIdxEquiv (n : ℕ) (φs : List 𝓕.States) (hn : n < φs.length)
 
 end CrAnSection
 
-end FieldStruct
+end FieldSpecification

HepLean/PerturbationTheory/FieldSpecification/CreateAnnihilate.lean

@@ -3,7 +3,7 @@ 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.FieldStruct.Basic
+import HepLean.PerturbationTheory.FieldSpecification.Basic
 import HepLean.PerturbationTheory.CreateAnnihilate
 /-!
 
@@ -11,8 +11,8 @@ import HepLean.PerturbationTheory.CreateAnnihilate
 
 -/
 
-namespace FieldStruct
-variable (𝓕 : FieldStruct)
+namespace FieldSpecification
+variable (𝓕 : FieldSpecification)
 
 /-- To each state the specificaition of the type of creation and annihlation parts.
   For asymptotic staes there is only one allowed part, whilst for position states
@@ -67,16 +67,16 @@ def crAnStatistics : 𝓕.CrAnStates → FieldStatistic :=
   𝓕.statesStatistic ∘ 𝓕.crAnStatesToStates
 
 /-- The field statistic of a `CrAnState`. -/
-scoped[FieldStruct] notation 𝓕 "|>ₛ" φ =>
+scoped[FieldSpecification] notation 𝓕 "|>ₛ" φ =>
     (crAnStatistics 𝓕) φ
 
 /-- The field statistic of a list of `CrAnState`s. -/
-scoped[FieldStruct] notation 𝓕 "|>ₛ" φ => FieldStatistic.ofList
+scoped[FieldSpecification] notation 𝓕 "|>ₛ" φ => FieldStatistic.ofList
     (crAnStatistics 𝓕) φ
 
 /-- The `CreateAnnihilate` value of a `CrAnState`s, i.e. whether it is a creation or
   annihilation operator. -/
-scoped[FieldStruct] infixl:80 "|>ᶜ" =>
+scoped[FieldSpecification] infixl:80 "|>ᶜ" =>
     crAnStatesToCreateAnnihilate
 
-end FieldStruct
+end FieldSpecification

HepLean/PerturbationTheory/FieldSpecification/Examples.lean

@@ -0,0 +1,36 @@
+/-
+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.Basic
+/-!
+
+# Specific examples of field specifications
+
+
+-/
+
+namespace FieldSpecification
+variable (𝓕 : FieldSpecification)
+
+/-- The Field specification corresponding to a single bosonic field. -/
+def singleBoson : FieldSpecification where
+  Fields := Unit
+  statistics := fun _ => FieldStatistic.bosonic
+
+/-- The Field specification corresponding to a single fermionic field. -/
+def singleFermion : FieldSpecification where
+  Fields := Unit
+  statistics := fun _ => FieldStatistic.fermionic
+
+/-- The Field specification corresponding to a two bosonic field and
+  two fermionic fields. -/
+def doubleBosonDoubleFermion : FieldSpecification where
+  Fields := Fin 2 ⊕ Fin 2
+  statistics := fun b =>
+    match b with
+    | Sum.inl _ => FieldStatistic.bosonic
+    | Sum.inr _ => FieldStatistic.fermionic
+
+end FieldSpecification

HepLean/PerturbationTheory/FieldSpecification/Filters.lean

@@ -11,8 +11,8 @@ import HepLean.PerturbationTheory.Koszul.KoszulSign
 
 -/
 
-namespace FieldStruct
-variable {𝓕 : FieldStruct}
+namespace FieldSpecification
+variable {𝓕 : FieldSpecification}
 
 /-- Given a list of creation and annihilation states, the filtered list only containing
   the creation states. As a schematic example, for the list:
@@ -86,4 +86,4 @@ lemma annihilateFilter_singleton_annihilate (φ : 𝓕.CrAnStates)
     annihilateFilter [φ] = [φ] := by
   simp [annihilateFilter, hφ]
 
-end FieldStruct
+end FieldSpecification

HepLean/PerturbationTheory/FieldSpecification/NormalOrder.lean

@@ -5,21 +5,17 @@ Authors: Joseph Tooby-Smith
 -/
 import HepLean.PerturbationTheory.Algebras.OperatorAlgebra.Basic
 import HepLean.PerturbationTheory.Koszul.KoszulSign
-import HepLean.PerturbationTheory.FieldStruct.Filters
+import HepLean.PerturbationTheory.FieldSpecification.Filters
 /-!
 
-# Normal Ordering
+# Normal Ordering of states
 
-The normal ordering puts all creation operators to the left and all annihilation operators to the
-right. It acts on `CrAnStates` and defines a linear map from the `CrAnAlgebra` to itself.
 
-The normal ordering satisfies a number of nice properties with relation to the operator
-algebra 𝓞.A.
 
 -/
 
-namespace FieldStruct
-variable {𝓕 : FieldStruct}
+namespace FieldSpecification
+variable {𝓕 : FieldSpecification}
 
 /-- The normal ordering relation on creation and annihlation operators.
   For a list of creation and annihlation states, this relation is designed
@@ -425,4 +421,4 @@ lemma normalOrderList_eq_createFilter_append_annihilateFilter : (φs : List 𝓕
       rw [orderedInsert_createFilter_append_annihilateFilter_annihilate φ hφ']
       rw [createFilter_cons_annihilate hφ', annihilateFilter_cons_annihilate hφ']
 
-end FieldStruct
+end FieldSpecification

HepLean/PerturbationTheory/FieldSpecification/TimeOrder.lean

@@ -8,15 +8,12 @@ import HepLean.PerturbationTheory.Algebras.StateAlgebra.Basic
 import HepLean.PerturbationTheory.Koszul.KoszulSign
 /-!
 
-# State algebra
-
-We define the state algebra of a field structure to be the free algebra
-generated by the states.
+# Time ordering of states
 
 -/
 
-namespace FieldStruct
-variable {𝓕 : FieldStruct}
+namespace FieldSpecification
+variable {𝓕 : FieldSpecification}
 
 /-- The time ordering relation on states. We have that `timeOrderRel φ0 φ1` is true
   if and only if `φ1` has a time less-then or equal to `φ0`, or `φ1` is a negative
@@ -173,4 +170,4 @@ lemma timeOrderList_eq_maxTimeField_timeOrderList (φ : 𝓕.States) (φs : List
   exact insertionSort_eq_insertionSortMin_cons timeOrderRel φ φs
 
 end
-end FieldStruct
+end FieldSpecification

HepLean/PerturbationTheory/FieldStatistics/ExchangeSign.lean

@@ -6,7 +6,7 @@ Authors: Joseph Tooby-Smith
 import HepLean.PerturbationTheory.FieldStatistics.Basic
 /-!
 
-# Exchange sign
+# Exchange sign for field statistics
 
 -/
 

HepLean/PerturbationTheory/WickContraction/Basic.lean

@@ -7,12 +7,12 @@ import HepLean.PerturbationTheory.Algebras.OperatorAlgebra.NormalOrder
 import HepLean.Mathematics.List.InsertIdx
 /-!
 
-# Contractions
+# Wick contractions
 
 -/
-open FieldStruct
+open FieldSpecification
 
-variable {𝓕 : FieldStruct}
+variable {𝓕 : FieldSpecification}
 
 /--
 Given a natural number `n` corresponding to the number of fields, a Wick contraction

HepLean/PerturbationTheory/WickContraction/Erase.lean

@@ -10,8 +10,8 @@ import HepLean.PerturbationTheory.WickContraction.Uncontracted
 
 -/
 
-open FieldStruct
-variable {𝓕 : FieldStruct}
+open FieldSpecification
+variable {𝓕 : FieldSpecification}
 
 namespace WickContraction
 variable {n : ℕ} (c : WickContraction n)

HepLean/PerturbationTheory/WickContraction/ExtractEquiv.lean

@@ -10,8 +10,8 @@ import HepLean.PerturbationTheory.WickContraction.Insert
 
 -/
 
-open FieldStruct
-variable {𝓕 : FieldStruct}
+open FieldSpecification
+variable {𝓕 : FieldSpecification}
 
 namespace WickContraction
 variable {n : ℕ} (c : WickContraction n)

HepLean/PerturbationTheory/WickContraction/Insert.lean

@@ -10,8 +10,8 @@ import HepLean.PerturbationTheory.WickContraction.Erase
 
 -/
 
-open FieldStruct
-variable {𝓕 : FieldStruct}
+open FieldSpecification
+variable {𝓕 : FieldSpecification}
 
 namespace WickContraction
 variable {n : ℕ} (c : WickContraction n)

HepLean/PerturbationTheory/WickContraction/InsertList.lean

@@ -6,12 +6,12 @@ Authors: Joseph Tooby-Smith
 import HepLean.PerturbationTheory.WickContraction.UncontractedList
 /-!
 
-# Inserting an element into a contraction
+# Inserting an element into a contraction based on a list
 
 -/
 
-open FieldStruct
-variable {𝓕 : FieldStruct}
+open FieldSpecification
+variable {𝓕 : FieldSpecification}
 
 namespace WickContraction
 variable {n : ℕ} (c : WickContraction n)

HepLean/PerturbationTheory/WickContraction/Involutions.lean

@@ -13,8 +13,8 @@ import HepLean.PerturbationTheory.WickContraction.InsertList
 
 -/
 
-open FieldStruct
-variable {𝓕 : FieldStruct}
+open FieldSpecification
+variable {𝓕 : FieldSpecification}
 namespace WickContraction
 variable {n : ℕ} (c : WickContraction n)
 open HepLean.List

HepLean/PerturbationTheory/WickContraction/IsFull.lean

@@ -13,8 +13,8 @@ We say that a contraction is full if it has no uncontracted fields.
 
 -/
 
-open FieldStruct
-variable {𝓕 : FieldStruct}
+open FieldSpecification
+variable {𝓕 : FieldSpecification}
 namespace WickContraction
 variable {n : ℕ} (c : WickContraction n)
 open HepLean.List

HepLean/PerturbationTheory/WickContraction/Sign.lean

@@ -11,8 +11,8 @@ import HepLean.PerturbationTheory.WickContraction.InsertList
 
 -/
 
-open FieldStruct
-variable {𝓕 : FieldStruct}
+open FieldSpecification
+variable {𝓕 : FieldSpecification}
 
 namespace WickContraction
 variable {n : ℕ} (c : WickContraction n)

HepLean/PerturbationTheory/WickContraction/TimeContract.lean

@@ -11,8 +11,8 @@ import HepLean.PerturbationTheory.Algebras.OperatorAlgebra.TimeContraction
 
 -/
 
-open FieldStruct
-variable {𝓕 : FieldStruct}
+open FieldSpecification
+variable {𝓕 : FieldSpecification}
 
 namespace WickContraction
 variable {n : ℕ} (c : WickContraction n)

HepLean/PerturbationTheory/WickContraction/Uncontracted.lean

@@ -9,8 +9,8 @@ import HepLean.PerturbationTheory.WickContraction.Basic
 # Uncontracted elements
 
 -/
-open FieldStruct
-variable {𝓕 : FieldStruct}
+open FieldSpecification
+variable {𝓕 : FieldSpecification}
 
 namespace WickContraction
 variable {n : ℕ} (c : WickContraction n)

HepLean/PerturbationTheory/WickContraction/UncontractedList.lean

@@ -6,12 +6,12 @@ Authors: Joseph Tooby-Smith
 import HepLean.PerturbationTheory.WickContraction.ExtractEquiv
 /-!
 
-# List of uncontracted elements
+# List of uncontracted elements of a Wick contraction
 
 -/
 
-open FieldStruct
-variable {𝓕 : FieldStruct}
+open FieldSpecification
+variable {𝓕 : FieldSpecification}
 
 namespace WickContraction
 variable {n : ℕ} (c : WickContraction n)

HepLean/PerturbationTheory/WicksTheorem.lean

@@ -15,8 +15,8 @@ Wick's theorem is related to Isserlis' theorem in mathematics.
 
 -/
 
-namespace FieldStruct
-variable {𝓕 : FieldStruct} {𝓞 : 𝓕.OperatorAlgebra}
+namespace FieldSpecification
+variable {𝓕 : FieldSpecification} {𝓞 : 𝓕.OperatorAlgebra}
 open CrAnAlgebra
 open StateAlgebra
 open OperatorAlgebra
@@ -361,4 +361,4 @@ theorem wicks_theorem : (φs : List 𝓕.States) → 𝓞.crAnF (ofStateAlgebra
     · exact fun k => lt_maxTimeFieldPosFin_not_timeOrder _ _ k
 termination_by φs => φs.length
 
-end FieldStruct
+end FieldSpecification