Merge pull request #251 from HEPLean/FeynmanDiagrams

feat: Wick species and informal lemmas

HepLean.lean

@@ -57,6 +57,7 @@ import HepLean.FeynmanDiagrams.Instances.Phi4
 import HepLean.FeynmanDiagrams.Momentum
 import HepLean.FeynmanDiagrams.Wick.Algebra
 import HepLean.FeynmanDiagrams.Wick.Contract
+import HepLean.FeynmanDiagrams.Wick.Species
 import HepLean.FeynmanDiagrams.Wick.String
 import HepLean.FlavorPhysics.CKMMatrix.Basic
 import HepLean.FlavorPhysics.CKMMatrix.Invariants

HepLean/FeynmanDiagrams/Wick/Algebra.lean

@@ -3,8 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
-import HepLean.FeynmanDiagrams.Basic
-import HepLean.Meta.Informal
+import HepLean.FeynmanDiagrams.Wick.Species
 /-!
 
 # Operator algebra
@@ -24,7 +23,7 @@ We will formally define the operator ring, in terms of the fields present in the
   https://physics.stackexchange.com/q/461929
 -/
 
-namespace TwoComplexScalar
+namespace Wick
 open CategoryTheory
 open FeynmanDiagram
 open PreFeynmanRule
@@ -101,4 +100,5 @@ informal_lemma timeOrder_pair where
     ``contraction]
 
 /-! TODO: Need to set up data and structure for vaccum expectation values. -/
-end TwoComplexScalar
+
+end Wick

HepLean/FeynmanDiagrams/Wick/Contract.lean

@@ -635,6 +635,11 @@ def unbound {ni : ℕ} {i : Fin ni → 𝓔} {n : ℕ} {c : Fin n → 𝓔}
     · exact List.Sorted.get_strictMono w.unboundList_sorted
     · exact fun ⦃a b⦄ a => a
 
+informal_definition HasEqualTimeContractions where
+  math :≈ "The condition for a Wick contraction to have two fields contracted
+    which are of equal time, i.e. come from the same vertex."
+  deps :≈ [``WickContract]
+
 end WickContract
 
 end TwoComplexScalar

HepLean/FeynmanDiagrams/Wick/Species.lean

@@ -0,0 +1,38 @@
+/-
+Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Joseph Tooby-Smith
+-/
+import HepLean.FeynmanDiagrams.Basic
+import HepLean.Meta.Informal
+/-!
+
+# Wick Species
+
+Note: There is very likely a much better name for what we here call a Wick Species.
+
+A Wick Species is a structure containing the basic information needed to write wick contractions
+for a theory, and calculate their corresponding Feynman diagrams.
+
+-/
+
+/-! TODO: There should be some sort of notion of a group action on a Wick Species. -/
+namespace Wick
+
+/-- The basic structure needed to write down Wick contractions for a theory and
+  calculate the corresponding Feynman diagrams.
+
+  WARNING: This definition is not yet complete. -/
+structure Species where
+  /-- The color of Field operators which appear in a theory. -/
+  𝓕 : Type
+  /-- The map taking a field operator to its dual operator. -/
+  ξ : 𝓕 → 𝓕
+  /-- The condition that `ξ` is an involution. -/
+  ξ_involutive : Function.Involutive ξ
+  /-- The color of vertices which appear in a theory. -/
+  𝓥 : Type
+  /-- The number of edges each vertex corresponds to. -/
+  𝓥Fields : 𝓥 → Σ n, Fin n → 𝓕
+
+end Wick

HepLean/FeynmanDiagrams/Wick/String.lean

@@ -3,8 +3,7 @@ Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
-import HepLean.FeynmanDiagrams.Basic
-import HepLean.Meta.Informal
+import HepLean.FeynmanDiagrams.Wick.Species
 /-!
 # Wick strings
 
@@ -133,7 +132,7 @@ def size {ni : ℕ} {i : Fin ni → 𝓔} {n : ℕ} {c : Fin n → 𝓔} {no : 
   | outgoing w e => size w + 1
   | endOutgoing w => size w + 1
 
-/-- The number of vertices in a Wick string. -/
+/-- The number of vertices in a Wick string. This does NOT include external vertices. -/
 def numVertex {ni : ℕ} {i : Fin ni → 𝓔} {n : ℕ} {c : Fin n → 𝓔} {no : ℕ} {o : Fin no → 𝓔}
     {f : WickStringLast} : WickString i c o f → ℕ := fun
   | empty => 0
@@ -144,7 +143,7 @@ def numVertex {ni : ℕ} {i : Fin ni → 𝓔} {n : ℕ} {c : Fin n → 𝓔} {n
   | outgoing w e => numVertex w
   | endOutgoing w => numVertex w
 
-/-- The vertices present in a Wick string. -/
+/-- The vertices present in a Wick string. This does NOT include external vertices. -/
 def vertices {ni : ℕ} {i : Fin ni → 𝓔} {n : ℕ} {c : Fin n → 𝓔} {no : ℕ} {o : Fin no → 𝓔}
     {f : WickStringLast} : (w : WickString i c o f) → Fin w.numVertex → 𝓥 := fun
   | empty => Fin.elim0
@@ -155,6 +154,11 @@ def vertices {ni : ℕ} {i : Fin ni → 𝓔} {n : ℕ} {c : Fin n → 𝓔} {no
   | outgoing w e => vertices w
   | endOutgoing w => vertices w
 
+informal_definition fieldToVertex where
+  math :≈ "A function which takes a field and returns the vertex it is associated with.
+    This is a map from `Fin n` to `Fin w.numVertex`"
+  deps :≈ [``WickString]
+
 informal_definition exponentialPrefactor where
   math :≈ "The combinatorical prefactor from the expansion of the
     exponential associated with a Wick string."