Merge pull request #305 from HEPLean/FieldOpAlgebra

feat: Prove static Wick Theorem

HepLean.lean

@@ -129,6 +129,7 @@ import HepLean.PerturbationTheory.Algebras.CrAnAlgebra.SuperCommute
 import HepLean.PerturbationTheory.Algebras.CrAnAlgebra.TimeOrder
 import HepLean.PerturbationTheory.Algebras.FieldOpAlgebra.Basic
 import HepLean.PerturbationTheory.Algebras.FieldOpAlgebra.NormalOrder
+import HepLean.PerturbationTheory.Algebras.FieldOpAlgebra.StaticWickTheorem
 import HepLean.PerturbationTheory.Algebras.FieldOpAlgebra.SuperCommute
 import HepLean.PerturbationTheory.Algebras.FieldOpAlgebra.TimeContraction
 import HepLean.PerturbationTheory.Algebras.FieldOpAlgebra.TimeOrder
@@ -157,6 +158,7 @@ import HepLean.PerturbationTheory.WickContraction.InsertAndContractNat
 import HepLean.PerturbationTheory.WickContraction.Involutions
 import HepLean.PerturbationTheory.WickContraction.IsFull
 import HepLean.PerturbationTheory.WickContraction.Sign
+import HepLean.PerturbationTheory.WickContraction.StaticContract
 import HepLean.PerturbationTheory.WickContraction.TimeContract
 import HepLean.PerturbationTheory.WickContraction.Uncontracted
 import HepLean.PerturbationTheory.WickContraction.UncontractedList

HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/Basic.lean

@@ -445,6 +445,13 @@ lemma ofFieldOpList_append (φs ψs : List 𝓕.States) :
   rw [ofStateList_append]
   simp
 
+lemma ofFieldOpList_cons (φ : 𝓕.States) (φs : List 𝓕.States) :
+    ofFieldOpList (φ :: φs) = ofFieldOp φ * ofFieldOpList φs := by
+  simp only [ofFieldOpList]
+  rw [ofStateList_cons]
+  simp only [map_mul]
+  rfl
+
 lemma ofFieldOpList_singleton (φ : 𝓕.States) :
     ofFieldOpList [φ] = ofFieldOp φ := by
   simp only [ofFieldOpList, ofFieldOp, ofStateList_singleton]

HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/NormalOrder.lean

@@ -249,6 +249,13 @@ lemma normalOrder_ofCrAnFieldOpList (φs : List 𝓕.CrAnStates) :
   rw [ofCrAnFieldOpList, normalOrder_eq_ι_normalOrderF, normalOrderF_ofCrAnList]
   rfl
 
