feat: Update FieldSpecification and asymptotic fields

HepLean.lean

@@ -148,7 +148,6 @@ import HepLean.PerturbationTheory.FieldOpFreeAlgebra.TimeOrder
 import HepLean.PerturbationTheory.FieldSpecification.Basic
 import HepLean.PerturbationTheory.FieldSpecification.CrAnFieldOp
 import HepLean.PerturbationTheory.FieldSpecification.CrAnSection
-import HepLean.PerturbationTheory.FieldSpecification.Examples
 import HepLean.PerturbationTheory.FieldSpecification.Filters
 import HepLean.PerturbationTheory.FieldSpecification.NormalOrder
 import HepLean.PerturbationTheory.FieldSpecification.TimeOrder

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 (φ : 𝓕.Fields × Lorentz.Contr 4) :
+lemma anPart_negAsymp (φ : 𝓕.asymptoticDOF × (Fin 3 → ℝ)) :
     anPart (FieldOp.inAsymp φ) = 0 := by
   simp [anPart, anPartF]
 
 @[simp]
-lemma anPart_position (φ : 𝓕.Fields × SpaceTime) :
+lemma anPart_position (φ : 𝓕.positionDOF × SpaceTime) :
     anPart (FieldOp.position φ) =
     ofCrAnFieldOp ⟨FieldOp.position φ, CreateAnnihilate.annihilate⟩ := by
   simp [anPart, ofCrAnFieldOp]
 
 @[simp]
