Physlib.QFT.PerturbationTheory.WickContraction.Singleton

Imports

/-
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
-/
module

public import Physlib.QFT.PerturbationTheory.WickContraction.SubContraction
public import Physlib.QFT.PerturbationTheory.WickContraction.StaticContract
public import Physlib.QFT.PerturbationTheory.WickContraction.TimeContract
public import Physlib.QFT.PerturbationTheory.WickContraction.Sign.Basic

Singleton of contractions

@[expose] public section

The Wick contraction formed from a single ordered pair.


def singleton {i j : Fin n} (hij : i < j) : WickContraction n :=
  ⟨{{i, j}}, by𝓕:FieldSpecificationn:ℕc:WickContraction ni:Fin nj:Fin nhij:i < j⊢ ∀ a ∈ {{i, j}}, a.card = 2
    intro i hi𝓕:FieldSpecificationn:ℕc:WickContraction ni✝:Fin nj:Fin nhij:i < ji:Finset (Fin n)hi:i ∈ {{i✝, j}}⊢ i.card = 2
    simp only [Finset.mem_singleton] at hi𝓕:FieldSpecificationn:ℕc:WickContraction ni✝:Fin nj:Fin nhij:i < ji:Finset (Fin n)hi:i = {i✝, j}⊢ i.card = 2
    subst hi𝓕:FieldSpecificationn:ℕc:WickContraction ni:Fin nj:Fin nhij:i < j⊢ {i, j}.card = 2
    rw [@Finset.card_eq_two𝓕:FieldSpecificationn:ℕc:WickContraction ni:Fin nj:Fin nhij:i < j⊢ ∃ x y, x ≠ y ∧ {i, j} = {x, y}𝓕:FieldSpecificationn:ℕc:WickContraction ni:Fin nj:Fin nhij:i < j⊢ ∃ x y, x ≠ y ∧ {i, j} = {x, y}]𝓕:FieldSpecificationn:ℕc:WickContraction ni:Fin nj:Fin nhij:i < j⊢ ∃ x y, x ≠ y ∧ {i, j} = {x, y}
    use i, jh𝓕:FieldSpecificationn:ℕc:WickContraction ni:Fin nj:Fin nhij:i < j⊢ i ≠ j ∧ {i, j} = {i, j}
    simp only [ne_eq, and_true]h𝓕:FieldSpecificationn:ℕc:WickContraction ni:Fin nj:Fin nhij:i < j⊢ ¬i = j
    omegaAll goals completed! 🐙, by𝓕:FieldSpecificationn:ℕc:WickContraction ni:Fin nj:Fin nhij:i < j⊢ ∀ a ∈ {{i, j}}, ∀ b ∈ {{i, j}}, a = b ∨ Disjoint a b
    intro i hi j hj𝓕:FieldSpecificationn:ℕc:WickContraction ni✝:Fin nj✝:Fin nhij:i < ji:Finset (Fin n)hi:i ∈ {{i✝, j✝}}j:Finset (Fin n)hj:j ∈ {{i✝, j✝}}⊢ i = j ∨ Disjoint i j
    simp_allAll goals completed! 🐙⟩

              lemma mem_singleton {i j : Fin n} (hij : i < j) :
    {i, j} ∈ (singleton hij).1 := byn:ℕi:Fin nj:Fin nhij:i < j⊢ {i, j} ∈ ↑(singleton hij)
  simp [singleton]All goals completed! 🐙lemma mem_singleton_iff {i j : Fin n} (hij : i < j) {a : Finset (Fin n)} :
    a ∈ (singleton hij).1 ↔ a = {i, j} := byn:ℕi:Fin nj:Fin nhij:i < ja:Finset (Fin n)⊢ a ∈ ↑(singleton hij) ↔ a = {i, j}
  simp [singleton]All goals completed! 🐙

