refactor: Rename OperatorAlgebra

HepLean.lean

@@ -121,9 +121,9 @@ import HepLean.Meta.TransverseTactics
 import HepLean.PerturbationTheory.Algebras.CrAnAlgebra.Basic
 import HepLean.PerturbationTheory.Algebras.CrAnAlgebra.NormalOrder
 import HepLean.PerturbationTheory.Algebras.CrAnAlgebra.SuperCommute
-import HepLean.PerturbationTheory.Algebras.OperatorAlgebra.Basic
+import HepLean.PerturbationTheory.Algebras.ProtoOperatorAlgebra.Basic
-import HepLean.PerturbationTheory.Algebras.OperatorAlgebra.NormalOrder
+import HepLean.PerturbationTheory.Algebras.ProtoOperatorAlgebra.NormalOrder
-import HepLean.PerturbationTheory.Algebras.OperatorAlgebra.TimeContraction
+import HepLean.PerturbationTheory.Algebras.ProtoOperatorAlgebra.TimeContraction
 import HepLean.PerturbationTheory.Algebras.StateAlgebra.Basic
 import HepLean.PerturbationTheory.Algebras.StateAlgebra.TimeOrder
 import HepLean.PerturbationTheory.CreateAnnihilate

HepLean/PerturbationTheory/Algebras/ProtoOperatorAlgebra/Basic.lean

@@ -18,7 +18,7 @@ open CrAnAlgebra
   to be isomorphic to the actual operator algebra of a field theory.
   These properties are sufficent to prove certain theorems about the Operator algebra
   in particular Wick's theorem. -/
-structure OperatorAlgebra where
+structure ProtoOperatorAlgebra where
   /-- The algebra representing the operator algebra. -/
   A : Type
   /-- The instance of the type `A` as a semi-ring. -/
