refactor: add more arguments to Wick String

HepLean/FeynmanDiagrams/Wick/Contract.lean

@@ -25,10 +25,15 @@ 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. -/
-inductive WickContract : {n : ℕ} → {c : Fin n → 𝓔} → (str : WickString c final) →
+inductive WickContract :
+     {ni : ℕ} → {i : Fin ni → 𝓔} → {n : ℕ} → {c : Fin n → 𝓔} →
+    {no : ℕ} → {o : Fin no → 𝓔} →
+    (str : WickString i c o 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
+  | string {ni : ℕ} {i : Fin ni → 𝓔} {n : ℕ} {c : Fin n → 𝓔}
-  | contr {n : ℕ} {c : Fin n → 𝓔} {str : WickString c final} {k : ℕ}
+    {no : ℕ} {o : Fin no → 𝓔} {str : WickString i c o final} : WickContract str Fin.elim0 Fin.elim0
+  | contr {ni : ℕ} {i : Fin ni → 𝓔} {n : ℕ} {c : Fin n → 𝓔}
+    {no : ℕ} {o : Fin no → 𝓔} {str : WickString i c o final} {k : ℕ}
     {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) →
@@ -38,13 +43,15 @@ inductive WickContract : {n : ℕ} → {c : Fin n → 𝓔} → (str : WickStrin
 namespace WickContract
 
 /-- The number of nodes of a Wick contraction. -/
-def size {n k : ℕ} {c : Fin n → 𝓔} {str : WickString c final} {b1 b2 : Fin k → Fin n} :
+def size  {ni : ℕ} {i : Fin ni → 𝓔} {n : ℕ} {c : Fin n → 𝓔}
+    {no : ℕ} {o : Fin no → 𝓔} {str : WickString i c o final} {k : ℕ} {b1 b2 : Fin k → Fin n} :
     WickContract str b1 b2 → ℕ := fun
   | string => 0
   | contr _ _ _ _ _ _ _ w => w.size + 1
 
 /-- The number of nodes in a wick contraction tree is the same as `k`. -/
-lemma size_eq_k {n k : ℕ} {c : Fin n → 𝓔} {str : WickString c final} {b1 b2 : Fin k → Fin n} :
+lemma size_eq_k {ni : ℕ} {i : Fin ni → 𝓔} {n : ℕ} {c : Fin n → 𝓔}
+    {no : ℕ} {o : Fin no → 𝓔} {str : WickString i c o final} {k : ℕ} {b1 b2 : Fin k → Fin n} :
     (w : WickContract str b1 b2) → w.size = k := fun
   | string => rfl
   | contr _ _ _ _ _ _ _ w => by
@@ -52,12 +59,15 @@ lemma size_eq_k {n k : ℕ} {c : Fin n → 𝓔} {str : WickString c final} {b1
 
 /-- The map giving the vertices on the left-hand-side of a contraction. -/
 @[nolint unusedArguments]
-def boundFst {n k : ℕ} {c : Fin n → 𝓔} {str : WickString c final} {b1 b2 : Fin k → Fin n} :
+def boundFst {ni : ℕ} {i : Fin ni → 𝓔} {n : ℕ} {c : Fin n → 𝓔}
+    {no : ℕ} {o : Fin no → 𝓔} {str : WickString i c o final}
+    {k : ℕ} {b1 b2 : Fin k → Fin n} :
     WickContract str b1 b2 → Fin k → Fin n := fun _ => b1
 
 @[simp]
-lemma boundFst_contr_castSucc {n k : ℕ} {c : Fin n → 𝓔} {str : WickString c final}
+lemma boundFst_contr_castSucc {ni : ℕ} {i : Fin ni → 𝓔} {n : ℕ} {c : Fin n → 𝓔}
-    {b1 b2 : Fin k → Fin n} (i j : Fin n)
+    {no : ℕ} {o : Fin no → 𝓔} {str : WickString i c o final}
+    {k : ℕ} {b1 b2 : Fin k → Fin n} (i j : Fin n)
     (h : c j = ξ (c i))
     (hilej : i < j)
     (hb1 : ∀ r, b1 r < i)
@@ -68,8 +78,9 @@ lemma boundFst_contr_castSucc {n k : ℕ} {c : Fin n → 𝓔} {str : WickString
   simp only [boundFst, Fin.snoc_castSucc]
 
 @[simp]
-lemma boundFst_contr_last {n k : ℕ} {c : Fin n → 𝓔} {str : WickString c final}
+lemma boundFst_contr_last {ni : ℕ} {i : Fin ni → 𝓔} {n : ℕ} {c : Fin n → 𝓔}
-    {b1 b2 : Fin k → Fin n} (i j : Fin n)
+    {no : ℕ} {o : Fin no → 𝓔} {str : WickString i c o final}
+    {k : ℕ} {b1 b2 : Fin k → Fin n} (i j : Fin n)
     (h : c j = ξ (c i))
     (hilej : i < j)
     (hb1 : ∀ r, b1 r < i)
@@ -79,8 +90,9 @@ lemma boundFst_contr_last {n k : ℕ} {c : Fin n → 𝓔} {str : WickString c f
     (contr i j h hilej hb1 hb2i hb2j w).boundFst (Fin.last k) = i := by
   simp only [boundFst, Fin.snoc_last]
 
-lemma boundFst_strictMono {n k : ℕ} {c : Fin n → 𝓔} {str : WickString c final}
+lemma boundFst_strictMono {ni : ℕ} {i : Fin ni → 𝓔} {n : ℕ} {c : Fin n → 𝓔}
-    {b1 b2 : Fin k → Fin n} : (w : WickContract str b1 b2) → StrictMono w.boundFst := fun
+    {no : ℕ} {o : Fin no → 𝓔} {str : WickString i c o final}
+    {k : ℕ} {b1 b2 : Fin k → Fin n} : (w : WickContract str b1 b2) → StrictMono w.boundFst := fun
   | string => fun k => Fin.elim0 k
   | contr i j _ _ hb1 _ _ w => by
     intro r s hrs
@@ -108,12 +120,15 @@ lemma boundFst_strictMono {n k : ℕ} {c : Fin n → 𝓔} {str : WickString c f
 
 /-- The map giving the vertices on the right-hand-side of a contraction. -/
 @[nolint unusedArguments]
-def boundSnd {n k : ℕ} {c : Fin n → 𝓔} {str : WickString c final} {b1 b2 : Fin k → Fin n} :
+def boundSnd {ni : ℕ} {i : Fin ni → 𝓔} {n : ℕ} {c : Fin n → 𝓔}
+    {no : ℕ} {o : Fin no → 𝓔} {str : WickString i c o final}
+    {k : ℕ} {b1 b2 : Fin k → Fin n} :
     WickContract str b1 b2 → Fin k → Fin n := fun _ => b2
 
 @[simp]
-lemma boundSnd_contr_castSucc {n k : ℕ} {c : Fin n → 𝓔} {str : WickString c final}
+lemma boundSnd_contr_castSucc {ni : ℕ} {i : Fin ni → 𝓔} {n : ℕ} {c : Fin n → 𝓔}
-    {b1 b2 : Fin k → Fin n} (i j : Fin n)
+    {no : ℕ} {o : Fin no → 𝓔} {str : WickString i c o final}
+    {k : ℕ} {b1 b2 : Fin k → Fin n} (i j : Fin n)
     (h : c j = ξ (c i))
     (hilej : i < j)
     (hb1 : ∀ r, b1 r < i)
@@ -124,8 +139,9 @@ lemma boundSnd_contr_castSucc {n k : ℕ} {c : Fin n → 𝓔} {str : WickString
   simp only [boundSnd, Fin.snoc_castSucc]
 
 @[simp]
-lemma boundSnd_contr_last {n k : ℕ} {c : Fin n → 𝓔} {str : WickString c final}
+lemma boundSnd_contr_last {ni : ℕ} {i : Fin ni → 𝓔} {n : ℕ} {c : Fin n → 𝓔}
-    {b1 b2 : Fin k → Fin n} (i j : Fin n)
+    {no : ℕ} {o : Fin no → 𝓔} {str : WickString i c o final}
+    {k : ℕ} {b1 b2 : Fin k → Fin n} (i j : Fin n)
     (h : c j = ξ (c i))
     (hilej : i < j)
     (hb1 : ∀ r, b1 r < i)
@@ -135,8 +151,10 @@ lemma boundSnd_contr_last {n k : ℕ} {c : Fin n → 𝓔} {str : WickString c f
     (contr i j h hilej hb1 hb2i hb2j w).boundSnd (Fin.last k) = j := by
   simp only [boundSnd, Fin.snoc_last]
 
-lemma boundSnd_injective {n k : ℕ} {c : Fin n → 𝓔} {str : WickString c final}
+lemma boundSnd_injective {ni : ℕ} {i : Fin ni → 𝓔} {n : ℕ} {c : Fin n → 𝓔}
-    {b1 b2 : Fin k → Fin n} : (w : WickContract str b1 b2) → Function.Injective w.boundSnd := fun
+    {no : ℕ} {o : Fin no → 𝓔} {str : WickString i c o final}
+    {k : ℕ} {b1 b2 : Fin k → Fin n} :
+    (w : WickContract str b1 b2) → Function.Injective w.boundSnd := fun
   | string => by
     intro i j _
     exact Fin.elim0 i
@@ -162,8 +180,9 @@ lemma boundSnd_injective {n k : ℕ} {c : Fin n → 𝓔} {str : WickString c fi
       · subst hs
         rfl
 
-lemma color_boundSnd_eq_dual_boundFst {n k : ℕ} {c : Fin n → 𝓔} {str : WickString c final}
+lemma color_boundSnd_eq_dual_boundFst {ni : ℕ} {i : Fin ni → 𝓔} {n : ℕ} {c : Fin n → 𝓔}
-    {b1 b2 : Fin k → Fin n} :
+    {no : ℕ} {o : Fin no → 𝓔} {str : WickString i c o final}
+    {k : ℕ} {b1 b2 : Fin k → Fin n} :
     (w : WickContract str b1 b2) → (i : Fin k) → c (w.boundSnd i) = ξ (c (w.boundFst i)) := fun
   | string => fun i => Fin.elim0 i
   | contr i j hij hilej hi _ _ w => fun r => by
@@ -174,8 +193,9 @@ lemma color_boundSnd_eq_dual_boundFst {n k : ℕ} {c : Fin n → 𝓔} {str : Wi
     · subst hr
       simpa using hij
 
-lemma boundFst_lt_boundSnd {n k : ℕ} {c : Fin n → 𝓔} {str : WickString c final}
+lemma boundFst_lt_boundSnd {ni : ℕ} {i : Fin ni → 𝓔} {n : ℕ} {c : Fin n → 𝓔}
-    {b1 b2 : Fin k → Fin n} : (w : WickContract str b1 b2) → (i : Fin k) →
+    {no : ℕ} {o : Fin no → 𝓔} {str : WickString i c o final}
+    {k : ℕ} {b1 b2 : Fin k → Fin n} : (w : WickContract str b1 b2) → (i : Fin k) →
     w.boundFst i < w.boundSnd i := fun
   | string => fun i => Fin.elim0 i
   | contr i j hij hilej hi _ _ w => fun r => by
@@ -187,8 +207,10 @@ lemma boundFst_lt_boundSnd {n k : ℕ} {c : Fin n → 𝓔} {str : WickString c
       simp only [boundFst_contr_last, boundSnd_contr_last]
       exact hilej
 
-lemma boundFst_neq_boundSnd {n k : ℕ} {c : Fin n → 𝓔} {str : WickString c final}
+lemma boundFst_neq_boundSnd {ni : ℕ} {i : Fin ni → 𝓔} {n : ℕ} {c : Fin n → 𝓔}
-    {b1 b2 : Fin k → Fin n} : (w : WickContract str b1 b2) → (r1 r2 : Fin k) → b1 r1 ≠ b2 r2 := fun
+    {no : ℕ} {o : Fin no → 𝓔} {str : WickString i c o final}
+    {k : ℕ} {b1 b2 : Fin k → Fin n} :
+    (w : WickContract str b1 b2) → (r1 r2 : Fin k) → b1 r1 ≠ b2 r2 := fun
   | string => fun i => Fin.elim0 i
   | contr i j _ hilej h1 h2i h2j w => fun r s => by
     rcases Fin.eq_castSucc_or_eq_last r with hr | hr
@@ -212,19 +234,23 @@ lemma boundFst_neq_boundSnd {n k : ℕ} {c : Fin n → 𝓔} {str : WickString c
 
 /-- Casts a Wick contraction from `WickContract str b1 b2` to `WickContract str b1' b2'` with a
   proof that `b1 = b1'` and `b2 = b2'`, and that they are defined from the same `k = k'`. -/
-def castMaps {n k k' : ℕ} {c : Fin n → 𝓔}
+def castMaps {ni : ℕ} {i : Fin ni → 𝓔} {n : ℕ} {c : Fin n → 𝓔}
-    {str : WickString c final} {b1 b2 : Fin k → Fin n} {b1' b2' : Fin k' → Fin n}
+    {no : ℕ} {o : Fin no → 𝓔} {str : WickString i c o final}
+    {k k' : ℕ}  {b1 b2 : Fin k → Fin n} {b1' b2' : Fin k' → Fin n}
     (hk : k = k')
     (hb1 : b1 = b1' ∘ Fin.cast hk) (hb2 : b2 = b2' ∘ Fin.cast hk) (w : WickContract str b1 b2) :
     WickContract str b1' b2' :=
   cast (by subst hk; rfl) (hb2 ▸ hb1 ▸ w)
 
 @[simp]
-lemma castMaps_rfl {n k : ℕ} {c : Fin n → 𝓔}{str : WickString c final}
+lemma castMaps_rfl {ni : ℕ} {i : Fin ni → 𝓔} {n : ℕ} {c : Fin n → 𝓔}
-    {b1 b2 : Fin k → Fin n} (w : WickContract str b1 b2) :
+    {no : ℕ} {o : Fin no → 𝓔} {str : WickString i c o final}
+    {k : ℕ} {b1 b2 : Fin k → Fin n} (w : WickContract str b1 b2) :
     castMaps rfl rfl rfl w = w := rfl
 
-lemma mem_snoc' {n k : ℕ} {c : Fin n → 𝓔} {str : WickString c final} {b1' b2' : Fin k → Fin n} :
+lemma mem_snoc' {ni : ℕ} {i : Fin ni → 𝓔} {n : ℕ} {c : Fin n → 𝓔}
+    {no : ℕ} {o : Fin no → 𝓔} {str : WickString i c o final}
+    {k : ℕ} {b1' b2' : Fin k → Fin n} :
     (w : WickContract str b1' b2') →
     {k' : ℕ} → (hk' : k'.succ = k) →
     (b1 b2 : Fin k' → Fin n) → (i j : Fin n) → (h : c j = ξ (c i)) →
@@ -266,14 +292,18 @@ lemma mem_snoc' {n k : ℕ} {c : Fin n → 𝓔} {str : WickString c final} {b1'
     subst hb1'' hb2'' hi hj
     simp
 
-lemma mem_snoc {n k : ℕ} {c : Fin n → 𝓔} {str : WickString c final} {b1 b2 : Fin k → Fin n}
+lemma mem_snoc {ni : ℕ} {i : Fin ni → 𝓔} {n : ℕ} {c : Fin n → 𝓔}
+    {no : ℕ} {o : Fin no → 𝓔} {str : WickString i c o final}
+    {k : ℕ} {b1 b2 : Fin k → Fin n}
     (i 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 (Fin.snoc b1 i) (Fin.snoc b2 j)) :
     ∃ (w' : WickContract str b1 b2), w = contr i j h hilej hb1 hb2i hb2j w' := by
   exact mem_snoc' w rfl b1 b2 i j h hilej hb1 hb2i hb2j rfl rfl
 
-lemma is_subsingleton {n k : ℕ} {c : Fin n → 𝓔} {str : WickString c final} {b1 b2 : Fin k → Fin n} :
+lemma is_subsingleton {ni : ℕ} {i : Fin ni → 𝓔} {n : ℕ} {c : Fin n → 𝓔}
+    {no : ℕ} {o : Fin no → 𝓔} {str : WickString i c o final}
+    {k : ℕ}  {b1 b2 : Fin k → Fin n} :
     Subsingleton (WickContract str b1 b2) := Subsingleton.intro fun w1 w2 => by
   induction k with
   | zero =>
@@ -301,7 +331,9 @@ lemma eq_snoc_castSucc {k n : ℕ} (b1 : Fin k.succ → Fin n) :
 /-- The construction of a Wick contraction from maps `b1 b2 : Fin k → Fin n`, with the former
   giving the first index to be contracted, and the latter the second index. These
   maps must satisfy a series of conditions. -/
-def fromMaps {n k : ℕ} {c : Fin n → 𝓔} {str : WickString c final} (b1 b2 : Fin k → Fin n)
+def fromMaps {ni : ℕ} {i : Fin ni → 𝓔} {n : ℕ} {c : Fin n → 𝓔}
+    {no : ℕ} {o : Fin no → 𝓔} {str : WickString i c o final}
+    {k : ℕ} (b1 b2 : Fin k → Fin n)
     (hi : ∀ i, c (b2 i) = ξ (c (b1 i)))
     (hb1ltb2 : ∀ i, b1 i < b2 i)
     (hb1 : StrictMono b1)
@@ -330,7 +362,9 @@ def fromMaps {n k : ℕ} {c : Fin n → 𝓔} {str : WickString c final} (b1 b2
 
 /-- Given a Wick contraction with `k.succ` contractions, returns the Wick contraction with
   `k` contractions by dropping the last contraction (defined by the first index contracted). -/
-def dropLast {n k : ℕ} {c : Fin n → 𝓔} {str : WickString c final} {b1 b2 : Fin k.succ → Fin n}
+def dropLast {ni : ℕ} {i : Fin ni → 𝓔} {n : ℕ} {c : Fin n → 𝓔}
+    {no : ℕ} {o : Fin no → 𝓔} {str : WickString i c o final}
+    {k : ℕ}  {b1 b2 : Fin k.succ → Fin n}
     (w : WickContract str b1 b2) : WickContract str (b1 ∘ Fin.castSucc) (b2 ∘ Fin.castSucc) :=
   fromMaps (b1 ∘ Fin.castSucc) (b2 ∘ Fin.castSucc)
     (fun i => color_boundSnd_eq_dual_boundFst w i.castSucc)
@@ -339,14 +373,17 @@ def dropLast {n k : ℕ} {c : Fin n → 𝓔} {str : WickString c final} {b1 b2
     (fun r1 r2 => boundFst_neq_boundSnd w r1.castSucc r2.castSucc)
     (Function.Injective.comp w.boundSnd_injective (Fin.castSucc_injective k))
 
-lemma eq_from_maps {n k : ℕ} {c : Fin n → 𝓔} {str : WickString c final} {b1 b2 : Fin k → Fin n}
+lemma eq_from_maps {ni : ℕ} {i : Fin ni → 𝓔} {n : ℕ} {c : Fin n → 𝓔}
+    {no : ℕ} {o : Fin no → 𝓔} {str : WickString i c o final}
+    {k : ℕ}  {b1 b2 : Fin k → Fin n}
     (w : WickContract str b1 b2) :
     w = fromMaps w.boundFst w.boundSnd w.color_boundSnd_eq_dual_boundFst
       w.boundFst_lt_boundSnd w.boundFst_strictMono w.boundFst_neq_boundSnd
       w.boundSnd_injective := is_subsingleton.allEq w _
 
-lemma eq_dropLast_contr {n k : ℕ} {c : Fin n → 𝓔} {str : WickString c final}
+lemma eq_dropLast_contr {ni : ℕ} {i : Fin ni → 𝓔} {n : ℕ} {c : Fin n → 𝓔}
-    {b1 b2 : Fin k.succ → Fin n} (w : WickContract str b1 b2) :
+    {no : ℕ} {o : Fin no → 𝓔} {str : WickString i c o final}
+    {k : ℕ} {b1 b2 : Fin k.succ → Fin n} (w : WickContract str b1 b2) :
   w = castMaps rfl (eq_snoc_castSucc b1).symm (eq_snoc_castSucc b2).symm
     (contr (b1 (Fin.last k)) (b2 (Fin.last k))
       (w.color_boundSnd_eq_dual_boundFst (Fin.last k))
@@ -359,12 +396,14 @@ lemma eq_dropLast_contr {n k : ℕ} {c : Fin n → 𝓔} {str : WickString c fin
   rfl
 
 /-- Wick contractions of a given Wick string with `k` different contractions. -/
-def Level {n : ℕ} {c : Fin n → 𝓔} (str : WickString c final) (k : ℕ) : Type :=
+def Level {ni : ℕ} {i : Fin ni → 𝓔} {n : ℕ} {c : Fin n → 𝓔}
+    {no : ℕ} {o : Fin no → 𝓔} (str : WickString i c o final) (k : ℕ) : Type :=
   Σ (b1 : Fin k → Fin n) (b2 : Fin k → Fin n), WickContract str b1 b2
 
 /-- There is a finite number of Wick contractions with no contractions. In particular,
   this is just the original Wick string. -/
-instance levelZeroFintype {n : ℕ} {c : Fin n → 𝓔} (str : WickString c final) :
+instance levelZeroFintype {ni : ℕ} {i : Fin ni → 𝓔} {n : ℕ} {c : Fin n → 𝓔}
+    {no : ℕ} {o : Fin no → 𝓔} (str : WickString i c o final) :
     Fintype (Level str 0) where
   elems := {⟨Fin.elim0, Fin.elim0, WickContract.string⟩}
   complete := by
@@ -378,7 +417,9 @@ instance levelZeroFintype {n : ℕ} {c : Fin n → 𝓔} (str : WickString c fin
       rw [is_subsingleton.allEq w string]
 
 /-- The pairs of additional indices which can be contracted given a Wick contraction. -/
-structure ContrPair {n : ℕ} {c : Fin n → 𝓔} {str : WickString c final} {b1 b2 : Fin k → Fin n}
+structure ContrPair {ni : ℕ} {i : Fin ni → 𝓔} {n : ℕ} {c : Fin n → 𝓔}
+    {no : ℕ} {o : Fin no → 𝓔} {str : WickString i c o final}
+    {k : ℕ} {b1 b2 : Fin k → Fin n}
     (w : WickContract str b1 b2) where
   /-- The first index in the contraction pair. -/
   i : Fin n
@@ -393,8 +434,9 @@ structure ContrPair {n : ℕ} {c : Fin n → 𝓔} {str : WickString c final} {b
 /-- The pairs of additional indices which can be contracted, given an existing wick contraction,
   is equivalent to the a subtype of `Fin n × Fin n` defined by certain conditions equivalent
   to the conditions appearing in `ContrPair`. -/
-def contrPairEquivSubtype {n : ℕ} {c : Fin n → 𝓔} {str : WickString c final}
+def contrPairEquivSubtype {ni : ℕ} {i : Fin ni → 𝓔} {n : ℕ} {c : Fin n → 𝓔}
-    {b1 b2 : Fin k → Fin n} (w : WickContract str b1 b2) :
+    {no : ℕ} {o : Fin no → 𝓔} {str : WickString i c o final}
+    {k : ℕ} {b1 b2 : Fin k → Fin n} (w : WickContract str b1 b2) :
     ContrPair w ≃ {x : Fin n × Fin n // c x.2 = ξ (c x.1) ∧ x.1 < x.2 ∧
       (∀ r, b1 r < x.1) ∧ (∀ r, b2 r ≠ x.1) ∧ (∀ r, b2 r ≠ x.2)} where
   toFun cp := ⟨⟨cp.i, cp.j⟩, ⟨cp.h, cp.hilej, cp.hb1, cp.hb2i, cp.hb2j⟩⟩
@@ -412,7 +454,9 @@ def contrPairEquivSubtype {n : ℕ} {c : Fin n → 𝓔} {str : WickString c fin
     obtain ⟨left_3, right⟩ := right
     simp_all only [ne_eq]
 
-lemma heq_eq {n : ℕ} {c : Fin n → 𝓔} {b1 b2 b1' b2' : Fin k → Fin n} {str : WickString c final}
+lemma heq_eq {ni : ℕ} {i : Fin ni → 𝓔} {n : ℕ} {c : Fin n → 𝓔}
+    {no : ℕ} {o : Fin no → 𝓔} {str : WickString i c o final}
+    {k : ℕ} {b1 b2 b1' b2' : Fin k → Fin n}
     (w : WickContract str b1 b2)
     (w' : WickContract str b1' b2') (h1 : b1 = b1') (h2 : b2 = b2') : HEq w w':= by
   subst h1 h2
@@ -421,7 +465,8 @@ lemma heq_eq {n : ℕ} {c : Fin n → 𝓔} {b1 b2 b1' b2' : Fin k → Fin n} {s
 
 /-- The equivalence between Wick contractions consisting of `k.succ` contractions and
   those with `k` contractions paired with a suitable contraction pair. -/
-def levelSuccEquiv {n : ℕ} {c : Fin n → 𝓔} (str : WickString c final) (k : ℕ) :
+def levelSuccEquiv {ni : ℕ} {i : Fin ni → 𝓔} {n : ℕ} {c : Fin n → 𝓔}
+    {no : ℕ} {o : Fin no → 𝓔} (str : WickString i c o final) (k : ℕ) :
     Level str k.succ ≃ (w : Level str k) × ContrPair w.2.2 where
   toFun w :=
     match w with
@@ -473,21 +518,29 @@ def levelSuccEquiv {n : ℕ} {c : Fin n → 𝓔} (str : WickString c final) (k
 
 /-- The sum of `boundFst` and `boundSnd`, giving on `Sum.inl k` the first index
   in the `k`th contraction, and on `Sum.inr k` the second index in the `k`th contraction. -/
-def bound {n k : ℕ} {c : Fin n → 𝓔} {str : WickString c final} {b1 b2 : Fin k → Fin n}
+def bound {ni : ℕ} {i : Fin ni → 𝓔} {n : ℕ} {c : Fin n → 𝓔}
+    {no : ℕ} {o : Fin no → 𝓔} {str : WickString i c o final}
+    {k : ℕ} {b1 b2 : Fin k → Fin n}
     (w : WickContract str b1 b2) : Fin k ⊕ Fin k → Fin n :=
   Sum.elim w.boundFst w.boundSnd
 
 /-- On `Sum.inl k` the map `bound` acts via `boundFst`. -/
 @[simp]
-lemma bound_inl {n k : ℕ} {c : Fin n → 𝓔} {str : WickString c final} {b1 b2 : Fin k → Fin n}
+lemma bound_inl {ni : ℕ} {i : Fin ni → 𝓔} {n : ℕ} {c : Fin n → 𝓔}
+    {no : ℕ} {o : Fin no → 𝓔} {str : WickString i c o final}
+    {k : ℕ} {b1 b2 : Fin k → Fin n}
     (w : WickContract str b1 b2) (i : Fin k) : w.bound (Sum.inl i) = w.boundFst i := rfl
 
 /-- On `Sum.inr k` the map `bound` acts via `boundSnd`. -/
 @[simp]
-lemma bound_inr {n k : ℕ} {c : Fin n → 𝓔} {str : WickString c final} {b1 b2 : Fin k → Fin n}
+lemma bound_inr {ni : ℕ} {i : Fin ni → 𝓔} {n : ℕ} {c : Fin n → 𝓔}
+    {no : ℕ} {o : Fin no → 𝓔} {str : WickString i c o final}
+    {k : ℕ} {b1 b2 : Fin k → Fin n}
     (w : WickContract str b1 b2) (i : Fin k) : w.bound (Sum.inr i) = w.boundSnd i := rfl
 
-lemma bound_injection {n k : ℕ} {c : Fin n → 𝓔} {str : WickString c final} {b1 b2 : Fin k → Fin n}
+lemma bound_injection {ni : ℕ} {i : Fin ni → 𝓔} {n : ℕ} {c : Fin n → 𝓔}
+    {no : ℕ} {o : Fin no → 𝓔} {str : WickString i c o final}
+    {k : ℕ} {b1 b2 : Fin k → Fin n}
     (w : WickContract str b1 b2) : Function.Injective w.bound := by
   intro x y h
   match x, y with
@@ -504,7 +557,9 @@ lemma bound_injection {n k : ℕ} {c : Fin n → 𝓔} {str : WickString c final
     simp only [bound_inr, bound_inl] at h
     exact False.elim (w.boundFst_neq_boundSnd y x h.symm)
 
-lemma bound_le_total {n k : ℕ} {c : Fin n → 𝓔} {str : WickString c final} {b1 b2 : Fin k → Fin n}
+lemma bound_le_total {ni : ℕ} {i : Fin ni → 𝓔} {n : ℕ} {c : Fin n → 𝓔}
+    {no : ℕ} {o : Fin no → 𝓔} {str : WickString i c o final}
+    {k : ℕ} {b1 b2 : Fin k → Fin n}
     (w : WickContract str b1 b2) : 2 * k ≤ n := by
   refine Fin.nonempty_embedding_iff.mp ⟨w.bound ∘ finSumFinEquiv.symm ∘ Fin.cast (Nat.two_mul k),
     ?_⟩
@@ -514,16 +569,24 @@ lemma bound_le_total {n k : ℕ} {c : Fin n → 𝓔} {str : WickString c final}
 
 /-- The list of fields (indexed by `Fin n`) in a Wick contraction which are not bound,
   i.e. which do not appear in any contraction. -/
-def unboundList {n k : ℕ} {c : Fin n → 𝓔} {str : WickString c final} {b1 b2 : Fin k → Fin n}
+def unboundList {ni : ℕ} {i : Fin ni → 𝓔} {n : ℕ} {c : Fin n → 𝓔}
+    {no : ℕ} {o : Fin no → 𝓔} {str : WickString i c o final}
+    {k : ℕ} {b1 b2 : Fin k → Fin n}
     (w : WickContract str b1 b2) : List (Fin n) :=
   List.filter (fun i => decide (∀ r, w.bound r ≠ i)) (List.finRange n)
 
-lemma unboundList_nodup {n k : ℕ} {c : Fin n → 𝓔} {str : WickString c final} {b1 b2 : Fin k → Fin n}
+/-- THe list of field positions which are not contracted has no duplicates. -/
+lemma unboundList_nodup {ni : ℕ} {i : Fin ni → 𝓔} {n : ℕ} {c : Fin n → 𝓔}
+    {no : ℕ} {o : Fin no → 𝓔} {str : WickString i c o final}
+    {k : ℕ} {b1 b2 : Fin k → Fin n}
     (w : WickContract str b1 b2) : (w.unboundList).Nodup :=
     List.Nodup.filter _ (List.nodup_finRange n)
 
-lemma unboundList_length {n k : ℕ} {c : Fin n → 𝓔} {str : WickString c final}
+/-- The length of the `unboundList` is equal to `n - 2 * k`. That is
-    {b1 b2 : Fin k → Fin n} (w : WickContract str b1 b2) :
+  the total number of fields minus the number of contracted fields. -/
+lemma unboundList_length {ni : ℕ} {i : Fin ni → 𝓔} {n : ℕ} {c : Fin n → 𝓔}
+    {no : ℕ} {o : Fin no → 𝓔} {str : WickString i c o final}
+    {k : ℕ} {b1 b2 : Fin k → Fin n} (w : WickContract str b1 b2) :
     w.unboundList.length = n - 2 * k := by
   rw [← List.Nodup.dedup w.unboundList_nodup]
   rw [← List.card_toFinset, unboundList]
@@ -548,29 +611,30 @@ lemma unboundList_length {n k : ℕ} {c : Fin n → 𝓔} {str : WickString c fi
     decide_eq_true_eq, Finset.mem_image, Finset.mem_univ, true_and, Sum.exists, not_or, not_exists]
   exact bound_injection w
 
-lemma unboundList_sorted {n k : ℕ} {c : Fin n → 𝓔} {str : WickString c final}
+lemma unboundList_sorted {ni : ℕ} {i : Fin ni → 𝓔} {n : ℕ} {c : Fin n → 𝓔}
-    {b1 b2 : Fin k → Fin n} (w : WickContract str b1 b2) :
+    {no : ℕ} {o : Fin no → 𝓔} {str : WickString i c o final}
+    {k : ℕ} {b1 b2 : Fin k → Fin n} (w : WickContract str b1 b2) :
     List.Sorted (fun i j => i < j) w.unboundList :=
   List.Pairwise.sublist (List.filter_sublist (List.finRange n)) (List.pairwise_lt_finRange n)
 
-/-- The map giving the fields which are not bound in a contraction. These
+/-- The ordered embedding giving the fields which are not bound in a contraction. These
   are the fields that will appear in a normal operator in Wick's theorem. -/
-def unbound {n k : ℕ} {c : Fin n → 𝓔} {str : WickString c final} {b1 b2 : Fin k → Fin n}
+def unbound {ni : ℕ} {i : Fin ni → 𝓔} {n : ℕ} {c : Fin n → 𝓔}
-    (w : WickContract str b1 b2) : Fin (n - 2 * k) → Fin n :=
+    {no : ℕ} {o : Fin no → 𝓔} {str : WickString i c o final}
-  w.unboundList.get ∘ Fin.cast w.unboundList_length.symm
+    {k : ℕ} {b1 b2 : Fin k → Fin n}
-
+    (w : WickContract str b1 b2) : Fin (n - 2 * k) ↪o Fin n where
-lemma unbound_injective {n k : ℕ} {c : Fin n → 𝓔} {str : WickString c final} {b1 b2 : Fin k → Fin n}
+  toFun := w.unboundList.get ∘ Fin.cast w.unboundList_length.symm
-    (w : WickContract str b1 b2) : Function.Injective w.unbound := by
+  inj' := by
-  apply Function.Injective.comp
+    apply Function.Injective.comp
-  · rw [← List.nodup_iff_injective_get]
+    · rw [← List.nodup_iff_injective_get]
-    exact w.unboundList_nodup
+      exact w.unboundList_nodup
-  · exact Fin.cast_injective _
+    · exact Fin.cast_injective _
-
+  map_rel_iff' := by
-lemma unbound_strictMono {n k : ℕ} {c : Fin n → 𝓔} {str : WickString c final}
+    refine fun {a b} => StrictMono.le_iff_le ?_
-    {b1 b2 : Fin k → Fin n} (w : WickContract str b1 b2) : StrictMono w.unbound := by
+    rw [Function.Embedding.coeFn_mk]
-  apply StrictMono.comp
+    apply StrictMono.comp
-  · refine List.Sorted.get_strictMono w.unboundList_sorted
+    · exact List.Sorted.get_strictMono w.unboundList_sorted
-  · exact fun ⦃a b⦄ a => a
+    · exact fun ⦃a b⦄ a => a
 
 end WickContract
 

HepLean/FeynmanDiagrams/Wick/String.lean

@@ -94,10 +94,12 @@ inductive WickStringLast where
 
 open WickStringLast
 
-/-! TODO: This definition should be adapted to include the in and out going fields as inputs. -/
 /-- 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. -/
+  allows us to identify which fields have the same space-time coordinate.
+
+  Note: Fields are added to `c` from right to left - matching how we would write this on
+  pen and paper. -/
 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
@@ -141,6 +143,17 @@ 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. -/
+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
+  | 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
+
 
 end WickString