lemma of_singleton_eq {i j : Fin n} (hij : i < j) (a : (singleton hij).1) :
    a = ⟨{i, j}, mem_singleton hij⟩ := byn:ℕi:Fin nj:Fin nhij:i < ja:↥↑(singleton hij)⊢ a = ⟨{i, j}, ⋯⟩
  have ha2 := a.2n:ℕi:Fin nj:Fin nhij:i < ja:↥↑(singleton hij)ha2:↑a ∈ ↑(singleton hij)⊢ a = ⟨{i, j}, ⋯⟩
  rw [@mem_singleton_iffn:ℕi:Fin nj:Fin nhij:i < ja:↥↑(singleton hij)ha2:↑a = {i, j}⊢ a = ⟨{i, j}, ⋯⟩n:ℕi:Fin nj:Fin nhij:i < ja:↥↑(singleton hij)ha2:↑a = {i, j}⊢ a = ⟨{i, j}, ⋯⟩] at ha2n:ℕi:Fin nj:Fin nhij:i < ja:↥↑(singleton hij)ha2:↑a = {i, j}⊢ a = ⟨{i, j}, ⋯⟩
  exact Subtype.coe_eq_of_eq_mk ha2All goals completed! 🐙lemma singleton_prod {φs : List 𝓕.FieldOp} {i j : Fin φs.length} (hij : i < j)
    (f : (singleton hij).1 → M) [CommMonoid M] :
    ∏ a, f a = f ⟨{i,j}, mem_singleton hij⟩:= by𝓕:FieldSpecificationM:Type u_1φs:List 𝓕.FieldOpi:Fin φs.lengthj:Fin φs.lengthhij:i < jf:↥↑(singleton hij) → Minst✝:CommMonoid M⊢ ∏ a, f a = f ⟨{i, j}, ⋯⟩
  simp [singleton, of_singleton_eq]All goals completed! 🐙@[simp]
lemma singleton_fstFieldOfContract {i j : Fin n} (hij : i < j) :
    (singleton hij).fstFieldOfContract ⟨{i, j}, mem_singleton hij⟩ = i := byn:ℕi:Fin nj:Fin nhij:i < j⊢ (singleton hij).fstFieldOfContract ⟨{i, j}, ⋯⟩ = i
  refine eq_fstFieldOfContract_of_mem (singleton hij) ⟨{i, j}, mem_singleton hij⟩ i j ?_ ?_ ?_refine_1n:ℕi:Fin nj:Fin nhij:i < j⊢ i ∈ ↑⟨{i, j}, ⋯⟩refine_2n:ℕi:Fin nj:Fin nhij:i < j⊢ j ∈ ↑⟨{i, j}, ⋯⟩refine_3n:ℕi:Fin nj:Fin nhij:i < j⊢ i < j
  ·refine_1n:ℕi:Fin nj:Fin nhij:i < j⊢ i ∈ ↑⟨{i, j}, ⋯⟩ simpAll goals completed! 🐙
  ·refine_2n:ℕi:Fin nj:Fin nhij:i < j⊢ j ∈ ↑⟨{i, j}, ⋯⟩ simpAll goals completed! 🐙
  ·refine_3n:ℕi:Fin nj:Fin nhij:i < j⊢ i < j exact hijAll goals completed! 🐙@[simp]
lemma singleton_sndFieldOfContract {i j : Fin n} (hij : i < j) :
    (singleton hij).sndFieldOfContract ⟨{i, j}, mem_singleton hij⟩ = j := byn:ℕi:Fin nj:Fin nhij:i < j⊢ (singleton hij).sndFieldOfContract ⟨{i, j}, ⋯⟩ = j
  refine eq_sndFieldOfContract_of_mem (singleton hij) ⟨{i, j}, mem_singleton hij⟩ i j ?_ ?_ ?_refine_1n:ℕi:Fin nj:Fin nhij:i < j⊢ i ∈ ↑⟨{i, j}, ⋯⟩refine_2n:ℕi:Fin nj:Fin nhij:i < j⊢ j ∈ ↑⟨{i, j}, ⋯⟩refine_3n:ℕi:Fin nj:Fin nhij:i < j⊢ i < j
  ·refine_1n:ℕi:Fin nj:Fin nhij:i < j⊢ i ∈ ↑⟨{i, j}, ⋯⟩ simpAll goals completed! 🐙
  ·refine_2n:ℕi:Fin nj:Fin nhij:i < j⊢ j ∈ ↑⟨{i, j}, ⋯⟩ simpAll goals completed! 🐙
  ·refine_3n:ℕi:Fin nj:Fin nhij:i < j⊢ i < j exact hijAll goals completed! 🐙

