refactor: Reorganize files

2024-12-19 14:25:09 +00:00 · 2024-12-19 14:25:09 +00:00 · c993de36f6
commit c993de36f6
parent 63c4cabdf4
16 changed files with 1408 additions and 1310 deletions
--- a/HepLean/PerturbationTheory/Wick/Koszul/Contraction.lean
+++ b/HepLean/PerturbationTheory/Wick/Koszul/Contraction.lean
@ -3,7 +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.PerturbationTheory.Wick.Koszul.OperatorMap
+import HepLean.PerturbationTheory.Wick.OperatorMap
 /-!

 # Koszul signs and ordering for lists and algebras
@ -100,7 +100,7 @@ structure Splitting {I : Type} (f : I → Type) [∀ i, Fintype (f i)]
  𝓑p : I → (Σ i, f i)
  𝓧n : I → ℂ
  𝓧p : I → ℂ
-  h𝓑 : ∀ i, ofListM f [i] 1 = ofList [𝓑n i] (𝓧n i) + ofList [𝓑p i] (𝓧p i)
+  h𝓑 : ∀ i, ofListLift f [i] 1 = ofList [𝓑n i] (𝓧n i) + ofList [𝓑p i] (𝓧p i)
  h𝓑n : ∀ i j, le1 (𝓑n i) j
  h𝓑p : ∀ i j, le1 j (𝓑p i)

