Merge pull request #252 from HEPLean/FeynmanDiagrams

feat: Add informal lemmas cf wick contract

HepLean/FeynmanDiagrams/Wick/Algebra.lean

@@ -34,10 +34,10 @@ informal_definition WickAlgebra where
     A structure with the following data:
     - A ℤ₂-graded algebra A.
     - A map from `ψ : 𝓔 × SpaceTime → A` where 𝓔 are field colors.
-    - A map `ψ₊ : 𝓔 × SpaceTime → A`.
-    - A map `ψ₋ : 𝓔 × SpaceTime → A`.
+    - A map `ψc : 𝓔 × SpaceTime → A`.
+    - A map `ψd : 𝓔 × SpaceTime → A`.
     Subject to the conditions:
-    - The sum of `ψ0` and `ψ1` is `ψ`.
+    - The sum of `ψc` and `ψd` is `ψ`.
     - Two fields super-commute if there colors are not dual to each other.
     - The super-commutator of two fields is always in the
       center of the algebra. "
@@ -65,8 +65,8 @@ informal_definition timeOrder where
 informal_definition normalOrder where
   math :≈ "A function from WickMonomial to WickAlgebra which takes a monomial and
     returns the element in `WickAlgebra` defined as follows
-    - The ψ₊ fields are move to the right.
-    - The ψ₋ fields are moved to the left.
+    - The ψd fields are move to the right.
+    - The ψc fields are moved to the left.
     - Othewise the order of the fields is preserved."
   ref :≈ "https://www.imperial.ac.uk/media/imperial-college/research-centres-and-groups/theoretical-physics/msc/current/qft/handouts/qftwickstheorem.pdf"
   deps :≈ [``WickAlgebra, ``WickMonomial]

HepLean/FeynmanDiagrams/Wick/Contract.lean

@@ -640,6 +640,15 @@ informal_definition HasEqualTimeContractions where
     which are of equal time, i.e. come from the same vertex."
   deps :≈ [``WickContract]
 
+informal_definition IsConnected where
+  math :≈ "The condition for a Wick contraction that for any two vertices
+    (including external vertices) are connected by contractions."
+  deps :≈ [``WickContract]
+
+informal_definition HasVacuumContributions where
+  math :≈ "The condition for a Wick contraction to have a vacuum contribution."
+  deps :≈ [``WickContract]
+
 end WickContract
 
 end TwoComplexScalar

HepLean/FeynmanDiagrams/Wick/Species.lean

@@ -22,7 +22,8 @@ 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. -/
+  WARNING: This definition is not yet complete.
+   -/
 structure Species where
   /-- The color of Field operators which appear in a theory. -/
   𝓕 : Type
@@ -32,7 +33,7 @@ structure Species where
   ξ_involutive : Function.Involutive ξ
   /-- The color of vertices which appear in a theory. -/
   𝓥 : Type
-  /-- The number of edges each vertex corresponds to. -/
+  /-- The edges each vertex corresponds to. -/
   𝓥Fields : 𝓥 → Σ n, Fin n → 𝓕
 
 end Wick

HepLean/FeynmanDiagrams/Wick/String.lean

@@ -133,41 +133,45 @@ def size {ni : ℕ} {i : Fin ni → 𝓔} {n : ℕ} {c : Fin n → 𝓔} {no : 
   | endOutgoing w => size w + 1
 
 /-- 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 → 𝓔}
+def numIntVertex {ni : ℕ} {i : Fin ni → 𝓔} {n : ℕ} {c : Fin n → 𝓔} {no : ℕ} {o : Fin no → 𝓔}
     {f : WickStringLast} : WickString i c o f → ℕ := fun
   | empty => 0
-  | incoming w e => numVertex w
-  | endIncoming w => numVertex w
-  | vertex w v => numVertex w + 1
-  | endVertex w => numVertex w
-  | outgoing w e => numVertex w
-  | endOutgoing w => numVertex w
+  | incoming w e => numIntVertex w
+  | endIncoming w => numIntVertex w
+  | vertex w v => numIntVertex w + 1
+  | endVertex w => numIntVertex w
+  | outgoing w e => numIntVertex w
+  | endOutgoing w => numIntVertex w
 
 /-- 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
+def intVertex {ni : ℕ} {i : Fin ni → 𝓔} {n : ℕ} {c : Fin n → 𝓔} {no : ℕ} {o : Fin no → 𝓔}
+    {f : WickStringLast} : (w : WickString i c o f) → Fin w.numIntVertex → 𝓥 := fun
   | empty => Fin.elim0
-  | incoming w e => vertices w
-  | endIncoming w => vertices w
-  | vertex w v => Fin.cons v (vertices w)
-  | endVertex w => vertices w
-  | 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`"
+  | incoming w e => intVertex w
+  | endIncoming w => intVertex w
+  | vertex w v => Fin.cons v (intVertex w)
+  | endVertex w => intVertex w
+  | outgoing w e => intVertex w
+  | endOutgoing w => intVertex w
+
+informal_definition intExtVertex where
+  math :≈ "The vertices present in a Wick string, including external vertices."
+  deps :≈ [``WickString]
+
+informal_definition fieldToIntExtVertex where
+  math :≈ "A function which takes a field and returns the internal or
+    external vertex it is associated with."
   deps :≈ [``WickString]
 
 informal_definition exponentialPrefactor where
   math :≈ "The combinatorical prefactor from the expansion of the
     exponential associated with a Wick string."
-  deps :≈ [``vertices, ``WickString]
+  deps :≈ [``intVertex, ``WickString]
 
 informal_definition vertexPrefactor where
   math :≈ "The prefactor arising from the coefficent of vertices in the
     Lagrangian. This should not take account of the exponential prefactor."
-  deps :≈ [``vertices, ``WickString]
+  deps :≈ [``intVertex, ``WickString]
 
 informal_definition minNoLoops where
   math :≈ "The minimum number of loops a Feynman diagram based on a given Wick string can have.