lemma singleton_sign_expand {φs : List 𝓕.FieldOp} {i j : Fin φs.length} (hij : i < j) :
    (singleton hij).sign = 𝓢(𝓕 |>ₛ φs[j], 𝓕 |>ₛ ⟨φs.get, (singleton hij).signFinset i j⟩) := by𝓕:FieldSpecificationφs:List 𝓕.FieldOpi:Fin φs.lengthj:Fin φs.lengthhij:i < j⊢ sign φs (singleton hij) =
  (exchangeSign (𝓕|>ₛφs[j])) (ofFinset 𝓕.fieldOpStatistic φs.get ((singleton hij).signFinset i j))
  rw [sign,𝓕:FieldSpecificationφs:List 𝓕.FieldOpi:Fin φs.lengthj:Fin φs.lengthhij:i < j⊢ ∏ a,
    (exchangeSign (𝓕|>ₛφs[(singleton hij).sndFieldOfContract a]))
      (ofFinset 𝓕.fieldOpStatistic φs.get
        ((singleton hij).signFinset ((singleton hij).fstFieldOfContract a) ((singleton hij).sndFieldOfContract a))) =
  (exchangeSign (𝓕|>ₛφs[j])) (ofFinset 𝓕.fieldOpStatistic φs.get ((singleton hij).signFinset i j))𝓕:FieldSpecificationφs:List 𝓕.FieldOpi:Fin φs.lengthj:Fin φs.lengthhij:i < j⊢ (exchangeSign (𝓕|>ₛφs[(singleton hij).sndFieldOfContract ⟨{i, j}, ⋯⟩]))
    (ofFinset 𝓕.fieldOpStatistic φs.get
      ((singleton hij).signFinset ((singleton hij).fstFieldOfContract ⟨{i, j}, ⋯⟩)
        ((singleton hij).sndFieldOfContract ⟨{i, j}, ⋯⟩))) =
  (exchangeSign (𝓕|>ₛφs[j])) (ofFinset 𝓕.fieldOpStatistic φs.get ((singleton hij).signFinset i j)) singleton_prod𝓕:FieldSpecificationφs:List 𝓕.FieldOpi:Fin φs.lengthj:Fin φs.lengthhij:i < j⊢ (exchangeSign (𝓕|>ₛφs[(singleton hij).sndFieldOfContract ⟨{i, j}, ⋯⟩]))
    (ofFinset 𝓕.fieldOpStatistic φs.get
      ((singleton hij).signFinset ((singleton hij).fstFieldOfContract ⟨{i, j}, ⋯⟩)
        ((singleton hij).sndFieldOfContract ⟨{i, j}, ⋯⟩))) =
  (exchangeSign (𝓕|>ₛφs[j])) (ofFinset 𝓕.fieldOpStatistic φs.get ((singleton hij).signFinset i j))𝓕:FieldSpecificationφs:List 𝓕.FieldOpi:Fin φs.lengthj:Fin φs.lengthhij:i < j⊢ (exchangeSign (𝓕|>ₛφs[(singleton hij).sndFieldOfContract ⟨{i, j}, ⋯⟩]))
    (ofFinset 𝓕.fieldOpStatistic φs.get
      ((singleton hij).signFinset ((singleton hij).fstFieldOfContract ⟨{i, j}, ⋯⟩)
        ((singleton hij).sndFieldOfContract ⟨{i, j}, ⋯⟩))) =
  (exchangeSign (𝓕|>ₛφs[j])) (ofFinset 𝓕.fieldOpStatistic φs.get ((singleton hij).signFinset i j))]𝓕:FieldSpecificationφs:List 𝓕.FieldOpi:Fin φs.lengthj:Fin φs.lengthhij:i < j⊢ (exchangeSign (𝓕|>ₛφs[(singleton hij).sndFieldOfContract ⟨{i, j}, ⋯⟩]))
    (ofFinset 𝓕.fieldOpStatistic φs.get
      ((singleton hij).signFinset ((singleton hij).fstFieldOfContract ⟨{i, j}, ⋯⟩)
        ((singleton hij).sndFieldOfContract ⟨{i, j}, ⋯⟩))) =
  (exchangeSign (𝓕|>ₛφs[j])) (ofFinset 𝓕.fieldOpStatistic φs.get ((singleton hij).signFinset i j))
  simpAll goals completed! 🐙