@ -114,7 +114,7 @@ def toCenterTerm {I : Type} (f : I → Type) [∀ i, Fintype (f i)]
  | _ :: _, ⟨_, .cons (aux := aux') none c⟩, S => toCenterTerm f q le1 F ⟨aux', c⟩ S
  | a :: _, ⟨_, .cons (aux := aux') (some n) c⟩, S => toCenterTerm f q le1 F ⟨aux', c⟩ S *
    superCommuteCoef q [aux'.get n] (List.take (↑n) aux') •
-      F (((superCommute fun i => q i.fst) (ofList [S.𝓑p a] (S.𝓧p a))) (ofListM f [aux'.get n] 1))
+      F (((superCommute fun i => q i.fst) (ofList [S.𝓑p a] (S.𝓧p a))) (ofListLift f [aux'.get n] 1))

 lemma toCenterTerm_none {I : Type} (f : I → Type) [∀ i, Fintype (f i)]
    (q : I → Fin 2) {r : List I}
@ -147,105 +147,16 @@ lemma toCenterTerm_center {I : Type} (f : I → Type) [∀ i, Fintype (f i)]
    refine Subalgebra.mul_mem (Subalgebra.center ℂ A) ?hx ?hy
    exact toCenterTerm_center f q le1 F ⟨aux', c⟩ S
    apply Subalgebra.smul_mem
-    rw [ofListM_expand]
+    rw [ofListLift_expand]
    rw [map_sum, map_sum]
    refine Subalgebra.sum_mem (Subalgebra.center ℂ A) ?hy.hx.h
    intro x _
-    simp only [CreatAnnilateSect.toList]
+    simp only [CreateAnnilateSect.toList]
    rw [ofList_singleton]
    exact OperatorMap.superCommute_ofList_singleton_ι_center (q := fun i => q i.1)
      (le1 := le1) F (S.𝓑p a) ⟨aux'[↑n], x.head⟩

 end Contractions

-lemma static_wick_nil {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
-    (q : I → Fin 2)
-    (le1 : (Σ i, f i) → (Σ i, f i) → Prop) [DecidableRel le1]
-    {A : Type} [Semiring A] [Algebra ℂ A]
-    (F : FreeAlgebra ℂ (Σ i, f i) →ₐ A) [OperatorMap (fun i => q i.1) le1 F]
-    (S : Contractions.Splitting f le1) :
-    F (ofListM f [] 1) = ∑ c : Contractions [],
-    c.toCenterTerm f q le1 F S *
-    F (koszulOrder le1 (fun i => q i.fst) (ofListM f c.normalize 1)) := by
-  rw [← Contractions.nilEquiv.symm.sum_comp]
-  simp only [Finset.univ_unique, PUnit.default_eq_unit, Contractions.nilEquiv, Equiv.coe_fn_symm_mk,
-    Finset.sum_const, Finset.card_singleton, one_smul]
-  dsimp [Contractions.normalize, Contractions.toCenterTerm]
-  simp [ofListM_empty]
-
-lemma static_wick_cons {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
-    (q : I → Fin 2)
-    (le1 : (Σ i, f i) → (Σ i, f i) → Prop) [DecidableRel le1]
-    [IsTrans ((i : I) × f i) le1] [IsTotal ((i : I) × f i) le1]
-    {A : Type} [Semiring A] [Algebra ℂ A] (r : List I) (a : I)
-    (F : FreeAlgebra ℂ (Σ i, f i) →ₐ A) [OperatorMap (fun i => q i.1) le1 F]
-    (S : Contractions.Splitting f le1)
-    (ih : F (ofListM f r 1) =
-    ∑ c : Contractions r, c.toCenterTerm f q le1 F S * F (koszulOrder le1 (fun i => q i.fst)
-      (ofListM f c.normalize 1))) :
-    F (ofListM f (a :: r) 1) = ∑ c : Contractions (a :: r),
-      c.toCenterTerm f q le1 F S *
-      F (koszulOrder le1 (fun i => q i.fst) (ofListM f c.normalize 1)) := by
-  rw [ofListM_cons_eq_ofListM, map_mul, ih, Finset.mul_sum,
-    ← Contractions.consEquiv.symm.sum_comp]
-  erw [Finset.sum_sigma]
-  congr
-  funext c
-  have hb := S.h𝓑 a
-  rw [← mul_assoc]
-  have hi := c.toCenterTerm_center f q le1 F S
-  rw [Subalgebra.mem_center_iff] at hi
-  rw [hi, mul_assoc, ← map_mul, hb, add_mul, map_add]
-  conv_lhs =>
-    rhs
-    lhs
-    rw [ofList_eq_smul_one]
-    rw [Algebra.smul_mul_assoc]
-    rw [ofList_singleton]
-  rw [mul_koszulOrder_le]
-  conv_lhs =>
-    rhs
-    lhs
-    rw [← map_smul, ← Algebra.smul_mul_assoc]
-    rw [← ofList_singleton, ← ofList_eq_smul_one]
-  conv_lhs =>
-    rhs
-    rhs
-    rw [ofList_eq_smul_one, Algebra.smul_mul_assoc, map_smul]
-  rw [le_all_mul_koszulOrder_ofListM_expand]
-  conv_lhs =>
-    rhs
-    rhs
-    rw [smul_add, Finset.smul_sum]
-    rw [← map_smul, ← map_smul, ← Algebra.smul_mul_assoc, ← ofList_eq_smul_one]
-    rhs
-    rhs
-    intro n
-    rw [← Algebra.smul_mul_assoc, smul_comm, ← map_smul, ← LinearMap.map_smul₂,
-      ← ofList_eq_smul_one]
-  rw [← add_assoc, ← map_add, ← map_add, ← add_mul, ← hb, ← ofListM_cons_eq_ofListM, mul_add]
-  rw [Fintype.sum_option]
-  congr 1
-  rw [Finset.mul_sum]
-  congr
-  funext n
-  rw [← mul_assoc]
-  rfl
-  exact S.h𝓑p a
-  exact S.h𝓑n a
-
-theorem static_wick_theorem {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
-    (q : I → Fin 2)
-    (le1 : (Σ i, f i) → (Σ i, f i) → Prop) [DecidableRel le1] [IsTrans ((i : I) × f i) le1]
-    [IsTotal ((i : I) × f i) le1]
-    {A : Type} [Semiring A] [Algebra ℂ A] (r : List I)
-    (F : FreeAlgebra ℂ (Σ i, f i) →ₐ A) [OperatorMap (fun i => q i.1) le1 F]
-    (S : Contractions.Splitting f le1) :
-    F (ofListM f r 1) = ∑ c : Contractions r, c.toCenterTerm f q le1 F S *
-      F (koszulOrder le1 (fun i => q i.fst) (ofListM f c.normalize 1)) := by
-  induction r with
-  | nil => exact static_wick_nil q le1 F S
-  | cons a r ih => exact static_wick_cons q le1 r a F S ih
-
 end
 end Wick
--- a/HepLean/PerturbationTheory/Wick/CreateAnnilateSection.lean
+++ b/HepLean/PerturbationTheory/Wick/CreateAnnilateSection.lean
@ -3,147 +3,32 @@ 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.PerturbationTheory.Wick.Koszul.Grade
+import HepLean.PerturbationTheory.Wick.Signs.StaticWickCoef
 /-!

-# Koszul signs and ordering for lists and algebras
+# Create and annihilate sections (of bundles)

 -/

 namespace Wick
 open HepLean.List

-noncomputable section
-
-def ofList {I : Type} (l : List I) (x : ℂ) : FreeAlgebra ℂ I :=
-  FreeAlgebra.equivMonoidAlgebraFreeMonoid.symm (MonoidAlgebra.single l x)
-
-lemma ofList_pair {I : Type} (l r : List I) (x y : ℂ) :
-    ofList (l ++ r) (x * y) = ofList l x * ofList r y := by
-  simp only [ofList, ← map_mul, MonoidAlgebra.single_mul_single, EmbeddingLike.apply_eq_iff_eq]
-  rfl
-
-lemma ofList_triple {I : Type} (la lb lc : List I) (xa xb xc : ℂ) :
-    ofList (la ++ lb ++ lc) (xa * xb * xc) = ofList la xa * ofList lb xb * ofList lc xc := by
-  rw [ofList_pair, ofList_pair]
-
-lemma ofList_triple_assoc {I : Type} (la lb lc : List I) (xa xb xc : ℂ) :
-    ofList (la ++ (lb ++ lc)) (xa * (xb * xc)) = ofList la xa * ofList lb xb * ofList lc xc := by
-  rw [ofList_pair, ofList_pair]
-  exact Eq.symm (mul_assoc (ofList la xa) (ofList lb xb) (ofList lc xc))
-
-lemma ofList_cons_eq_ofList {I : Type} (l : List I) (i : I) (x : ℂ) :
-    ofList (i :: l) x = ofList [i] 1 * ofList l x := by
-  simp only [ofList, ← map_mul, MonoidAlgebra.single_mul_single, one_mul,
-    EmbeddingLike.apply_eq_iff_eq]
-  rfl
-
-lemma ofList_singleton {I : Type} (i : I) :
-    ofList [i] 1 = FreeAlgebra.ι ℂ i := by
-  simp only [ofList, FreeAlgebra.equivMonoidAlgebraFreeMonoid, MonoidAlgebra.of_apply,
-    MonoidAlgebra.single, AlgEquiv.ofAlgHom_symm_apply, MonoidAlgebra.lift_single, one_smul]
-  rfl
-
-lemma ofList_eq_smul_one {I : Type} (l : List I) (x : ℂ) :
-    ofList l x = x • ofList l 1 := by
-  simp only [ofList]
-  rw [← map_smul]
-  simp
-
-lemma ofList_empty {I : Type} : ofList [] 1 = (1 : FreeAlgebra ℂ I) := by
-  simp only [ofList, EmbeddingLike.map_eq_one_iff]
-  rfl
-
-lemma ofList_empty' {I : Type} : ofList [] x = x • (1 : FreeAlgebra ℂ I) := by
-  rw [ofList_eq_smul_one, ofList_empty]
-
-lemma koszulOrder_ofList {I : Type} (r : I → I → Prop) [DecidableRel r] (q : I → Fin 2)
-    (l : List I) (x : ℂ) :
-    koszulOrder r q (ofList l x) = (koszulSign r q l) • ofList (List.insertionSort r l) x := by
-  rw [ofList]
-  rw [koszulOrder_single]
-  change ofList (List.insertionSort r l) _ = _
-  rw [ofList_eq_smul_one]
-  conv_rhs => rw [ofList_eq_smul_one]
-  rw [smul_smul]
-
-lemma ofList_insertionSort_eq_koszulOrder {I : Type} (r : I → I → Prop) [DecidableRel r]
-    (q : I → Fin 2) (l : List I) (x : ℂ) :
-    ofList (List.insertionSort r l) x = (koszulSign r q l) • koszulOrder r q (ofList l x) := by
-  rw [koszulOrder_ofList]
-  rw [smul_smul]
-  rw [koszulSign_mul_self]
-  simp
-
-def freeAlgebraMap {I : Type} (f : I → Type) [∀ i, Fintype (f i)] :
-    FreeAlgebra ℂ I →ₐ[ℂ] FreeAlgebra ℂ (Σ i, f i) :=
-  FreeAlgebra.lift ℂ fun i => ∑ (j : f i), FreeAlgebra.ι ℂ ⟨i, j⟩
-
-lemma freeAlgebraMap_ι {I : Type} (f : I → Type) [∀ i, Fintype (f i)] (i : I) :
-    freeAlgebraMap f (FreeAlgebra.ι ℂ i) = ∑ (b : f i), FreeAlgebra.ι ℂ ⟨i, b⟩ := by
-  simp [freeAlgebraMap]
-
-def ofListM {I : Type} (f : I → Type) [∀ i, Fintype (f i)] (l : List I) (x : ℂ) :
-    FreeAlgebra ℂ (Σ i, f i) :=
-  freeAlgebraMap f (ofList l x)
-
-lemma ofListM_empty {I : Type} (f : I → Type) [∀ i, Fintype (f i)] :
-  ofListM f [] 1 = 1 := by
-  simp only [ofListM, EmbeddingLike.map_eq_one_iff]
-  rw [ofList_empty]
-  exact map_one (freeAlgebraMap f)
-
-lemma ofListM_empty_smul {I : Type} (f : I → Type) [∀ i, Fintype (f i)] (x : ℂ) :
-  ofListM f [] x = x • 1 := by
-  simp only [ofListM, EmbeddingLike.map_eq_one_iff]
-  rw [ofList_eq_smul_one]
-  rw [ofList_empty]
-  simp
-
-lemma ofListM_cons {I : Type} (f : I → Type) [∀ i, Fintype (f i)] (i : I) (r : List I) (x : ℂ) :
-    ofListM f (i :: r) x = (∑ j : f i, FreeAlgebra.ι ℂ ⟨i, j⟩) * (ofListM f r x) := by
-  rw [ofListM, ofList_cons_eq_ofList, ofList_singleton, map_mul]
-  conv_lhs => lhs; rw [freeAlgebraMap]
-  rw [ofListM]
-  simp
-
-lemma ofListM_singleton {I : Type} (f : I → Type) [∀ i, Fintype (f i)] (i : I) (x : ℂ) :
-    ofListM f [i] x = ∑ j : f i, x • FreeAlgebra.ι ℂ ⟨i, j⟩ := by
-  simp only [ofListM]
-  rw [ofList_eq_smul_one, ofList_singleton, map_smul]
-  rw [freeAlgebraMap_ι]
-  rw [Finset.smul_sum]
-
-lemma ofListM_singleton_one {I : Type} (f : I → Type) [∀ i, Fintype (f i)] (i : I) :
-    ofListM f [i] 1 = ∑ j : f i, FreeAlgebra.ι ℂ ⟨i, j⟩ := by
-  simp only [ofListM]
-  rw [ofList_eq_smul_one, ofList_singleton, map_smul]
-  rw [freeAlgebraMap_ι]
-  rw [Finset.smul_sum]
-  simp
-
-lemma ofListM_cons_eq_ofListM {I : Type} (f : I → Type) [∀ i, Fintype (f i)] (i : I)
-    (r : List I) (x : ℂ) :
-    ofListM f (i :: r) x = ofListM f [i] 1 * ofListM f r x := by
-  rw [ofListM_cons, ofListM_singleton]
-  simp only [one_smul]
-
-def CreatAnnilateSect {I : Type} (f : I → Type) [∀ i, Fintype (f i)] (l : List I) : Type :=
+def CreateAnnilateSect {I : Type} (f : I → Type) [∀ i, Fintype (f i)] (l : List I) : Type :=
  Π i, f (l.get i)

-namespace CreatAnnilateSect
+namespace CreateAnnilateSect

-variable {I : Type} {f : I → Type} [∀ i, Fintype (f i)] {l : List I} (a : CreatAnnilateSect f l)
+variable {I : Type} {f : I → Type} [∀ i, Fintype (f i)] {l : List I} (a : CreateAnnilateSect f l)

-instance fintype : Fintype (CreatAnnilateSect f l) := Pi.fintype
+instance fintype : Fintype (CreateAnnilateSect f l) := Pi.fintype

-def tail : {l : List I} → (a : CreatAnnilateSect f l) → CreatAnnilateSect f l.tail
+def tail : {l : List I} → (a : CreateAnnilateSect f l) → CreateAnnilateSect f l.tail
  | [], a => a
  | _ :: _, a => fun i => a (Fin.succ i)

-def head {i : I} (a : CreatAnnilateSect f (i :: l)) : f i := a ⟨0, Nat.zero_lt_succ l.length⟩
+def head {i : I} (a : CreateAnnilateSect f (i :: l)) : f i := a ⟨0, Nat.zero_lt_succ l.length⟩

-def toList : {l : List I} → (a : CreatAnnilateSect f l) → List (Σ i, f i)
+def toList : {l : List I} → (a : CreateAnnilateSect f l) → List (Σ i, f i)
  | [], _ => []
  | i :: _, a => ⟨i, a.head⟩ :: toList a.tail

@ -155,16 +40,16 @@ lemma toList_length : (toList a).length = l.length := by
    simp only [toList, List.length_cons, Fin.zero_eta]
    rw [ih]

-lemma toList_tail : {l : List I} → (a : CreatAnnilateSect f l) → toList a.tail = (toList a).tail
+lemma toList_tail : {l : List I} → (a : CreateAnnilateSect f l) → toList a.tail = (toList a).tail
  | [], _ => rfl
  | i :: l, a => by
    simp [toList]

-lemma toList_cons {i : I} (a : CreatAnnilateSect f (i :: l)) :
+lemma toList_cons {i : I} (a : CreateAnnilateSect f (i :: l)) :
    (toList a) = ⟨i, a.head⟩ :: toList a.tail := by
  rfl

-lemma toList_get (a : CreatAnnilateSect f l) :
+lemma toList_get (a : CreateAnnilateSect f l) :
    (toList a).get = (fun i => ⟨l.get i, a i⟩) ∘ Fin.cast (by simp) := by
  induction l with
  | nil =>
@ -206,7 +91,7 @@ lemma toList_grade (q : I → Fin 2) :

@[simp]
 lemma toList_grade_take {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
-    (q : I → Fin 2) : (r : List I) → (a : CreatAnnilateSect f r) → (n : ℕ) →
+    (q : I → Fin 2) : (r : List I) → (a : CreateAnnilateSect f r) → (n : ℕ) →
    grade (fun i => q i.fst) (List.take n a.toList) = grade q (List.take n r)
  | [], _, _ => by
    simp [toList]
@ -217,12 +102,12 @@ lemma toList_grade_take {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
    rw [toList_grade_take q r a.tail n]

 def extractEquiv {I : Type} {f : I → Type} [(i : I) → Fintype (f i)] {l : List I}
-    (n : Fin l.length) : CreatAnnilateSect f l ≃
-    f (l.get n) × CreatAnnilateSect f (l.eraseIdx n) := by
+    (n : Fin l.length) : CreateAnnilateSect f l ≃
+    f (l.get n) × CreateAnnilateSect f (l.eraseIdx n) := by
  match l with
  | [] => exact Fin.elim0 n
  | l0 :: l =>
-    let e1 : CreatAnnilateSect f ((l0 :: l).eraseIdx n) ≃ Π i, f ((l0 :: l).get (n.succAbove i)) :=
+    let e1 : CreateAnnilateSect f ((l0 :: l).eraseIdx n) ≃ Π i, f ((l0 :: l).get (n.succAbove i)) :=
      Equiv.piCongr (Fin.castOrderIso (by rw [eraseIdx_cons_length])).toEquiv
      fun x => Equiv.cast (congrArg f (by
      rw [HepLean.List.eraseIdx_get]
@ -252,15 +137,15 @@ def extractEquiv {I : Type} {f : I → Type} [(i : I) → Fintype (f i)] {l : Li
    exact (Fin.insertNthEquiv _ _).symm.trans (Equiv.prodCongr (Equiv.refl _) e1.symm)

 lemma extractEquiv_symm_toList_get_same {I : Type} {f : I → Type} [(i : I) → Fintype (f i)]
-    {l : List I} (n : Fin l.length) (a0 : f (l.get n)) (a : CreatAnnilateSect f (l.eraseIdx n)) :
+    {l : List I} (n : Fin l.length) (a0 : f (l.get n)) (a : CreateAnnilateSect f (l.eraseIdx n)) :
    ((extractEquiv n).symm (a0, a)).toList[n] = ⟨l[n], a0⟩ := by
  match l with
  | [] => exact Fin.elim0 n
  | l0 :: l =>
-    trans (((CreatAnnilateSect.extractEquiv n).symm (a0, a)).toList).get (Fin.cast (by simp) n)
+    trans (((CreateAnnilateSect.extractEquiv n).symm (a0, a)).toList).get (Fin.cast (by simp) n)
    · simp only [List.length_cons, List.get_eq_getElem, Fin.coe_cast]
      rfl
-    rw [CreatAnnilateSect.toList_get]
+    rw [CreateAnnilateSect.toList_get]
    simp only [List.get_eq_getElem, List.length_cons, extractEquiv, RelIso.coe_fn_toEquiv,
      Fin.castOrderIso_apply, Equiv.symm_trans_apply, Equiv.symm_symm, Equiv.prodCongr_symm,
      Equiv.refl_symm, Equiv.prodCongr_apply, Equiv.coe_refl, Prod.map_apply, id_eq,
@ -270,11 +155,11 @@ lemma extractEquiv_symm_toList_get_same {I : Type} {f : I → Type} [(i : I) →
    erw [Fin.insertNthEquiv_apply]
    simp only [Fin.insertNth_apply_same]

-def eraseIdx (n : Fin l.length) : CreatAnnilateSect f (l.eraseIdx n) :=
+def eraseIdx (n : Fin l.length) : CreateAnnilateSect f (l.eraseIdx n) :=
  (extractEquiv n a).2

@[simp]
-lemma eraseIdx_zero_tail {i : I} {l : List I} (a : CreatAnnilateSect f (i :: l)) :
+lemma eraseIdx_zero_tail {i : I} {l : List I} (a : CreateAnnilateSect f (i :: l)) :
    (eraseIdx a (@OfNat.ofNat (Fin (l.length + 1)) 0 Fin.instOfNat : Fin (l.length + 1))) =
    a.tail := by
  simp only [List.length_cons, Fin.val_zero, List.eraseIdx_cons_zero, eraseIdx, List.get_eq_getElem,
@ -284,7 +169,7 @@ lemma eraseIdx_zero_tail {i : I} {l : List I} (a : CreatAnnilateSect f (i :: l))
  rfl

 lemma eraseIdx_succ_head {i : I} {l : List I} (n : ℕ) (hn : n + 1 < (i :: l).length)
-    (a : CreatAnnilateSect f (i :: l)) : (eraseIdx a ⟨n + 1, hn⟩).head = a.head := by
+    (a : CreateAnnilateSect f (i :: l)) : (eraseIdx a ⟨n + 1, hn⟩).head = a.head := by
  rw [eraseIdx, extractEquiv]
  simp only [List.length_cons, List.get_eq_getElem, List.getElem_cons_succ, List.eraseIdx_cons_succ,
    RelIso.coe_fn_toEquiv, Fin.castOrderIso_apply, Equiv.trans_apply, Equiv.prodCongr_apply,
@ -305,7 +190,7 @@ lemma eraseIdx_succ_head {i : I} {l : List I} (n : ℕ) (hn : n + 1 < (i :: l).l
  simp [Fin.ext_iff]

 lemma eraseIdx_succ_tail {i : I} {l : List I} (n : ℕ) (hn : n + 1 < (i :: l).length)
-    (a : CreatAnnilateSect f (i :: l)) :
+    (a : CreateAnnilateSect f (i :: l)) :
    (eraseIdx a ⟨n + 1, hn⟩).tail = eraseIdx a.tail ⟨n, Nat.succ_lt_succ_iff.mp hn⟩ := by
  match l with
  | [] =>
@ -365,7 +250,7 @@ lemma eraseIdx_succ_tail {i : I} {l : List I} (n : ℕ) (hn : n + 1 < (i :: l).l
      omega
    next h_1 => simp_all only [not_lt, Fin.val_succ, Fin.coe_cast]

-lemma eraseIdx_toList : {l : List I} → {n : Fin l.length} → (a : CreatAnnilateSect f l) →
+lemma eraseIdx_toList : {l : List I} → {n : Fin l.length} → (a : CreateAnnilateSect f l) →
    (eraseIdx a n).toList = a.toList.eraseIdx n
  | [], n, _ => Fin.elim0 n
  | r0 :: r, ⟨0, h⟩, a => by
@ -379,7 +264,7 @@ lemma eraseIdx_toList : {l : List I} → {n : Fin l.length} → (a : CreatAnnila
      rw [eraseIdx_succ_tail]

 lemma extractEquiv_symm_eraseIdx {I : Type} {f : I → Type} [(i : I) → Fintype (f i)]
-    {l : List I} (n : Fin l.length) (a0 : f l[↑n]) (a : CreatAnnilateSect f (l.eraseIdx n)) :
+    {l : List I} (n : Fin l.length) (a0 : f l[↑n]) (a : CreateAnnilateSect f (l.eraseIdx n)) :
    ((extractEquiv n).symm (a0, a)).eraseIdx n = a := by
  match l with
  | [] => exact Fin.elim0 n
@ -389,7 +274,7 @@ lemma extractEquiv_symm_eraseIdx {I : Type} {f : I → Type} [(i : I) → Fintyp

 lemma toList_koszulSignInsert {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
    (q : I → Fin 2) (le1 : I → I → Prop) [DecidableRel le1]
-    (l : List I) (a : CreatAnnilateSect f l) (x : (i : I) × f i) :
+    (l : List I) (a : CreateAnnilateSect f l) (x : (i : I) × f i) :
    koszulSignInsert (fun i j => le1 i.fst j.fst) (fun i => q i.fst) x a.toList =
    koszulSignInsert le1 q x.1 l := by
  induction l with
@ -400,7 +285,7 @@ lemma toList_koszulSignInsert {I : Type} {f : I → Type} [∀ i, Fintype (f i)]

 lemma toList_koszulSign {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
    (q : I → Fin 2) (le1 : I → I → Prop) [DecidableRel le1]
-    (l : List I) (a : CreatAnnilateSect f l) :
+    (l : List I) (a : CreateAnnilateSect f l) :
    koszulSign (fun i j => le1 i.fst j.fst) (fun i => q i.fst) a.toList =
    koszulSign le1 q l := by
  induction l with
@ -413,7 +298,7 @@ lemma toList_koszulSign {I : Type} {f : I → Type} [∀ i, Fintype (f i)]

 lemma insertionSortEquiv_toList {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
    (le1 : I → I → Prop) [DecidableRel le1](l : List I)
-      (a : CreatAnnilateSect f l) :
+      (a : CreateAnnilateSect f l) :
    insertionSortEquiv (fun i j => le1 i.fst j.fst) a.toList =
    (Fin.castOrderIso (by simp)).toEquiv.trans ((insertionSortEquiv le1 l).trans
    (Fin.castOrderIso (by simp)).toEquiv) := by
@ -466,7 +351,7 @@ lemma insertionSortEquiv_toList {I : Type} {f : I → Type} [∀ i, Fintype (f i
    have h3 : (List.insertionSort le1 (List.map (fun i => i.1) a.tail.toList)) =
      List.insertionSort le1 l := by
      congr
-      have h3' (l : List I) (a : CreatAnnilateSect f l) :
+      have h3' (l : List I) (a : CreateAnnilateSect f l) :
        List.map (fun i => i.1) a.toList = l := by
        induction l with
        | nil => rfl
@ -481,14 +366,14 @@ lemma insertionSortEquiv_toList {I : Type} {f : I → Type} [∀ i, Fintype (f i
      Fin.cast_trans, Fin.cast_eq_self, Fin.coe_cast]
    rfl

-def sort (le1 : I → I → Prop) [DecidableRel le1] : CreatAnnilateSect f (List.insertionSort le1 l) :=
+def sort (le1 : I → I → Prop) [DecidableRel le1] : CreateAnnilateSect f (List.insertionSort le1 l) :=
  Equiv.piCongr (HepLean.List.insertionSortEquiv le1 l) (fun i => (Equiv.cast (by
      congr 1
      rw [← HepLean.List.insertionSortEquiv_get]
      simp))) a

 lemma sort_toList {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
-    (le1 : I → I → Prop) [DecidableRel le1] (l : List I) (a : CreatAnnilateSect f l) :
+    (le1 : I → I → Prop) [DecidableRel le1] (l : List I) (a : CreateAnnilateSect f l) :
    (a.sort le1).toList = List.insertionSort (fun i j => le1 i.fst j.fst) a.toList := by
  let l1 := List.insertionSort (fun i j => le1 i.fst j.fst) a.toList
  let l2 := (a.sort le1).toList
@ -516,66 +401,6 @@ lemma sort_toList {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
  rw [hget]
  simp

-end CreatAnnilateSect
+end CreateAnnilateSect

-lemma ofListM_expand {I : Type} (f : I → Type) [∀ i, Fintype (f i)] (x : ℂ) :
-    (l : List I) → ofListM f l x = ∑ (a : CreatAnnilateSect f l), ofList a.toList x
-  | [] => by
-    simp only [ofListM, CreatAnnilateSect, List.length_nil, List.get_eq_getElem, Finset.univ_unique,
-      CreatAnnilateSect.toList, Finset.sum_const, Finset.card_singleton, one_smul]
-    rw [ofList_eq_smul_one, map_smul, ofList_empty, ofList_eq_smul_one, ofList_empty, map_one]
-  | i :: l => by
-    rw [ofListM_cons, ofListM_expand f x l]
-    conv_rhs => rw [← (CreatAnnilateSect.extractEquiv
-        ⟨0, by exact Nat.zero_lt_succ l.length⟩).symm.sum_comp (α := FreeAlgebra ℂ _)]
-    erw [Finset.sum_product]
-    rw [Finset.sum_mul]
-    conv_lhs =>
-      rhs
-      intro n
-      rw [Finset.mul_sum]
-    congr
-    funext j
-    congr
-    funext n
-    rw [← ofList_singleton, ← ofList_pair, one_mul]
-    rfl
-
-lemma koszulOrder_ofListM {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
-    (q : I → Fin 2) (le1 : I → I → Prop) [DecidableRel le1]
-    (l : List I) (x : ℂ) : koszulOrder (fun i j => le1 i.1 j.1) (fun i => q i.fst) (ofListM f l x) =
-    freeAlgebraMap f (koszulOrder le1 q (ofList l x)) := by
-  rw [koszulOrder_ofList]
-  rw [map_smul]
-  change _ = _ • ofListM _ _ _
-  rw [ofListM_expand]
-  rw [map_sum]
-  conv_lhs =>
-    rhs
-    intro a
-    rw [koszulOrder_ofList]
-    rw [CreatAnnilateSect.toList_koszulSign]
-  rw [← Finset.smul_sum]
-  apply congrArg
-  conv_lhs =>
-    rhs
-    intro n
-    rw [← CreatAnnilateSect.sort_toList]
-  rw [ofListM_expand]
-  refine Fintype.sum_equiv
-    ((HepLean.List.insertionSortEquiv le1 l).piCongr fun i => Equiv.cast ?_) _ _ ?_
-  congr 1
-  · rw [← HepLean.List.insertionSortEquiv_get]
-    simp
-  · intro x
-    rfl
-
-lemma koszulOrder_ofListM_eq_ofListM {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
-    (q : I → Fin 2) (le1 : I → I → Prop) [DecidableRel le1]
-    (l : List I) (x : ℂ) : koszulOrder (fun i j => le1 i.1 j.1) (fun i => q i.fst) (ofListM f l x) =
-    koszulSign le1 q l • ofListM f (List.insertionSort le1 l) x := by
-  rw [koszulOrder_ofListM, koszulOrder_ofList, map_smul]
-  rfl
-
-end
 end Wick
--- a/HepLean/PerturbationTheory/Wick/Koszul/Grade.lean
+++ b/HepLean/PerturbationTheory/Wick/Koszul/Grade.lean
@ -1,636 +0,0 @@
-/-
-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.Mathematics.List
-import HepLean.PerturbationTheory.Wick.Koszul.Order
-/-!
-
-# Koszul signs and ordering for lists and algebras
-
-/
-
-namespace Wick
-open HepLean.List
-
-def grade {I : Type} (q : I → Fin 2) : (l : List I) → Fin 2
-  | [] => 0
-  | a :: l => if q a = grade q l then 0 else 1
-
-@[simp]
-lemma grade_freeMonoid {I : Type} (q : I → Fin 2) (i : I) : grade q (FreeMonoid.of i) = q i := by
-  simp only [grade, Fin.isValue]
-  have ha (a : Fin 2) : (if a = 0 then 0 else 1) = a := by
-    fin_cases a <;> rfl
-  rw [ha]
-
-@[simp]
-lemma grade_empty {I : Type} (q : I → Fin 2) : grade q [] = 0 := by
-  simp [grade]
-
-@[simp]
-lemma grade_append {I : Type} (q : I → Fin 2) (l r : List I) :
-    grade q (l ++ r) = if grade q l = grade q r then 0 else 1 := by
-  induction l with
-  | nil =>
-    simp only [List.nil_append, grade_empty, Fin.isValue]
-    have ha (a : Fin 2) : (if 0 = a then 0 else 1) = a := by
-      fin_cases a <;> rfl
-    exact Eq.symm (Fin.eq_of_val_eq (congrArg Fin.val (ha (grade q r))))
-  | cons a l ih =>
-    simp only [grade, List.append_eq, Fin.isValue]
-    erw [ih]
-    have hab (a b c : Fin 2) : (if a = if b = c then 0 else 1 then (0 : Fin 2) else 1) =
-        if (if a = b then 0 else 1) = c then 0 else 1 := by
-      fin_cases a <;> fin_cases b <;> fin_cases c <;> rfl
-    exact hab (q a) (grade q l) (grade q r)
-
-lemma grade_orderedInsert {I : Type} (q : I → Fin 2) (le1 : I → I → Prop) [DecidableRel le1]
-    (l : List I) (i : I) : grade q (List.orderedInsert le1 i l) = grade q (i :: l) := by
-  induction l with
-  | nil => simp
-  | cons j l ih =>
-    simp only [List.orderedInsert]
-    by_cases hij : le1 i j
-    · simp [hij]
-    · simp only [hij, ↓reduceIte]
-      rw [grade]
-      rw [ih]
-      simp only [grade, Fin.isValue]
-      have h1 (a b c : Fin 2) : (if a = if b = c then 0 else 1 then (0 : Fin 2) else 1) =
-          if b = if a = c then 0 else 1 then 0 else 1 := by
-        fin_cases a <;> fin_cases b <;> fin_cases c <;> rfl
-      exact h1 _ _ _
-
-@[simp]
-lemma grade_insertionSort {I : Type} (q : I → Fin 2) (le1 : I → I → Prop) [DecidableRel le1]
-    (l : List I) : grade q (List.insertionSort le1 l) = grade q l := by
-  induction l with
-  | nil => simp
-  | cons j l ih =>
-    simp only [List.insertionSort, grade, Fin.isValue]
-    rw [grade_orderedInsert]
-    simp only [grade, Fin.isValue]
-    rw [ih]
-
-lemma grade_count {I : Type} (q : I → Fin 2) (l : List I) :
-    grade q l = if Nat.mod (List.countP (fun i => decide (q i = 1)) l) 2 = 0 then 0 else 1 := by
-  induction l with
-  | nil => simp
-  | cons r0 r ih =>
-    simp only [grade, Fin.isValue]
-    rw [List.countP_cons]
-    simp only [Fin.isValue, decide_eq_true_eq]
-    rw [ih]
-    by_cases h: q r0 = 1
-    · simp only [h, Fin.isValue, ↓reduceIte]
-      split
-      next h1 =>
-        simp_all only [Fin.isValue, ↓reduceIte, one_ne_zero]
-        split
-        next h2 =>
-          simp_all only [Fin.isValue, one_ne_zero]
-          have ha (a : ℕ) (ha : a % 2 = 0) : (a + 1) % 2 ≠ 0 := by
-            omega
-          exact ha (List.countP (fun i => decide (q i = 1)) r) h1 h2
-        next h2 => simp_all only [Fin.isValue]
-      next h1 =>
-        simp_all only [Fin.isValue, ↓reduceIte]
-        split
-        next h2 => simp_all only [Fin.isValue]
-        next h2 =>
-          simp_all only [Fin.isValue, zero_ne_one]
-          have ha (a : ℕ) (ha : ¬ a % 2 = 0) : (a + 1) % 2 = 0 := by
-            omega
-          exact h2 (ha (List.countP (fun i => decide (q i = 1)) r) h1)
-    · have h0 : q r0 = 0 := by omega
-      simp only [h0, Fin.isValue, zero_ne_one, ↓reduceIte, add_zero]
-      by_cases hn : (List.countP (fun i => decide (q i = 1)) r).mod 2 = 0
-      · simp [hn]
-      · simp [hn]
-
-lemma grade_perm {I : Type} (q : I → Fin 2) {l l' : List I} (h : l.Perm l') :
-    grade q l = grade q l' := by
-  rw [grade_count, grade_count, h.countP_eq]
-
-def superCommuteCoef {I : Type} (q : I → Fin 2) (la lb : List I) : ℂ :=
-  if grade q la = 1 ∧ grade q lb = 1 then - 1 else 1
-
-lemma superCommuteCoef_comm {I : Type} (q : I → Fin 2) (la lb : List I) :
-    superCommuteCoef q la lb = superCommuteCoef q lb la := by
-  simp only [superCommuteCoef, Fin.isValue]
-  congr 1
-  exact Eq.propIntro (fun a => id (And.symm a)) fun a => id (And.symm a)
-
-lemma superCommuteCoef_perm_snd {I : Type} (q : I → Fin 2) (la lb lb' : List I)
-    (h : lb.Perm lb') :
-    superCommuteCoef q la lb = superCommuteCoef q la lb' := by
-  rw [superCommuteCoef, superCommuteCoef, grade_perm q h]
-
-lemma superCommuteCoef_mul_self {I : Type} (q : I → Fin 2) (l lb : List I) :
-    superCommuteCoef q l lb * superCommuteCoef q l lb = 1 := by
-  simp only [superCommuteCoef, Fin.isValue, mul_ite, mul_neg, mul_one]
-  have ha (a b : Fin 2) : (if a = 1 ∧ b = 1 then -if a = 1 ∧ b = 1 then -1 else 1
-    else if a = 1 ∧ b = 1 then -1 else 1) = (1 : ℂ) := by
-      fin_cases a <;> fin_cases b
-      any_goals rfl
-      simp
-  exact ha (grade q l) (grade q lb)
-
-lemma superCommuteCoef_empty {I : Type} (q : I → Fin 2) (la : List I) :
-    superCommuteCoef q la [] = 1 := by
-  simp only [superCommuteCoef, Fin.isValue, grade_empty, zero_ne_one, and_false, ↓reduceIte]
-
-lemma superCommuteCoef_append {I : Type} (q : I → Fin 2) (la lb lc : List I) :
-    superCommuteCoef q la (lb ++ lc) = superCommuteCoef q la lb * superCommuteCoef q la lc := by
-  simp only [superCommuteCoef, Fin.isValue, grade_append, ite_eq_right_iff, zero_ne_one, imp_false,
-    mul_ite, mul_neg, mul_one]
-  by_cases hla : grade q la = 1
-  · by_cases hlb : grade q lb = 1
-    · by_cases hlc : grade q lc = 1
-      · simp [hlc, hlb, hla]
-      · have hc : grade q lc = 0 := by
-          omega
-        simp [hc, hlb, hla]
-    · have hb : grade q lb = 0 := by
-        omega
-      by_cases hlc : grade q lc = 1
-      · simp [hlc, hb]
-      · have hc : grade q lc = 0 := by
-          omega
-        simp [hc, hb]
-  · have ha : grade q la = 0 := by
-      omega
-    simp [ha]
-
-lemma superCommuteCoef_cons {I : Type} (q : I → Fin 2) (i : I) (la lb : List I) :
-    superCommuteCoef q la (i :: lb) = superCommuteCoef q la [i] * superCommuteCoef q la lb := by
-  trans superCommuteCoef q la ([i] ++ lb)
-  simp only [List.singleton_append]
-  rw [superCommuteCoef_append]
-
-def superCommuteCoefM {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
-    (q : I → Fin 2) (l : List (Σ i, f i)) (r : List I) : ℂ :=
-    (if grade (fun i => q i.fst) l = 1 ∧ grade q r = 1 then -1 else 1)
-
-lemma superCommuteCoefM_empty {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
-    (q : I → Fin 2) (l : List (Σ i, f i)) :
-    superCommuteCoefM q l [] = 1 := by
-  simp [superCommuteCoefM]
-
-def superCommuteCoefLE {I : Type} (q : I → Fin 2) (le1 :I → I → Prop) (r : List I)
-    [DecidableRel le1] (i : I) (n : Fin r.length) : ℂ :=
-  koszulSign le1 q r *
-  superCommuteCoef q [i] (List.take (↑((HepLean.List.insertionSortEquiv le1 r) n))
-    (List.insertionSort le1 r)) *
-  koszulSign le1 q (r.eraseIdx ↑n)
-
-lemma superCommuteCoefLE_eq_q {I : Type} (q : I → Fin 2) (le1 :I → I → Prop) (r : List I)
-    [DecidableRel le1] (i : I) (n : Fin r.length)
-    (hq : q i = q (r.get n)) :
-    superCommuteCoefLE q le1 r i n =
-    koszulSign le1 q r *
-    superCommuteCoef q [r.get n] (List.take (↑(insertionSortEquiv le1 r n))
-      (List.insertionSort le1 r)) *
-    koszulSign le1 q (r.eraseIdx ↑n) := by
-  simp [superCommuteCoefLE, superCommuteCoef, grade, hq]
-
-lemma koszulSignInsert_eq_filter {I : Type} (q : I → Fin 2) (le1 : I → I → Prop) [DecidableRel le1]
-    (r0 : I) : (r : List I) →
-    koszulSignInsert le1 q r0 r =
-    koszulSignInsert le1 q r0 (List.filter (fun i => decide (¬ le1 r0 i)) r)
-  | [] => by
-    simp [koszulSignInsert]
-  | r1 :: r => by
-    dsimp only [koszulSignInsert, Fin.isValue]
-    simp only [Fin.isValue, List.filter, decide_not]
-    by_cases h : le1 r0 r1
-    · simp only [h, ↓reduceIte, decide_True, Bool.not_true]
-      rw [koszulSignInsert_eq_filter]
-      congr
-      simp
-    · simp only [h, ↓reduceIte, Fin.isValue, decide_False, Bool.not_false]
-      dsimp only [Fin.isValue, koszulSignInsert]
-      simp only [Fin.isValue, h, ↓reduceIte]
-      rw [koszulSignInsert_eq_filter]
-      congr
-      simp only [decide_not]
-      simp
-
-lemma koszulSignInsert_eq_grade {I : Type} (q : I → Fin 2) (le1 : I → I → Prop) [DecidableRel le1]
-    (r0 : I) (r : List I) : koszulSignInsert le1 q r0 r = if grade q [r0] = 1 ∧
-    grade q (List.filter (fun i => decide (¬ le1 r0 i)) r) = 1 then -1 else 1 := by
-  induction r with
-  | nil =>
-    simp [koszulSignInsert]
-  | cons r1 r ih =>
-    rw [koszulSignInsert_eq_filter]
-    by_cases hr1 : ¬ le1 r0 r1
-    · rw [List.filter_cons_of_pos]
-      · dsimp only [koszulSignInsert, Fin.isValue, decide_not]
-        rw [if_neg hr1]
-        dsimp only [Fin.isValue, grade, ite_eq_right_iff, zero_ne_one, imp_false, decide_not]
-        simp only [Fin.isValue, decide_not, ite_eq_right_iff, zero_ne_one, imp_false]
-        have ha (a b c : Fin 2) : (if a = 1 ∧ b = 1 then -if ¬a = 0 ∧
-          c = 1 then -1 else (1 : ℂ)
-          else if ¬a = 0 ∧ c = 1 then -1 else 1) =
-          if ¬a = 0 ∧ ¬b = c then -1 else 1 := by
-          fin_cases a <;> fin_cases b <;> fin_cases c
-          any_goals rfl
-          simp
-        rw [← ha (q r0) (q r1) (grade q (List.filter (fun a => !decide (le1 r0 a)) r))]
-        congr
-        · rw [koszulSignInsert_eq_filter] at ih
-          simpa [grade] using ih
-        · rw [koszulSignInsert_eq_filter] at ih
-          simpa [grade] using ih
-      · simp [hr1]
-    · rw [List.filter_cons_of_neg]
-      simp only [decide_not, Fin.isValue]
-      rw [koszulSignInsert_eq_filter] at ih
-      simpa [grade] using ih
-      simpa using hr1
-
-lemma koszulSignInsert_eq_perm {I : Type} (q : I → Fin 2) (le1 : I → I → Prop) (r r' : List I)
-    (a : I) [DecidableRel le1] (h : r.Perm r') :
-    koszulSignInsert le1 q a r = koszulSignInsert le1 q a r' := by
-  rw [koszulSignInsert_eq_grade]
-  rw [koszulSignInsert_eq_grade]
-  congr 1
-  simp only [Fin.isValue, decide_not, eq_iff_iff, and_congr_right_iff]
-  intro h'
-  have hg : grade q (List.filter (fun i => !decide (le1 a i)) r) =
-      grade q (List.filter (fun i => !decide (le1 a i)) r') := by
-    rw [grade_count, grade_count]
-    rw [List.countP_filter, List.countP_filter]
-    rw [h.countP_eq]
-  rw [hg]
-
-lemma koszulSignInsert_eq_sort {I : Type} (q : I → Fin 2) (le1 : I → I → Prop) (r : List I)
-    (a : I) [DecidableRel le1] :
-    koszulSignInsert le1 q a r = koszulSignInsert le1 q a (List.insertionSort le1 r) := by
-  apply koszulSignInsert_eq_perm
-  exact List.Perm.symm (List.perm_insertionSort le1 r)
-
-lemma koszulSignInsert_eq_cons {I : Type} (q : I → Fin 2) (le1 : I → I → Prop) [DecidableRel le1]
-    [IsTotal I le1] [IsTrans I le1] (r0 : I) (r : List I) :
-    koszulSignInsert le1 q r0 r = koszulSignInsert le1 q r0 (r0 :: r) := by
-  simp only [koszulSignInsert, Fin.isValue, and_self]
-  have h1 : le1 r0 r0 := by
-    simpa using IsTotal.total (r := le1) r0 r0
-  simp [h1]
-
-def insertSign {I : Type} (q : I → Fin 2) (n : ℕ)
-    (r0 : I) (r : List I) : ℂ :=
-  superCommuteCoef q [r0] (List.take n r)
-
-lemma take_insert_same {I : Type} (i : I) :
-    (n : ℕ) → (r : List I) →
-    List.take n (List.insertIdx n i r) = List.take n r
-  | 0, _ => by simp
-  | _+1, [] => by simp
-  | n+1, a::as => by
-    simp only [List.insertIdx_succ_cons, List.take_succ_cons, List.cons.injEq, true_and]
-    exact take_insert_same i n as
-
-lemma insertSign_insert {I : Type} (q : I → Fin 2) (n : ℕ)
-    (r0 : I) (r : List I) : insertSign q n r0 r = insertSign q n r0 (List.insertIdx n r0 r) := by
-  simp only [insertSign]
-  congr 1
-  rw [take_insert_same]
-
-lemma take_eraseIdx_same {I : Type} :
-    (n : ℕ) → (r : List I) →
-    List.take n (List.eraseIdx r n) = List.take n r
-  | 0, _ => by simp
-  | _+1, [] => by simp
-  | n+1, a::as => by
-    simp only [List.eraseIdx_cons_succ, List.take_succ_cons, List.cons.injEq, true_and]
-    exact take_eraseIdx_same n as
-
-lemma insertSign_eraseIdx {I : Type} (q : I → Fin 2) (n : ℕ)
-    (r0 : I) (r : List I) : insertSign q n r0 (r.eraseIdx n) = insertSign q n r0 r := by
-  simp only [insertSign]
-  congr 1
-  rw [take_eraseIdx_same]
-
-lemma insertSign_zero {I : Type} (q : I → Fin 2) (r0 : I) (r : List I) :
-    insertSign q 0 r0 r = 1 := by
-  simp [insertSign, superCommuteCoef]
-
-lemma insertSign_succ_cons {I : Type} (q : I → Fin 2) (n : ℕ)
-    (r0 r1 : I) (r : List I) : insertSign q (n + 1) r0 (r1 :: r) =
-    superCommuteCoef q [r0] [r1] * insertSign q n r0 r := by
-  simp only [insertSign, List.take_succ_cons]
-  rw [superCommuteCoef_cons]
-
-lemma take_insert_gt {I : Type} (i : I) :
-    (n m : ℕ) → (h : n < m) → (r : List I) →
-    List.take n (List.insertIdx m i r) = List.take n r
-  | 0, 0, _, _ => by simp
-  | 0, m + 1, _, _ => by simp
-  | n+1, m + 1, _, [] => by simp
-  | n+1, m + 1, h, a::as => by
-    simp only [List.insertIdx_succ_cons, List.take_succ_cons, List.cons.injEq, true_and]
-    refine take_insert_gt i n m (Nat.succ_lt_succ_iff.mp h) as
-
-lemma insertSign_insert_gt {I : Type} (q : I → Fin 2) (n m : ℕ)
-    (r0 r1 : I) (r : List I) (hn : n < m) :
-    insertSign q n r0 (List.insertIdx m r1 r) = insertSign q n r0 r := by
-  rw [insertSign, insertSign]
-  congr 1
-  exact take_insert_gt r1 n m hn r
-
-lemma take_insert_let {I : Type} (i : I) :
-    (n m : ℕ) → (h : m ≤ n) → (r : List I) → (hm : m ≤ r.length) →
-    (List.take (n + 1) (List.insertIdx m i r)).Perm (i :: List.take n r)
-  | 0, 0, h, _, _ => by simp
-  | m + 1, 0, h, r, _ => by simp
-  | n + 1, m + 1, h, [], hm => by
-    simp at hm
-  | n + 1, m + 1, h, a::as, hm => by
-    simp only [List.insertIdx_succ_cons, List.take_succ_cons]
-    have hp : (i :: a :: List.take n as).Perm (a :: i :: List.take n as) := by
-      exact List.Perm.swap a i (List.take n as)
-    refine List.Perm.trans ?_ hp.symm
-    refine List.Perm.cons a ?_
-    exact take_insert_let i n m (Nat.le_of_succ_le_succ h) as (Nat.le_of_succ_le_succ hm)
-
-lemma insertSign_insert_lt_eq_insertSort {I : Type} (q : I → Fin 2) (n m : ℕ)
-    (r0 r1 : I) (r : List I) (hn : m ≤ n) (hm : m ≤ r.length) :
-    insertSign q (n + 1) r0 (List.insertIdx m r1 r) = insertSign q (n + 1) r0 (r1 :: r) := by
-  rw [insertSign, insertSign]
-  apply superCommuteCoef_perm_snd
-  simp only [List.take_succ_cons]
-  refine take_insert_let r1 n m hn r hm
-
-lemma insertSign_insert_lt {I : Type} (q : I → Fin 2) (n m : ℕ)
-    (r0 r1 : I) (r : List I) (hn : m ≤ n) (hm : m ≤ r.length) :
-    insertSign q (n + 1) r0 (List.insertIdx m r1 r) = superCommuteCoef q [r0] [r1] *
-    insertSign q n r0 r := by
-  rw [insertSign_insert_lt_eq_insertSort, insertSign_succ_cons]
-  exact hn
-  exact hm
-
-def koszulSignCons {I : Type} (q : I → Fin 2) (le1 : I → I → Prop) [DecidableRel le1] (r0 r1 : I) :
-    ℂ :=
-  if le1 r0 r1 then 1 else
-  if q r0 = 1 ∧ q r1 = 1 then -1 else 1
-
-lemma koszulSignCons_eq_superComuteCoef {I : Type} (q : I → Fin 2) (le1 : I → I → Prop)
-    [DecidableRel le1] (r0 r1 : I) : koszulSignCons q le1 r0 r1 =
-    if le1 r0 r1 then 1 else superCommuteCoef q [r0] [r1] := by
-  simp only [koszulSignCons, Fin.isValue, superCommuteCoef, grade, ite_eq_right_iff, zero_ne_one,
-    imp_false]
-  congr 1
-  by_cases h0 : q r0 = 1
-  · by_cases h1 : q r1 = 1
-    · simp [h0, h1]
-    · have h1 : q r1 = 0 := by omega
-      simp [h0, h1]
-  · have h0 : q r0 = 0 := by omega
-    by_cases h1 : q r1 = 1
-    · simp [h0, h1]
-    · have h1 : q r1 = 0 := by omega
-      simp [h0, h1]
-
-lemma koszulSignInsert_cons {I : Type} (q : I → Fin 2) (le1 : I → I → Prop) [DecidableRel le1]
-    [IsTotal I le1] [IsTrans I le1] (r0 r1 : I) (r : List I) :
-    koszulSignInsert le1 q r0 (r1 :: r) = koszulSignCons q le1 r0 r1 *
-    koszulSignInsert le1 q r0 r := by
-  simp [koszulSignInsert, koszulSignCons]
-
-lemma koszulSignInsert_eq_insertSign {I : Type} (q : I → Fin 2) (le1 : I → I → Prop)
-    [DecidableRel le1] [IsTotal I le1] [IsTrans I le1] (r0 : I) (r : List I) :
-    koszulSignInsert le1 q r0 r = insertSign q (orderedInsertPos le1 (List.insertionSort le1 r) r0)
-      r0 (List.insertionSort le1 r) := by
-  rw [koszulSignInsert_eq_cons, koszulSignInsert_eq_sort, koszulSignInsert_eq_filter,
-    koszulSignInsert_eq_grade, insertSign, superCommuteCoef]
-  congr
-  simp only [List.filter_filter, Bool.and_self]
-  rw [List.insertionSort]
-  nth_rewrite 1 [List.orderedInsert_eq_take_drop]
-  rw [List.filter_append]
-  have h1 : List.filter (fun a => decide ¬le1 r0 a)
-    (List.takeWhile (fun b => decide ¬le1 r0 b) (List.insertionSort le1 r))
-    = (List.takeWhile (fun b => decide ¬le1 r0 b) (List.insertionSort le1 r)) := by
-    induction r with
-    | nil => simp
-    | cons r1 r ih =>
-      simp only [decide_not, List.insertionSort, List.filter_eq_self, Bool.not_eq_eq_eq_not,
-        Bool.not_true, decide_eq_false_iff_not]
-      intro a ha
-      have ha' := List.mem_takeWhile_imp ha
-      simp_all
-  rw [h1]
-  rw [List.filter_cons]
-  simp only [decide_not, (IsTotal.to_isRefl le1).refl r0, not_true_eq_false, decide_False,
-    Bool.false_eq_true, ↓reduceIte]
-  rw [orderedInsertPos_take]
-  simp only [decide_not, List.append_right_eq_self, List.filter_eq_nil_iff, Bool.not_eq_eq_eq_not,
-    Bool.not_true, decide_eq_false_iff_not, Decidable.not_not]
-  intro a ha
-  refine List.Sorted.rel_of_mem_take_of_mem_drop
-    (k := (orderedInsertPos le1 (List.insertionSort le1 r) r0).1 + 1)
-    (List.sorted_insertionSort le1 (r0 :: r)) ?_ ?_
-  · simp only [List.insertionSort, List.orderedInsert_eq_take_drop, decide_not]
-    rw [List.take_append_eq_append_take]
-    rw [List.take_of_length_le]
-    · simp [orderedInsertPos]
-    · simp [orderedInsertPos]
-  · simp only [List.insertionSort, List.orderedInsert_eq_take_drop, decide_not]
-    rw [List.drop_append_eq_append_drop]
-    rw [List.drop_of_length_le]
-    · simpa [orderedInsertPos] using ha
-    · simp [orderedInsertPos]
-
-lemma koszulSignInsert_insertIdx {I : Type} (q : I → Fin 2) (le1 : I → I → Prop) [DecidableRel le1]
-    (i j : I) [IsTotal I le1] [IsTrans I le1] (r : List I) (n : ℕ) (hn : n ≤ r.length) :
-    koszulSignInsert le1 q j (List.insertIdx n i r) = koszulSignInsert le1 q j (i :: r) := by
-  apply koszulSignInsert_eq_perm
-  exact List.perm_insertIdx i r hn
-
-lemma take_insertIdx {I : Type} (i : I) : (r : List I) → (n : ℕ) → (hn : n ≤ r.length) →
-    List.take n (List.insertIdx n i r) = List.take n r
-  | [], 0, h => by
-    simp
-  | [], n + 1, h => by
-    simp at h
-  | r0 :: r, 0, h => by
-    simp
-  | r0 :: r, n + 1, h => by
-    simp only [List.insertIdx_succ_cons, List.take_succ_cons, List.cons.injEq, true_and]
-    exact take_insertIdx i r n (Nat.le_of_lt_succ h)
-
-lemma koszulSign_insertIdx {I : Type} (q : I → Fin 2) (le1 : I → I → Prop) [DecidableRel le1]
-    (i : I) [IsTotal I le1] [IsTrans I le1] : (r : List I) → (n : ℕ) → (hn : n ≤ r.length) →
-    koszulSign le1 q (List.insertIdx n i r) = insertSign q n i r
-      * koszulSign le1 q r
-      * insertSign q (insertionSortEquiv le1 (List.insertIdx n i r) ⟨n, by
-        rw [List.length_insertIdx _ _ hn]
-        omega⟩) i
-        (List.insertionSort le1 (List.insertIdx n i r))
-  | [], 0, h => by
-    simp [koszulSign, insertSign, superCommuteCoef, koszulSignInsert]
-  | [], n + 1, h => by
-    simp at h
-  | r0 :: r, 0, h => by
-    simp only [List.insertIdx_zero, List.insertionSort, List.length_cons, Fin.zero_eta]
-    rw [koszulSign]
-    trans koszulSign le1 q (r0 :: r) * koszulSignInsert le1 q i (r0 :: r)
-    ring
-    simp only [insertionSortEquiv, List.length_cons, Nat.succ_eq_add_one, List.insertionSort,
-      orderedInsertEquiv, OrderIso.toEquiv_symm, Fin.symm_castOrderIso, HepLean.Fin.equivCons_trans,
-      Equiv.trans_apply, HepLean.Fin.equivCons_zero, HepLean.Fin.finExtractOne_apply_eq,
-      Fin.isValue, HepLean.Fin.finExtractOne_symm_inl_apply, RelIso.coe_fn_toEquiv,
-      Fin.castOrderIso_apply, Fin.cast_mk, Fin.eta]
-    conv_rhs =>
-      rhs
-      rhs
-      rw [orderedInsert_eq_insertIdx_orderedInsertPos]
-    conv_rhs =>
-      rhs
-      rw [← insertSign_insert]
-      change insertSign q (↑(orderedInsertPos le1 ((List.insertionSort le1 (r0 :: r))) i)) i
-        (List.insertionSort le1 (r0 :: r))
-      rw [← koszulSignInsert_eq_insertSign q le1]
-    rw [insertSign_zero]
-    simp
-  | r0 :: r, n + 1, h => by
-    conv_lhs =>
-      rw [List.insertIdx_succ_cons]
-      rw [koszulSign]
-    rw [koszulSign_insertIdx]
-    conv_rhs =>
-      rhs
-      simp only [List.insertIdx_succ_cons]
-      simp only [List.insertionSort, List.length_cons, insertionSortEquiv, Nat.succ_eq_add_one,
-        Equiv.trans_apply, HepLean.Fin.equivCons_succ]
-      erw [orderedInsertEquiv_fin_succ]
-      simp only [Fin.eta, Fin.coe_cast]
-      rhs
-      rw [orderedInsert_eq_insertIdx_orderedInsertPos]
-    conv_rhs =>
-      lhs
-      rw [insertSign_succ_cons, koszulSign]
-    ring_nf
-    conv_lhs =>
-      lhs
-      rw [mul_assoc, mul_comm]
-    rw [mul_assoc]
-    conv_rhs =>
-      rw [mul_assoc, mul_assoc]
-    congr 1
-    let rs := (List.insertionSort le1 (List.insertIdx n i r))
-    have hnsL : n < (List.insertIdx n i r).length := by
-      rw [List.length_insertIdx _ _]
-      simp only [List.length_cons, add_le_add_iff_right] at h
-      omega
-      exact Nat.le_of_lt_succ h
-    let ni : Fin rs.length := (insertionSortEquiv le1 (List.insertIdx n i r))
-      ⟨n, hnsL⟩
-    let nro : Fin (rs.length + 1) :=
-      ⟨↑(orderedInsertPos le1 rs r0), orderedInsertPos_lt_length le1 rs r0⟩
-    rw [koszulSignInsert_insertIdx, koszulSignInsert_cons]
-    trans koszulSignInsert le1 q r0 r * (koszulSignCons q le1 r0 i *insertSign q ni i rs)
-    · simp only [rs, ni]
-      ring
-    trans koszulSignInsert le1 q r0 r * (superCommuteCoef q [i] [r0] *
-          insertSign q (nro.succAbove ni) i (List.insertIdx nro r0 rs))
-    swap
-    · simp only [rs, nro, ni]
-      ring
-    congr 1
-    simp only [Fin.succAbove]
-    have hns : rs.get ni = i := by
-      simp only [Fin.eta, rs]
-      rw [← insertionSortEquiv_get]
-      simp only [Function.comp_apply, Equiv.symm_apply_apply, List.get_eq_getElem, ni]
-      simp_all only [List.length_cons, add_le_add_iff_right, List.getElem_insertIdx_self]
-    have hms : (List.orderedInsert le1 r0 rs).get ⟨nro, by simp⟩ = r0 := by
-      simp [nro]
-    have hc1 : ni.castSucc < nro → ¬ le1 r0 i := by
-      intro hninro
-      rw [← hns]
-      exact lt_orderedInsertPos_rel le1 r0 rs ni hninro
-    have hc2 : ¬ ni.castSucc < nro → le1 r0 i := by
-      intro hninro
-      rw [← hns]
-      refine gt_orderedInsertPos_rel le1 r0 rs ?_ ni hninro
-      exact List.sorted_insertionSort le1 (List.insertIdx n i r)
-    by_cases hn : ni.castSucc < nro
-    · simp only [hn, ↓reduceIte, Fin.coe_castSucc]
-      rw [insertSign_insert_gt]
-      swap
-      · exact hn
-      congr 1
-      rw [koszulSignCons_eq_superComuteCoef]
-      simp only [hc1 hn, ↓reduceIte]
-      rw [superCommuteCoef_comm]
-    · simp only [hn, ↓reduceIte, Fin.val_succ]
-      rw [insertSign_insert_lt]
-      rw [← mul_assoc]
-      congr 1
-      rw [superCommuteCoef_mul_self]
-      rw [koszulSignCons]
-      simp only [hc2 hn, ↓reduceIte]
-      exact Nat.le_of_not_lt hn
-      exact Nat.le_of_lt_succ (orderedInsertPos_lt_length le1 rs r0)
-    · exact Nat.le_of_lt_succ h
-    · exact Nat.le_of_lt_succ h
-
-lemma insertIdx_eraseIdx {I : Type} :
-    (n : ℕ) → (r : List I) → (hn : n < r.length) →
-    List.insertIdx n (r.get ⟨n, hn⟩) (r.eraseIdx n) = r
-  | n, [], hn => by
-    simp at hn
-  | 0, r0 :: r, hn => by
-    simp
-  | n + 1, r0 :: r, hn => by
-    simp only [List.length_cons, List.get_eq_getElem, List.getElem_cons_succ,
-      List.eraseIdx_cons_succ, List.insertIdx_succ_cons, List.cons.injEq, true_and]
-    exact insertIdx_eraseIdx n r _
-
-lemma superCommuteCoefLE_eq_get {I : Type} (q : I → Fin 2) (le1 :I → I → Prop) (r : List I)
-    [DecidableRel le1] [IsTotal I le1] [IsTrans I le1] (i : I) (n : Fin r.length)
-    (heq : q i = q (r.get n)) :
-    superCommuteCoefLE q le1 r i n = superCommuteCoef q [r.get n] (r.take n) := by
-  rw [superCommuteCoefLE_eq_q]
-  let r' := r.eraseIdx ↑n
-  have hr : List.insertIdx n (r.get n) (r.eraseIdx n) = r := by
-    exact insertIdx_eraseIdx n.1 r n.prop
-  conv_lhs =>
-    lhs
-    lhs
-    rw [← hr]
-    rw [koszulSign_insertIdx q le1 (r.get n) ((r.eraseIdx ↑n)) n (by
-      rw [List.length_eraseIdx]
-      simp only [Fin.is_lt, ↓reduceIte]
-      omega)]
-    rhs
-    rhs
-    rw [hr]
-  conv_lhs =>
-    lhs
-    lhs
-    rhs
-    enter [2, 1, 1]
-    rw [insertionSortEquiv_congr _ _ hr]
-  simp only [List.get_eq_getElem, Equiv.trans_apply, RelIso.coe_fn_toEquiv, Fin.castOrderIso_apply,
-    Fin.cast_mk, Fin.eta, Fin.coe_cast]
-  conv_lhs =>
-    lhs
-    rw [mul_assoc]
-    rhs
-    rw [insertSign]
-    rw [superCommuteCoef_mul_self]
-  simp only [mul_one]
-  rw [mul_assoc]
-  rw [koszulSign_mul_self]
-  simp only [mul_one]
-  rw [insertSign_eraseIdx]
-  rfl
-  exact heq
-
-end Wick
--- a/HepLean/PerturbationTheory/Wick/Koszul/SuperCommuteM.lean
+++ b/HepLean/PerturbationTheory/Wick/Koszul/SuperCommuteM.lean
@ -1,198 +0,0 @@
-/-
-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.PerturbationTheory.Wick.Koszul.SuperCommute
-/-!
-
-# Koszul signs and ordering for lists and algebras
-
-/
-
-namespace Wick
-
-noncomputable section
-
-lemma superCommute_ofList_ofListM {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
-    (q : I → Fin 2) (l : List (Σ i, f i)) (r : List I) (x y : ℂ) :
-    superCommute (fun i => q i.1) (ofList l x) (ofListM f r y) =
-    ofList l x * ofListM f r y +
-    (if grade (fun i => q i.1) l = 1 ∧ grade q r = 1 then
-    ofListM f r y * ofList l x else - ofListM f r y * ofList l x) := by
-  conv_lhs => rw [ofListM_expand]
-  rw [map_sum]
-  conv_rhs =>
-    lhs
-    rw [ofListM_expand, Finset.mul_sum]
-  conv_rhs =>
-    rhs
-    rhs
-    rw [ofListM_expand, ← Finset.sum_neg_distrib, Finset.sum_mul]
-  conv_rhs =>
-    rhs
-    lhs
-    rw [ofListM_expand, Finset.sum_mul]
-  rw [← Finset.sum_ite_irrel]
-  rw [← Finset.sum_add_distrib]
-  congr
-  funext a
-  rw [superCommute_ofList_ofList]
-  congr 1
-  · exact ofList_pair l a.toList x y
-  congr 1
-  · simp
-  · exact ofList_pair a.toList l y x
-  · rw [ofList_pair]
-    simp only [neg_mul]
-
-lemma superCommute_ofList_ofListM_superCommuteCoefM {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
-    (q : I → Fin 2) (l : List (Σ i, f i)) (r : List I) (x y : ℂ) :
-    superCommute (fun i => q i.1) (ofList l x) (ofListM f r y) =
-    ofList l x * ofListM f r y - superCommuteCoefM q l r • ofListM f r y * ofList l x := by
-  rw [superCommute_ofList_ofListM, superCommuteCoefM]
-  by_cases hq : grade (fun i => q i.fst) l = 1 ∧ grade q r = 1
-  · simp [hq]
-  · simp only [Fin.isValue, hq, ↓reduceIte, neg_mul, one_smul]
-    abel
-
-lemma ofList_ofListM_superCommute {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
-    (q : I → Fin 2) (l : List (Σ i, f i)) (r : List I) (x y : ℂ) :
-    ofList l x * ofListM f r y = superCommuteCoefM q l r • ofListM f r y * ofList l x
-    + superCommute (fun i => q i.1) (ofList l x) (ofListM f r y) := by
-  rw [superCommute_ofList_ofListM_superCommuteCoefM]
-  abel
-
-lemma ofListM_ofList_superCommute {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
-    (q : I → Fin 2) (l : List (Σ i, f i)) (r : List I) (x y : ℂ) :
-  ofListM f r y * ofList l x = superCommuteCoefM q l r • (ofList l x * ofListM f r y)
-    - superCommuteCoefM q l r • superCommute (fun i => q i.1) (ofList l x) (ofListM f r y) := by
-  rw [ofList_ofListM_superCommute, superCommuteCoefM]
-  by_cases hq : grade (fun i => q i.fst) l = 1 ∧ grade q r = 1
-  · simp [hq]
-  · simp [hq]
-
-lemma superCommuteCoefM_append {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
-    (q : I → Fin 2) (l : List (Σ i, f i)) (r1 r2 : List I) :
-    superCommuteCoefM q l (r1 ++ r2) = superCommuteCoefM q l r1 * superCommuteCoefM q l r2 := by
-  simp only [superCommuteCoefM, Fin.isValue, grade_append, ite_eq_right_iff, zero_ne_one, imp_false,
-    mul_ite, mul_neg, mul_one]
-  by_cases hla : grade (fun i => q i.1) l = 1
-  · by_cases hlb : grade q r1 = 1
-    · by_cases hlc : grade q r2 = 1
-      · simp [hlc, hlb, hla]
-      · have hc : grade q r2 = 0 := by
-          omega
-        simp [hc, hlb, hla]
-    · have hb : grade q r1 = 0 := by
-        omega
-      by_cases hlc : grade q r2 = 1
-      · simp [hlc, hb]
-      · have hc : grade q r2 = 0 := by
-          omega
-        simp [hc, hb]
-  · have ha : grade (fun i => q i.1) l = 0 := by
-      omega
-    simp [ha]
-
-def superCommuteTakeM {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
-    (q : I → Fin 2) (l : List (Σ i, f i)) (r : List I) (x y : ℂ) (n : ℕ)
-    (hn : n < r.length) : FreeAlgebra ℂ (Σ i, f i) :=
-  superCommuteCoefM q l (List.take n r) •
-  (ofListM f (List.take n r) 1 *
-  superCommute (fun i => q i.1) (ofList l x) (freeAlgebraMap f (FreeAlgebra.ι ℂ (r.get ⟨n, hn⟩)))
-  * ofListM f (List.drop (n + 1) r) y)
-
-lemma superCommuteM_ofList_cons {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
-    (q : I → Fin 2) (l : List (Σ i, f i)) (r : List I) (x y : ℂ) (b1 : I) :
-    superCommute (fun i => q i.1) (ofList l x) (ofListM f (b1 :: r) y) =
-    superCommute (fun i => q i.1) (ofList l x) (freeAlgebraMap f (FreeAlgebra.ι ℂ b1))
-    * ofListM f r y + superCommuteCoefM q l [b1] •
-    (ofListM f [b1] 1) * superCommute (fun i => q i.1) (ofList l x) (ofListM f r y) := by
-  rw [ofListM_cons]
-  conv_lhs =>
-    rhs
-    rw [ofListM_expand]
-    rw [Finset.mul_sum]
-  rw [map_sum]
-  trans ∑ (n : CreatAnnilateSect f r), ∑ j : f b1, ((superCommute fun i => q i.fst) (ofList l x))
-    ((FreeAlgebra.ι ℂ ⟨b1, j⟩) * ofList n.toList y)
-  · apply congrArg
-    funext n
-    rw [← map_sum]
-    congr
-    rw [Finset.sum_mul]
-  conv_rhs =>
-    lhs
-    rw [ofListM_expand, Finset.mul_sum]
-  conv_rhs =>
-    rhs
-    rhs
-    rw [ofListM_expand]
-    rw [map_sum]
-  conv_rhs =>
-    rhs
-    rw [Finset.mul_sum]
-  rw [← Finset.sum_add_distrib]
-  congr
-  funext n
-  rw [freeAlgebraMap_ι, map_sum, Finset.sum_mul]
-  conv_rhs =>
-    rhs
-    rw [ofListM_singleton]
-    rw [Finset.smul_sum, Finset.sum_mul]
-  rw [← Finset.sum_add_distrib]
-  congr
-  funext b
-  trans ((superCommute fun i => q i.fst) (ofList l x)) (ofList (⟨b1, b⟩ :: n.toList) y)
-  · congr
-    rw [ofList_cons_eq_ofList]
-    rw [ofList_singleton]
-  rw [superCommute_ofList_cons]
-  congr
-  rw [ofList_singleton]
-  simp
-
-lemma superCommute_ofList_ofListM_sum {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
-    (q : I → Fin 2) (l : List (Σ i, f i)) (r : List I) (x y : ℂ) :
-    superCommute (fun i => q i.1) (ofList l x) (ofListM f r y) =
-    ∑ (n : Fin r.length), superCommuteTakeM q l r x y n n.prop := by
-  induction r with
-  | nil =>
-    simp only [superCommute_ofList_ofListM, Fin.isValue, grade_empty, zero_ne_one, and_false,
-      ↓reduceIte, neg_mul, List.length_nil, Finset.univ_eq_empty, Finset.sum_empty]
-    rw [ofListM, ofList_empty']
-    simp
-  | cons b r ih =>
-    rw [superCommuteM_ofList_cons]
-    have h0 : ((superCommute fun i => q i.fst) (ofList l x))
-        ((freeAlgebraMap f) (FreeAlgebra.ι ℂ b)) * ofListM f r y =
-        superCommuteTakeM q l (b :: r) x y 0 (Nat.zero_lt_succ r.length) := by
-      simp [superCommuteTakeM, superCommuteCoefM_empty, ofListM_empty]
-    rw [h0]
-    have hf (g : Fin (b :: r).length → FreeAlgebra ℂ ((i : I) × f i)) : ∑ n, g n = g ⟨0,
-        Nat.zero_lt_succ r.length⟩ + ∑ n, g (Fin.succ n) := by
-      exact Fin.sum_univ_succAbove g ⟨0, Nat.zero_lt_succ r.length⟩
-    rw [hf]
-    congr
-    rw [ih]
-    rw [Finset.mul_sum]
-    congr
-    funext n
-    simp only [superCommuteTakeM, Fin.eta, List.get_eq_getElem, Algebra.mul_smul_comm,
-      Algebra.smul_mul_assoc, smul_smul, List.length_cons, Fin.val_succ, List.take_succ_cons,
-      List.getElem_cons_succ, List.drop_succ_cons]
-    congr 1
-    · rw [mul_comm, ← superCommuteCoefM_append]
-      rfl
-    · simp only [← mul_assoc, mul_eq_mul_right_iff]
-      apply Or.inl
-      apply Or.inl
-      rw [ofListM, ofListM, ofListM]
-      rw [← map_mul]
-      congr
-      rw [← ofList_pair, one_mul]
-      rfl
-
-end
-end Wick
--- a/HepLean/PerturbationTheory/Wick/Koszul/Order.lean
+++ b/HepLean/PerturbationTheory/Wick/Koszul/Order.lean
@ -6,6 +6,7 @@ Authors: Joseph Tooby-Smith
 import Mathlib.Algebra.FreeAlgebra
 import Mathlib.Algebra.Lie.OfAssociative
 import Mathlib.Analysis.Complex.Basic
+import HepLean.PerturbationTheory.Wick.Signs.StaticWickCoef
 /-!

 # Koszul signs and ordering for lists and algebras
@ -14,133 +15,6 @@ import Mathlib.Analysis.Complex.Basic

 namespace Wick

-/-- Gives a factor of `-1` when inserting `a` into a list `List I` in the ordered position
-  for each fermion-fermion cross. -/
-def koszulSignInsert {I : Type} (r : I → I → Prop) [DecidableRel r] (q : I → Fin 2) (a : I) :
-    List I → ℂ
-  | [] => 1
-  | b :: l => if r a b then koszulSignInsert r q a l else
-    if q a = 1 ∧ q b = 1 then - koszulSignInsert r q a l else koszulSignInsert r q a l
-
-/-- When inserting a boson the `koszulSignInsert` is always `1`. -/
-lemma koszulSignInsert_boson {I : Type} (r : I → I → Prop) [DecidableRel r] (q : I → Fin 2) (a : I)
-    (ha : q a = 0) : (l : List I) → koszulSignInsert r q a l = 1
-  | [] => by
-    simp [koszulSignInsert]
-  | b :: l => by
-    simp only [koszulSignInsert, Fin.isValue, ite_eq_left_iff]
-    rw [koszulSignInsert_boson r q a ha l, ha]
-    simp only [Fin.isValue, zero_ne_one, false_and, ↓reduceIte, ite_self]
-
-@[simp]
-lemma koszulSignInsert_mul_self {I : Type} (r : I → I → Prop) [DecidableRel r] (q : I → Fin 2)
-    (a : I) : (l : List I) → koszulSignInsert r q a l * koszulSignInsert r q a l = 1
-  | [] => by
-    simp [koszulSignInsert]
-  | b :: l => by
-    simp only [koszulSignInsert, Fin.isValue, mul_ite, ite_mul, neg_mul, mul_neg]
-    by_cases hr : r a b
-    · simp only [hr, ↓reduceIte]
-      rw [koszulSignInsert_mul_self]
-    · simp only [hr, ↓reduceIte, Fin.isValue]
-      by_cases hq : q a = 1 ∧ q b = 1
-      · simp only [hq, Fin.isValue, and_self, ↓reduceIte, neg_neg]
-        rw [koszulSignInsert_mul_self]
-      · simp only [Fin.isValue, hq, ↓reduceIte]
-        rw [koszulSignInsert_mul_self]
-
-lemma koszulSignInsert_le_forall {I : Type} (r : I → I → Prop) [DecidableRel r] (q : I → Fin 2)
-    (a : I) (l : List I) (hi : ∀ b, r a b) : koszulSignInsert r q a l = 1 := by
-  induction l with
-  | nil => rfl
-  | cons j l ih =>
-    simp only [koszulSignInsert, Fin.isValue, ite_eq_left_iff]
-    rw [ih]
-    simp only [Fin.isValue, ite_eq_left_iff, ite_eq_right_iff, and_imp]
-    intro h
-    exact False.elim (h (hi j))
-
-lemma koszulSignInsert_ge_forall_append {I : Type} (r : I → I → Prop) [DecidableRel r]
-    (q : I → Fin 2) (l : List I) (j i : I) (hi : ∀ j, r j i) :
-    koszulSignInsert r q j l = koszulSignInsert r q j (l ++ [i]) := by
-  induction l with
-  | nil => simp [koszulSignInsert, hi]
-  | cons b l ih =>
-    simp only [koszulSignInsert, Fin.isValue, List.append_eq]
-    by_cases hr : r j b
-    · rw [if_pos hr, if_pos hr]
-      rw [ih]
-    · rw [if_neg hr, if_neg hr]
-      rw [ih]
-
-/-- Gives a factor of `- 1` for every fermion-fermion (`q` is `1`) crossing that occurs when sorting
-  a list of based on `r`. -/
-def koszulSign {I : Type} (r : I → I → Prop) [DecidableRel r] (q : I → Fin 2) :
-    List I → ℂ
-  | [] => 1
-  | a :: l => koszulSignInsert r q a l * koszulSign r q l
-
-def natTestQ : ℕ → Fin 2 := fun n => if n % 2 = 0 then 0 else 1
-
-lemma koszulSign_mul_self {I : Type} (r : I → I → Prop) [DecidableRel r] (q : I → Fin 2)
-    (l : List I) : koszulSign r q l * koszulSign r q l = 1 := by
-  induction l with
-  | nil => simp [koszulSign]
-  | cons a l ih =>
-    simp only [koszulSign]
-    trans (koszulSignInsert r q a l * koszulSignInsert r q a l) *
-      (koszulSign r q l * koszulSign r q l)
-    ring
-    rw [ih]
-    rw [koszulSignInsert_mul_self, mul_one]
-
-@[simp]
-lemma koszulSign_freeMonoid_of {I : Type} (r : I → I → Prop) [DecidableRel r] (q : I → Fin 2)
-    (i : I) : koszulSign r q (FreeMonoid.of i) = 1 := by
-  change koszulSign r q [i] = 1
-  simp only [koszulSign, mul_one]
-  rfl
-
-lemma koszulSignInsert_erase_boson {I : Type} (q : I → Fin 2) (le1 :I → I → Prop)
-    [DecidableRel le1] (r0 : I) :
-    (r : List I) → (n : Fin r.length) → (heq : q (r.get n) = 0) →
-    koszulSignInsert le1 q r0 (r.eraseIdx n) = koszulSignInsert le1 q r0 r
-  | [], _, _ => by
-    simp
-  | r1 :: r, ⟨0, h⟩, hr => by
-    simp only [List.eraseIdx_zero, List.tail_cons]
-    simp only [List.length_cons, Fin.zero_eta, List.get_eq_getElem, Fin.val_zero,
-      List.getElem_cons_zero, Fin.isValue] at hr
-    rw [koszulSignInsert]
-    simp [hr]
-  | r1 :: r, ⟨n + 1, h⟩, hr => by
-    simp only [List.eraseIdx_cons_succ]
-    rw [koszulSignInsert, koszulSignInsert]
-    rw [koszulSignInsert_erase_boson q le1 r0 r ⟨n, Nat.succ_lt_succ_iff.mp h⟩ hr]
-
-lemma koszulSign_erase_boson {I : Type} (q : I → Fin 2) (le1 :I → I → Prop)
-    [DecidableRel le1] :
-    (r : List I) → (n : Fin r.length) → (heq : q (r.get n) = 0) →
-    koszulSign le1 q (r.eraseIdx n) = koszulSign le1 q r
-  | [], _ => by
-    simp
-  | r0 :: r, ⟨0, h⟩ => by
-    simp only [List.length_cons, Fin.zero_eta, List.get_eq_getElem, Fin.val_zero,
-      List.getElem_cons_zero, Fin.isValue, List.eraseIdx_zero, List.tail_cons, koszulSign]
-    intro h
-    rw [koszulSignInsert_boson]
-    simp only [one_mul]
-    exact h
-  | r0 :: r, ⟨n + 1, h⟩ => by
-    simp only [List.length_cons, List.get_eq_getElem, List.getElem_cons_succ, Fin.isValue,
-      List.eraseIdx_cons_succ]
-    intro h'
-    rw [koszulSign, koszulSign]
-    rw [koszulSign_erase_boson q le1 r ⟨n, Nat.succ_lt_succ_iff.mp h⟩]
-    congr 1
-    rw [koszulSignInsert_erase_boson q le1 r0 r ⟨n, Nat.succ_lt_succ_iff.mp h⟩ h']
-    exact h'
-
 noncomputable section

 /-- Given a relation `r` on `I` sorts elements of `MonoidAlgebra ℂ (FreeMonoid I)` by `r` giving it
--- a/HepLean/PerturbationTheory/Wick/OfList.lean
+++ b/HepLean/PerturbationTheory/Wick/OfList.lean
@ -0,0 +1,194 @@
+/-
+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.PerturbationTheory.Wick.CreateAnnilateSection
+import HepLean.PerturbationTheory.Wick.KoszulOrder
+/-!
+
+# Koszul signs and ordering for lists and algebras
+
+-/
+
+namespace Wick
+open HepLean.List
+
+noncomputable section
+
+def ofList {I : Type} (l : List I) (x : ℂ) : FreeAlgebra ℂ I :=
+  FreeAlgebra.equivMonoidAlgebraFreeMonoid.symm (MonoidAlgebra.single l x)
+
+lemma ofList_pair {I : Type} (l r : List I) (x y : ℂ) :
+    ofList (l ++ r) (x * y) = ofList l x * ofList r y := by
+  simp only [ofList, ← map_mul, MonoidAlgebra.single_mul_single, EmbeddingLike.apply_eq_iff_eq]
+  rfl
+
+lemma ofList_triple {I : Type} (la lb lc : List I) (xa xb xc : ℂ) :
+    ofList (la ++ lb ++ lc) (xa * xb * xc) = ofList la xa * ofList lb xb * ofList lc xc := by
+  rw [ofList_pair, ofList_pair]
+
+lemma ofList_triple_assoc {I : Type} (la lb lc : List I) (xa xb xc : ℂ) :
+    ofList (la ++ (lb ++ lc)) (xa * (xb * xc)) = ofList la xa * ofList lb xb * ofList lc xc := by
+  rw [ofList_pair, ofList_pair]
+  exact Eq.symm (mul_assoc (ofList la xa) (ofList lb xb) (ofList lc xc))
+
+lemma ofList_cons_eq_ofList {I : Type} (l : List I) (i : I) (x : ℂ) :
+    ofList (i :: l) x = ofList [i] 1 * ofList l x := by
+  simp only [ofList, ← map_mul, MonoidAlgebra.single_mul_single, one_mul,
+    EmbeddingLike.apply_eq_iff_eq]
+  rfl
+
+lemma ofList_singleton {I : Type} (i : I) :
+    ofList [i] 1 = FreeAlgebra.ι ℂ i := by
+  simp only [ofList, FreeAlgebra.equivMonoidAlgebraFreeMonoid, MonoidAlgebra.of_apply,
+    MonoidAlgebra.single, AlgEquiv.ofAlgHom_symm_apply, MonoidAlgebra.lift_single, one_smul]
+  rfl
+
+lemma ofList_eq_smul_one {I : Type} (l : List I) (x : ℂ) :
+    ofList l x = x • ofList l 1 := by
+  simp only [ofList]
+  rw [← map_smul]
+  simp
+
+lemma ofList_empty {I : Type} : ofList [] 1 = (1 : FreeAlgebra ℂ I) := by
+  simp only [ofList, EmbeddingLike.map_eq_one_iff]
+  rfl
+
+lemma ofList_empty' {I : Type} : ofList [] x = x • (1 : FreeAlgebra ℂ I) := by
+  rw [ofList_eq_smul_one, ofList_empty]
+
+lemma koszulOrder_ofList {I : Type} (r : I → I → Prop) [DecidableRel r] (q : I → Fin 2)
+    (l : List I) (x : ℂ) :
+    koszulOrder r q (ofList l x) = (koszulSign r q l) • ofList (List.insertionSort r l) x := by
+  rw [ofList]
+  rw [koszulOrder_single]
+  change ofList (List.insertionSort r l) _ = _
+  rw [ofList_eq_smul_one]
+  conv_rhs => rw [ofList_eq_smul_one]
+  rw [smul_smul]
+
+lemma ofList_insertionSort_eq_koszulOrder {I : Type} (r : I → I → Prop) [DecidableRel r]
+    (q : I → Fin 2) (l : List I) (x : ℂ) :
+    ofList (List.insertionSort r l) x = (koszulSign r q l) • koszulOrder r q (ofList l x) := by
+  rw [koszulOrder_ofList]
+  rw [smul_smul]
+  rw [koszulSign_mul_self]
+  simp
+
+def sumFiber {I : Type} (f : I → Type) [∀ i, Fintype (f i)] :
+    FreeAlgebra ℂ I →ₐ[ℂ] FreeAlgebra ℂ (Σ i, f i) :=
+  FreeAlgebra.lift ℂ fun i => ∑ (j : f i), FreeAlgebra.ι ℂ ⟨i, j⟩
+
+lemma sumFiber_ι {I : Type} (f : I → Type) [∀ i, Fintype (f i)] (i : I) :
+    sumFiber f (FreeAlgebra.ι ℂ i) = ∑ (b : f i), FreeAlgebra.ι ℂ ⟨i, b⟩ := by
+  simp [sumFiber]
+
+def ofListLift {I : Type} (f : I → Type) [∀ i, Fintype (f i)] (l : List I) (x : ℂ) :
+    FreeAlgebra ℂ (Σ i, f i) :=
+  sumFiber f (ofList l x)
+
+lemma ofListLift_empty {I : Type} (f : I → Type) [∀ i, Fintype (f i)] :
+  ofListLift f [] 1 = 1 := by
+  simp only [ofListLift, EmbeddingLike.map_eq_one_iff]
+  rw [ofList_empty]
+  exact map_one (sumFiber f)
+
+lemma ofListLift_empty_smul {I : Type} (f : I → Type) [∀ i, Fintype (f i)] (x : ℂ) :
+  ofListLift f [] x = x • 1 := by
+  simp only [ofListLift, EmbeddingLike.map_eq_one_iff]
+  rw [ofList_eq_smul_one]
+  rw [ofList_empty]
+  simp
+
+lemma ofListLift_cons {I : Type} (f : I → Type) [∀ i, Fintype (f i)] (i : I) (r : List I) (x : ℂ) :
+    ofListLift f (i :: r) x = (∑ j : f i, FreeAlgebra.ι ℂ ⟨i, j⟩) * (ofListLift f r x) := by
+  rw [ofListLift, ofList_cons_eq_ofList, ofList_singleton, map_mul]
+  conv_lhs => lhs; rw [sumFiber]
+  rw [ofListLift]
+  simp
+
+lemma ofListLift_singleton {I : Type} (f : I → Type) [∀ i, Fintype (f i)] (i : I) (x : ℂ) :
+    ofListLift f [i] x = ∑ j : f i, x • FreeAlgebra.ι ℂ ⟨i, j⟩ := by
+  simp only [ofListLift]
+  rw [ofList_eq_smul_one, ofList_singleton, map_smul]
+  rw [sumFiber_ι]
+  rw [Finset.smul_sum]
+
+lemma ofListLift_singleton_one {I : Type} (f : I → Type) [∀ i, Fintype (f i)] (i : I) :
+    ofListLift f [i] 1 = ∑ j : f i, FreeAlgebra.ι ℂ ⟨i, j⟩ := by
+  simp only [ofListLift]
+  rw [ofList_eq_smul_one, ofList_singleton, map_smul]
+  rw [sumFiber_ι]
+  rw [Finset.smul_sum]
+  simp
+
+lemma ofListLift_cons_eq_ofListLift {I : Type} (f : I → Type) [∀ i, Fintype (f i)] (i : I)
+    (r : List I) (x : ℂ) :
+    ofListLift f (i :: r) x = ofListLift f [i] 1 * ofListLift f r x := by
+  rw [ofListLift_cons, ofListLift_singleton]
+  simp only [one_smul]
+
+lemma ofListLift_expand {I : Type} (f : I → Type) [∀ i, Fintype (f i)] (x : ℂ) :
+    (l : List I) → ofListLift f l x = ∑ (a : CreateAnnilateSect f l), ofList a.toList x
+  | [] => by
+    simp only [ofListLift, CreateAnnilateSect, List.length_nil, List.get_eq_getElem,
+      Finset.univ_unique, CreateAnnilateSect.toList, Finset.sum_const, Finset.card_singleton,
+      one_smul]
+    rw [ofList_eq_smul_one, map_smul, ofList_empty, ofList_eq_smul_one, ofList_empty, map_one]
+  | i :: l => by
+    rw [ofListLift_cons, ofListLift_expand f x l]
+    conv_rhs => rw [← (CreateAnnilateSect.extractEquiv
+        ⟨0, by exact Nat.zero_lt_succ l.length⟩).symm.sum_comp (α := FreeAlgebra ℂ _)]
+    erw [Finset.sum_product]
+    rw [Finset.sum_mul]
+    conv_lhs =>
+      rhs
+      intro n
+      rw [Finset.mul_sum]
+    congr
+    funext j
+    congr
+    funext n
+    rw [← ofList_singleton, ← ofList_pair, one_mul]
+    rfl
+
+lemma koszulOrder_ofListLift {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
+    (q : I → Fin 2) (le1 : I → I → Prop) [DecidableRel le1]
+    (l : List I) (x : ℂ) : koszulOrder (fun i j => le1 i.1 j.1) (fun i => q i.fst) (ofListLift f l x) =
+    sumFiber f (koszulOrder le1 q (ofList l x)) := by
+  rw [koszulOrder_ofList]
+  rw [map_smul]
+  change _ = _ • ofListLift _ _ _
+  rw [ofListLift_expand]
+  rw [map_sum]
+  conv_lhs =>
+    rhs
+    intro a
+    rw [koszulOrder_ofList]
+    rw [CreateAnnilateSect.toList_koszulSign]
+  rw [← Finset.smul_sum]
+  apply congrArg
+  conv_lhs =>
+    rhs
+    intro n
+    rw [← CreateAnnilateSect.sort_toList]
+  rw [ofListLift_expand]
+  refine Fintype.sum_equiv
+    ((HepLean.List.insertionSortEquiv le1 l).piCongr fun i => Equiv.cast ?_) _ _ ?_
+  congr 1
+  · rw [← HepLean.List.insertionSortEquiv_get]
+    simp
+  · intro x
+    rfl
+
+lemma koszulOrder_ofListLift_eq_ofListLift {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
+    (q : I → Fin 2) (le1 : I → I → Prop) [DecidableRel le1]
+    (l : List I) (x : ℂ) : koszulOrder (fun i j => le1 i.1 j.1) (fun i => q i.fst)
+    (ofListLift f l x) =
+    koszulSign le1 q l • ofListLift f (List.insertionSort le1 l) x := by
+  rw [koszulOrder_ofListLift, koszulOrder_ofList, map_smul]
+  rfl
+
+end
+end Wick
--- a/HepLean/PerturbationTheory/Wick/Koszul/OperatorMap.lean
+++ b/HepLean/PerturbationTheory/Wick/Koszul/OperatorMap.lean
@ -3,7 +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.PerturbationTheory.Wick.Koszul.SuperCommuteM
+import HepLean.PerturbationTheory.Wick.SuperCommute
 /-!

 # Koszul signs and ordering for lists and algebras
@ -45,12 +45,12 @@ lemma superCommute_ofList_singleton_ι_center [OperatorMap q le1 F] (i j :I) :

 end OperatorMap

-lemma superCommuteTake_operatorMap {I : Type} (q : I → Fin 2)
+lemma superCommuteSplit_operatorMap {I : Type} (q : I → Fin 2)
    (le1 : I → I → Prop) [DecidableRel le1]
    (lb : List I) (xa xb : ℂ) (n : ℕ)
    (hn : n < lb.length) {A : Type} [Semiring A] [Algebra ℂ A] (f : FreeAlgebra ℂ I →ₐ[ℂ] A)
    [OperatorMap q le1 f] (i : I) :
-    f (superCommuteTake q [i] lb xa xb n hn) =
+    f (superCommuteSplit q [i] lb xa xb n hn) =
    f (superCommute q (ofList [i] xa) (FreeAlgebra.ι ℂ (lb.get ⟨n, hn⟩)))
    * (superCommuteCoef q [i] (List.take n lb) •
    f (ofList (List.eraseIdx lb n) xb)) := by
@ -58,29 +58,29 @@ lemma superCommuteTake_operatorMap {I : Type} (q : I → Fin 2)
      Subalgebra.center ℂ A :=
    OperatorMap.superCommute_ofList_singleton_ι_center (le1 := le1) f i (lb.get ⟨n, hn⟩)
  rw [Subalgebra.mem_center_iff] at hn
-  rw [superCommuteTake, map_mul, map_mul, map_smul, hn, mul_assoc, smul_mul_assoc,
+  rw [superCommuteSplit, map_mul, map_mul, map_smul, hn, mul_assoc, smul_mul_assoc,
    ← map_mul, ← ofList_pair]
  congr
  · exact Eq.symm (List.eraseIdx_eq_take_drop_succ lb n)
  · exact one_mul xb

-lemma superCommuteTakeM_operatorMap {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
+lemma superCommuteLiftSplit_operatorMap {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
    (q : I → Fin 2) (c : (Σ i, f i)) (r : List I) (x y : ℂ) (n : ℕ)
    (hn : n < r.length)
    (le1 : (Σ i, f i) → (Σ i, f i) → Prop) [DecidableRel le1]
    {A : Type} [Semiring A] [Algebra ℂ A] (F : FreeAlgebra ℂ (Σ i, f i) →ₐ[ℂ] A)
    [OperatorMap (fun i => q i.1) le1 F] :
-    F (superCommuteTakeM q [c] r x y n hn) = superCommuteCoefM q [c] (List.take n r) •
+    F (superCommuteLiftSplit q [c] r x y n hn) = superCommuteLiftCoef q [c] (List.take n r) •
    (F (superCommute (fun i => q i.1) (ofList [c] x)
-    (freeAlgebraMap f (FreeAlgebra.ι ℂ (r.get ⟨n, hn⟩))))
-    * F (ofListM f (List.eraseIdx r n) y)) := by
-  rw [superCommuteTakeM]
+    (sumFiber f (FreeAlgebra.ι ℂ (r.get ⟨n, hn⟩))))
+    * F (ofListLift f (List.eraseIdx r n) y)) := by
+  rw [superCommuteLiftSplit]
  rw [map_smul]
  congr
  rw [map_mul, map_mul]
-  have h1 : F ((superCommute fun i => q i.fst) (ofList [c] x) ((freeAlgebraMap f)
+  have h1 : F ((superCommute fun i => q i.fst) (ofList [c] x) ((sumFiber f)
    (FreeAlgebra.ι ℂ (r.get ⟨n, hn⟩)))) ∈ Subalgebra.center ℂ A := by
-      rw [freeAlgebraMap_ι]
+      rw [sumFiber_ι]
      rw [map_sum, map_sum]
      refine Subalgebra.sum_mem _ ?_
      intro n
@ -88,7 +88,7 @@ lemma superCommuteTakeM_operatorMap {I : Type} {f : I → Type} [∀ i, Fintype
  rw [Subalgebra.mem_center_iff] at h1
  rw [h1, mul_assoc, ← map_mul]
  congr
-  rw [ofListM, ofListM, ofListM, ← map_mul]
+  rw [ofListLift, ofListLift, ofListLift, ← map_mul]
  congr
  rw [← ofList_pair, one_mul]
  congr
@ -109,7 +109,7 @@ lemma superCommute_koszulOrder_le_ofList {I : Type}
  conv_lhs =>
    enter [2, 2]
    intro n
-    rw [superCommuteTake_operatorMap (le1 := le1)]
+    rw [superCommuteSplit_operatorMap (le1 := le1)]
    enter [1, 2, 2, 2]
    change ((List.insertionSort le1 r).get ∘ (HepLean.List.insertionSortEquiv le1 r)) n
    rw [HepLean.List.insertionSort_get_comp_insertionSortEquiv]
@ -150,7 +150,7 @@ lemma koszulOrder_of_le_all_ofList {I : Type}
  conv_lhs =>
    enter [2, 2]
    rw [← ofList_singleton]
-    rw [ofListM_ofList_superCommute' q]
+    rw [ofListLift_ofList_superCommute' q]
  rw [map_sub]
  rw [sub_eq_add_neg]
  rw [map_add]
@ -164,7 +164,7 @@ lemma koszulOrder_of_le_all_ofList {I : Type}
    rhs
    rw [superCommute_ofList_sum]
    rw [map_sum, map_sum]
-    dsimp [superCommuteTake]
+    dsimp [superCommuteSplit]
    rw [ofList_singleton]
    rhs
    intro n
@ -243,29 +243,29 @@ lemma le_all_mul_koszulOrder_ofList_expand {I : Type}
    rfl
  exact fun j => hi j

-lemma le_all_mul_koszulOrder_ofListM_expand {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
+lemma le_all_mul_koszulOrder_ofListLift_expand {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
    (q : I → Fin 2) (r : List I) (x : ℂ) (le1 : (Σ i, f i) → (Σ i, f i) → Prop) [DecidableRel le1]
    [IsTotal (Σ i, f i) le1] [IsTrans (Σ i, f i) le1]
    (i : (Σ i, f i)) (hi : ∀ (j : (Σ i, f i)), le1 j i)
    {A : Type} [Semiring A] [Algebra ℂ A]
    (F : FreeAlgebra ℂ (Σ i, f i) →ₐ A) [OperatorMap (fun i => q i.1) le1 F] :
-    F (ofList [i] 1 * koszulOrder le1 (fun i => q i.1) (ofListM f r x)) =
-    F ((koszulOrder le1 fun i => q i.fst) (ofList [i] 1 * ofListM f r x)) +
+    F (ofList [i] 1 * koszulOrder le1 (fun i => q i.1) (ofListLift f r x)) =
+    F ((koszulOrder le1 fun i => q i.fst) (ofList [i] 1 * ofListLift f r x)) +
    ∑ n : (Fin r.length), superCommuteCoef q [r.get n] (List.take (↑n) r) •
-      F (((superCommute fun i => q i.fst) (ofList [i] 1)) (ofListM f [r.get n] 1)) *
-    F ((koszulOrder le1 fun i => q i.fst) (ofListM f (r.eraseIdx ↑n) x)) := by
+      F (((superCommute fun i => q i.fst) (ofList [i] 1)) (ofListLift f [r.get n] 1)) *
+    F ((koszulOrder le1 fun i => q i.fst) (ofListLift f (r.eraseIdx ↑n) x)) := by
  match r with
  | [] =>
    simp only [map_mul, List.length_nil, Finset.univ_eq_empty, List.get_eq_getElem, List.take_nil,
      List.eraseIdx_nil, Algebra.smul_mul_assoc, Finset.sum_empty, add_zero]
-    rw [ofListM_empty_smul]
+    rw [ofListLift_empty_smul]
    simp only [map_smul, koszulOrder_one, map_one, Algebra.mul_smul_comm, mul_one]
    rw [ofList_singleton, koszulOrder_ι]
  | r0 :: r =>
-  rw [ofListM_expand, map_sum, Finset.mul_sum, map_sum]
-  let e1 (a : CreatAnnilateSect f (r0 :: r)) :
+  rw [ofListLift_expand, map_sum, Finset.mul_sum, map_sum]
+  let e1 (a : CreateAnnilateSect f (r0 :: r)) :
        Option (Fin a.toList.length) ≃ Option (Fin (r0 :: r).length) :=
-      Equiv.optionCongr (Fin.castOrderIso (CreatAnnilateSect.toList_length a)).toEquiv
+      Equiv.optionCongr (Fin.castOrderIso (CreateAnnilateSect.toList_length a)).toEquiv
  conv_lhs =>
    rhs
    intro a
@ -287,25 +287,25 @@ lemma le_all_mul_koszulOrder_ofListM_expand {I : Type} {f : I → Type} [∀ i,
    rw [ofList_cons_eq_ofList]
  · congr
    funext n
-    rw [← (CreatAnnilateSect.extractEquiv n).symm.sum_comp]
+    rw [← (CreateAnnilateSect.extractEquiv n).symm.sum_comp]
    simp only [List.get_eq_getElem, List.length_cons, Equiv.optionCongr_symm, OrderIso.toEquiv_symm,
      Fin.symm_castOrderIso, Equiv.optionCongr_apply, RelIso.coe_fn_toEquiv, Option.map_some',
      Fin.castOrderIso_apply, Algebra.smul_mul_assoc, e1]
    erw [Finset.sum_product]
-    have h1 (a0 : f (r0 :: r)[↑n]) (a : CreatAnnilateSect f ((r0 :: r).eraseIdx ↑n)) :
+    have h1 (a0 : f (r0 :: r)[↑n]) (a : CreateAnnilateSect f ((r0 :: r).eraseIdx ↑n)) :
      superCommuteCenterOrder (fun i => q i.fst)
-        ((CreatAnnilateSect.extractEquiv n).symm (a0, a)).toList i F
+        ((CreateAnnilateSect.extractEquiv n).symm (a0, a)).toList i F
      (some (Fin.cast (by simp) n)) =
      superCommuteCoef q [(r0 :: r).get n] (List.take (↑n) (r0 :: r)) •
      F (((superCommute fun i => q i.fst) (ofList [i] 1))
      (FreeAlgebra.ι ℂ ⟨(r0 :: r).get n, a0⟩)) := by
      simp only [superCommuteCenterOrder, List.get_eq_getElem, List.length_cons, Fin.coe_cast]
-      erw [CreatAnnilateSect.extractEquiv_symm_toList_get_same]
+      erw [CreateAnnilateSect.extractEquiv_symm_toList_get_same]
      have hsc : superCommuteCoef (fun i => q i.fst) [⟨(r0 :: r).get n, a0⟩]
-        (List.take (↑n) ((CreatAnnilateSect.extractEquiv n).symm (a0, a)).toList) =
+        (List.take (↑n) ((CreateAnnilateSect.extractEquiv n).symm (a0, a)).toList) =
        superCommuteCoef q [(r0 :: r).get n] (List.take (↑n) ((r0 :: r))) := by
        simp only [superCommuteCoef, List.get_eq_getElem, List.length_cons, Fin.isValue,
-          CreatAnnilateSect.toList_grade_take]
+          CreateAnnilateSect.toList_grade_take]
        rfl
      erw [hsc]
      rfl
@ -329,19 +329,19 @@ lemma le_all_mul_koszulOrder_ofListM_expand {I : Type} {f : I → Type} [∀ i,
      rhs
      rhs
      lhs
-      rw [← CreatAnnilateSect.eraseIdx_toList]
-      erw [CreatAnnilateSect.extractEquiv_symm_eraseIdx]
+      rw [← CreateAnnilateSect.eraseIdx_toList]
+      erw [CreateAnnilateSect.extractEquiv_symm_eraseIdx]
    rw [← Finset.sum_mul]
    conv_lhs =>
      lhs
      rw [← Finset.smul_sum]
-      erw [← map_sum, ← map_sum, ← ofListM_singleton_one]
+      erw [← map_sum, ← map_sum, ← ofListLift_singleton_one]
    conv_lhs =>
      rhs
      rw [← map_sum, ← map_sum]
      simp only [List.get_eq_getElem, List.length_cons, Equiv.symm_apply_apply,
        Algebra.smul_mul_assoc]
-      erw [← ofListM_expand]
+      erw [← ofListLift_expand]
    simp only [List.get_eq_getElem, List.length_cons, Algebra.smul_mul_assoc]

 end
--- a/HepLean/PerturbationTheory/Wick/Signs/Grade.lean
+++ b/HepLean/PerturbationTheory/Wick/Signs/Grade.lean
@ -0,0 +1,100 @@
+/-
+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 Mathlib.Algebra.FreeAlgebra
+import Mathlib.Algebra.Lie.OfAssociative
+import Mathlib.Analysis.Complex.Basic
+/-!
+
+# Koszul sign insert
+
+-/
+
+namespace Wick
+
+def grade {I : Type} (q : I → Fin 2) : (l : List I) → Fin 2
+  | [] => 0
+  | a :: l => if q a = grade q l then 0 else 1
+
+@[simp]
+lemma grade_freeMonoid {I : Type} (q : I → Fin 2) (i : I) : grade q (FreeMonoid.of i) = q i := by
+  simp only [grade, Fin.isValue]
+  have ha (a : Fin 2) : (if a = 0 then 0 else 1) = a := by
+    fin_cases a <;> rfl
+  rw [ha]
+
+@[simp]
+lemma grade_empty {I : Type} (q : I → Fin 2) : grade q [] = 0 := by
+  simp [grade]
+
+@[simp]
+lemma grade_append {I : Type} (q : I → Fin 2) (l r : List I) :
+    grade q (l ++ r) = if grade q l = grade q r then 0 else 1 := by
+  induction l with
+  | nil =>
+    simp only [List.nil_append, grade_empty, Fin.isValue]
+    have ha (a : Fin 2) : (if 0 = a then 0 else 1) = a := by
+      fin_cases a <;> rfl
+    exact Eq.symm (Fin.eq_of_val_eq (congrArg Fin.val (ha (grade q r))))
+  | cons a l ih =>
+    simp only [grade, List.append_eq, Fin.isValue]
+    erw [ih]
+    have hab (a b c : Fin 2) : (if a = if b = c then 0 else 1 then (0 : Fin 2) else 1) =
+        if (if a = b then 0 else 1) = c then 0 else 1 := by
+      fin_cases a <;> fin_cases b <;> fin_cases c <;> rfl
+    exact hab (q a) (grade q l) (grade q r)
+
+lemma grade_count {I : Type} (q : I → Fin 2) (l : List I) :
+    grade q l = if Nat.mod (List.countP (fun i => decide (q i = 1)) l) 2 = 0 then 0 else 1 := by
+  induction l with
+  | nil => simp
+  | cons r0 r ih =>
+    simp only [grade, Fin.isValue]
+    rw [List.countP_cons]
+    simp only [Fin.isValue, decide_eq_true_eq]
+    rw [ih]
+    by_cases h: q r0 = 1
+    · simp only [h, Fin.isValue, ↓reduceIte]
+      split
+      next h1 =>
+        simp_all only [Fin.isValue, ↓reduceIte, one_ne_zero]
+        split
+        next h2 =>
+          simp_all only [Fin.isValue, one_ne_zero]
+          have ha (a : ℕ) (ha : a % 2 = 0) : (a + 1) % 2 ≠ 0 := by
+            omega
+          exact ha (List.countP (fun i => decide (q i = 1)) r) h1 h2
+        next h2 => simp_all only [Fin.isValue]
+      next h1 =>
+        simp_all only [Fin.isValue, ↓reduceIte]
+        split
+        next h2 => simp_all only [Fin.isValue]
+        next h2 =>
+          simp_all only [Fin.isValue, zero_ne_one]
+          have ha (a : ℕ) (ha : ¬ a % 2 = 0) : (a + 1) % 2 = 0 := by
+            omega
+          exact h2 (ha (List.countP (fun i => decide (q i = 1)) r) h1)
+    · have h0 : q r0 = 0 := by omega
+      simp only [h0, Fin.isValue, zero_ne_one, ↓reduceIte, add_zero]
+      by_cases hn : (List.countP (fun i => decide (q i = 1)) r).mod 2 = 0
+      · simp [hn]
+      · simp [hn]
+
+lemma grade_perm {I : Type} (q : I → Fin 2) {l l' : List I} (h : l.Perm l') :
+    grade q l = grade q l' := by
+  rw [grade_count, grade_count, h.countP_eq]
+
+lemma grade_orderedInsert {I : Type} (q : I → Fin 2) (le1 : I → I → Prop) [DecidableRel le1]
+    (l : List I) (i : I) : grade q (List.orderedInsert le1 i l) = grade q (i :: l) := by
+  apply grade_perm
+  exact List.perm_orderedInsert le1 i l
+
+@[simp]
+lemma grade_insertionSort {I : Type} (q : I → Fin 2) (le1 : I → I → Prop) [DecidableRel le1]
+    (l : List I) : grade q (List.insertionSort le1 l) = grade q l := by
+  apply grade_perm
+  exact List.perm_insertionSort le1 l
+
+end Wick
--- a/HepLean/PerturbationTheory/Wick/Signs/InsertSign.lean
+++ b/HepLean/PerturbationTheory/Wick/Signs/InsertSign.lean
@ -0,0 +1,109 @@
+/-
+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.Mathematics.List
+import HepLean.PerturbationTheory.Wick.Signs.SuperCommuteCoef
+/-!
+
+# Koszul signs and ordering for lists and algebras
+
+-/
+
+namespace Wick
+open HepLean.List
+
+
+def insertSign {I : Type} (q : I → Fin 2) (n : ℕ) (r0 : I) (r : List I) : ℂ :=
+  superCommuteCoef q [r0] (List.take n r)
+
+lemma take_insert_same {I : Type} (i : I) :
+    (n : ℕ) → (r : List I) →
+    List.take n (List.insertIdx n i r) = List.take n r
+  | 0, _ => by simp
+  | _+1, [] => by simp
+  | n+1, a::as => by
+    simp only [List.insertIdx_succ_cons, List.take_succ_cons, List.cons.injEq, true_and]
+    exact take_insert_same i n as
+
+lemma insertSign_insert {I : Type} (q : I → Fin 2) (n : ℕ)
+    (r0 : I) (r : List I) : insertSign q n r0 r = insertSign q n r0 (List.insertIdx n r0 r) := by
+  simp only [insertSign]
+  congr 1
+  rw [take_insert_same]
+
+lemma take_eraseIdx_same {I : Type} :
+    (n : ℕ) → (r : List I) →
+    List.take n (List.eraseIdx r n) = List.take n r
+  | 0, _ => by simp
+  | _+1, [] => by simp
+  | n+1, a::as => by
+    simp only [List.eraseIdx_cons_succ, List.take_succ_cons, List.cons.injEq, true_and]
+    exact take_eraseIdx_same n as
+
+lemma insertSign_eraseIdx {I : Type} (q : I → Fin 2) (n : ℕ)
+    (r0 : I) (r : List I) : insertSign q n r0 (r.eraseIdx n) = insertSign q n r0 r := by
+  simp only [insertSign]
+  congr 1
+  rw [take_eraseIdx_same]
+
+lemma insertSign_zero {I : Type} (q : I → Fin 2) (r0 : I) (r : List I) :
+    insertSign q 0 r0 r = 1 := by
+  simp [insertSign, superCommuteCoef]
+
+lemma insertSign_succ_cons {I : Type} (q : I → Fin 2) (n : ℕ)
+    (r0 r1 : I) (r : List I) : insertSign q (n + 1) r0 (r1 :: r) =
+    superCommuteCoef q [r0] [r1] * insertSign q n r0 r := by
+  simp only [insertSign, List.take_succ_cons]
+  rw [superCommuteCoef_cons]
+
+lemma take_insert_gt {I : Type} (i : I) :
+    (n m : ℕ) → (h : n < m) → (r : List I) →
+    List.take n (List.insertIdx m i r) = List.take n r
+  | 0, 0, _, _ => by simp
+  | 0, m + 1, _, _ => by simp
+  | n+1, m + 1, _, [] => by simp
+  | n+1, m + 1, h, a::as => by
+    simp only [List.insertIdx_succ_cons, List.take_succ_cons, List.cons.injEq, true_and]
+    refine take_insert_gt i n m (Nat.succ_lt_succ_iff.mp h) as
+
+lemma insertSign_insert_gt {I : Type} (q : I → Fin 2) (n m : ℕ)
+    (r0 r1 : I) (r : List I) (hn : n < m) :
+    insertSign q n r0 (List.insertIdx m r1 r) = insertSign q n r0 r := by
+  rw [insertSign, insertSign]
+  congr 1
+  exact take_insert_gt r1 n m hn r
+
+lemma take_insert_let {I : Type} (i : I) :
+    (n m : ℕ) → (h : m ≤ n) → (r : List I) → (hm : m ≤ r.length) →
+    (List.take (n + 1) (List.insertIdx m i r)).Perm (i :: List.take n r)
+  | 0, 0, h, _, _ => by simp
+  | m + 1, 0, h, r, _ => by simp
+  | n + 1, m + 1, h, [], hm => by
+    simp at hm
+  | n + 1, m + 1, h, a::as, hm => by
+    simp only [List.insertIdx_succ_cons, List.take_succ_cons]
+    have hp : (i :: a :: List.take n as).Perm (a :: i :: List.take n as) := by
+      exact List.Perm.swap a i (List.take n as)
+    refine List.Perm.trans ?_ hp.symm
+    refine List.Perm.cons a ?_
+    exact take_insert_let i n m (Nat.le_of_succ_le_succ h) as (Nat.le_of_succ_le_succ hm)
+
+lemma insertSign_insert_lt_eq_insertSort {I : Type} (q : I → Fin 2) (n m : ℕ)
+    (r0 r1 : I) (r : List I) (hn : m ≤ n) (hm : m ≤ r.length) :
+    insertSign q (n + 1) r0 (List.insertIdx m r1 r) = insertSign q (n + 1) r0 (r1 :: r) := by
+  rw [insertSign, insertSign]
+  apply superCommuteCoef_perm_snd
+  simp only [List.take_succ_cons]
+  refine take_insert_let r1 n m hn r hm
+
+lemma insertSign_insert_lt {I : Type} (q : I → Fin 2) (n m : ℕ)
+    (r0 r1 : I) (r : List I) (hn : m ≤ n) (hm : m ≤ r.length) :
+    insertSign q (n + 1) r0 (List.insertIdx m r1 r) = superCommuteCoef q [r0] [r1] *
+    insertSign q n r0 r := by
+  rw [insertSign_insert_lt_eq_insertSort, insertSign_succ_cons]
+  exact hn
+  exact hm
+
+end Wick
--- a/HepLean/PerturbationTheory/Wick/Signs/KoszulSign.lean
+++ b/HepLean/PerturbationTheory/Wick/Signs/KoszulSign.lean
@ -0,0 +1,235 @@
+/-
+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 Mathlib.Algebra.FreeAlgebra
+import Mathlib.Algebra.Lie.OfAssociative
+import Mathlib.Analysis.Complex.Basic
+import HepLean.PerturbationTheory.Wick.Signs.KoszulSignInsert
+/-!
+
+# Koszul sign insert
+
+-/
+
+namespace Wick
+
+open HepLean.List
+
+/-- Gives a factor of `- 1` for every fermion-fermion (`q` is `1`) crossing that occurs when sorting
+  a list of based on `r`. -/
+def koszulSign {I : Type} (r : I → I → Prop) [DecidableRel r] (q : I → Fin 2) :
+    List I → ℂ
+  | [] => 1
+  | a :: l => koszulSignInsert r q a l * koszulSign r q l
+
+
+lemma koszulSign_mul_self {I : Type} (r : I → I → Prop) [DecidableRel r] (q : I → Fin 2)
+    (l : List I) : koszulSign r q l * koszulSign r q l = 1 := by
+  induction l with
+  | nil => simp [koszulSign]
+  | cons a l ih =>
+    simp only [koszulSign]
+    trans (koszulSignInsert r q a l * koszulSignInsert r q a l) *
+      (koszulSign r q l * koszulSign r q l)
+    ring
+    rw [ih]
+    rw [koszulSignInsert_mul_self, mul_one]
+
+@[simp]
+lemma koszulSign_freeMonoid_of {I : Type} (r : I → I → Prop) [DecidableRel r] (q : I → Fin 2)
+    (i : I) : koszulSign r q (FreeMonoid.of i) = 1 := by
+  change koszulSign r q [i] = 1
+  simp only [koszulSign, mul_one]
+  rfl
+
+lemma koszulSignInsert_erase_boson {I : Type} (q : I → Fin 2) (le1 :I → I → Prop)
+    [DecidableRel le1] (r0 : I) :
+    (r : List I) → (n : Fin r.length) → (heq : q (r.get n) = 0) →
+    koszulSignInsert le1 q r0 (r.eraseIdx n) = koszulSignInsert le1 q r0 r
+  | [], _, _ => by
+    simp
+  | r1 :: r, ⟨0, h⟩, hr => by
+    simp only [List.eraseIdx_zero, List.tail_cons]
+    simp only [List.length_cons, Fin.zero_eta, List.get_eq_getElem, Fin.val_zero,
+      List.getElem_cons_zero, Fin.isValue] at hr
+    rw [koszulSignInsert]
+    simp [hr]
+  | r1 :: r, ⟨n + 1, h⟩, hr => by
+    simp only [List.eraseIdx_cons_succ]
+    rw [koszulSignInsert, koszulSignInsert]
+    rw [koszulSignInsert_erase_boson q le1 r0 r ⟨n, Nat.succ_lt_succ_iff.mp h⟩ hr]
+
+lemma koszulSign_erase_boson {I : Type} (q : I → Fin 2) (le1 :I → I → Prop)
+    [DecidableRel le1] :
+    (r : List I) → (n : Fin r.length) → (heq : q (r.get n) = 0) →
+    koszulSign le1 q (r.eraseIdx n) = koszulSign le1 q r
+  | [], _ => by
+    simp
+  | r0 :: r, ⟨0, h⟩ => by
+    simp only [List.length_cons, Fin.zero_eta, List.get_eq_getElem, Fin.val_zero,
+      List.getElem_cons_zero, Fin.isValue, List.eraseIdx_zero, List.tail_cons, koszulSign]
+    intro h
+    rw [koszulSignInsert_boson]
+    simp only [one_mul]
+    exact h
+  | r0 :: r, ⟨n + 1, h⟩ => by
+    simp only [List.length_cons, List.get_eq_getElem, List.getElem_cons_succ, Fin.isValue,
+      List.eraseIdx_cons_succ]
+    intro h'
+    rw [koszulSign, koszulSign]
+    rw [koszulSign_erase_boson q le1 r ⟨n, Nat.succ_lt_succ_iff.mp h⟩]
+    congr 1
+    rw [koszulSignInsert_erase_boson q le1 r0 r ⟨n, Nat.succ_lt_succ_iff.mp h⟩ h']
+    exact h'
+
+
+
+def koszulSignCons {I : Type} (q : I → Fin 2) (le1 : I → I → Prop) [DecidableRel le1] (r0 r1 : I) :
+    ℂ :=
+  if le1 r0 r1 then 1 else
+  if q r0 = 1 ∧ q r1 = 1 then -1 else 1
+
+lemma koszulSignCons_eq_superComuteCoef {I : Type} (q : I → Fin 2) (le1 : I → I → Prop)
+    [DecidableRel le1] (r0 r1 : I) : koszulSignCons q le1 r0 r1 =
+    if le1 r0 r1 then 1 else superCommuteCoef q [r0] [r1] := by
+  simp only [koszulSignCons, Fin.isValue, superCommuteCoef, grade, ite_eq_right_iff, zero_ne_one,
+    imp_false]
+  congr 1
+  by_cases h0 : q r0 = 1
+  · by_cases h1 : q r1 = 1
+    · simp [h0, h1]
+    · have h1 : q r1 = 0 := by omega
+      simp [h0, h1]
+  · have h0 : q r0 = 0 := by omega
+    by_cases h1 : q r1 = 1
+    · simp [h0, h1]
+    · have h1 : q r1 = 0 := by omega
+      simp [h0, h1]
+
+lemma koszulSignInsert_cons {I : Type} (q : I → Fin 2) (le1 : I → I → Prop) [DecidableRel le1]
+    [IsTotal I le1] [IsTrans I le1] (r0 r1 : I) (r : List I) :
+    koszulSignInsert le1 q r0 (r1 :: r) = (koszulSignCons q le1 r0 r1) *
+    koszulSignInsert le1 q r0 r := by
+  simp [koszulSignInsert, koszulSignCons]
+
+lemma koszulSign_insertIdx {I : Type} (q : I → Fin 2) (le1 : I → I → Prop) [DecidableRel le1]
+    (i : I) [IsTotal I le1] [IsTrans I le1] : (r : List I) → (n : ℕ) → (hn : n ≤ r.length) →
+    koszulSign le1 q (List.insertIdx n i r) = insertSign q n i r
+      * koszulSign le1 q r
+      * insertSign q (insertionSortEquiv le1 (List.insertIdx n i r) ⟨n, by
+        rw [List.length_insertIdx _ _ hn]
+        omega⟩) i
+        (List.insertionSort le1 (List.insertIdx n i r))
+  | [], 0, h => by
+    simp [koszulSign, insertSign, superCommuteCoef, koszulSignInsert]
+  | [], n + 1, h => by
+    simp at h
+  | r0 :: r, 0, h => by
+    simp only [List.insertIdx_zero, List.insertionSort, List.length_cons, Fin.zero_eta]
+    rw [koszulSign]
+    trans koszulSign le1 q (r0 :: r) * koszulSignInsert le1 q i (r0 :: r)
+    ring
+    simp only [insertionSortEquiv, List.length_cons, Nat.succ_eq_add_one, List.insertionSort,
+      orderedInsertEquiv, OrderIso.toEquiv_symm, Fin.symm_castOrderIso, HepLean.Fin.equivCons_trans,
+      Equiv.trans_apply, HepLean.Fin.equivCons_zero, HepLean.Fin.finExtractOne_apply_eq,
+      Fin.isValue, HepLean.Fin.finExtractOne_symm_inl_apply, RelIso.coe_fn_toEquiv,
+      Fin.castOrderIso_apply, Fin.cast_mk, Fin.eta]
+    conv_rhs =>
+      rhs
+      rhs
+      rw [orderedInsert_eq_insertIdx_orderedInsertPos]
+    conv_rhs =>
+      rhs
+      rw [← insertSign_insert]
+      change insertSign q (↑(orderedInsertPos le1 ((List.insertionSort le1 (r0 :: r))) i)) i
+        (List.insertionSort le1 (r0 :: r))
+      rw [← koszulSignInsert_eq_insertSign q le1]
+    rw [insertSign_zero]
+    simp
+  | r0 :: r, n + 1, h => by
+    conv_lhs =>
+      rw [List.insertIdx_succ_cons]
+      rw [koszulSign]
+    rw [koszulSign_insertIdx]
+    conv_rhs =>
+      rhs
+      simp only [List.insertIdx_succ_cons]
+      simp only [List.insertionSort, List.length_cons, insertionSortEquiv, Nat.succ_eq_add_one,
+        Equiv.trans_apply, HepLean.Fin.equivCons_succ]
+      erw [orderedInsertEquiv_fin_succ]
+      simp only [Fin.eta, Fin.coe_cast]
+      rhs
+      rw [orderedInsert_eq_insertIdx_orderedInsertPos]
+    conv_rhs =>
+      lhs
+      rw [insertSign_succ_cons, koszulSign]
+    ring_nf
+    conv_lhs =>
+      lhs
+      rw [mul_assoc, mul_comm]
+    rw [mul_assoc]
+    conv_rhs =>
+      rw [mul_assoc, mul_assoc]
+    congr 1
+    let rs := (List.insertionSort le1 (List.insertIdx n i r))
+    have hnsL : n < (List.insertIdx n i r).length := by
+      rw [List.length_insertIdx _ _]
+      simp only [List.length_cons, add_le_add_iff_right] at h
+      omega
+      exact Nat.le_of_lt_succ h
+    let ni : Fin rs.length := (insertionSortEquiv le1 (List.insertIdx n i r))
+      ⟨n, hnsL⟩
+    let nro : Fin (rs.length + 1) :=
+      ⟨↑(orderedInsertPos le1 rs r0), orderedInsertPos_lt_length le1 rs r0⟩
+    rw [koszulSignInsert_insertIdx, koszulSignInsert_cons]
+    trans koszulSignInsert le1 q r0 r * (koszulSignCons q le1 r0 i *insertSign q ni i rs)
+    · simp only [rs, ni]
+      ring
+    trans koszulSignInsert le1 q r0 r * (superCommuteCoef q [i] [r0] *
+          insertSign q (nro.succAbove ni) i (List.insertIdx nro r0 rs))
+    swap
+    · simp only [rs, nro, ni]
+      ring
+    congr 1
+    simp only [Fin.succAbove]
+    have hns : rs.get ni = i := by
+      simp only [Fin.eta, rs]
+      rw [← insertionSortEquiv_get]
+      simp only [Function.comp_apply, Equiv.symm_apply_apply, List.get_eq_getElem, ni]
+      simp_all only [List.length_cons, add_le_add_iff_right, List.getElem_insertIdx_self]
+    have hms : (List.orderedInsert le1 r0 rs).get ⟨nro, by simp⟩ = r0 := by
+      simp [nro]
+    have hc1 : ni.castSucc < nro → ¬ le1 r0 i := by
+      intro hninro
+      rw [← hns]
+      exact lt_orderedInsertPos_rel le1 r0 rs ni hninro
+    have hc2 : ¬ ni.castSucc < nro → le1 r0 i := by
+      intro hninro
+      rw [← hns]
+      refine gt_orderedInsertPos_rel le1 r0 rs ?_ ni hninro
+      exact List.sorted_insertionSort le1 (List.insertIdx n i r)
+    by_cases hn : ni.castSucc < nro
+    · simp only [hn, ↓reduceIte, Fin.coe_castSucc]
+      rw [insertSign_insert_gt]
+      swap
+      · exact hn
+      congr 1
+      rw [koszulSignCons_eq_superComuteCoef]
+      simp only [hc1 hn, ↓reduceIte]
+      rw [superCommuteCoef_comm]
+    · simp only [hn, ↓reduceIte, Fin.val_succ]
+      rw [insertSign_insert_lt]
+      rw [← mul_assoc]
+      congr 1
+      rw [superCommuteCoef_mul_self]
+      rw [koszulSignCons]
+      simp only [hc2 hn, ↓reduceIte]
+      exact Nat.le_of_not_lt hn
+      exact Nat.le_of_lt_succ (orderedInsertPos_lt_length le1 rs r0)
+    · exact Nat.le_of_lt_succ h
+    · exact Nat.le_of_lt_succ h
+
+
+end Wick
--- a/HepLean/PerturbationTheory/Wick/Signs/KoszulSignInsert.lean
+++ b/HepLean/PerturbationTheory/Wick/Signs/KoszulSignInsert.lean
@ -0,0 +1,214 @@
+/-
+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 Mathlib.Algebra.FreeAlgebra
+import Mathlib.Algebra.Lie.OfAssociative
+import Mathlib.Analysis.Complex.Basic
+import HepLean.PerturbationTheory.Wick.Signs.InsertSign
+/-!
+
+# Koszul sign insert
+
+-/
+
+namespace Wick
+
+open HepLean.List
+/-- Gives a factor of `-1` when inserting `a` into a list `List I` in the ordered position
+  for each fermion-fermion cross. -/
+def koszulSignInsert {I : Type} (r : I → I → Prop) [DecidableRel r] (q : I → Fin 2) (a : I) :
+    List I → ℂ
+  | [] => 1
+  | b :: l => if r a b then koszulSignInsert r q a l else
+    if q a = 1 ∧ q b = 1 then - koszulSignInsert r q a l else koszulSignInsert r q a l
+
+/-- When inserting a boson the `koszulSignInsert` is always `1`. -/
+lemma koszulSignInsert_boson {I : Type} (r : I → I → Prop) [DecidableRel r] (q : I → Fin 2) (a : I)
+    (ha : q a = 0) : (l : List I) → koszulSignInsert r q a l = 1
+  | [] => by
+    simp [koszulSignInsert]
+  | b :: l => by
+    simp only [koszulSignInsert, Fin.isValue, ite_eq_left_iff]
+    rw [koszulSignInsert_boson r q a ha l, ha]
+    simp only [Fin.isValue, zero_ne_one, false_and, ↓reduceIte, ite_self]
+
+@[simp]
+lemma koszulSignInsert_mul_self {I : Type} (r : I → I → Prop) [DecidableRel r] (q : I → Fin 2)
+    (a : I) : (l : List I) → koszulSignInsert r q a l * koszulSignInsert r q a l = 1
+  | [] => by
+    simp [koszulSignInsert]
+  | b :: l => by
+    simp only [koszulSignInsert, Fin.isValue, mul_ite, ite_mul, neg_mul, mul_neg]
+    by_cases hr : r a b
+    · simp only [hr, ↓reduceIte]
+      rw [koszulSignInsert_mul_self]
+    · simp only [hr, ↓reduceIte, Fin.isValue]
+      by_cases hq : q a = 1 ∧ q b = 1
+      · simp only [hq, Fin.isValue, and_self, ↓reduceIte, neg_neg]
+        rw [koszulSignInsert_mul_self]
+      · simp only [Fin.isValue, hq, ↓reduceIte]
+        rw [koszulSignInsert_mul_self]
+
+lemma koszulSignInsert_le_forall {I : Type} (r : I → I → Prop) [DecidableRel r] (q : I → Fin 2)
+    (a : I) (l : List I) (hi : ∀ b, r a b) : koszulSignInsert r q a l = 1 := by
+  induction l with
+  | nil => rfl
+  | cons j l ih =>
+    simp only [koszulSignInsert, Fin.isValue, ite_eq_left_iff]
+    rw [ih]
+    simp only [Fin.isValue, ite_eq_left_iff, ite_eq_right_iff, and_imp]
+    intro h
+    exact False.elim (h (hi j))
+
+lemma koszulSignInsert_ge_forall_append {I : Type} (r : I → I → Prop) [DecidableRel r]
+    (q : I → Fin 2) (l : List I) (j i : I) (hi : ∀ j, r j i) :
+    koszulSignInsert r q j l = koszulSignInsert r q j (l ++ [i]) := by
+  induction l with
+  | nil => simp [koszulSignInsert, hi]
+  | cons b l ih =>
+    simp only [koszulSignInsert, Fin.isValue, List.append_eq]
+    by_cases hr : r j b
+    · rw [if_pos hr, if_pos hr]
+      rw [ih]
+    · rw [if_neg hr, if_neg hr]
+      rw [ih]
+
+lemma koszulSignInsert_eq_filter {I : Type} (q : I → Fin 2) (le1 : I → I → Prop) [DecidableRel le1]
+    (r0 : I) : (r : List I) →
+    koszulSignInsert le1 q r0 r =
+    koszulSignInsert le1 q r0 (List.filter (fun i => decide (¬ le1 r0 i)) r)
+  | [] => by
+    simp [koszulSignInsert]
+  | r1 :: r => by
+    dsimp only [koszulSignInsert, Fin.isValue]
+    simp only [Fin.isValue, List.filter, decide_not]
+    by_cases h : le1 r0 r1
+    · simp only [h, ↓reduceIte, decide_True, Bool.not_true]
+      rw [koszulSignInsert_eq_filter]
+      congr
+      simp
+    · simp only [h, ↓reduceIte, Fin.isValue, decide_False, Bool.not_false]
+      dsimp only [Fin.isValue, koszulSignInsert]
+      simp only [Fin.isValue, h, ↓reduceIte]
+      rw [koszulSignInsert_eq_filter]
+      congr
+      simp only [decide_not]
+      simp
+
+lemma koszulSignInsert_eq_cons {I : Type} (q : I → Fin 2) (le1 : I → I → Prop) [DecidableRel le1]
+    [IsTotal I le1] [IsTrans I le1] (r0 : I) (r : List I) :
+    koszulSignInsert le1 q r0 r = koszulSignInsert le1 q r0 (r0 :: r) := by
+  simp only [koszulSignInsert, Fin.isValue, and_self]
+  have h1 : le1 r0 r0 := by
+    simpa using IsTotal.total (r := le1) r0 r0
+  simp [h1]
+
+
+lemma koszulSignInsert_eq_grade {I : Type} (q : I → Fin 2) (le1 : I → I → Prop) [DecidableRel le1]
+    (r0 : I) (r : List I) : koszulSignInsert le1 q r0 r = if grade q [r0] = 1 ∧
+    grade q (List.filter (fun i => decide (¬ le1 r0 i)) r) = 1 then -1 else 1 := by
+  induction r with
+  | nil =>
+    simp [koszulSignInsert]
+  | cons r1 r ih =>
+    rw [koszulSignInsert_eq_filter]
+    by_cases hr1 : ¬ le1 r0 r1
+    · rw [List.filter_cons_of_pos]
+      · dsimp only [koszulSignInsert, Fin.isValue, decide_not]
+        rw [if_neg hr1]
+        dsimp only [Fin.isValue, grade, ite_eq_right_iff, zero_ne_one, imp_false, decide_not]
+        simp only [Fin.isValue, decide_not, ite_eq_right_iff, zero_ne_one, imp_false]
+        have ha (a b c : Fin 2) : (if a = 1 ∧ b = 1 then -if ¬a = 0 ∧
+          c = 1 then -1 else (1 : ℂ)
+          else if ¬a = 0 ∧ c = 1 then -1 else 1) =
+          if ¬a = 0 ∧ ¬b = c then -1 else 1 := by
+          fin_cases a <;> fin_cases b <;> fin_cases c
+          any_goals rfl
+          simp
+        rw [← ha (q r0) (q r1) (grade q (List.filter (fun a => !decide (le1 r0 a)) r))]
+        congr
+        · rw [koszulSignInsert_eq_filter] at ih
+          simpa [grade] using ih
+        · rw [koszulSignInsert_eq_filter] at ih
+          simpa [grade] using ih
+      · simp [hr1]
+    · rw [List.filter_cons_of_neg]
+      simp only [decide_not, Fin.isValue]
+      rw [koszulSignInsert_eq_filter] at ih
+      simpa [grade] using ih
+      simpa using hr1
+
+lemma koszulSignInsert_eq_perm {I : Type} (q : I → Fin 2) (le1 : I → I → Prop) (r r' : List I)
+    (a : I) [DecidableRel le1] (h : r.Perm r') :
+    koszulSignInsert le1 q a r = koszulSignInsert le1 q a r' := by
+  rw [koszulSignInsert_eq_grade]
+  rw [koszulSignInsert_eq_grade]
+  congr 1
+  simp only [Fin.isValue, decide_not, eq_iff_iff, and_congr_right_iff]
+  intro h'
+  have hg : grade q (List.filter (fun i => !decide (le1 a i)) r) =
+      grade q (List.filter (fun i => !decide (le1 a i)) r') := by
+    rw [grade_count, grade_count]
+    rw [List.countP_filter, List.countP_filter]
+    rw [h.countP_eq]
+  rw [hg]
+
+lemma koszulSignInsert_eq_sort {I : Type} (q : I → Fin 2) (le1 : I → I → Prop) (r : List I)
+    (a : I) [DecidableRel le1] :
+    koszulSignInsert le1 q a r = koszulSignInsert le1 q a (List.insertionSort le1 r) := by
+  apply koszulSignInsert_eq_perm
+  exact List.Perm.symm (List.perm_insertionSort le1 r)
+
+lemma koszulSignInsert_eq_insertSign {I : Type} (q : I → Fin 2) (le1 : I → I → Prop)
+    [DecidableRel le1] [IsTotal I le1] [IsTrans I le1] (r0 : I) (r : List I) :
+    koszulSignInsert le1 q r0 r = insertSign q (orderedInsertPos le1 (List.insertionSort le1 r) r0)
+      r0 (List.insertionSort le1 r) := by
+  rw [koszulSignInsert_eq_cons, koszulSignInsert_eq_sort, koszulSignInsert_eq_filter,
+    koszulSignInsert_eq_grade, insertSign, superCommuteCoef]
+  congr
+  simp only [List.filter_filter, Bool.and_self]
+  rw [List.insertionSort]
+  nth_rewrite 1 [List.orderedInsert_eq_take_drop]
+  rw [List.filter_append]
+  have h1 : List.filter (fun a => decide ¬le1 r0 a)
+    (List.takeWhile (fun b => decide ¬le1 r0 b) (List.insertionSort le1 r))
+    = (List.takeWhile (fun b => decide ¬le1 r0 b) (List.insertionSort le1 r)) := by
+    induction r with
+    | nil => simp
+    | cons r1 r ih =>
+      simp only [decide_not, List.insertionSort, List.filter_eq_self, Bool.not_eq_eq_eq_not,
+        Bool.not_true, decide_eq_false_iff_not]
+      intro a ha
+      have ha' := List.mem_takeWhile_imp ha
+      simp_all
+  rw [h1]
+  rw [List.filter_cons]
+  simp only [decide_not, (IsTotal.to_isRefl le1).refl r0, not_true_eq_false, decide_False,
+    Bool.false_eq_true, ↓reduceIte]
+  rw [orderedInsertPos_take]
+  simp only [decide_not, List.append_right_eq_self, List.filter_eq_nil_iff, Bool.not_eq_eq_eq_not,
+    Bool.not_true, decide_eq_false_iff_not, Decidable.not_not]
+  intro a ha
+  refine List.Sorted.rel_of_mem_take_of_mem_drop
+    (k := (orderedInsertPos le1 (List.insertionSort le1 r) r0).1 + 1)
+    (List.sorted_insertionSort le1 (r0 :: r)) ?_ ?_
+  · simp only [List.insertionSort, List.orderedInsert_eq_take_drop, decide_not]
+    rw [List.take_append_eq_append_take]
+    rw [List.take_of_length_le]
+    · simp [orderedInsertPos]
+    · simp [orderedInsertPos]
+  · simp only [List.insertionSort, List.orderedInsert_eq_take_drop, decide_not]
+    rw [List.drop_append_eq_append_drop]
+    rw [List.drop_of_length_le]
+    · simpa [orderedInsertPos] using ha
+    · simp [orderedInsertPos]
+
+lemma koszulSignInsert_insertIdx {I : Type} (q : I → Fin 2) (le1 : I → I → Prop) [DecidableRel le1]
+    (i j : I) [IsTotal I le1] [IsTrans I le1] (r : List I) (n : ℕ) (hn : n ≤ r.length) :
+    koszulSignInsert le1 q j (List.insertIdx n i r) = koszulSignInsert le1 q j (i :: r) := by
+  apply koszulSignInsert_eq_perm
+  exact List.perm_insertIdx i r hn
+
+end Wick
--- a/HepLean/PerturbationTheory/Wick/Signs/StaticWickCoef.lean
+++ b/HepLean/PerturbationTheory/Wick/Signs/StaticWickCoef.lean
@ -0,0 +1,91 @@
+/-
+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 Mathlib.Algebra.FreeAlgebra
+import Mathlib.Algebra.Lie.OfAssociative
+import Mathlib.Analysis.Complex.Basic
+import HepLean.PerturbationTheory.Wick.Signs.KoszulSign
+/-!
+
+# Koszul sign insert
+
+-/
+
+namespace Wick
+
+open HepLean.List
+
+def superCommuteCoefLE {I : Type} (q : I → Fin 2) (le1 :I → I → Prop) (r : List I)
+    [DecidableRel le1] (i : I) (n : Fin r.length) : ℂ :=
+  koszulSign le1 q r *
+  superCommuteCoef q [i] (List.take (↑((HepLean.List.insertionSortEquiv le1 r) n))
+    (List.insertionSort le1 r)) *
+  koszulSign le1 q (r.eraseIdx ↑n)
+
+lemma superCommuteCoefLE_eq_q {I : Type} (q : I → Fin 2) (le1 :I → I → Prop) (r : List I)
+    [DecidableRel le1] (i : I) (n : Fin r.length)
+    (hq : q i = q (r.get n)) :
+    superCommuteCoefLE q le1 r i n =
+    koszulSign le1 q r *
+    superCommuteCoef q [r.get n] (List.take (↑(insertionSortEquiv le1 r n))
+      (List.insertionSort le1 r)) *
+    koszulSign le1 q (r.eraseIdx ↑n) := by
+  simp [superCommuteCoefLE, superCommuteCoef, grade, hq]
+
+
+lemma insertIdx_eraseIdx {I : Type} :
+    (n : ℕ) → (r : List I) → (hn : n < r.length) →
+    List.insertIdx n (r.get ⟨n, hn⟩) (r.eraseIdx n) = r
+  | n, [], hn => by
+    simp at hn
+  | 0, r0 :: r, hn => by
+    simp
+  | n + 1, r0 :: r, hn => by
+    simp only [List.length_cons, List.get_eq_getElem, List.getElem_cons_succ,
+      List.eraseIdx_cons_succ, List.insertIdx_succ_cons, List.cons.injEq, true_and]
+    exact insertIdx_eraseIdx n r _
+
+lemma superCommuteCoefLE_eq_get {I : Type} (q : I → Fin 2) (le1 :I → I → Prop) (r : List I)
+    [DecidableRel le1] [IsTotal I le1] [IsTrans I le1] (i : I) (n : Fin r.length)
+    (heq : q i = q (r.get n)) :
+    superCommuteCoefLE q le1 r i n = superCommuteCoef q [r.get n] (r.take n) := by
+  rw [superCommuteCoefLE_eq_q]
+  let r' := r.eraseIdx ↑n
+  have hr : List.insertIdx n (r.get n) (r.eraseIdx n) = r := by
+    exact insertIdx_eraseIdx n.1 r n.prop
+  conv_lhs =>
+    lhs
+    lhs
+    rw [← hr]
+    rw [koszulSign_insertIdx q le1 (r.get n) ((r.eraseIdx ↑n)) n (by
+      rw [List.length_eraseIdx]
+      simp only [Fin.is_lt, ↓reduceIte]
+      omega)]
+    rhs
+    rhs
+    rw [hr]
+  conv_lhs =>
+    lhs
+    lhs
+    rhs
+    enter [2, 1, 1]
+    rw [insertionSortEquiv_congr _ _ hr]
+  simp only [List.get_eq_getElem, Equiv.trans_apply, RelIso.coe_fn_toEquiv, Fin.castOrderIso_apply,
+    Fin.cast_mk, Fin.eta, Fin.coe_cast]
+  conv_lhs =>
+    lhs
+    rw [mul_assoc]
+    rhs
+    rw [insertSign]
+    rw [superCommuteCoef_mul_self]
+  simp only [mul_one]
+  rw [mul_assoc]
+  rw [koszulSign_mul_self]
+  simp only [mul_one]
+  rw [insertSign_eraseIdx]
+  rfl
+  exact heq
+
+end Wick
--- a/HepLean/PerturbationTheory/Wick/Signs/SuperCommuteCoef.lean
+++ b/HepLean/PerturbationTheory/Wick/Signs/SuperCommuteCoef.lean
@ -0,0 +1,83 @@
+/-
+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.Mathematics.List
+import HepLean.PerturbationTheory.Wick.Signs.Grade
+/-!
+
+# Koszul signs and ordering for lists and algebras
+
+-/
+
+namespace Wick
+open HepLean.List
+
+def superCommuteCoef {I : Type} (q : I → Fin 2) (la lb : List I) : ℂ :=
+  if grade q la = 1 ∧ grade q lb = 1 then - 1 else 1
+
+lemma superCommuteCoef_comm {I : Type} (q : I → Fin 2) (la lb : List I) :
+    superCommuteCoef q la lb = superCommuteCoef q lb la := by
+  simp only [superCommuteCoef, Fin.isValue]
+  congr 1
+  exact Eq.propIntro (fun a => id (And.symm a)) fun a => id (And.symm a)
+
+def superCommuteLiftCoef {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
+    (q : I → Fin 2) (l : List (Σ i, f i)) (r : List I) : ℂ :=
+    (if grade (fun i => q i.fst) l = 1 ∧ grade q r = 1 then -1 else 1)
+
+lemma superCommuteLiftCoef_empty {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
+    (q : I → Fin 2) (l : List (Σ i, f i)) :
+    superCommuteLiftCoef q l [] = 1 := by
+  simp [superCommuteLiftCoef]
+
+lemma superCommuteCoef_perm_snd {I : Type} (q : I → Fin 2) (la lb lb' : List I)
+    (h : lb.Perm lb') :
+    superCommuteCoef q la lb = superCommuteCoef q la lb' := by
+  rw [superCommuteCoef, superCommuteCoef, grade_perm q h]
+
+lemma superCommuteCoef_mul_self {I : Type} (q : I → Fin 2) (l lb : List I) :
+    superCommuteCoef q l lb * superCommuteCoef q l lb = 1 := by
+  simp only [superCommuteCoef, Fin.isValue, mul_ite, mul_neg, mul_one]
+  have ha (a b : Fin 2) : (if a = 1 ∧ b = 1 then -if a = 1 ∧ b = 1 then -1 else 1
+    else if a = 1 ∧ b = 1 then -1 else 1) = (1 : ℂ) := by
+      fin_cases a <;> fin_cases b
+      any_goals rfl
+      simp
+  exact ha (grade q l) (grade q lb)
+
+lemma superCommuteCoef_empty {I : Type} (q : I → Fin 2) (la : List I) :
+    superCommuteCoef q la [] = 1 := by
+  simp only [superCommuteCoef, Fin.isValue, grade_empty, zero_ne_one, and_false, ↓reduceIte]
+
+lemma superCommuteCoef_append {I : Type} (q : I → Fin 2) (la lb lc : List I) :
+    superCommuteCoef q la (lb ++ lc) = superCommuteCoef q la lb * superCommuteCoef q la lc := by
+  simp only [superCommuteCoef, Fin.isValue, grade_append, ite_eq_right_iff, zero_ne_one, imp_false,
+    mul_ite, mul_neg, mul_one]
+  by_cases hla : grade q la = 1
+  · by_cases hlb : grade q lb = 1
+    · by_cases hlc : grade q lc = 1
+      · simp [hlc, hlb, hla]
+      · have hc : grade q lc = 0 := by
+          omega
+        simp [hc, hlb, hla]
+    · have hb : grade q lb = 0 := by
+        omega
+      by_cases hlc : grade q lc = 1
+      · simp [hlc, hb]
+      · have hc : grade q lc = 0 := by
+          omega
+        simp [hc, hb]
+  · have ha : grade q la = 0 := by
+      omega
+    simp [ha]
+
+lemma superCommuteCoef_cons {I : Type} (q : I → Fin 2) (i : I) (la lb : List I) :
+    superCommuteCoef q la (i :: lb) = superCommuteCoef q la [i] * superCommuteCoef q la lb := by
+  trans superCommuteCoef q la ([i] ++ lb)
+  simp only [List.singleton_append]
+  rw [superCommuteCoef_append]
+
+
+end Wick
--- a/HepLean/PerturbationTheory/Wick/StaticTheorem.lean
+++ b/HepLean/PerturbationTheory/Wick/StaticTheorem.lean
@ -0,0 +1,109 @@
+/-
+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.PerturbationTheory.Wick.Contraction
+/-!
+
+# Static Wick's theorem
+
+-/
+
+namespace Wick
+
+noncomputable section
+
+open HepLean.List
+
+lemma static_wick_nil {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
+    (q : I → Fin 2)
+    (le1 : (Σ i, f i) → (Σ i, f i) → Prop) [DecidableRel le1]
+    {A : Type} [Semiring A] [Algebra ℂ A]
+    (F : FreeAlgebra ℂ (Σ i, f i) →ₐ A) [OperatorMap (fun i => q i.1) le1 F]
+    (S : Contractions.Splitting f le1) :
+    F (ofListLift f [] 1) = ∑ c : Contractions [],
+    c.toCenterTerm f q le1 F S *
+    F (koszulOrder le1 (fun i => q i.fst) (ofListLift f c.normalize 1)) := by
+  rw [← Contractions.nilEquiv.symm.sum_comp]
+  simp only [Finset.univ_unique, PUnit.default_eq_unit, Contractions.nilEquiv, Equiv.coe_fn_symm_mk,
+    Finset.sum_const, Finset.card_singleton, one_smul]
+  dsimp [Contractions.normalize, Contractions.toCenterTerm]
+  simp [ofListLift_empty]
+
+lemma static_wick_cons {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
+    (q : I → Fin 2)
+    (le1 : (Σ i, f i) → (Σ i, f i) → Prop) [DecidableRel le1]
+    [IsTrans ((i : I) × f i) le1] [IsTotal ((i : I) × f i) le1]
+    {A : Type} [Semiring A] [Algebra ℂ A] (r : List I) (a : I)
+    (F : FreeAlgebra ℂ (Σ i, f i) →ₐ A) [OperatorMap (fun i => q i.1) le1 F]
+    (S : Contractions.Splitting f le1)
+    (ih : F (ofListLift f r 1) =
+    ∑ c : Contractions r, c.toCenterTerm f q le1 F S * F (koszulOrder le1 (fun i => q i.fst)
+      (ofListLift f c.normalize 1))) :
+    F (ofListLift f (a :: r) 1) = ∑ c : Contractions (a :: r),
+      c.toCenterTerm f q le1 F S *
+      F (koszulOrder le1 (fun i => q i.fst) (ofListLift f c.normalize 1)) := by
+  rw [ofListLift_cons_eq_ofListLift, map_mul, ih, Finset.mul_sum,
+    ← Contractions.consEquiv.symm.sum_comp]
+  erw [Finset.sum_sigma]
+  congr
+  funext c
+  have hb := S.h𝓑 a
+  rw [← mul_assoc]
+  have hi := c.toCenterTerm_center f q le1 F S
+  rw [Subalgebra.mem_center_iff] at hi
+  rw [hi, mul_assoc, ← map_mul, hb, add_mul, map_add]
+  conv_lhs =>
+    rhs
+    lhs
+    rw [ofList_eq_smul_one]
+    rw [Algebra.smul_mul_assoc]
+    rw [ofList_singleton]
+  rw [mul_koszulOrder_le]
+  conv_lhs =>
+    rhs
+    lhs
+    rw [← map_smul, ← Algebra.smul_mul_assoc]
+    rw [← ofList_singleton, ← ofList_eq_smul_one]
+  conv_lhs =>
+    rhs
+    rhs
+    rw [ofList_eq_smul_one, Algebra.smul_mul_assoc, map_smul]
+  rw [le_all_mul_koszulOrder_ofListLift_expand]
+  conv_lhs =>
+    rhs
+    rhs
+    rw [smul_add, Finset.smul_sum]
+    rw [← map_smul, ← map_smul, ← Algebra.smul_mul_assoc, ← ofList_eq_smul_one]
+    rhs
+    rhs
+    intro n
+    rw [← Algebra.smul_mul_assoc, smul_comm, ← map_smul, ← LinearMap.map_smul₂,
+      ← ofList_eq_smul_one]
+  rw [← add_assoc, ← map_add, ← map_add, ← add_mul, ← hb, ← ofListLift_cons_eq_ofListLift, mul_add]
+  rw [Fintype.sum_option]
+  congr 1
+  rw [Finset.mul_sum]
+  congr
+  funext n
+  rw [← mul_assoc]
+  rfl
+  exact S.h𝓑p a
+  exact S.h𝓑n a
+
+theorem static_wick_theorem {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
+    (q : I → Fin 2)
+    (le1 : (Σ i, f i) → (Σ i, f i) → Prop) [DecidableRel le1] [IsTrans ((i : I) × f i) le1]
+    [IsTotal ((i : I) × f i) le1]
+    {A : Type} [Semiring A] [Algebra ℂ A] (r : List I)
+    (F : FreeAlgebra ℂ (Σ i, f i) →ₐ A) [OperatorMap (fun i => q i.1) le1 F]
+    (S : Contractions.Splitting f le1) :
+    F (ofListLift f r 1) = ∑ c : Contractions r, c.toCenterTerm f q le1 F S *
+    F (koszulOrder le1 (fun i => q i.fst) (ofListLift f c.normalize 1)) := by
+  induction r with
+  | nil => exact static_wick_nil q le1 F S
+  | cons a r ih => exact static_wick_cons q le1 r a F S ih
+
+end
+end Wick
--- a/HepLean/PerturbationTheory/Wick/Koszul/SuperCommute.lean
+++ b/HepLean/PerturbationTheory/Wick/Koszul/SuperCommute.lean
@ -3,7 +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.PerturbationTheory.Wick.Koszul.OfList
+import HepLean.PerturbationTheory.Wick.OfList
 /-!

 # Koszul signs and ordering for lists and algebras
@ -193,7 +193,7 @@ lemma superCommute_ofList_mul {I : Type} (q : I → Fin 2) (la lb lc : List I) (
    mul_neg, smul_add, one_smul, smul_neg]
    abel

-def superCommuteTake {I : Type} (q : I → Fin 2) (la lb : List I) (xa xb : ℂ) (n : ℕ)
+def superCommuteSplit {I : Type} (q : I → Fin 2) (la lb : List I) (xa xb : ℂ) (n : ℕ)
  (hn : n < lb.length) : FreeAlgebra ℂ I :=
  superCommuteCoef q la (List.take n lb) •
  ofList (List.take n lb) 1 *
@ -212,7 +212,7 @@ lemma superCommute_ofList_cons {I : Type} (q : I → Fin 2) (la lb : List I) (xa

 lemma superCommute_ofList_sum {I : Type} (q : I → Fin 2) (la lb : List I) (xa xb : ℂ) :
    superCommute q (ofList la xa) (ofList lb xb) =
-    ∑ (n : Fin lb.length), superCommuteTake q la lb xa xb n n.prop := by
+    ∑ (n : Fin lb.length), superCommuteSplit q la lb xa xb n n.prop := by
  induction lb with
  | nil =>
    simp only [superCommute_ofList_ofList, List.append_nil, Fin.isValue, grade_empty, zero_ne_one,
@ -223,8 +223,8 @@ lemma superCommute_ofList_sum {I : Type} (q : I → Fin 2) (la lb : List I) (xa
  | cons b lb ih =>
    rw [superCommute_ofList_cons, ih]
    have h0 : ((superCommute q) (ofList la xa)) (FreeAlgebra.ι ℂ b) * ofList lb xb =
-        superCommuteTake q la (b :: lb) xa xb 0 (Nat.zero_lt_succ lb.length) := by
-      simp [superCommuteTake, superCommuteCoef_empty, ofList_empty]
+        superCommuteSplit q la (b :: lb) xa xb 0 (Nat.zero_lt_succ lb.length) := by
+      simp [superCommuteSplit, superCommuteCoef_empty, ofList_empty]
    rw [h0]
    have hf (f : Fin (b :: lb).length → FreeAlgebra ℂ I) : ∑ n, f n = f ⟨0,
        Nat.zero_lt_succ lb.length⟩ + ∑ n, f (Fin.succ n) := by
@ -234,7 +234,7 @@ lemma superCommute_ofList_sum {I : Type} (q : I → Fin 2) (la lb : List I) (xa
    rw [Finset.mul_sum]
    congr
    funext n
-    simp only [superCommuteTake, Fin.eta, List.get_eq_getElem, Algebra.smul_mul_assoc,
+    simp only [superCommuteSplit, Fin.eta, List.get_eq_getElem, Algebra.smul_mul_assoc,
      Algebra.mul_smul_comm, smul_smul, List.length_cons, Fin.val_succ, List.take_succ_cons,
      List.getElem_cons_succ, List.drop_succ_cons]
    congr 1
@ -258,7 +258,7 @@ lemma ofList_ofList_superCommute {I : Type} (q : I → Fin 2) (la lb : List I) (
  rw [superCommute_ofList_ofList_superCommuteCoef]
  abel

-lemma ofListM_ofList_superCommute' {I : Type}
+lemma ofListLift_ofList_superCommute' {I : Type}
    (q : I → Fin 2) (l : List I) (r : List I) (x y : ℂ) :
  ofList r y * ofList l x = superCommuteCoef q l r • (ofList l x * ofList r y)
    - superCommuteCoef q l r • superCommute q (ofList l x) (ofList r y) := by
@ -268,5 +268,186 @@ lemma ofListM_ofList_superCommute' {I : Type}
  · simp [hq, superCommuteCoef]
  · simp [hq]

+
+lemma superCommute_ofList_ofListLift {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
+    (q : I → Fin 2) (l : List (Σ i, f i)) (r : List I) (x y : ℂ) :
+    superCommute (fun i => q i.1) (ofList l x) (ofListLift f r y) =
+    ofList l x * ofListLift f r y +
+    (if grade (fun i => q i.1) l = 1 ∧ grade q r = 1 then
+    ofListLift f r y * ofList l x else - ofListLift f r y * ofList l x) := by
+  conv_lhs => rw [ofListLift_expand]
+  rw [map_sum]
+  conv_rhs =>
+    lhs
+    rw [ofListLift_expand, Finset.mul_sum]
+  conv_rhs =>
+    rhs
+    rhs
+    rw [ofListLift_expand, ← Finset.sum_neg_distrib, Finset.sum_mul]
+  conv_rhs =>
+    rhs
+    lhs
+    rw [ofListLift_expand, Finset.sum_mul]
+  rw [← Finset.sum_ite_irrel]
+  rw [← Finset.sum_add_distrib]
+  congr
+  funext a
+  rw [superCommute_ofList_ofList]
+  congr 1
+  · exact ofList_pair l a.toList x y
+  congr 1
+  · simp
+  · exact ofList_pair a.toList l y x
+  · rw [ofList_pair]
+    simp only [neg_mul]
+
+lemma superCommute_ofList_ofListLift_superCommuteLiftCoef {I : Type} {f : I → Type}
+    [∀ i, Fintype (f i)]
+    (q : I → Fin 2) (l : List (Σ i, f i)) (r : List I) (x y : ℂ) :
+    superCommute (fun i => q i.1) (ofList l x) (ofListLift f r y) =
+    ofList l x * ofListLift f r y - superCommuteLiftCoef q l r • ofListLift f r y * ofList l x := by
+  rw [superCommute_ofList_ofListLift, superCommuteLiftCoef]
+  by_cases hq : grade (fun i => q i.fst) l = 1 ∧ grade q r = 1
+  · simp [hq]
+  · simp only [Fin.isValue, hq, ↓reduceIte, neg_mul, one_smul]
+    abel
+
+lemma ofList_ofListLift_superCommute {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
+    (q : I → Fin 2) (l : List (Σ i, f i)) (r : List I) (x y : ℂ) :
+    ofList l x * ofListLift f r y = superCommuteLiftCoef q l r • ofListLift f r y * ofList l x
+    + superCommute (fun i => q i.1) (ofList l x) (ofListLift f r y) := by
+  rw [superCommute_ofList_ofListLift_superCommuteLiftCoef]
+  abel
+
+lemma ofListLift_ofList_superCommute {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
+    (q : I → Fin 2) (l : List (Σ i, f i)) (r : List I) (x y : ℂ) :
+  ofListLift f r y * ofList l x = superCommuteLiftCoef q l r • (ofList l x * ofListLift f r y)
+    - superCommuteLiftCoef q l r • superCommute (fun i => q i.1) (ofList l x) (ofListLift f r y) := by
+  rw [ofList_ofListLift_superCommute, superCommuteLiftCoef]
+  by_cases hq : grade (fun i => q i.fst) l = 1 ∧ grade q r = 1
+  · simp [hq]
+  · simp [hq]
+
+lemma superCommuteLiftCoef_append {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
+    (q : I → Fin 2) (l : List (Σ i, f i)) (r1 r2 : List I) :
+    superCommuteLiftCoef q l (r1 ++ r2) = superCommuteLiftCoef q l r1 * superCommuteLiftCoef q l r2 := by
+  simp only [superCommuteLiftCoef, Fin.isValue, grade_append, ite_eq_right_iff, zero_ne_one, imp_false,
+    mul_ite, mul_neg, mul_one]
+  by_cases hla : grade (fun i => q i.1) l = 1
+  · by_cases hlb : grade q r1 = 1
+    · by_cases hlc : grade q r2 = 1
+      · simp [hlc, hlb, hla]
+      · have hc : grade q r2 = 0 := by
+          omega
+        simp [hc, hlb, hla]
+    · have hb : grade q r1 = 0 := by
+        omega
+      by_cases hlc : grade q r2 = 1
+      · simp [hlc, hb]
+      · have hc : grade q r2 = 0 := by
+          omega
+        simp [hc, hb]
+  · have ha : grade (fun i => q i.1) l = 0 := by
+      omega
+    simp [ha]
+
+def superCommuteLiftSplit {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
+    (q : I → Fin 2) (l : List (Σ i, f i)) (r : List I) (x y : ℂ) (n : ℕ)
+    (hn : n < r.length) : FreeAlgebra ℂ (Σ i, f i) :=
+  superCommuteLiftCoef q l (List.take n r) •
+  (ofListLift f (List.take n r) 1 *
+  superCommute (fun i => q i.1) (ofList l x) (sumFiber f (FreeAlgebra.ι ℂ (r.get ⟨n, hn⟩)))
+  * ofListLift f (List.drop (n + 1) r) y)
+
+lemma superCommute_ofList_ofListLift_cons {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
+    (q : I → Fin 2) (l : List (Σ i, f i)) (r : List I) (x y : ℂ) (b1 : I) :
+    superCommute (fun i => q i.1) (ofList l x) (ofListLift f (b1 :: r) y) =
+    superCommute (fun i => q i.1) (ofList l x) (sumFiber f (FreeAlgebra.ι ℂ b1))
+    * ofListLift f r y + superCommuteLiftCoef q l [b1] •
+    (ofListLift f [b1] 1) * superCommute (fun i => q i.1) (ofList l x) (ofListLift f r y) := by
+  rw [ofListLift_cons]
+  conv_lhs =>
+    rhs
+    rw [ofListLift_expand]
+    rw [Finset.mul_sum]
+  rw [map_sum]
+  trans ∑ (n : CreateAnnilateSect f r), ∑ j : f b1, ((superCommute fun i => q i.fst) (ofList l x))
+    ((FreeAlgebra.ι ℂ ⟨b1, j⟩) * ofList n.toList y)
+  · apply congrArg
+    funext n
+    rw [← map_sum]
+    congr
+    rw [Finset.sum_mul]
+  conv_rhs =>
+    lhs
+    rw [ofListLift_expand, Finset.mul_sum]
+  conv_rhs =>
+    rhs
+    rhs
+    rw [ofListLift_expand]
+    rw [map_sum]
+  conv_rhs =>
+    rhs
+    rw [Finset.mul_sum]
+  rw [← Finset.sum_add_distrib]
+  congr
+  funext n
+  rw [sumFiber_ι, map_sum, Finset.sum_mul]
+  conv_rhs =>
+    rhs
+    rw [ofListLift_singleton]
+    rw [Finset.smul_sum, Finset.sum_mul]
+  rw [← Finset.sum_add_distrib]
+  congr
+  funext b
+  trans ((superCommute fun i => q i.fst) (ofList l x)) (ofList (⟨b1, b⟩ :: n.toList) y)
+  · congr
+    rw [ofList_cons_eq_ofList]
+    rw [ofList_singleton]
+  rw [superCommute_ofList_cons]
+  congr
+  rw [ofList_singleton]
+  simp
+
+lemma superCommute_ofList_ofListLift_sum {I : Type} {f : I → Type} [∀ i, Fintype (f i)]
+    (q : I → Fin 2) (l : List (Σ i, f i)) (r : List I) (x y : ℂ) :
+    superCommute (fun i => q i.1) (ofList l x) (ofListLift f r y) =
+    ∑ (n : Fin r.length), superCommuteLiftSplit q l r x y n n.prop := by
+  induction r with
+  | nil =>
+    simp only [superCommute_ofList_ofListLift, Fin.isValue, grade_empty, zero_ne_one, and_false,
+      ↓reduceIte, neg_mul, List.length_nil, Finset.univ_eq_empty, Finset.sum_empty]
+    rw [ofListLift, ofList_empty']
+    simp
+  | cons b r ih =>
+    rw [superCommute_ofList_ofListLift_cons]
+    have h0 : ((superCommute fun i => q i.fst) (ofList l x))
+        ((sumFiber f) (FreeAlgebra.ι ℂ b)) * ofListLift f r y =
+        superCommuteLiftSplit q l (b :: r) x y 0 (Nat.zero_lt_succ r.length) := by
+      simp [superCommuteLiftSplit, superCommuteLiftCoef_empty, ofListLift_empty]
+    rw [h0]
+    have hf (g : Fin (b :: r).length → FreeAlgebra ℂ ((i : I) × f i)) : ∑ n, g n = g ⟨0,
+        Nat.zero_lt_succ r.length⟩ + ∑ n, g (Fin.succ n) := by
+      exact Fin.sum_univ_succAbove g ⟨0, Nat.zero_lt_succ r.length⟩
+    rw [hf]
+    congr
+    rw [ih]
+    rw [Finset.mul_sum]
+    congr
+    funext n
+    simp only [superCommuteLiftSplit, Fin.eta, List.get_eq_getElem, Algebra.mul_smul_comm,
+      Algebra.smul_mul_assoc, smul_smul, List.length_cons, Fin.val_succ, List.take_succ_cons,
+      List.getElem_cons_succ, List.drop_succ_cons]
+    congr 1
+    · rw [mul_comm, ← superCommuteLiftCoef_append]
+      rfl
+    · simp only [← mul_assoc, mul_eq_mul_right_iff]
+      apply Or.inl
+      apply Or.inl
+      rw [ofListLift, ofListLift, ofListLift]
+      rw [← map_mul]
+      congr
+      rw [← ofList_pair, one_mul]
+      rfl
 end
 end Wick