-lemma anPart_posAsymp (φ : 𝓕.Fields × Lorentz.Contr 4) :
+lemma anPart_posAsymp (φ : 𝓕.asymptoticDOF × (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 (φ : 𝓕.Fields × Lorentz.Contr 4) :
+lemma crPart_negAsymp (φ : 𝓕.asymptoticDOF × (Fin 3 → ℝ)) :
     crPart (FieldOp.inAsymp φ) = ofCrAnFieldOp ⟨FieldOp.inAsymp φ, ()⟩ := by
   simp [crPart, ofCrAnFieldOp]
 
 @[simp]
-lemma crPart_position (φ : 𝓕.Fields × SpaceTime) :
+lemma crPart_position (φ : 𝓕.positionDOF × SpaceTime) :
     crPart (FieldOp.position φ) =
     ofCrAnFieldOp ⟨FieldOp.position φ, CreateAnnihilate.create⟩ := by
   simp [crPart, ofCrAnFieldOp]
 
 @[simp]
-lemma crPart_posAsymp (φ : 𝓕.Fields × Lorentz.Contr 4) :
+lemma crPart_posAsymp (φ : 𝓕.asymptoticDOF × (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 (φ : 𝓕.Fields × Lorentz.Contr 4) :
+lemma crPartF_negAsymp (φ : 𝓕.asymptoticDOF × (Fin 3 → ℝ)) :
     crPartF (FieldOp.inAsymp φ) = ofCrAnOpF ⟨FieldOp.inAsymp φ, ()⟩ := by
   simp [crPartF]
 
 @[simp]
-lemma crPartF_position (φ : 𝓕.Fields × SpaceTime) :
+lemma crPartF_position (φ : 𝓕.positionDOF × SpaceTime) :
     crPartF (FieldOp.position φ) =
     ofCrAnOpF ⟨FieldOp.position φ, CreateAnnihilate.create⟩ := by
   simp [crPartF]
 
 @[simp]
-lemma crPartF_posAsymp (φ : 𝓕.Fields × Lorentz.Contr 4) :
+lemma crPartF_posAsymp (φ : 𝓕.asymptoticDOF × (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 (φ : 𝓕.Fields × Lorentz.Contr 4) :
+lemma anPartF_negAsymp (φ : 𝓕.asymptoticDOF × (Fin 3 → ℝ)) :
     anPartF (FieldOp.inAsymp φ) = 0 := by
   simp [anPartF]
 
 @[simp]
-lemma anPartF_position (φ : 𝓕.Fields × SpaceTime) :
+lemma anPartF_position (φ : 𝓕.positionDOF × SpaceTime) :
     anPartF (FieldOp.position φ) =
     ofCrAnOpF ⟨FieldOp.position φ, CreateAnnihilate.annihilate⟩ := by
   simp [anPartF]
 
 @[simp]
-lemma anPartF_posAsymp (φ : 𝓕.Fields × Lorentz.Contr 4) :
+lemma anPartF_posAsymp (φ : 𝓕.asymptoticDOF × (Fin 3 → ℝ)) :
     anPartF (FieldOp.outAsymp φ) = ofCrAnOpF ⟨FieldOp.outAsymp φ, ()⟩ := by
   simp [anPartF]
 

HepLean/PerturbationTheory/FieldSpecification/Basic.lean

@@ -23,44 +23,57 @@ From each field we can create three different types of `FieldOp`.
 
 These states carry the same field statistic as the field they are derived from.
 
+## Some references
+
+- https://particle.physics.ucdavis.edu/modernsusy/slides/slideimages/spinorfeynrules.pdf
+
 -/
 
-remark fieldSpecification_intro := "The raw ingredients of a field theory are:
-  - The specification of the fields.
-  - Whether each field is a boson or a fermion.
-  - Vertices present in the Lagrangian.
-  - The coefficent of each vertex.
-
-  We call the first two of these ingredients the `FieldSpecification` of the theory. "
-
-/-- A field specification is a type, `Fields`, elements of which are fields
-  present in a theory, and a map `statistics` from `Fields` to `FieldStatistic` which
-  identifies each field as a boson or a fermion. -/
+/-- 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:
+  - A type `positionDOF` containing the degree-of-freedom in position-based field
+  operators (excluding space-time position). Thus a sutible (but not unique) choice
+    - Real-scalar fields correspond to a single element of `positionDOF`.
+    - Complex-scalar fields correspond to two elements of `positionDOF`, one for the field and one
+      for its conjugate.
+    - Dirac fermions correspond to eight elements of `positionDOF`. One for each Lorentz index of the
+      field and its conjugate. (These are not all independent)
+    - Weyl fermions correspond to four elements of `positionDOF`. One for each Lorentz index of the
+      field. (These are not all independent)
+  - A type `asymptoticDOF` containing the degree-of-freedom in asymptotic field operators. Thus a
+    sutible (but not unique) choice is
+    - Real-scalar fields correspond to a single element of `asymptoticDOF`.
+    - Complex-scalar fields correspond to two elements of `asymptoticDOF`, one for the field and one
+      for its conjugate.
+    - Dirac fermions correspond to four elements of `asymptoticDOF`, two for each type of spin.
+    - Weyl fermions correspond to two elements of `asymptoticDOF`, one for each spin.
+  - A specification `statisticsPos` on a `positionDOF` is Fermionic or Bosonic.
+  - A specification `statisticsAsym` on a `asymptoticDOF` is Fermionic or Bosonic.
+-/
 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
+  /-- Degrees of freedom for position based field operators. -/
+  positionDOF : Type
+  /-- Degrees of freedom for asymptotic based field operators. -/
+  asymptoticDOF : Type
+  /-- The specification if the `positionDOF` are Fermionic or Bosonic. -/
+  statisticsPos : positionDOF → FieldStatistic
+  /-- The specification if the `asymptoticDOF` are Fermionic or Bosonic. -/
+  statisticsAsym : asymptoticDOF → 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 `4`-momentum.
+- an incoming asymptotic field operator `.inAsymp` specified by a field and a `3`-momentum.
 - an position operator `.position` specified by a field and a point in spacetime.
-- an outgoing asymptotic field operator `.outAsymp` specified by a field and a `4`-momentum.
+- an outgoing asymptotic field operator `.outAsymp` specified by a field and a `3`-momentum.
 -/
 inductive FieldOp (𝓕 : FieldSpecification) where
-  | inAsymp : 𝓕.Fields × Lorentz.Contr 4 → 𝓕.FieldOp
-  | position : 𝓕.Fields × SpaceTime → 𝓕.FieldOp
-  | outAsymp : 𝓕.Fields × Lorentz.Contr 4 → 𝓕.FieldOp
+  | inAsymp : 𝓕.asymptoticDOF × (Fin 3 → ℝ) → 𝓕.FieldOp
+  | position : 𝓕.positionDOF × SpaceTime → 𝓕.FieldOp
+  | outAsymp : 𝓕.asymptoticDOF × (Fin 3 → ℝ) → 𝓕.FieldOp
 
-/-- Taking a field operator to its underlying field. -/
-def fieldOpToField : 𝓕.FieldOp → 𝓕.Fields
-  | FieldOp.inAsymp φ => φ.1
-  | FieldOp.position φ => φ.1
-  | FieldOp.outAsymp φ => φ.1
 
 /-- The bool on `FieldOp` which is true only for position field operator. -/
 def statesIsPosition : 𝓕.FieldOp → Bool
@@ -68,7 +81,11 @@ def statesIsPosition : 𝓕.FieldOp → Bool
   | _ => false
 
 /-- The statistics associated to a field operator. -/
-def statesStatistic : 𝓕.FieldOp → FieldStatistic := 𝓕.statistics ∘ 𝓕.fieldOpToField
+def statesStatistic : 𝓕.FieldOp → FieldStatistic := fun f =>
+  match f with
+  | FieldOp.inAsymp (a, _) => 𝓕.statisticsAsym a
+  | FieldOp.position (a, _) => 𝓕.statisticsPos a
+  | FieldOp.outAsymp (a, _) => 𝓕.statisticsAsym a
 
 /-- The field statistics associated with a field operator. -/
 scoped[FieldSpecification] notation 𝓕 "|>ₛ" φ => statesStatistic 𝓕 φ

HepLean/PerturbationTheory/FieldSpecification/Examples.lean

@@ -1,40 +0,0 @@
-/-
-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.
-  The type of fields is the unit type, and the statistic of the unique element of the unit
-  type is bosonic. -/
-def singleBoson : FieldSpecification where
-  Fields := Unit
-  statistics := fun _ => FieldStatistic.bosonic
-
-/-- The Field specification corresponding to a single fermionic field.
-  The type of fields is the unit type, and the statistic of the unique element of the unit
-  type is fermionic. -/
-def singleFermion : FieldSpecification where
-  Fields := Unit
-  statistics := fun _ => FieldStatistic.fermionic
-
-/-- The Field specification corresponding to two bosonic fields and two fermionic fields.
-  The type of fields is `Fin 2 ⊕ Fin 2`, and the statistic of the two `.inl` (left) elements
-  is bosonic and the statistic of the two `.inr` (right) elements is fermionic. -/
-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

scripts/MetaPrograms/notes.lean

@@ -130,7 +130,6 @@ def perturbationTheory : Note where
     .name `FieldStatistic.instCommGroup,
     .name `FieldStatistic.exchangeSign,
     .h2 "Field specifications",
-    .name `fieldSpecification_intro,
     .name `FieldSpecification,
     .h2 "Field operators",
     .name `FieldSpecification.FieldOp,