lemma singleton_getDual?_eq_none_iff_neq {i j : Fin n} (hij : i < j) (a : Fin n) :
    (singleton hij).getDual? a = none ↔ (i ≠ a ∧ j ≠ a) := byn:ℕi:Fin nj:Fin nhij:i < ja:Fin n⊢ (singleton hij).getDual? a = none ↔ i ≠ a ∧ j ≠ a
  rw [getDual?_eq_none_iff_mem_uncontractedn:ℕi:Fin nj:Fin nhij:i < ja:Fin n⊢ a ∈ (singleton hij).uncontracted ↔ i ≠ a ∧ j ≠ an:ℕi:Fin nj:Fin nhij:i < ja:Fin n⊢ a ∈ (singleton hij).uncontracted ↔ i ≠ a ∧ j ≠ a]n:ℕi:Fin nj:Fin nhij:i < ja:Fin n⊢ a ∈ (singleton hij).uncontracted ↔ i ≠ a ∧ j ≠ a
  rw [mem_uncontracted_iff_not_contractedn:ℕi:Fin nj:Fin nhij:i < ja:Fin n⊢ (∀ p ∈ ↑(singleton hij), a ∉ p) ↔ i ≠ a ∧ j ≠ an:ℕi:Fin nj:Fin nhij:i < ja:Fin n⊢ (∀ p ∈ ↑(singleton hij), a ∉ p) ↔ i ≠ a ∧ j ≠ a]n:ℕi:Fin nj:Fin nhij:i < ja:Fin n⊢ (∀ p ∈ ↑(singleton hij), a ∉ p) ↔ i ≠ a ∧ j ≠ a
  simp only [singleton, Finset.mem_singleton, forall_eq, Finset.mem_insert, not_or, ne_eq]n:ℕi:Fin nj:Fin nhij:i < ja:Fin n⊢ ¬a = i ∧ ¬a = j ↔ ¬i = a ∧ ¬j = a
  omegaAll goals completed! 🐙

lemma singleton_uncontractedEmd_ne_left {φs : List 𝓕.FieldOp} {i j : Fin φs.length} (hij : i < j)
    (a : Fin [singleton hij]ᵘᶜ.length) :
    (singleton hij).uncontractedListEmd a ≠ i := by𝓕:FieldSpecificationφs:List 𝓕.FieldOpi:Fin φs.lengthj:Fin φs.lengthhij:i < ja:Fin [singleton hij]ᵘᶜ.length⊢ uncontractedListEmd a ≠ i
  by_contra hn𝓕:FieldSpecificationφs:List 𝓕.FieldOpi:Fin φs.lengthj:Fin φs.lengthhij:i < ja:Fin [singleton hij]ᵘᶜ.lengthhn:uncontractedListEmd a = i⊢ False
  have h1 : (singleton hij).uncontractedListEmd a ∈ (singleton hij).uncontracted := by𝓕:FieldSpecificationφs:List 𝓕.FieldOpi:Fin φs.lengthj:Fin φs.lengthhij:i < ja:Fin [singleton hij]ᵘᶜ.length⊢ uncontractedListEmd a ≠ i𝓕:FieldSpecificationφs:List 𝓕.FieldOpi:Fin φs.lengthj:Fin φs.lengthhij:i < ja:Fin [singleton hij]ᵘᶜ.lengthhn:uncontractedListEmd a = ih1:uncontractedListEmd a ∈ (singleton hij).uncontracted⊢ False
    simp [uncontractedListEmd]𝓕:FieldSpecificationφs:List 𝓕.FieldOpi:Fin φs.lengthj:Fin φs.lengthhij:i < ja:Fin [singleton hij]ᵘᶜ.lengthhn:uncontractedListEmd a = ih1:uncontractedListEmd a ∈ (singleton hij).uncontracted⊢ False𝓕:FieldSpecificationφs:List 𝓕.FieldOpi:Fin φs.lengthj:Fin φs.lengthhij:i < ja:Fin [singleton hij]ᵘᶜ.lengthhn:uncontractedListEmd a = ih1:uncontractedListEmd a ∈ (singleton hij).uncontracted⊢ False
  have h2 : i ∉ (singleton hij).uncontracted := by𝓕:FieldSpecificationφs:List 𝓕.FieldOpi:Fin φs.lengthj:Fin φs.lengthhij:i < ja:Fin [singleton hij]ᵘᶜ.length⊢ uncontractedListEmd a ≠ i𝓕:FieldSpecificationφs:List 𝓕.FieldOpi:Fin φs.lengthj:Fin φs.lengthhij:i < ja:Fin [singleton hij]ᵘᶜ.lengthhn:uncontractedListEmd a = ih1:uncontractedListEmd a ∈ (singleton hij).uncontractedh2:i ∉ (singleton hij).uncontracted⊢ False
    rw [mem_uncontracted_iff_not_contracted𝓕:FieldSpecificationφs:List 𝓕.FieldOpi:Fin φs.lengthj:Fin φs.lengthhij:i < ja:Fin [singleton hij]ᵘᶜ.lengthhn:uncontractedListEmd a = ih1:uncontractedListEmd a ∈ (singleton hij).uncontracted⊢ ¬∀ p ∈ ↑(singleton hij), i ∉ p𝓕:FieldSpecificationφs:List 𝓕.FieldOpi:Fin φs.lengthj:Fin φs.lengthhij:i < ja:Fin [singleton hij]ᵘᶜ.lengthhn:uncontractedListEmd a = ih1:uncontractedListEmd a ∈ (singleton hij).uncontracted⊢ ¬∀ p ∈ ↑(singleton hij), i ∉ p𝓕:FieldSpecificationφs:List 𝓕.FieldOpi:Fin φs.lengthj:Fin φs.lengthhij:i < ja:Fin [singleton hij]ᵘᶜ.lengthhn:uncontractedListEmd a = ih1:uncontractedListEmd a ∈ (singleton hij).uncontractedh2:i ∉ (singleton hij).uncontracted⊢ False]𝓕:FieldSpecificationφs:List 𝓕.FieldOpi:Fin φs.lengthj:Fin φs.lengthhij:i < ja:Fin [singleton hij]ᵘᶜ.lengthhn:uncontractedListEmd a = ih1:uncontractedListEmd a ∈ (singleton hij).uncontracted⊢ ¬∀ p ∈ ↑(singleton hij), i ∉ p𝓕:FieldSpecificationφs:List 𝓕.FieldOpi:Fin φs.lengthj:Fin φs.lengthhij:i < ja:Fin [singleton hij]ᵘᶜ.lengthhn:uncontractedListEmd a = ih1:uncontractedListEmd a ∈ (singleton hij).uncontractedh2:i ∉ (singleton hij).uncontracted⊢ False
    simp [singleton]𝓕:FieldSpecificationφs:List 𝓕.FieldOpi:Fin φs.lengthj:Fin φs.lengthhij:i < ja:Fin [singleton hij]ᵘᶜ.lengthhn:uncontractedListEmd a = ih1:uncontractedListEmd a ∈ (singleton hij).uncontractedh2:i ∉ (singleton hij).uncontracted⊢ False𝓕:FieldSpecificationφs:List 𝓕.FieldOpi:Fin φs.lengthj:Fin φs.lengthhij:i < ja:Fin [singleton hij]ᵘᶜ.lengthhn:uncontractedListEmd a = ih1:uncontractedListEmd a ∈ (singleton hij).uncontractedh2:i ∉ (singleton hij).uncontracted⊢ False
  simp_allAll goals completed! 🐙