@@ -43,9 +43,9 @@ structure OperatorAlgebra where
     (_ : ¬ (𝓕 |>ₛ φ) = (𝓕 |>ₛ φ')),
     crAnF (superCommute (ofCrAnState φ) (ofCrAnState φ')) = 0
 
-namespace OperatorAlgebra
+namespace ProtoOperatorAlgebra
 open FieldStatistic
-variable {𝓕 : FieldSpecification} (𝓞 : 𝓕.OperatorAlgebra)
+variable {𝓕 : FieldSpecification} (𝓞 : 𝓕.ProtoOperatorAlgebra)
 
 /-- The algebra `𝓞.A` carries the instance of a semi-ring induced via `A_seimRing`. -/
 instance : Semiring 𝓞.A := 𝓞.A_semiRing
@@ -198,5 +198,5 @@ lemma crAnF_superCommute_ofCrAnState_ofStateList_eq_sum (φ : 𝓕.CrAnStates) (
   · congr
     rw [← map_mul, ← ofStateList_append, ← List.eraseIdx_eq_take_drop_succ]
 
-end OperatorAlgebra
+end ProtoOperatorAlgebra
 end FieldSpecification

HepLean/PerturbationTheory/Algebras/ProtoOperatorAlgebra/NormalOrder.lean

@@ -14,8 +14,8 @@ import HepLean.PerturbationTheory.Koszul.KoszulSign
 namespace FieldSpecification
 variable {𝓕 : FieldSpecification}
 
-namespace OperatorAlgebra
+namespace ProtoOperatorAlgebra
-variable {𝓞 : OperatorAlgebra 𝓕}
+variable {𝓞 : ProtoOperatorAlgebra 𝓕}
 open CrAnAlgebra
 open FieldStatistic
 
@@ -390,6 +390,6 @@ lemma crAnF_ofState_normalOrder_insert (φ : 𝓕.States) (φs : List 𝓕.State
   rw [← ofStateList_append, ← ofStateList_append]
   simp
 
-end OperatorAlgebra
+end ProtoOperatorAlgebra
 
 end FieldSpecification

HepLean/PerturbationTheory/Algebras/ProtoOperatorAlgebra/TimeContraction.lean

@@ -3,7 +3,7 @@ Copyright (c) 2025 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.Algebras.OperatorAlgebra.NormalOrder
+import HepLean.PerturbationTheory.Algebras.ProtoOperatorAlgebra.NormalOrder
 import HepLean.PerturbationTheory.Algebras.StateAlgebra.TimeOrder
 /-!
 
@@ -19,9 +19,9 @@ variable {𝓕 : FieldSpecification}
 open CrAnAlgebra
 noncomputable section
 
-namespace OperatorAlgebra
+namespace ProtoOperatorAlgebra
 
-variable (𝓞 : 𝓕.OperatorAlgebra)
+variable (𝓞 : 𝓕.ProtoOperatorAlgebra)
 open FieldStatistic
 
 /-- The time contraction of two States as an element of `𝓞.A` defined
@@ -86,7 +86,7 @@ lemma timeContract_zero_of_diff_grade (φ ψ : 𝓕.States) (h : (𝓕 |>ₛ φ)
     have ht := IsTotal.total (r := 𝓕.timeOrderRel) φ ψ
     simp_all
 
-end OperatorAlgebra
+end ProtoOperatorAlgebra
 
 end
 end FieldSpecification

HepLean/PerturbationTheory/FieldSpecification/Filters.lean

@@ -3,7 +3,7 @@ Copyright (c) 2025 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.Algebras.OperatorAlgebra.Basic
+import HepLean.PerturbationTheory.Algebras.ProtoOperatorAlgebra.Basic
 import HepLean.PerturbationTheory.Koszul.KoszulSign
 /-!
 

HepLean/PerturbationTheory/FieldSpecification/NormalOrder.lean

@@ -3,7 +3,7 @@ Copyright (c) 2025 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.Algebras.OperatorAlgebra.Basic
+import HepLean.PerturbationTheory.Algebras.ProtoOperatorAlgebra.Basic
 import HepLean.PerturbationTheory.Koszul.KoszulSign
 import HepLean.PerturbationTheory.FieldSpecification.Filters
 /-!

HepLean/PerturbationTheory/WickContraction/Basic.lean

@@ -3,7 +3,7 @@ Copyright (c) 2025 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.Algebras.OperatorAlgebra.NormalOrder
+import HepLean.PerturbationTheory.Algebras.ProtoOperatorAlgebra.NormalOrder
 import HepLean.Mathematics.List.InsertIdx
 /-!
 

HepLean/PerturbationTheory/WickContraction/Involutions.lean

@@ -5,7 +5,7 @@ Authors: Joseph Tooby-Smith
 -/
 import HepLean.PerturbationTheory.WickContraction.Uncontracted
 import HepLean.PerturbationTheory.Algebras.StateAlgebra.TimeOrder
-import HepLean.PerturbationTheory.Algebras.OperatorAlgebra.TimeContraction
+import HepLean.PerturbationTheory.Algebras.ProtoOperatorAlgebra.TimeContraction
 import HepLean.PerturbationTheory.WickContraction.InsertList
 /-!
 

HepLean/PerturbationTheory/WickContraction/IsFull.lean

@@ -19,6 +19,7 @@ namespace WickContraction
 variable {n : ℕ} (c : WickContraction n)
 open HepLean.List
 open FieldStatistic
+open Nat
 
 /-- A contraction is full if there are no uncontracted fields, i.e. the finite set
   of uncontracted fields is empty. -/
@@ -46,8 +47,6 @@ def isFullInvolutionEquiv : {c : WickContraction n // IsFull c} ≃
   left_inv c := by simp
   right_inv f := by simp
 
-open Nat
-
 /-- If `n` is even then the number of full contractions is `(n-1)!!`. -/
 theorem card_of_isfull_even (he : Even n) :
     Fintype.card {c : WickContraction n // IsFull c} = (n - 1)‼ := by

HepLean/PerturbationTheory/WickContraction/Sign.lean

@@ -85,8 +85,7 @@ lemma signFinset_insertList_none (φ : 𝓕.States) (φs : List 𝓕.States)
 
 lemma stat_ofFinset_of_insertListLiftFinset (φ : 𝓕.States) (φs : List 𝓕.States)
     (i : Fin φs.length.succ) (a : Finset (Fin φs.length)) :
-    (𝓕 |>ₛ ⟨(φs.insertIdx i φ).get, insertListLiftFinset φ i a⟩) =
+    (𝓕 |>ₛ ⟨(φs.insertIdx i φ).get, insertListLiftFinset φ i a⟩) = 𝓕 |>ₛ ⟨φs.get, a⟩ := by
-    𝓕 |>ₛ ⟨φs.get, a⟩ := by
   simp only [ofFinset, Nat.succ_eq_add_one]
   congr 1
   rw [get_eq_insertIdx_succAbove φ _ i]
@@ -823,8 +822,7 @@ lemma stat_signFinset_insert_some_self_fst
             simpa [Option.get_map] using hy2
 
 lemma stat_signFinset_insert_some_self_snd (φ : 𝓕.States) (φs : List 𝓕.States)
-    (c : WickContraction φs.length)
+    (c : WickContraction φs.length) (i : Fin φs.length.succ) (j : c.uncontracted) :
-    (i : Fin φs.length.succ) (j : c.uncontracted) :
     (𝓕 |>ₛ ⟨(φs.insertIdx i φ).get,
     (signFinset (c.insertList φ φs i (some j))
       (finCongr (insertIdx_length_fin φ φs i).symm (i.succAbove j))
@@ -832,8 +830,7 @@ lemma stat_signFinset_insert_some_self_snd (φ : 𝓕.States) (φs : List 𝓕.S
     𝓕 |>ₛ ⟨φs.get,
     (Finset.univ.filter (fun x => j < x ∧ i.succAbove x < i ∧ ((c.getDual? x = none) ∨
       ∀ (h : (c.getDual? x).isSome), j < ((c.getDual? x).get h))))⟩ := by
-  rw [get_eq_insertIdx_succAbove φ _ i]
+  rw [get_eq_insertIdx_succAbove φ _ i, ofFinset_finset_map]
-  rw [ofFinset_finset_map]
   swap
   refine
     (Equiv.comp_injective i.succAbove (finCongr (Eq.symm (insertIdx_length_fin φ φs i)))).mpr ?hi.a
@@ -905,55 +902,43 @@ lemma stat_signFinset_insert_some_self_snd (φ : 𝓕.States) (φs : List 𝓕.S
             exact Fin.succAbove_lt_succAbove_iff.mpr hy2
 
 lemma signInsertSomeCoef_eq_finset (φ : 𝓕.States) (φs : List 𝓕.States)
-    (c : WickContraction φs.length)
+    (c : WickContraction φs.length) (i : Fin φs.length.succ) (j : c.uncontracted)
-    (i : Fin φs.length.succ) (j : c.uncontracted) (hφj : (𝓕 |>ₛ φ) = (𝓕 |>ₛ φs[j.1])) :
+    (hφj : (𝓕 |>ₛ φ) = (𝓕 |>ₛ φs[j.1])) :  c.signInsertSomeCoef φ φs i j =
-    c.signInsertSomeCoef φ φs i j =
     if i < i.succAbove j then
-    𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ⟨φs.get,
+      𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ⟨φs.get,
-    (Finset.univ.filter (fun x => i < i.succAbove x ∧ x < j ∧ ((c.getDual? x = none) ∨
+      (Finset.univ.filter (fun x => i < i.succAbove x ∧ x < j ∧ ((c.getDual? x = none) ∨
-      ∀ (h : (c.getDual? x).isSome), i < i.succAbove ((c.getDual? x).get h))))⟩) else
+        ∀ (h : (c.getDual? x).isSome), i < i.succAbove ((c.getDual? x).get h))))⟩)
-    𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ⟨φs.get,
+    else
-      (Finset.univ.filter (fun x => j < x ∧ i.succAbove x < i ∧ ((c.getDual? x = none) ∨
+      𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ⟨φs.get,
-      ∀ (h : (c.getDual? x).isSome), j < ((c.getDual? x).get h))))⟩) := by
+        (Finset.univ.filter (fun x => j < x ∧ i.succAbove x < i ∧ ((c.getDual? x = none) ∨
-  rw [signInsertSomeCoef_if]
+        ∀ (h : (c.getDual? x).isSome), j < ((c.getDual? x).get h))))⟩) := by
-  rw [stat_signFinset_insert_some_self_snd]
+  rw [signInsertSomeCoef_if, stat_signFinset_insert_some_self_snd,
-  rw [stat_signFinset_insert_some_self_fst]
+    stat_signFinset_insert_some_self_fst]
   simp [hφj]
 
 lemma signInsertSome_mul_filter_contracted_of_lt (φ : 𝓕.States) (φs : List 𝓕.States)
     (c : WickContraction φs.length) (i : Fin φs.length.succ) (k : c.uncontracted)
-    (hk : i.succAbove k < i)
+    (hk : i.succAbove k < i) (hg : GradingCompliant φs c ∧ (𝓕 |>ₛ φ) = 𝓕 |>ₛ φs[k.1]) :
-    (hg : GradingCompliant φs c ∧ 𝓕.statesStatistic φ = 𝓕.statesStatistic φs[k.1]) :
     signInsertSome φ φs c i k *
     𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ⟨φs.get, c.uncontracted.filter (fun x => x ≤ ↑k)⟩)
     = 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ⟨φs.get, Finset.univ.filter (fun x => i.succAbove x < i)⟩) := by
-  rw [signInsertSome, signInsertSomeProd_eq_finset, signInsertSomeCoef_eq_finset]
+  rw [signInsertSome, signInsertSomeProd_eq_finset (hφj := hg.2) (hg := hg.1),
-  rw [if_neg (by omega), ← map_mul, ← map_mul]
+    signInsertSomeCoef_eq_finset (hφj := hg.2), if_neg (by omega), ← map_mul, ← map_mul]
   congr 1
   rw [mul_eq_iff_eq_mul, ofFinset_union_disjoint]
   swap
-  · rw [Finset.disjoint_filter]
+  · /- Disjointness needed for `ofFinset_union_disjoint`. -/
+    rw [Finset.disjoint_filter]
     intro j _ h
     simp only [Nat.succ_eq_add_one, not_lt, not_and, not_forall, not_or, not_le]
     intro h1
     use h1
     omega
-  trans 𝓕 |>ₛ ⟨φs.get, (Finset.filter (fun x =>
-      (↑k < x ∧ i.succAbove x < i ∧ (c.getDual? x = none ∨
-      ∀ (h : (c.getDual? x).isSome = true), ↑k < (c.getDual? x).get h))
-      ∨ ((c.getDual? x).isSome = true ∧
-      ∀ (h : (c.getDual? x).isSome = true), x < ↑k ∧
-      (i.succAbove x < i ∧ i < i.succAbove ((c.getDual? x).get h) ∨
-      ↑k < (c.getDual? x).get h ∧ ¬i.succAbove x < i))) Finset.univ)⟩
-  · congr
-    ext j
-    simp
   rw [ofFinset_union, ← mul_eq_one_iff, ofFinset_union]
   simp only [Nat.succ_eq_add_one, not_lt]
-  apply stat_ofFinset_eq_one_of_gradingCompliant
+  apply stat_ofFinset_eq_one_of_gradingCompliant _ _ _ hg.1
-  · exact hg.1
+  · /- The `c.getDual? i = none` case for `stat_ofFinset_eq_one_of_gradingCompliant`. -/
-  /- the getDual? is none case-/
+    intro j hn
-  · intro j hn
     simp only [uncontracted, Finset.mem_sdiff, Finset.mem_union, Finset.mem_filter, Finset.mem_univ,
       hn, Option.isSome_none, Bool.false_eq_true, IsEmpty.forall_iff, or_self, and_true, or_false,
       true_and, and_self, Finset.mem_inter, not_and, not_lt, Classical.not_imp, not_le, and_imp]
@@ -978,8 +963,8 @@ lemma signInsertSome_mul_filter_contracted_of_lt (φ : 𝓕.States) (φs : List
           apply Fin.ne_succAbove i j
           omega
         · exact h1'
-  /- the getDual? is some case-/
+  · /- The `(c.getDual? i).isSome` case for `stat_ofFinset_eq_one_of_gradingCompliant`. -/
-  · intro j hj
+    intro j hj
     have hn : ¬ c.getDual? j = none := by exact Option.isSome_iff_ne_none.mp hj
     simp only [uncontracted, Finset.mem_sdiff, Finset.mem_union, Finset.mem_filter, Finset.mem_univ,
       hn, hj, forall_true_left, false_or, true_and, and_false, false_and, Finset.mem_inter,
@@ -1033,28 +1018,24 @@ lemma signInsertSome_mul_filter_contracted_of_lt (φ : 𝓕.States) (φs : List
       · simp_all only [Fin.getElem_fin, ne_eq, not_lt, false_and, false_or, or_false, and_self,
         or_true, imp_self]
         omega
-  · exact hg.2
-  · exact hg.2
-  · exact hg.1
 
 lemma signInsertSome_mul_filter_contracted_of_not_lt (φ : 𝓕.States) (φs : List 𝓕.States)
     (c : WickContraction φs.length) (i : Fin φs.length.succ) (k : c.uncontracted)
-    (hk : ¬ i.succAbove k < i)
+    (hk : ¬ i.succAbove k < i) (hg : GradingCompliant φs c ∧ (𝓕 |>ₛ φ) = 𝓕 |>ₛ φs[k.1]) :
-    (hg : GradingCompliant φs c ∧ 𝓕.statesStatistic φ = 𝓕.statesStatistic φs[k.1]) :
     signInsertSome φ φs c i k *
     𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ⟨φs.get, c.uncontracted.filter (fun x => x < ↑k)⟩)
     = 𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ⟨φs.get, Finset.univ.filter (fun x => i.succAbove x < i)⟩) := by
   have hik : i.succAbove ↑k ≠ i := by exact Fin.succAbove_ne i ↑k
-  rw [signInsertSome, signInsertSomeProd_eq_finset, signInsertSomeCoef_eq_finset]
+  rw [signInsertSome, signInsertSomeProd_eq_finset (hφj := hg.2) (hg := hg.1),
-  rw [if_pos (by omega), ← map_mul, ← map_mul]
+    signInsertSomeCoef_eq_finset (hφj := hg.2), if_pos (by omega), ← map_mul, ← map_mul]
   congr 1
   rw [mul_eq_iff_eq_mul, ofFinset_union, ofFinset_union]
   apply (mul_eq_one_iff _ _).mp
   rw [ofFinset_union]
   simp only [Nat.succ_eq_add_one, not_lt]
-  apply stat_ofFinset_eq_one_of_gradingCompliant
+  apply stat_ofFinset_eq_one_of_gradingCompliant _ _ _ hg.1
-  · exact hg.1
+  · /- The `c.getDual? i = none` case for `stat_ofFinset_eq_one_of_gradingCompliant`. -/
-  · intro j hj
+    intro j hj
     have hijsucc : i.succAbove j ≠ i := by exact Fin.succAbove_ne i j
     simp only [uncontracted, Finset.mem_sdiff, Finset.mem_union, Finset.mem_filter, Finset.mem_univ,
       hj, Option.isSome_none, Bool.false_eq_true, IsEmpty.forall_iff, or_self, and_true, true_and,
@@ -1072,7 +1053,8 @@ lemma signInsertSome_mul_filter_contracted_of_not_lt (φ : 𝓕.States) (φs : L
           omega
     simp only [hij, true_and] at h ⊢
     omega
-  · intro j hj
+  · /- The `(c.getDual? i).isSome` case for `stat_ofFinset_eq_one_of_gradingCompliant`. -/
+    intro j hj
     have hn : ¬ c.getDual? j = none := by exact Option.isSome_iff_ne_none.mp hj
     have hijSuc : i.succAbove j ≠ i := by exact Fin.succAbove_ne i j
     have hkneqj : ↑k ≠ j := by
@@ -1136,8 +1118,5 @@ lemma signInsertSome_mul_filter_contracted_of_not_lt (φ : 𝓕.States) (φs : L
         simp only [hijn, true_and, hijn', and_false, or_false, or_true, imp_false, not_lt,
           forall_const]
         exact fun h => lt_of_le_of_ne h (Fin.succAbove_ne i ((c.getDual? j).get hj))
-  · exact hg.2
-  · exact hg.2
-  · exact hg.1
 
 end WickContraction

HepLean/PerturbationTheory/WickContraction/TimeContract.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Joseph Tooby-Smith
 -/
 import HepLean.PerturbationTheory.WickContraction.Sign
-import HepLean.PerturbationTheory.Algebras.OperatorAlgebra.TimeContraction
+import HepLean.PerturbationTheory.Algebras.ProtoOperatorAlgebra.TimeContraction
 /-!
 
 # Time contractions
@@ -27,14 +27,14 @@ open HepLean.List
 /-- Given a Wick contraction `c` associated with a list `φs`, the
   product of all time-contractions of pairs of contracted elements in `φs`,
   as a member of the center of `𝓞.A`. -/
-noncomputable def timeContract (𝓞 : 𝓕.OperatorAlgebra) {φs : List 𝓕.States}
+noncomputable def timeContract (𝓞 : 𝓕.ProtoOperatorAlgebra) {φs : List 𝓕.States}
     (c : WickContraction φs.length) :
     Subalgebra.center ℂ 𝓞.A :=
   ∏ (a : c.1), ⟨𝓞.timeContract (φs.get (c.fstFieldOfContract a)) (φs.get (c.sndFieldOfContract a)),
     𝓞.timeContract_mem_center _ _⟩
 
 @[simp]
-lemma timeContract_insertList_none (𝓞 : 𝓕.OperatorAlgebra) (φ : 𝓕.States) (φs : List 𝓕.States)
+lemma timeContract_insertList_none (𝓞 : 𝓕.ProtoOperatorAlgebra) (φ : 𝓕.States) (φs : List 𝓕.States)
     (c : WickContraction φs.length) (i : Fin φs.length.succ) :
     (c.insertList φ φs i none).timeContract 𝓞 = c.timeContract 𝓞 := by
   rw [timeContract, insertList_none_prod_contractions]
@@ -42,7 +42,7 @@ lemma timeContract_insertList_none (𝓞 : 𝓕.OperatorAlgebra) (φ : 𝓕.Stat
   ext a
   simp
 
-lemma timeConract_insertList_some (𝓞 : 𝓕.OperatorAlgebra) (φ : 𝓕.States) (φs : List 𝓕.States)
+lemma timeConract_insertList_some (𝓞 : 𝓕.ProtoOperatorAlgebra) (φ : 𝓕.States) (φs : List 𝓕.States)
     (c : WickContraction φs.length) (i : Fin φs.length.succ) (j : c.uncontracted) :
     (c.insertList φ φs i (some j)).timeContract 𝓞 =
     (if i < i.succAbove j then
@@ -62,7 +62,7 @@ lemma timeConract_insertList_some (𝓞 : 𝓕.OperatorAlgebra) (φ : 𝓕.State
 open FieldStatistic
 
 lemma timeConract_insertList_some_eq_mul_contractStateAtIndex_lt
-    (𝓞 : 𝓕.OperatorAlgebra) (φ : 𝓕.States) (φs : List 𝓕.States)
+    (𝓞 : 𝓕.ProtoOperatorAlgebra) (φ : 𝓕.States) (φs : List 𝓕.States)
     (c : WickContraction φs.length) (i : Fin φs.length.succ) (k : c.uncontracted)
     (ht : 𝓕.timeOrderRel φ φs[k.1]) (hik : i < i.succAbove k) :
     (c.insertList φ φs i (some k)).timeContract 𝓞 =
@@ -71,7 +71,7 @@ lemma timeConract_insertList_some_eq_mul_contractStateAtIndex_lt
     ((uncontractedStatesEquiv φs c) (some k)) * c.timeContract 𝓞) := by
   rw [timeConract_insertList_some]
   simp only [Nat.succ_eq_add_one, Fin.getElem_fin, ite_mul, instCommGroup.eq_1,
-    OperatorAlgebra.contractStateAtIndex, uncontractedStatesEquiv, Equiv.optionCongr_apply,
+    ProtoOperatorAlgebra.contractStateAtIndex, uncontractedStatesEquiv, Equiv.optionCongr_apply,
     Equiv.coe_trans, Option.map_some', Function.comp_apply, finCongr_apply, Fin.coe_cast,
     List.getElem_map, uncontractedList_getElem_uncontractedIndexEquiv_symm, List.get_eq_getElem,
     Algebra.smul_mul_assoc]
@@ -97,7 +97,7 @@ lemma timeConract_insertList_some_eq_mul_contractStateAtIndex_lt
     · exact ht
 
 lemma timeConract_insertList_some_eq_mul_contractStateAtIndex_not_lt
-    (𝓞 : 𝓕.OperatorAlgebra) (φ : 𝓕.States) (φs : List 𝓕.States)
+    (𝓞 : 𝓕.ProtoOperatorAlgebra) (φ : 𝓕.States) (φs : List 𝓕.States)
     (c : WickContraction φs.length) (i : Fin φs.length.succ) (k : c.uncontracted)
     (ht : ¬ 𝓕.timeOrderRel φs[k.1] φ) (hik : ¬ i < i.succAbove k) :
     (c.insertList φ φs i (some k)).timeContract 𝓞 =
@@ -106,7 +106,7 @@ lemma timeConract_insertList_some_eq_mul_contractStateAtIndex_not_lt
     ((uncontractedStatesEquiv φs c) (some k)) * c.timeContract 𝓞) := by
   rw [timeConract_insertList_some]
   simp only [Nat.succ_eq_add_one, Fin.getElem_fin, ite_mul, instCommGroup.eq_1,
-    OperatorAlgebra.contractStateAtIndex, uncontractedStatesEquiv, Equiv.optionCongr_apply,
+    ProtoOperatorAlgebra.contractStateAtIndex, uncontractedStatesEquiv, Equiv.optionCongr_apply,
     Equiv.coe_trans, Option.map_some', Function.comp_apply, finCongr_apply, Fin.coe_cast,
     List.getElem_map, uncontractedList_getElem_uncontractedIndexEquiv_symm, List.get_eq_getElem,
     Algebra.smul_mul_assoc]
@@ -148,7 +148,7 @@ lemma timeConract_insertList_some_eq_mul_contractStateAtIndex_not_lt
   simp_all only [Fin.getElem_fin, Nat.succ_eq_add_one, not_lt, false_or]
   exact ht
 
-lemma timeContract_of_not_gradingCompliant (𝓞 : 𝓕.OperatorAlgebra) (φs : List 𝓕.States)
+lemma timeContract_of_not_gradingCompliant (𝓞 : 𝓕.ProtoOperatorAlgebra) (φs : List 𝓕.States)
     (c : WickContraction φs.length) (h : ¬ GradingCompliant φs c) :
     c.timeContract 𝓞 = 0 := by
   rw [timeContract]
@@ -159,7 +159,7 @@ lemma timeContract_of_not_gradingCompliant (𝓞 : 𝓕.OperatorAlgebra) (φs :
   simp only [Finset.univ_eq_attach, Finset.mem_attach]
   apply Subtype.eq
   simp only [List.get_eq_getElem, ZeroMemClass.coe_zero]
-  rw [OperatorAlgebra.timeContract_zero_of_diff_grade]
+  rw [ProtoOperatorAlgebra.timeContract_zero_of_diff_grade]
   simp [ha2]
 
 end WickContraction

HepLean/PerturbationTheory/WickContraction/UncontractedList.lean

@@ -497,19 +497,18 @@ lemma orderedInsert_succAboveEmb_uncontractedList_eq_insertIdx (c : WickContract
     (List.orderedInsert (· ≤ ·) i (List.map i.succAboveEmb c.uncontractedList)) =
     (List.map i.succAboveEmb c.uncontractedList).insertIdx (uncontractedListOrderPos c i) i := by
   rw [orderedInsert_eq_insertIdx_of_fin_list_sorted]
-  swap
+  · congr 1
-  exact uncontractedList_succAboveEmb_sorted c i
+    simp only [Nat.succ_eq_add_one, Fin.val_fin_lt, Fin.coe_succAboveEmb, uncontractedListOrderPos]
-  congr 1
+    rw [List.filter_map]
-  simp only [Nat.succ_eq_add_one, Fin.val_fin_lt, Fin.coe_succAboveEmb, uncontractedListOrderPos]
+    simp only [List.length_map]
-  rw [List.filter_map]
+    congr
-  simp only [List.length_map]
+    funext x
-  congr
+    simp only [Function.comp_apply, Fin.succAbove, decide_eq_decide]
-  funext x
+    split
-  simp only [Function.comp_apply, Fin.succAbove, decide_eq_decide]
+    · simp only [Fin.lt_def, Fin.coe_castSucc]
-  split
+    · rename_i h
-  simp only [Fin.lt_def, Fin.coe_castSucc]
+      simp_all only [Fin.lt_def, Fin.coe_castSucc, not_lt, Fin.val_succ]
-  rename_i h
+      omega
-  simp_all only [Fin.lt_def, Fin.coe_castSucc, not_lt, Fin.val_succ]
+  · exact uncontractedList_succAboveEmb_sorted c i
-  omega
 
 end WickContraction

HepLean/PerturbationTheory/WicksTheorem.lean

@@ -16,10 +16,10 @@ Wick's theorem is related to Isserlis' theorem in mathematics.
 -/
 
 namespace FieldSpecification
-variable {𝓕 : FieldSpecification} {𝓞 : 𝓕.OperatorAlgebra}
+variable {𝓕 : FieldSpecification} {𝓞 : 𝓕.ProtoOperatorAlgebra}
 open CrAnAlgebra
 open StateAlgebra
-open OperatorAlgebra
+open ProtoOperatorAlgebra
 open HepLean.List
 open WickContraction
 open FieldStatistic