+@[simp]
+lemma normalOrder_one_eq_one : normalOrder (𝓕 := 𝓕) 1 = 1 := by
+  have h1 : 1 = ofCrAnFieldOpList (𝓕 := 𝓕) [] := by simp [ofCrAnFieldOpList]
+  rw [h1]
+  rw [normalOrder_ofCrAnFieldOpList]
+  simp
+
 lemma ofCrAnFieldOpList_eq_normalOrder (φs : List 𝓕.CrAnStates) :
     ofCrAnFieldOpList (normalOrderList φs) = normalOrderSign φs • 𝓝(ofCrAnFieldOpList φs) := by
   rw [normalOrder_ofCrAnFieldOpList, smul_smul, normalOrderSign, Wick.koszulSign_mul_self,

HepLean/PerturbationTheory/Algebras/FieldOpAlgebra/StaticWickTheorem.lean

@@ -0,0 +1,104 @@
+/-
+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.WickContraction.StaticContract
+import HepLean.PerturbationTheory.WicksTheorem
+import HepLean.Meta.Remark.Basic
+/-!
+
+# Static Wick's theorem
+
+-/
+
+namespace FieldSpecification
+variable {𝓕 : FieldSpecification}
+open CrAnAlgebra
+
+open HepLean.List
+open WickContraction
+open FieldStatistic
+namespace FieldOpAlgebra
+
+lemma static_wick_theorem_nil : ofFieldOpList [] = ∑ (φsΛ : WickContraction [].length),
+    φsΛ.sign (𝓕 := 𝓕) • φsΛ.staticContract * 𝓝(ofFieldOpList [φsΛ]ᵘᶜ) := by
+  simp only [ofFieldOpList, ofStateList_nil, map_one, List.length_nil]
+  rw [sum_WickContraction_nil, uncontractedListGet, nil_zero_uncontractedList]
+  simp [sign, empty, staticContract]
+
+theorem static_wick_theorem : (φs : List 𝓕.States) →
+    ofFieldOpList φs = ∑ (φsΛ : WickContraction φs.length),
+    φsΛ.sign • φsΛ.staticContract * 𝓝(ofFieldOpList [φsΛ]ᵘᶜ)
+  | [] => static_wick_theorem_nil
+  | φ :: φs => by
+    rw [ofFieldOpList_cons]
+    rw [static_wick_theorem φs]
+    rw [show  (φ :: φs) = φs.insertIdx (⟨0, Nat.zero_lt_succ φs.length⟩ : Fin φs.length.succ) φ
+      from rfl]
+    conv_rhs => rw [insertLift_sum ]
+    rw [Finset.mul_sum]
+    apply Finset.sum_congr rfl
+    intro c _
+    trans  (sign φs c • ↑c.staticContract * (ofFieldOp φ * normalOrder (ofFieldOpList [c]ᵘᶜ)))
+    · have ht := Subalgebra.mem_center_iff.mp (Subalgebra.smul_mem (Subalgebra.center ℂ _)
+        (c.staticContract).2 c.sign )
+      conv_rhs => rw [← mul_assoc, ← ht]
+      simp [mul_assoc]
+    rw [ofFieldOp_mul_normalOrder_ofFieldOpList_eq_sum]
+    rw [Finset.mul_sum]
+    rw [uncontractedStatesEquiv_list_sum]
+    refine Finset.sum_congr rfl (fun n _ => ?_)
+    match n with
+    | none =>
+      simp only [contractStateAtIndex, uncontractedStatesEquiv, Equiv.optionCongr_apply,
+        Equiv.coe_trans, Option.map_none', one_mul, Algebra.smul_mul_assoc, Nat.succ_eq_add_one,
+        Fin.zero_eta, Fin.val_zero, List.insertIdx_zero, staticContract_insertAndContract_none,
+        insertAndContract_uncontractedList_none_zero]
+      erw [sign_insert_none_zero]
+      rfl
+    | some n =>
+      simp only [Algebra.smul_mul_assoc, Nat.succ_eq_add_one, Fin.zero_eta, Fin.val_zero,
+        List.insertIdx_zero]
+      rw [normalOrder_uncontracted_some]
+      simp [← mul_assoc]
+      rw [← smul_mul_assoc]
+      conv_rhs => rw [← smul_mul_assoc]
+      congr 1
+      rw [staticConract_insertAndContract_some_eq_mul_contractStateAtIndex_lt]
+      swap
+      · simp
+      rw [smul_smul]
+      by_cases hn :  GradingCompliant φs c ∧ (𝓕|>ₛφ) = (𝓕|>ₛ φs[n.1])
+      · congr 1
+        swap
+        · have h1 := c.staticContract.2
+          rw [@Subalgebra.mem_center_iff] at h1
+          rw [h1]
+        erw [sign_insert_some]
+        rw [mul_assoc, mul_comm c.sign, ← mul_assoc]
+        rw [signInsertSome_mul_filter_contracted_of_not_lt]
+        simp only [instCommGroup.eq_1, Fin.zero_succAbove, Fin.not_lt_zero, Finset.filter_False,
+          ofFinset_empty, map_one, one_mul]
+        simp only [Fin.zero_succAbove, Fin.not_lt_zero, not_false_eq_true]
+        exact hn
+      · simp at hn
+        by_cases h0 : ¬ GradingCompliant φs c
+        · rw [staticContract_of_not_gradingCompliant]
+          simp only [ZeroMemClass.coe_zero, zero_mul, smul_zero, instCommGroup.eq_1, mul_zero]
+          exact h0
+        · simp_all
+          have h1 :  contractStateAtIndex φ [c]ᵘᶜ
+              ((uncontractedStatesEquiv φs c) (some n)) = 0 := by
+            simp only [contractStateAtIndex, uncontractedStatesEquiv, Equiv.optionCongr_apply,
+              Equiv.coe_trans, Option.map_some', Function.comp_apply, finCongr_apply,
+              instCommGroup.eq_1, Fin.coe_cast, Fin.getElem_fin, smul_eq_zero]
+            right
+            simp [uncontractedListGet]
+            rw [superCommute_anPart_ofState_diff_grade_zero]
+            exact hn
+          rw [h1]
+          simp
+
+end FieldOpAlgebra
+end FieldSpecification

HepLean/PerturbationTheory/WickContraction/InsertAndContract.lean

@@ -304,4 +304,11 @@ lemma insertAndContract_uncontractedList_none_map (φ : 𝓕.States) {φs : List
   conv_rhs => rw [get_eq_insertIdx_succAbove φ φs i]
   rfl
 
+@[simp]
+lemma insertAndContract_uncontractedList_none_zero (φ : 𝓕.States) {φs : List 𝓕.States}
+    (φsΛ : WickContraction φs.length) :
+    [φsΛ ↩Λ φ 0 none]ᵘᶜ = φ :: [φsΛ]ᵘᶜ := by
+  rw [insertAndContract_uncontractedList_none_map]
+  simp [uncontractedListOrderPos]
+
 end WickContraction

HepLean/PerturbationTheory/WickContraction/Sign.lean

@@ -409,6 +409,11 @@ lemma signInsertNone_eq_prod_prod (φ : 𝓕.States) (φs : List 𝓕.States)
   erw [hG a]
   rfl
 
+lemma sign_insert_none_zero (φ : 𝓕.States) (φs : List 𝓕.States) (φsΛ : WickContraction φs.length) :
+    (φsΛ ↩Λ φ 0 none).sign = φsΛ.sign := by
+  rw [sign_insert_none]
+  simp [signInsertNone]
+
 lemma signInsertNone_eq_prod_getDual?_Some (φ : 𝓕.States) (φs : List 𝓕.States)
     (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (hG : GradingCompliant φs φsΛ) :
     φsΛ.signInsertNone φ φs i = ∏ (x : Fin φs.length),

HepLean/PerturbationTheory/WickContraction/StaticContract.lean

@@ -0,0 +1,114 @@
+/-
+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.WickContraction.Sign
+import HepLean.PerturbationTheory.Algebras.FieldOpAlgebra.TimeContraction
+/-!
+
+# Time contractions
+
+-/
+
+open FieldSpecification
+variable {𝓕 : FieldSpecification}
+
+namespace WickContraction
+variable {n : ℕ} (c : WickContraction n)
+open HepLean.List
+open FieldOpAlgebra
+/-- Given a Wick contraction `φsΛ` 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 staticContract {φs : List 𝓕.States}
+    (φsΛ : WickContraction φs.length) :
+    Subalgebra.center ℂ 𝓕.FieldOpAlgebra :=
+  ∏ (a : φsΛ.1), ⟨[anPart (φs.get (φsΛ.fstFieldOfContract a)),
+    ofFieldOp (φs.get (φsΛ.sndFieldOfContract a))]ₛ,
+      superCommute_anPart_ofFieldOp_mem_center _ _⟩
+
+@[simp]
+lemma staticContract_insertAndContract_none (φ : 𝓕.States) (φs : List 𝓕.States)
+    (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) :
+    (φsΛ ↩Λ φ i none).staticContract = φsΛ.staticContract := by
+  rw [staticContract, insertAndContract_none_prod_contractions]
+  congr
+  ext a
+  simp
+
+/-- For `φsΛ` a Wick contraction for `φs = φ₀…φₙ`, the time contraction
+  `(φsΛ ↩Λ φ i (some j)).timeContract 𝓞` is equal to the multiple of
+- the time contraction of `φ` with `φⱼ` if `i < i.succAbove j` else
+    `φⱼ` with `φ`.
+- `φsΛ.timeContract 𝓞`.
+This follows from the fact that `(φsΛ ↩Λ φ i (some j))` has one more contracted pair than `φsΛ`,
+corresponding to `φ` contracted with `φⱼ`. The order depends on whether we insert `φ` before
+or after `φⱼ`. -/
+lemma staticContract_insertAndContract_some
+    (φ : 𝓕.States) (φs : List 𝓕.States)
+    (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (j : φsΛ.uncontracted) :
+    (φsΛ ↩Λ φ i (some j)).staticContract =
+    (if i < i.succAbove j then
+      ⟨[anPart φ, ofFieldOp φs[j.1]]ₛ, superCommute_anPart_ofFieldOp_mem_center _ _⟩
+    else ⟨[anPart  φs[j.1], ofFieldOp φ]ₛ, superCommute_anPart_ofFieldOp_mem_center _ _⟩) *
+    φsΛ.staticContract := by
+  rw [staticContract, insertAndContract_some_prod_contractions]
+  congr 1
+  · simp only [Nat.succ_eq_add_one, insertAndContract_fstFieldOfContract_some_incl, finCongr_apply,
+    List.get_eq_getElem, insertAndContract_sndFieldOfContract_some_incl, Fin.getElem_fin]
+    split
+    · simp
+    · simp
+  · congr
+    ext a
+    simp
+
+open FieldStatistic
+
+lemma staticConract_insertAndContract_some_eq_mul_contractStateAtIndex_lt
+    (φ : 𝓕.States) (φs : List 𝓕.States)
+    (φsΛ : WickContraction φs.length) (i : Fin φs.length.succ) (k : φsΛ.uncontracted)
+    (hik : i < i.succAbove k) :
+    (φsΛ ↩Λ φ i (some k)).staticContract =
+    𝓢(𝓕 |>ₛ φ, 𝓕 |>ₛ ⟨φs.get, (φsΛ.uncontracted.filter (fun x => x < k))⟩)
+    • (contractStateAtIndex φ [φsΛ]ᵘᶜ ((uncontractedStatesEquiv φs φsΛ) (some k)) *
+      φsΛ.staticContract) := by
+  rw [staticContract_insertAndContract_some]
+  simp only [Nat.succ_eq_add_one, Fin.getElem_fin, ite_mul, instCommGroup.eq_1,
+    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, uncontractedListGet]
+  · simp only [hik, ↓reduceIte, MulMemClass.coe_mul]
+    trans (1 : ℂ) • ((superCommute (anPart φ)) (ofFieldOp φs[k.1]) * ↑φsΛ.staticContract)
+    · simp
+    simp only [smul_smul]
+    congr 1
+    have h1 : ofList 𝓕.statesStatistic (List.take (↑(φsΛ.uncontractedIndexEquiv.symm k))
+        (List.map φs.get φsΛ.uncontractedList))
+        = (𝓕 |>ₛ ⟨φs.get, (Finset.filter (fun x => x < k) φsΛ.uncontracted)⟩) := by
+      simp only [ofFinset]
+      congr
+      rw [← List.map_take]
+      congr
+      rw [take_uncontractedIndexEquiv_symm]
+      rw [filter_uncontractedList]
+    rw [h1]
+    simp only [exchangeSign_mul_self]
+
+lemma staticContract_of_not_gradingCompliant (φs : List 𝓕.States)
+    (φsΛ : WickContraction φs.length) (h : ¬ GradingCompliant φs φsΛ) :
+    φsΛ.staticContract = 0 := by
+  rw [staticContract]
+  simp only [GradingCompliant, Fin.getElem_fin, Subtype.forall, not_forall] at h
+  obtain ⟨a, ha⟩ := h
+  obtain ⟨ha, ha2⟩ := ha
+  apply Finset.prod_eq_zero (i := ⟨a, ha⟩)
+  simp only [Finset.univ_eq_attach, Finset.mem_attach]
+  apply Subtype.eq
+  simp only [List.get_eq_getElem, ZeroMemClass.coe_zero]
+  rw [superCommute_anPart_ofState_diff_grade_zero]
+  simp [ha2]
+
+end WickContraction