lemma singleton_uncontractedEmd_ne_right {φs : List 𝓕.FieldOp} {i j : Fin φs.length} (hij : i < j)
    (a : Fin [singleton hij]ᵘᶜ.length) :
    (singleton hij).uncontractedListEmd a ≠ j := by𝓕:FieldSpecificationφs:List 𝓕.FieldOpi:Fin φs.lengthj:Fin φs.lengthhij:i < ja:Fin [singleton hij]ᵘᶜ.length⊢ uncontractedListEmd a ≠ j
  by_contra hn𝓕:FieldSpecificationφs:List 𝓕.FieldOpi:Fin φs.lengthj:Fin φs.lengthhij:i < ja:Fin [singleton hij]ᵘᶜ.lengthhn:uncontractedListEmd a = j⊢ False
  have h1 : (singleton hij).uncontractedListEmd a ∈ (singleton hij).uncontracted := by𝓕:FieldSpecificationφs:List 𝓕.FieldOpi:Fin φs.lengthj:Fin φs.lengthhij:i < ja:Fin [singleton hij]ᵘᶜ.length⊢ uncontractedListEmd a ≠ j𝓕:FieldSpecificationφs:List 𝓕.FieldOpi:Fin φs.lengthj:Fin φs.lengthhij:i < ja:Fin [singleton hij]ᵘᶜ.lengthhn:uncontractedListEmd a = jh1:uncontractedListEmd a ∈ (singleton hij).uncontracted⊢ False
    simp [uncontractedListEmd]𝓕:FieldSpecificationφs:List 𝓕.FieldOpi:Fin φs.lengthj:Fin φs.lengthhij:i < ja:Fin [singleton hij]ᵘᶜ.lengthhn:uncontractedListEmd a = jh1:uncontractedListEmd a ∈ (singleton hij).uncontracted⊢ False𝓕:FieldSpecificationφs:List 𝓕.FieldOpi:Fin φs.lengthj:Fin φs.lengthhij:i < ja:Fin [singleton hij]ᵘᶜ.lengthhn:uncontractedListEmd a = jh1:uncontractedListEmd a ∈ (singleton hij).uncontracted⊢ False
  have h2 : j ∉ (singleton hij).uncontracted := by𝓕:FieldSpecificationφs:List 𝓕.FieldOpi:Fin φs.lengthj:Fin φs.lengthhij:i < ja:Fin [singleton hij]ᵘᶜ.length⊢ uncontractedListEmd a ≠ j𝓕:FieldSpecificationφs:List 𝓕.FieldOpi:Fin φs.lengthj:Fin φs.lengthhij:i < ja:Fin [singleton hij]ᵘᶜ.lengthhn:uncontractedListEmd a = jh1:uncontractedListEmd a ∈ (singleton hij).uncontractedh2:j ∉ (singleton hij).uncontracted⊢ False
    rw [mem_uncontracted_iff_not_contracted𝓕:FieldSpecificationφs:List 𝓕.FieldOpi:Fin φs.lengthj:Fin φs.lengthhij:i < ja:Fin [singleton hij]ᵘᶜ.lengthhn:uncontractedListEmd a = jh1:uncontractedListEmd a ∈ (singleton hij).uncontracted⊢ ¬∀ p ∈ ↑(singleton hij), j ∉ p𝓕:FieldSpecificationφs:List 𝓕.FieldOpi:Fin φs.lengthj:Fin φs.lengthhij:i < ja:Fin [singleton hij]ᵘᶜ.lengthhn:uncontractedListEmd a = jh1:uncontractedListEmd a ∈ (singleton hij).uncontracted⊢ ¬∀ p ∈ ↑(singleton hij), j ∉ p𝓕:FieldSpecificationφs:List 𝓕.FieldOpi:Fin φs.lengthj:Fin φs.lengthhij:i < ja:Fin [singleton hij]ᵘᶜ.lengthhn:uncontractedListEmd a = jh1:uncontractedListEmd a ∈ (singleton hij).uncontractedh2:j ∉ (singleton hij).uncontracted⊢ False]𝓕:FieldSpecificationφs:List 𝓕.FieldOpi:Fin φs.lengthj:Fin φs.lengthhij:i < ja:Fin [singleton hij]ᵘᶜ.lengthhn:uncontractedListEmd a = jh1:uncontractedListEmd a ∈ (singleton hij).uncontracted⊢ ¬∀ p ∈ ↑(singleton hij), j ∉ p𝓕:FieldSpecificationφs:List 𝓕.FieldOpi:Fin φs.lengthj:Fin φs.lengthhij:i < ja:Fin [singleton hij]ᵘᶜ.lengthhn:uncontractedListEmd a = jh1:uncontractedListEmd a ∈ (singleton hij).uncontractedh2:j ∉ (singleton hij).uncontracted⊢ False
    simp [singleton]𝓕:FieldSpecificationφs:List 𝓕.FieldOpi:Fin φs.lengthj:Fin φs.lengthhij:i < ja:Fin [singleton hij]ᵘᶜ.lengthhn:uncontractedListEmd a = jh1:uncontractedListEmd a ∈ (singleton hij).uncontractedh2:j ∉ (singleton hij).uncontracted⊢ False𝓕:FieldSpecificationφs:List 𝓕.FieldOpi:Fin φs.lengthj:Fin φs.lengthhij:i < ja:Fin [singleton hij]ᵘᶜ.lengthhn:uncontractedListEmd a = jh1:uncontractedListEmd a ∈ (singleton hij).uncontractedh2:j ∉ (singleton hij).uncontracted⊢ False
  simp_allAll goals completed! 🐙

