feat: Some modifictions to Wick contract etc

HepLean/FeynmanDiagrams/Wick/Algebra.lean

@@ -15,6 +15,12 @@ This file is currently a stub.
 
 We will formally define the operator ring, in terms of the fields present in the theory.
 
+## Futher reading
+
+- https://physics.stackexchange.com/questions/258718/ and links therein
+- Ryan Thorngren (https://physics.stackexchange.com/users/10336/ryan-thorngren), Fermions,
+  different species and (anti-)commutation rules, URL (version: 2019-02-20):
+  https://physics.stackexchange.com/q/461929
 -/
 
 namespace TwoComplexScalar

HepLean/FeynmanDiagrams/Wick/Contract.lean

@@ -24,12 +24,12 @@ open PreFeynmanRule
 
 /-- A Wick contraction for a Wick string is a series of pairs `i` and `j` of indices
   to be contracted, subject to ordering and subject to the condition that they can
-  be contracted (although this may need to be removed for full generality). -/
+  be contracted. -/
 inductive WickContract : {n : ℕ} → {c : Fin n → 𝓔} → (str : WickString c final) →
     {k : ℕ} → (b1 : Fin k → Fin n) → (b2 : Fin k → Fin n) → Type where
   | string {n : ℕ} {c : Fin n → 𝓔} {str : WickString c final} : WickContract str Fin.elim0 Fin.elim0
   | contr {n : ℕ} {c : Fin n → 𝓔} {str : WickString c final} {k : ℕ}
-    {b1 : Fin k → Fin n} {b2 : Fin k → Fin n}: (i : Fin n) →
+    {b1 : Fin k → Fin n} {b2 : Fin k → Fin n} : (i : Fin n) →
     (j : Fin n) → (h : c j = ξ (c i)) →
     (hilej : i < j) → (hb1 : ∀ r, b1 r < i) → (hb2i : ∀ r, b2 r ≠ i) → (hb2j : ∀ r, b2 r ≠ j) →
     (w : WickContract str b1 b2) →

HepLean/FeynmanDiagrams/Wick/String.lean

@@ -98,16 +98,50 @@ open WickStringLast
 /-- A wick string is a representation of a string of fields from a theory.
   E.g. `φ(x1) φ(x2) φ(y) φ(y) φ(y) φ(x3)`. The use of vertices in the Wick string
   allows us to identify which fields have the same space-time coordinate. -/
-inductive WickString : {n : ℕ} → (c : Fin n → 𝓔) → WickStringLast → Type where
-  | empty : WickString Fin.elim0 incoming
-  | incoming {n : ℕ} {c : Fin n → 𝓔} (w : WickString c incoming) (e : 𝓔) :
-      WickString (Fin.cons e c) incoming
-  | endIncoming {n : ℕ} {c : Fin n → 𝓔} (w : WickString c incoming) : WickString c vertex
-  | vertex {n : ℕ} {c : Fin n → 𝓔} (w : WickString c vertex) (v : 𝓥) :
-      WickString (Fin.append (𝓥Edges v) c) vertex
-  | endVertex {n : ℕ} {c : Fin n → 𝓔} (w : WickString c vertex) : WickString c outgoing
-  | outgoing {n : ℕ} {c : Fin n → 𝓔} (w : WickString c outgoing) (e : 𝓔) :
-      WickString (Fin.cons e c) outgoing
-  | endOutgoing {n : ℕ} {c : Fin n → 𝓔} (w : WickString c outgoing) : WickString c final
+inductive WickString : {ni : ℕ} → (i : Fin ni → 𝓔) → {n : ℕ} → (c : Fin n → 𝓔) →
+  {no : ℕ} → (o : Fin no → 𝓔) → WickStringLast → Type where
+  | empty : WickString Fin.elim0 Fin.elim0 Fin.elim0 incoming
+  | incoming {n ni no : ℕ} {i : Fin ni → 𝓔} {c : Fin n → 𝓔}
+       {o : Fin no → 𝓔} (w : WickString i c o incoming) (e : 𝓔) :
+      WickString (Fin.cons e i) (Fin.cons e c) o incoming
+  | endIncoming {n ni no : ℕ} {i : Fin ni → 𝓔} {c : Fin n → 𝓔}
+       {o : Fin no → 𝓔} (w : WickString i c o incoming) : WickString i c o vertex
+  | vertex {n ni no : ℕ} {i : Fin ni → 𝓔} {c : Fin n → 𝓔}
+       {o : Fin no → 𝓔} (w : WickString i c o vertex) (v : 𝓥) :
+      WickString i (Fin.append (𝓥Edges v) c) o vertex
+  | endVertex {n ni no : ℕ} {i : Fin ni → 𝓔} {c : Fin n → 𝓔}
+       {o : Fin no → 𝓔} (w : WickString i c o vertex) : WickString i c o outgoing
+  | outgoing {n ni no : ℕ} {i : Fin ni → 𝓔} {c : Fin n → 𝓔}
+       {o : Fin no → 𝓔} (w : WickString i c o outgoing) (e : 𝓔) :
+      WickString i (Fin.cons e c) (Fin.cons e o) outgoing
+  | endOutgoing {n ni no : ℕ} {i : Fin ni → 𝓔} {c : Fin n → 𝓔}
+       {o : Fin no → 𝓔} (w : WickString i c o outgoing) : WickString i c o final
+
+namespace WickString
+
+/-- The number of nodes in a Wick string. This is used to help prove termination. -/
+def size {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 => size w + 1
+  | endIncoming w => size w + 1
+  | vertex w v => size w + 1
+  | endVertex w => size w + 1
+  | outgoing w e => size w + 1
+  | endOutgoing w => size w + 1
+
+/-- The number of vertices in a Wick string. -/
+def numVertex {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
+
+
+end WickString
 
 end TwoComplexScalar