@[simp]
lemma mem_signFinset {i j : Fin n} (hij : i < j) (a : Fin n) :
    a ∈ (singleton hij).signFinset i j ↔ i < a ∧ a < j := byn:ℕi:Fin nj:Fin nhij:i < ja:Fin n⊢ a ∈ (singleton hij).signFinset i j ↔ i < a ∧ a < j
  simp only [signFinset, Finset.mem_filter, Finset.mem_univ, true_and, and_congr_right_iff,
    and_iff_left_iff_imp]n:ℕi:Fin nj:Fin nhij:i < ja:Fin n⊢ i < a →
  a < j →
    (singleton hij).getDual? a = none ∨
      ∀ (h : ((singleton hij).getDual? a).isSome = true), i < ((singleton hij).getDual? a).get h
  intro h1 h2n:ℕi:Fin nj:Fin nhij:i < ja:Fin nh1:i < ah2:a < j⊢ (singleton hij).getDual? a = none ∨
  ∀ (h : ((singleton hij).getDual? a).isSome = true), i < ((singleton hij).getDual? a).get h
  rw [@singleton_getDual?_eq_none_iff_neqn:ℕi:Fin nj:Fin nhij:i < ja:Fin nh1:i < ah2:a < j⊢ i ≠ a ∧ j ≠ a ∨ ∀ (h : ((singleton hij).getDual? a).isSome = true), i < ((singleton hij).getDual? a).get hn:ℕi:Fin nj:Fin nhij:i < ja:Fin nh1:i < ah2:a < j⊢ i ≠ a ∧ j ≠ a ∨ ∀ (h : ((singleton hij).getDual? a).isSome = true), i < ((singleton hij).getDual? a).get h]n:ℕi:Fin nj:Fin nhij:i < ja:Fin nh1:i < ah2:a < j⊢ i ≠ a ∧ j ≠ a ∨ ∀ (h : ((singleton hij).getDual? a).isSome = true), i < ((singleton hij).getDual? a).get h
  apply Or.inln:ℕi:Fin nj:Fin nhij:i < ja:Fin nh1:i < ah2:a < j⊢ i ≠ a ∧ j ≠ a
  omegaAll goals completed! 🐙lemma subContraction_singleton_eq_singleton {φs : List 𝓕.FieldOp}
    (φsΛ : WickContraction φs.length)
    (a : φsΛ.1) : φsΛ.subContraction {a.1} (by𝓕:FieldSpecificationn:ℕc:WickContraction nφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengtha:↥↑φsΛ⊢ {↑a} ⊆ ↑φsΛ simpAll goals completed! 🐙) =
    singleton (φsΛ.fstFieldOfContract_lt_sndFieldOfContract a) := by𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengtha:↥↑φsΛ⊢ subContraction {↑a} ⋯ = singleton ⋯
  apply Subtype.ext𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengtha:↥↑φsΛ⊢ ↑(subContraction {↑a} ⋯) = ↑(singleton ⋯)
  simp only [subContraction, singleton, Finset.singleton_inj]𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengtha:↥↑φsΛ⊢ ↑a = {φsΛ.fstFieldOfContract a, φsΛ.sndFieldOfContract a}
  exact finset_eq_fstFieldOfContract_sndFieldOfContract φsΛ aAll goals completed! 🐙

lemma singleton_timeContract {φs : List 𝓕.FieldOp} {i j : Fin φs.length} (hij : i < j) :
    (singleton hij).timeContract =
    ⟨WickAlgebra.timeContract φs[i] φs[j], timeContract_mem_center _ _⟩ := by𝓕:FieldSpecificationφs:List 𝓕.FieldOpi:Fin φs.lengthj:Fin φs.lengthhij:i < j⊢ (singleton hij).timeContract = ⟨WickAlgebra.timeContract φs[i] φs[j], ⋯⟩
  rw [timeContract,𝓕:FieldSpecificationφs:List 𝓕.FieldOpi:Fin φs.lengthj:Fin φs.lengthhij:i < j⊢ ∏ a,
    ⟨WickAlgebra.timeContract (φs.get ((singleton hij).fstFieldOfContract a))
        (φs.get ((singleton hij).sndFieldOfContract a)),
      ⋯⟩ =
  ⟨WickAlgebra.timeContract φs[i] φs[j], ⋯⟩𝓕:FieldSpecificationφs:List 𝓕.FieldOpi:Fin φs.lengthj:Fin φs.lengthhij:i < j⊢ ⟨WickAlgebra.timeContract (φs.get ((singleton hij).fstFieldOfContract ⟨{i, j}, ⋯⟩))
      (φs.get ((singleton hij).sndFieldOfContract ⟨{i, j}, ⋯⟩)),
    ⋯⟩ =
  ⟨WickAlgebra.timeContract φs[i] φs[j], ⋯⟩ singleton_prod𝓕:FieldSpecificationφs:List 𝓕.FieldOpi:Fin φs.lengthj:Fin φs.lengthhij:i < j⊢ ⟨WickAlgebra.timeContract (φs.get ((singleton hij).fstFieldOfContract ⟨{i, j}, ⋯⟩))
      (φs.get ((singleton hij).sndFieldOfContract ⟨{i, j}, ⋯⟩)),
    ⋯⟩ =
  ⟨WickAlgebra.timeContract φs[i] φs[j], ⋯⟩𝓕:FieldSpecificationφs:List 𝓕.FieldOpi:Fin φs.lengthj:Fin φs.lengthhij:i < j⊢ ⟨WickAlgebra.timeContract (φs.get ((singleton hij).fstFieldOfContract ⟨{i, j}, ⋯⟩))
      (φs.get ((singleton hij).sndFieldOfContract ⟨{i, j}, ⋯⟩)),
    ⋯⟩ =
  ⟨WickAlgebra.timeContract φs[i] φs[j], ⋯⟩]𝓕:FieldSpecificationφs:List 𝓕.FieldOpi:Fin φs.lengthj:Fin φs.lengthhij:i < j⊢ ⟨WickAlgebra.timeContract (φs.get ((singleton hij).fstFieldOfContract ⟨{i, j}, ⋯⟩))
      (φs.get ((singleton hij).sndFieldOfContract ⟨{i, j}, ⋯⟩)),
    ⋯⟩ =
  ⟨WickAlgebra.timeContract φs[i] φs[j], ⋯⟩
  simpAll goals completed! 🐙

lemma singleton_staticContract {φs : List 𝓕.FieldOp} {i j : Fin φs.length} (hij : i < j) :
    (singleton hij).staticContract.1 =
    [anPart φs[i], ofFieldOp φs[j]]ₛ := by𝓕:FieldSpecificationφs:List 𝓕.FieldOpi:Fin φs.lengthj:Fin φs.lengthhij:i < j⊢ ↑(singleton hij).staticContract = (superCommute (anPart φs[i])) (ofFieldOp φs[j])
  rw [staticContract,𝓕:FieldSpecificationφs:List 𝓕.FieldOpi:Fin φs.lengthj:Fin φs.lengthhij:i < j⊢ ↑(∏ a,
      ⟨(superCommute (anPart (φs.get ((singleton hij).fstFieldOfContract a))))
          (ofFieldOp (φs.get ((singleton hij).sndFieldOfContract a))),
        ⋯⟩) =
  (superCommute (anPart φs[i])) (ofFieldOp φs[j])𝓕:FieldSpecificationφs:List 𝓕.FieldOpi:Fin φs.lengthj:Fin φs.lengthhij:i < j⊢ ↑⟨(superCommute (anPart (φs.get ((singleton hij).fstFieldOfContract ⟨{i, j}, ⋯⟩))))
        (ofFieldOp (φs.get ((singleton hij).sndFieldOfContract ⟨{i, j}, ⋯⟩))),
      ⋯⟩ =
  (superCommute (anPart φs[i])) (ofFieldOp φs[j]) singleton_prod𝓕:FieldSpecificationφs:List 𝓕.FieldOpi:Fin φs.lengthj:Fin φs.lengthhij:i < j⊢ ↑⟨(superCommute (anPart (φs.get ((singleton hij).fstFieldOfContract ⟨{i, j}, ⋯⟩))))
        (ofFieldOp (φs.get ((singleton hij).sndFieldOfContract ⟨{i, j}, ⋯⟩))),
      ⋯⟩ =
  (superCommute (anPart φs[i])) (ofFieldOp φs[j])𝓕:FieldSpecificationφs:List 𝓕.FieldOpi:Fin φs.lengthj:Fin φs.lengthhij:i < j⊢ ↑⟨(superCommute (anPart (φs.get ((singleton hij).fstFieldOfContract ⟨{i, j}, ⋯⟩))))
        (ofFieldOp (φs.get ((singleton hij).sndFieldOfContract ⟨{i, j}, ⋯⟩))),
      ⋯⟩ =
  (superCommute (anPart φs[i])) (ofFieldOp φs[j])]𝓕:FieldSpecificationφs:List 𝓕.FieldOpi:Fin φs.lengthj:Fin φs.lengthhij:i < j⊢ ↑⟨(superCommute (anPart (φs.get ((singleton hij).fstFieldOfContract ⟨{i, j}, ⋯⟩))))
        (ofFieldOp (φs.get ((singleton hij).sndFieldOfContract ⟨{i, j}, ⋯⟩))),
      ⋯⟩ =
  (superCommute (anPart φs[i])) (ofFieldOp φs[j])
  simpAll goals completed! 🐙