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.Join

Time contractions

@[expose] public section

The condition on a Wick contraction which is true iff and only if every contraction is between two fields of equal time.

def EqTimeOnly {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) : Prop := ∀ (i j), {i, j} ∈ φsΛ.1 → timeOrderRel φs[i] φs[j]
instance {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) : Decidable (EqTimeOnly φsΛ) := inferInstanceAs (Decidable (∀ (i j), {i, j} ∈ φsΛ.1 → timeOrderRel φs[i] φs[j]))lemma timeOrderRel_of_eqTimeOnly_pair {i j : Fin φs.length} (h : {i, j} ∈ φsΛ.1) (hc : EqTimeOnly φsΛ) : timeOrderRel φs[i] φs[j] := hc i j hlemma timeOrderRel_both_of_eqTimeOnly {i j : Fin φs.length} (h : {i, j} ∈ φsΛ.1) (hc : EqTimeOnly φsΛ) : timeOrderRel φs[i] φs[j] ∧ timeOrderRel φs[j] φs[i] := ⟨timeOrderRel_of_eqTimeOnly_pair φsΛ h hc, timeOrderRel_of_eqTimeOnly_pair φsΛ (𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.lengthj:Fin φs.lengthh:{i, j} ∈ ↑φsΛhc:φsΛ.EqTimeOnly⊢ {j, i} ∈ ↑φsΛ All goals completed! 🐙) hc⟩𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthh:∀ (a : ↥↑φsΛ), timeOrderRel φs[φsΛ.fstFieldOfContract a] φs[φsΛ.sndFieldOfContract a] ∧ timeOrderRel φs[φsΛ.sndFieldOfContract a] φs[φsΛ.fstFieldOfContract a]i:Fin φs.lengthj:Fin φs.lengthh1:{i, j} ∈ ↑φsΛh':timeOrderRel φs[φsΛ.fstFieldOfContract ⟨{i, j}, h1⟩] φs[φsΛ.sndFieldOfContract ⟨{i, j}, h1⟩] ∧ timeOrderRel φs[φsΛ.sndFieldOfContract ⟨{i, j}, h1⟩] φs[φsΛ.fstFieldOfContract ⟨{i, j}, h1⟩]hij✝:¬i < jhij:i ≠ jhj:φsΛ.fstFieldOfContract ⟨{i, j}, h1⟩ = jhi:φsΛ.sndFieldOfContract ⟨{i, j}, h1⟩ = i⊢ timeOrderRel φs[↑i] φs[↑j] All goals completed! 🐙𝓕:FieldSpecificationφs:List 𝓕.FieldOp⊢ ∀ (a : ↥↑empty), timeOrderRel φs[empty.fstFieldOfContract a] φs[empty.sndFieldOfContract a] ∧ timeOrderRel φs[empty.sndFieldOfContract a] φs[empty.fstFieldOfContract a] All goals completed! 🐙

Let φs be a list of 𝓕.FieldOp and φsΛ a WickContraction of φs within which every contraction involves two 𝓕.FieldOps that have the same time, then φsΛ.staticContract = φsΛ.timeContract.

𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthh:φsΛ.EqTimeOnlya:↥↑φsΛ⊢ timeOrderRel φs[↑(φsΛ.fstFieldOfContract a)] φs[↑(φsΛ.sndFieldOfContract a)] 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthh:φsΛ.EqTimeOnlya:↥↑φsΛ⊢ {φsΛ.fstFieldOfContract a, φsΛ.sndFieldOfContract a} ∈ ↑φsΛ All goals completed! 🐙
lemma eqTimeOnly_congr {φs φs' : List 𝓕.FieldOp} (h : φs = φs') (φsΛ : WickContraction φs.length) : (congr (𝓕:FieldSpecificationn:ℕc:WickContraction nφs✝:List 𝓕.FieldOpφsΛ✝:WickContraction φs✝.lengthφs:List 𝓕.FieldOpφs':List 𝓕.FieldOph:φs = φs'φsΛ:WickContraction φs.length⊢ φs.length = φs'.length All goals completed! 🐙) φsΛ).EqTimeOnly (φs := φs') ↔ φsΛ.EqTimeOnly := 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφs':List 𝓕.FieldOph:φs = φs'φsΛ:WickContraction φs.length⊢ ((congr ⋯) φsΛ).EqTimeOnly ↔ φsΛ.EqTimeOnly 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.length⊢ ((congr ⋯) φsΛ).EqTimeOnly ↔ φsΛ.EqTimeOnly All goals completed! 🐙𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthh:∀ (a : ↥↑φsΛ), timeOrderRel φs[φsΛ.fstFieldOfContract a] φs[φsΛ.sndFieldOfContract a] ∧ timeOrderRel φs[φsΛ.sndFieldOfContract a] φs[φsΛ.fstFieldOfContract a]S:Finset (Finset (Fin φs.length))ha:S ⊆ ↑φsΛa:↥↑(quotContraction S ha)⊢ timeOrderRel φs[↑(φsΛ.fstFieldOfContract ⟨Finset.map uncontractedListEmd ↑a, ⋯⟩)] φs[↑(φsΛ.sndFieldOfContract ⟨Finset.map uncontractedListEmd ↑a, ⋯⟩)] ∧ timeOrderRel φs[↑(φsΛ.sndFieldOfContract ⟨Finset.map uncontractedListEmd ↑a, ⋯⟩)] φs[↑(φsΛ.fstFieldOfContract ⟨Finset.map uncontractedListEmd ↑a, ⋯⟩)] All goals completed! 🐙𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthh:0 < (↑φsΛ).cardh1✝:φsΛ.EqTimeOnlya:Finset (Fin φs.length)ha:a ∈ ↑φsΛφsucΛ:WickContraction [singleton ⋯]ᵘᶜ.length := (congr ⋯) (quotContraction {a} ⋯)h1:(↑(subContraction {a} ⋯)).card + (↑(quotContraction {a} ⋯)).card = (↑φsΛ).card⊢ (↑(quotContraction {a} ⋯)).card + 1 = (↑φsΛ).card 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthh:0 < (↑φsΛ).cardh1✝:φsΛ.EqTimeOnlya:Finset (Fin φs.length)ha:a ∈ ↑φsΛφsucΛ:WickContraction [singleton ⋯]ᵘᶜ.length := (congr ⋯) (quotContraction {a} ⋯)h1:1 + (↑(quotContraction {a} ⋯)).card = (↑φsΛ).card⊢ (↑(quotContraction {a} ⋯)).card + 1 = (↑φsΛ).card All goals completed! 🐙𝓕:FieldSpecificationφs:List 𝓕.FieldOpa:𝓕.WickAlgebrab:𝓕.WickAlgebran:ℕi:Fin φs.lengthj:Fin φs.lengthhij:i < jφsucΛ:WickContraction [singleton hij]ᵘᶜ.lengthhl:((singleton hij).join φsucΛ).EqTimeOnlyhn:(↑((singleton hij).join φsucΛ)).card = n.succh2:timeOrderRel φs[i] φs[j] ∧ timeOrderRel φs[j] φs[i]h3:φsucΛ.EqTimeOnlyh4:(↑φsucΛ).card + 1 = (↑((singleton hij).join φsucΛ)).cardih:timeOrder (a * ↑φsucΛ.timeContract * b) = ↑φsucΛ.timeContract * timeOrder (a * b)⊢ WickAlgebra.timeContract φs[i] φs[j] * (↑φsucΛ.timeContract * timeOrder (a * b)) = WickAlgebra.timeContract φs[↑i] φs[↑j] * ↑φsucΛ.timeContract * timeOrder (a * b)𝓕:FieldSpecificationφs:List 𝓕.FieldOpa:𝓕.WickAlgebrab:𝓕.WickAlgebran:ℕi:Fin φs.lengthj:Fin φs.lengthhij:i < jφsucΛ:WickContraction [singleton hij]ᵘᶜ.lengthhl:((singleton hij).join φsucΛ).EqTimeOnlyhn:(↑((singleton hij).join φsucΛ)).card = n.succh2:timeOrderRel φs[i] φs[j] ∧ timeOrderRel φs[j] φs[i]h3:φsucΛ.EqTimeOnlyh4:(↑φsucΛ).card + 1 = (↑((singleton hij).join φsucΛ)).card⊢ timeOrderRel φs[i] φs[j]𝓕:FieldSpecificationφs:List 𝓕.FieldOpa:𝓕.WickAlgebrab:𝓕.WickAlgebran:ℕi:Fin φs.lengthj:Fin φs.lengthhij:i < jφsucΛ:WickContraction [singleton hij]ᵘᶜ.lengthhl:((singleton hij).join φsucΛ).EqTimeOnlyhn:(↑((singleton hij).join φsucΛ)).card = n.succh2:timeOrderRel φs[i] φs[j] ∧ timeOrderRel φs[j] φs[i]h3:φsucΛ.EqTimeOnlyh4:(↑φsucΛ).card + 1 = (↑((singleton hij).join φsucΛ)).card⊢ timeOrderRel φs[j] φs[i] 𝓕:FieldSpecificationφs:List 𝓕.FieldOpa:𝓕.WickAlgebrab:𝓕.WickAlgebran:ℕi:Fin φs.lengthj:Fin φs.lengthhij:i < jφsucΛ:WickContraction [singleton hij]ᵘᶜ.lengthhl:((singleton hij).join φsucΛ).EqTimeOnlyhn:(↑((singleton hij).join φsucΛ)).card = n.succh2:timeOrderRel φs[i] φs[j] ∧ timeOrderRel φs[j] φs[i]h3:φsucΛ.EqTimeOnlyh4:(↑φsucΛ).card + 1 = (↑((singleton hij).join φsucΛ)).card⊢ timeOrderRel φs[i] φs[j]𝓕:FieldSpecificationφs:List 𝓕.FieldOpa:𝓕.WickAlgebrab:𝓕.WickAlgebran:ℕi:Fin φs.lengthj:Fin φs.lengthhij:i < jφsucΛ:WickContraction [singleton hij]ᵘᶜ.lengthhl:((singleton hij).join φsucΛ).EqTimeOnlyhn:(↑((singleton hij).join φsucΛ)).card = n.succh2:timeOrderRel φs[i] φs[j] ∧ timeOrderRel φs[j] φs[i]h3:φsucΛ.EqTimeOnlyh4:(↑φsucΛ).card + 1 = (↑((singleton hij).join φsucΛ)).card⊢ timeOrderRel φs[j] φs[i] all_goals All goals completed! 🐙lemma timeOrder_timeContract_mul_of_eqTimeOnly_mid {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) (hl : φsΛ.EqTimeOnly) (a b : 𝓕.WickAlgebra) : 𝓣(a * φsΛ.timeContract.1 * b) = φsΛ.timeContract.1 * 𝓣(a * b) := timeOrder_timeContract_mul_of_eqTimeOnly_mid_induction φsΛ hl a b φsΛ.1.card rfl

Let φs be a list of 𝓕.FieldOp, φsΛ a WickContraction of φs within which every contraction involves two 𝓕.FieldOps that have the same time and b a general element in 𝓕.WickAlgebra. Then 𝓣(φsΛ.timeContract.1 * b) = φsΛ.timeContract.1 * 𝓣(b).

This follows from properties of orderings and the ideal defining 𝓕.WickAlgebra.

𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthhl:φsΛ.EqTimeOnlyb:𝓕.WickAlgebra⊢ ↑φsΛ.timeContract * timeOrder (1 * b) = ↑φsΛ.timeContract * timeOrder b All goals completed! 🐙
All goals completed! 🐙 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengtha:Finset (Fin φs.length)ha:a ∈ ↑φsΛhr:timeOrderRel φs[↑(φsΛ.fstFieldOfContract ⟨a, ⋯⟩)] φs[↑(φsΛ.sndFieldOfContract ⟨a, ⋯⟩)] → ¬timeOrderRel φs[↑(φsΛ.sndFieldOfContract ⟨a, ⋯⟩)] φs[↑(φsΛ.fstFieldOfContract ⟨a, ⋯⟩)]φsucΛ:WickContraction [singleton ⋯]ᵘᶜ.length := (congr ⋯) (quotContraction {a} ⋯)⊢ ¬timeOrderRel φs[↑(φsΛ.fstFieldOfContract ⟨a, ha⟩)] φs[↑(φsΛ.sndFieldOfContract ⟨a, ha⟩)] ∨ ¬timeOrderRel φs[↑(φsΛ.sndFieldOfContract ⟨a, ha⟩)] φs[↑(φsΛ.fstFieldOfContract ⟨a, ha⟩)] All goals completed! 🐙𝓕:FieldSpecificationφs:List 𝓕.FieldOpi:Fin φs.lengthj:Fin φs.lengthhij:i < jφsucΛ:WickContraction [singleton hij]ᵘᶜ.lengthhr:¬timeOrderRel φs[i] φs[j] ∨ ¬timeOrderRel φs[j] φs[i]hl:¬((singleton hij).join φsucΛ).EqTimeOnly⊢ timeOrder (0 * ↑φsucΛ.timeContract) = 0𝓕:FieldSpecificationφs:List 𝓕.FieldOpi:Fin φs.lengthj:Fin φs.lengthhij:i < jφsucΛ:WickContraction [singleton hij]ᵘᶜ.lengthhr:¬timeOrderRel φs[i] φs[j] ∨ ¬timeOrderRel φs[j] φs[i]hl:¬((singleton hij).join φsucΛ).EqTimeOnly⊢ ¬(timeOrderRel φs[↑i] φs[↑j] ∧ timeOrderRel φs[↑j] φs[↑i]) 𝓕:FieldSpecificationφs:List 𝓕.FieldOpi:Fin φs.lengthj:Fin φs.lengthhij:i < jφsucΛ:WickContraction [singleton hij]ᵘᶜ.lengthhr:¬timeOrderRel φs[i] φs[j] ∨ ¬timeOrderRel φs[j] φs[i]hl:¬((singleton hij).join φsucΛ).EqTimeOnly⊢ ¬(timeOrderRel φs[↑i] φs[↑j] ∧ timeOrderRel φs[↑j] φs[↑i]) All goals completed! 🐙

Let φs be a list of 𝓕.FieldOp and φsΛ a WickContraction with at least one contraction between 𝓕.FieldOp that do not have the same time. Then 𝓣(φsΛ.staticContract.1) = 0.

𝓕:FieldSpecificationφs:List 𝓕.FieldOpi:Fin φs.lengthj:Fin φs.lengthhij:i < jφsucΛ:WickContraction [singleton hij]ᵘᶜ.lengthhr:¬timeOrderRel φs[i] φs[j] ∨ ¬timeOrderRel φs[j] φs[i]hl:¬((singleton hij).join φsucΛ).EqTimeOnly⊢ timeOrder (0 * ↑φsucΛ.staticContract) = 0𝓕:FieldSpecificationφs:List 𝓕.FieldOpi:Fin φs.lengthj:Fin φs.lengthhij:i < jφsucΛ:WickContraction [singleton hij]ᵘᶜ.lengthhr:¬timeOrderRel φs[i] φs[j] ∨ ¬timeOrderRel φs[j] φs[i]hl:¬((singleton hij).join φsucΛ).EqTimeOnly⊢ ¬(timeOrderRel φs[i] φs[j] ∧ timeOrderRel φs[j] φs[i]) 𝓕:FieldSpecificationφs:List 𝓕.FieldOpi:Fin φs.lengthj:Fin φs.lengthhij:i < jφsucΛ:WickContraction [singleton hij]ᵘᶜ.lengthhr:¬timeOrderRel φs[i] φs[j] ∨ ¬timeOrderRel φs[j] φs[i]hl:¬((singleton hij).join φsucΛ).EqTimeOnly⊢ ¬(timeOrderRel φs[i] φs[j] ∧ timeOrderRel φs[j] φs[i]) All goals completed! 🐙

The condition on a Wick contraction which is true if it has at least one contraction which is between two equal time fields.

def HaveEqTime {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) : Prop := ∃ (i j : Fin φs.length) (h : {i, j} ∈ φsΛ.1), timeOrderRel φs[i] φs[j] ∧ timeOrderRel φs[j] φs[i]
𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengtha:Finset (Fin φs.length)h1:a ∈ ↑φsΛh2:timeOrderRel φs[↑(φsΛ.fstFieldOfContract ⟨a, ⋯⟩)] φs[↑(φsΛ.sndFieldOfContract ⟨a, ⋯⟩)]h3:timeOrderRel φs[↑(φsΛ.sndFieldOfContract ⟨a, ⋯⟩)] φs[↑(φsΛ.fstFieldOfContract ⟨a, ⋯⟩)]⊢ ↑⟨a, h1⟩ ∈ ↑φsΛ All goals completed! 🐙𝓕:FieldSpecificationφs:List 𝓕.FieldOp⊢ ¬∃ a, ∃ (h : a ∈ ↑empty), timeOrderRel φs[empty.fstFieldOfContract ⟨a, h⟩] φs[empty.sndFieldOfContract ⟨a, h⟩] ∧ timeOrderRel φs[empty.sndFieldOfContract ⟨a, h⟩] φs[empty.fstFieldOfContract ⟨a, h⟩] All goals completed! 🐙

Given a Wick contraction the subset of contracted pairs between equal time fields.

def eqTimeContractSet {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) : Finset (Finset (Fin φs.length)) := Finset.univ.filter (fun a => a ∈ φsΛ.1 ∧ ∀ (h : a ∈ φsΛ.1), timeOrderRel φs[φsΛ.fstFieldOfContract ⟨a, h⟩] φs[φsΛ.sndFieldOfContract ⟨a, h⟩] ∧ timeOrderRel φs[φsΛ.sndFieldOfContract ⟨a, h⟩] φs[φsΛ.fstFieldOfContract ⟨a, h⟩])
lemma eqTimeContractSet_subset {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) : eqTimeContractSet φsΛ ⊆ φsΛ.1 := 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.length⊢ φsΛ.eqTimeContractSet ⊆ ↑φsΛ 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengtha:Finset (Fin φs.length)ha:a ∈ φsΛ.eqTimeContractSet⊢ a ∈ ↑φsΛ 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengtha:Finset (Fin φs.length)ha:a ∈ ↑φsΛ ∧ ∀ (h : a ∈ ↑φsΛ), timeOrderRel φs[φsΛ.fstFieldOfContract ⟨a, h⟩] φs[φsΛ.sndFieldOfContract ⟨a, h⟩] ∧ timeOrderRel φs[φsΛ.sndFieldOfContract ⟨a, h⟩] φs[φsΛ.fstFieldOfContract ⟨a, h⟩]⊢ a ∈ ↑φsΛ All goals completed! 🐙lemma mem_of_mem_eqTimeContractSet{φs : List 𝓕.FieldOp} {φsΛ : WickContraction φs.length} {a : Finset (Fin φs.length)} (h : a ∈ eqTimeContractSet φsΛ) : a ∈ φsΛ.1 := eqTimeContractSet_subset φsΛ h𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengthb:Finset (Fin [φsΛ]ᵘᶜ.length)h1:b ∈ ↑φsucΛ ∧ ∀ (h : b ∈ ↑φsucΛ), timeOrderRel [φsΛ]ᵘᶜ[↑(φsucΛ.fstFieldOfContract ⟨b, h⟩)] [φsΛ]ᵘᶜ[↑(φsucΛ.sndFieldOfContract ⟨b, h⟩)] ∧ timeOrderRel [φsΛ]ᵘᶜ[↑(φsucΛ.sndFieldOfContract ⟨b, h⟩)] [φsΛ]ᵘᶜ[↑(φsucΛ.fstFieldOfContract ⟨b, h⟩)]h':(Finset.mapEmbedding uncontractedListEmd) b ∈ ↑(φsΛ.join φsucΛ)h2:timeOrderRel [φsΛ]ᵘᶜ[↑(φsucΛ.fstFieldOfContract ⟨b, ⋯⟩)] [φsΛ]ᵘᶜ[↑(φsucΛ.sndFieldOfContract ⟨b, ⋯⟩)] ∧ timeOrderRel [φsΛ]ᵘᶜ[↑(φsucΛ.sndFieldOfContract ⟨b, ⋯⟩)] [φsΛ]ᵘᶜ[↑(φsucΛ.fstFieldOfContract ⟨b, ⋯⟩)]hj:⟨(Finset.mapEmbedding uncontractedListEmd) b, h'⟩ = joinLiftRight ⟨b, ⋯⟩⊢ timeOrderRel φs[↑((φsΛ.join φsucΛ).fstFieldOfContract ⟨(Finset.mapEmbedding uncontractedListEmd) b, h'⟩)] φs[↑((φsΛ.join φsucΛ).sndFieldOfContract ⟨(Finset.mapEmbedding uncontractedListEmd) b, h'⟩)] ∧ timeOrderRel φs[↑((φsΛ.join φsucΛ).sndFieldOfContract ⟨(Finset.mapEmbedding uncontractedListEmd) b, h'⟩)] φs[↑((φsΛ.join φsucΛ).fstFieldOfContract ⟨(Finset.mapEmbedding uncontractedListEmd) b, h'⟩)] 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengthb:Finset (Fin [φsΛ]ᵘᶜ.length)h1:b ∈ ↑φsucΛ ∧ ∀ (h : b ∈ ↑φsucΛ), timeOrderRel [φsΛ]ᵘᶜ[↑(φsucΛ.fstFieldOfContract ⟨b, h⟩)] [φsΛ]ᵘᶜ[↑(φsucΛ.sndFieldOfContract ⟨b, h⟩)] ∧ timeOrderRel [φsΛ]ᵘᶜ[↑(φsucΛ.sndFieldOfContract ⟨b, h⟩)] [φsΛ]ᵘᶜ[↑(φsucΛ.fstFieldOfContract ⟨b, h⟩)]h':(Finset.mapEmbedding uncontractedListEmd) b ∈ ↑(φsΛ.join φsucΛ)h2:timeOrderRel [φsΛ]ᵘᶜ[↑(φsucΛ.fstFieldOfContract ⟨b, ⋯⟩)] [φsΛ]ᵘᶜ[↑(φsucΛ.sndFieldOfContract ⟨b, ⋯⟩)] ∧ timeOrderRel [φsΛ]ᵘᶜ[↑(φsucΛ.sndFieldOfContract ⟨b, ⋯⟩)] [φsΛ]ᵘᶜ[↑(φsucΛ.fstFieldOfContract ⟨b, ⋯⟩)]hj:⟨(Finset.mapEmbedding uncontractedListEmd) b, h'⟩ = joinLiftRight ⟨b, ⋯⟩⊢ timeOrderRel [φsΛ]ᵘᶜ[↑(φsucΛ.fstFieldOfContract ⟨b, ⋯⟩)] [φsΛ]ᵘᶜ[↑(φsucΛ.sndFieldOfContract ⟨b, ⋯⟩)] ∧ timeOrderRel [φsΛ]ᵘᶜ[↑(φsucΛ.sndFieldOfContract ⟨b, ⋯⟩)] [φsΛ]ᵘᶜ[↑(φsucΛ.fstFieldOfContract ⟨b, ⋯⟩)] All goals completed! 🐙𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthh:¬∃ a, ∃ (h : a ∈ ↑φsΛ), timeOrderRel φs[φsΛ.fstFieldOfContract ⟨a, h⟩] φs[φsΛ.sndFieldOfContract ⟨a, h⟩] ∧ timeOrderRel φs[φsΛ.sndFieldOfContract ⟨a, h⟩] φs[φsΛ.fstFieldOfContract ⟨a, h⟩]a:Finset (Fin φs.length)hn:a ∈ φsΛ.eqTimeContractSet⊢ False 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengtha:Finset (Fin φs.length)hn:a ∈ φsΛ.eqTimeContractSeth:∀ (x : Finset (Fin φs.length)) (x_1 : x ∈ ↑φsΛ), timeOrderRel φs[↑(φsΛ.fstFieldOfContract ⟨x, ⋯⟩)] φs[↑(φsΛ.sndFieldOfContract ⟨x, ⋯⟩)] → ¬timeOrderRel φs[↑(φsΛ.sndFieldOfContract ⟨x, ⋯⟩)] φs[↑(φsΛ.fstFieldOfContract ⟨x, ⋯⟩)]⊢ False 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengtha:Finset (Fin φs.length)h:∀ (x : Finset (Fin φs.length)) (x_1 : x ∈ ↑φsΛ), timeOrderRel φs[↑(φsΛ.fstFieldOfContract ⟨x, ⋯⟩)] φs[↑(φsΛ.sndFieldOfContract ⟨x, ⋯⟩)] → ¬timeOrderRel φs[↑(φsΛ.sndFieldOfContract ⟨x, ⋯⟩)] φs[↑(φsΛ.fstFieldOfContract ⟨x, ⋯⟩)]hn:a ∈ ↑φsΛ ∧ ∀ (h : a ∈ ↑φsΛ), timeOrderRel φs[↑(φsΛ.fstFieldOfContract ⟨a, h⟩)] φs[↑(φsΛ.sndFieldOfContract ⟨a, h⟩)] ∧ timeOrderRel φs[↑(φsΛ.sndFieldOfContract ⟨a, h⟩)] φs[↑(φsΛ.fstFieldOfContract ⟨a, h⟩)]⊢ False All goals completed! 🐙𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthh:∀ (a : ↥↑φsΛ), timeOrderRel φs[φsΛ.fstFieldOfContract a] φs[φsΛ.sndFieldOfContract a] ∧ timeOrderRel φs[φsΛ.sndFieldOfContract a] φs[φsΛ.fstFieldOfContract a]a:Finset (Fin φs.length)⊢ ∀ (h : a ∈ ↑φsΛ), timeOrderRel φs[↑(φsΛ.fstFieldOfContract ⟨a, h⟩)] φs[↑(φsΛ.sndFieldOfContract ⟨a, h⟩)] ∧ timeOrderRel φs[↑(φsΛ.sndFieldOfContract ⟨a, h⟩)] φs[↑(φsΛ.fstFieldOfContract ⟨a, h⟩)] All goals completed! 🐙𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.length⊢ ∀ (a : ↥↑(subContraction φsΛ.eqTimeContractSet ⋯)), timeOrderRel φs[(subContraction φsΛ.eqTimeContractSet ⋯).fstFieldOfContract a] φs[(subContraction φsΛ.eqTimeContractSet ⋯).sndFieldOfContract a] ∧ timeOrderRel φs[(subContraction φsΛ.eqTimeContractSet ⋯).sndFieldOfContract a] φs[(subContraction φsΛ.eqTimeContractSet ⋯).fstFieldOfContract a] 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengtha:↥↑(subContraction φsΛ.eqTimeContractSet ⋯)⊢ timeOrderRel φs[(subContraction φsΛ.eqTimeContractSet ⋯).fstFieldOfContract a] φs[(subContraction φsΛ.eqTimeContractSet ⋯).sndFieldOfContract a] ∧ timeOrderRel φs[(subContraction φsΛ.eqTimeContractSet ⋯).sndFieldOfContract a] φs[(subContraction φsΛ.eqTimeContractSet ⋯).fstFieldOfContract a] 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengtha:↥↑(subContraction φsΛ.eqTimeContractSet ⋯)ha2:↑a ∈ ↑(subContraction φsΛ.eqTimeContractSet ⋯)⊢ timeOrderRel φs[(subContraction φsΛ.eqTimeContractSet ⋯).fstFieldOfContract a] φs[(subContraction φsΛ.eqTimeContractSet ⋯).sndFieldOfContract a] ∧ timeOrderRel φs[(subContraction φsΛ.eqTimeContractSet ⋯).sndFieldOfContract a] φs[(subContraction φsΛ.eqTimeContractSet ⋯).fstFieldOfContract a] 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengtha:↥↑(subContraction φsΛ.eqTimeContractSet ⋯)ha2:↑a ∈ ↑φsΛ ∧ ∀ (h : ↑a ∈ ↑φsΛ), timeOrderRel φs[↑(φsΛ.fstFieldOfContract ⟨↑a, h⟩)] φs[↑(φsΛ.sndFieldOfContract ⟨↑a, h⟩)] ∧ timeOrderRel φs[↑(φsΛ.sndFieldOfContract ⟨↑a, h⟩)] φs[↑(φsΛ.fstFieldOfContract ⟨↑a, h⟩)]⊢ timeOrderRel φs[(subContraction φsΛ.eqTimeContractSet ⋯).fstFieldOfContract a] φs[(subContraction φsΛ.eqTimeContractSet ⋯).sndFieldOfContract a] ∧ timeOrderRel φs[(subContraction φsΛ.eqTimeContractSet ⋯).sndFieldOfContract a] φs[(subContraction φsΛ.eqTimeContractSet ⋯).fstFieldOfContract a] 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengtha:↥↑(subContraction φsΛ.eqTimeContractSet ⋯)ha2:↑a ∈ ↑φsΛ ∧ ∀ (h : ↑a ∈ ↑φsΛ), timeOrderRel φs[↑(φsΛ.fstFieldOfContract ⟨↑a, h⟩)] φs[↑(φsΛ.sndFieldOfContract ⟨↑a, h⟩)] ∧ timeOrderRel φs[↑(φsΛ.sndFieldOfContract ⟨↑a, h⟩)] φs[↑(φsΛ.fstFieldOfContract ⟨↑a, h⟩)]⊢ timeOrderRel φs[↑(φsΛ.fstFieldOfContract ⟨↑a, ⋯⟩)] φs[↑(φsΛ.sndFieldOfContract ⟨↑a, ⋯⟩)] ∧ timeOrderRel φs[↑(φsΛ.sndFieldOfContract ⟨↑a, ⋯⟩)] φs[↑(φsΛ.fstFieldOfContract ⟨↑a, ⋯⟩)] All goals completed! 🐙𝓕:FieldSpecificationφs:List 𝓕.FieldOpi:Fin φs.lengthj:Fin φs.lengthφsΛ:WickContraction φs.lengthh:{i, j} ∈ ↑φsΛhij:¬i < jhineqj:i ≠ jhji:j < ih1:φsΛ.fstFieldOfContract ⟨{i, j}, h⟩ = jh2:φsΛ.sndFieldOfContract ⟨{i, j}, h⟩ = i⊢ ({i, j} ∈ ↑φsΛ ∧ ∀ (h : {i, j} ∈ ↑φsΛ), timeOrderRel φs[↑(φsΛ.fstFieldOfContract ⟨{i, j}, h⟩)] φs[↑(φsΛ.sndFieldOfContract ⟨{i, j}, h⟩)] ∧ timeOrderRel φs[↑(φsΛ.sndFieldOfContract ⟨{i, j}, h⟩)] φs[↑(φsΛ.fstFieldOfContract ⟨{i, j}, h⟩)]) ↔ timeOrderRel φs[↑i] φs[↑j] ∧ timeOrderRel φs[↑j] φs[↑i] 𝓕:FieldSpecificationφs:List 𝓕.FieldOpi:Fin φs.lengthj:Fin φs.lengthφsΛ:WickContraction φs.lengthh:{i, j} ∈ ↑φsΛhij:¬i < jhineqj:i ≠ jhji:j < ih1:φsΛ.fstFieldOfContract ⟨{i, j}, h⟩ = jh2:φsΛ.sndFieldOfContract ⟨{i, j}, h⟩ = i⊢ ({i, j} ∈ ↑φsΛ ∧ ∀ (h : {i, j} ∈ ↑φsΛ), timeOrderRel φs[↑j] φs[↑i] ∧ timeOrderRel φs[↑i] φs[↑j]) ↔ timeOrderRel φs[↑i] φs[↑j] ∧ timeOrderRel φs[↑j] φs[↑i] 𝓕:FieldSpecificationφs:List 𝓕.FieldOpi:Fin φs.lengthj:Fin φs.lengthφsΛ:WickContraction φs.lengthh:{i, j} ∈ ↑φsΛh1:φsΛ.fstFieldOfContract ⟨{i, j}, h⟩ = jh2:φsΛ.sndFieldOfContract ⟨{i, j}, h⟩ = ihij:j ≤ ihineqj:¬i = jhji:j < i⊢ timeOrderRel φs[↑j] φs[↑i] ∧ timeOrderRel φs[↑i] φs[↑j] ↔ timeOrderRel φs[↑i] φs[↑j] ∧ timeOrderRel φs[↑j] φs[↑i] All goals completed! 🐙𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthi:Fin φs.lengthj:Fin φs.lengthhij:timeOrderRel φs[↑i] φs[↑j]h1:{i, j} ∈ ↑φsΛh2:timeOrderRel φs[↑j] φs[↑i]⊢ timeOrderRel φs[i] φs[j] ∧ timeOrderRel φs[j] φs[i] All goals completed! 🐙𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.length⊢ ¬∃ a, ∃ (h : a ∈ ↑(quotContraction φsΛ.eqTimeContractSet ⋯)), timeOrderRel [subContraction φsΛ.eqTimeContractSet ⋯]ᵘᶜ[(quotContraction φsΛ.eqTimeContractSet ⋯).fstFieldOfContract ⟨a, h⟩] [subContraction φsΛ.eqTimeContractSet ⋯]ᵘᶜ[(quotContraction φsΛ.eqTimeContractSet ⋯).sndFieldOfContract ⟨a, h⟩] ∧ timeOrderRel [subContraction φsΛ.eqTimeContractSet ⋯]ᵘᶜ[(quotContraction φsΛ.eqTimeContractSet ⋯).sndFieldOfContract ⟨a, h⟩] [subContraction φsΛ.eqTimeContractSet ⋯]ᵘᶜ[(quotContraction φsΛ.eqTimeContractSet ⋯).fstFieldOfContract ⟨a, h⟩] 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.length⊢ ∀ (x : Finset (Fin [subContraction φsΛ.eqTimeContractSet ⋯]ᵘᶜ.length)) (x_1 : x ∈ ↑(quotContraction φsΛ.eqTimeContractSet ⋯)), timeOrderRel [subContraction φsΛ.eqTimeContractSet ⋯]ᵘᶜ[↑((quotContraction φsΛ.eqTimeContractSet ⋯).fstFieldOfContract ⟨x, ⋯⟩)] [subContraction φsΛ.eqTimeContractSet ⋯]ᵘᶜ[↑((quotContraction φsΛ.eqTimeContractSet ⋯).sndFieldOfContract ⟨x, ⋯⟩)] → ¬timeOrderRel [subContraction φsΛ.eqTimeContractSet ⋯]ᵘᶜ[↑((quotContraction φsΛ.eqTimeContractSet ⋯).sndFieldOfContract ⟨x, ⋯⟩)] [subContraction φsΛ.eqTimeContractSet ⋯]ᵘᶜ[↑((quotContraction φsΛ.eqTimeContractSet ⋯).fstFieldOfContract ⟨x, ⋯⟩)] 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengtha:Finset (Fin [subContraction φsΛ.eqTimeContractSet ⋯]ᵘᶜ.length)ha:a ∈ ↑(quotContraction φsΛ.eqTimeContractSet ⋯)⊢ timeOrderRel [subContraction φsΛ.eqTimeContractSet ⋯]ᵘᶜ[↑((quotContraction φsΛ.eqTimeContractSet ⋯).fstFieldOfContract ⟨a, ⋯⟩)] [subContraction φsΛ.eqTimeContractSet ⋯]ᵘᶜ[↑((quotContraction φsΛ.eqTimeContractSet ⋯).sndFieldOfContract ⟨a, ⋯⟩)] → ¬timeOrderRel [subContraction φsΛ.eqTimeContractSet ⋯]ᵘᶜ[↑((quotContraction φsΛ.eqTimeContractSet ⋯).sndFieldOfContract ⟨a, ⋯⟩)] [subContraction φsΛ.eqTimeContractSet ⋯]ᵘᶜ[↑((quotContraction φsΛ.eqTimeContractSet ⋯).fstFieldOfContract ⟨a, ⋯⟩)] erw [𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengtha:Finset (Fin [subContraction φsΛ.eqTimeContractSet ⋯]ᵘᶜ.length)ha:a ∈ ↑(quotContraction φsΛ.eqTimeContractSet ⋯)⊢ timeOrderRel φs[uncontractedListEmd ((quotContraction φsΛ.eqTimeContractSet ⋯).fstFieldOfContract ⟨a, ⋯⟩)] [subContraction φsΛ.eqTimeContractSet ⋯]ᵘᶜ[↑((quotContraction φsΛ.eqTimeContractSet ⋯).sndFieldOfContract ⟨a, ⋯⟩)] → ¬timeOrderRel [subContraction φsΛ.eqTimeContractSet ⋯]ᵘᶜ[↑((quotContraction φsΛ.eqTimeContractSet ⋯).sndFieldOfContract ⟨a, ⋯⟩)] φs[uncontractedListEmd ((quotContraction φsΛ.eqTimeContractSet ⋯).fstFieldOfContract ⟨a, ⋯⟩)] 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengtha:Finset (Fin [subContraction φsΛ.eqTimeContractSet ⋯]ᵘᶜ.length)ha:a ∈ ↑(quotContraction φsΛ.eqTimeContractSet ⋯)⊢ timeOrderRel φs[uncontractedListEmd ((quotContraction φsΛ.eqTimeContractSet ⋯).fstFieldOfContract ⟨a, ⋯⟩)] φs[uncontractedListEmd ((quotContraction φsΛ.eqTimeContractSet ⋯).sndFieldOfContract ⟨a, ⋯⟩)] → ¬timeOrderRel φs[uncontractedListEmd ((quotContraction φsΛ.eqTimeContractSet ⋯).sndFieldOfContract ⟨a, ⋯⟩)] φs[uncontractedListEmd ((quotContraction φsΛ.eqTimeContractSet ⋯).fstFieldOfContract ⟨a, ⋯⟩)]𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengtha:Finset (Fin [subContraction φsΛ.eqTimeContractSet ⋯]ᵘᶜ.length)ha:a ∈ ↑(quotContraction φsΛ.eqTimeContractSet ⋯)⊢ timeOrderRel φs[uncontractedListEmd ((quotContraction φsΛ.eqTimeContractSet ⋯).fstFieldOfContract ⟨a, ⋯⟩)] φs[uncontractedListEmd ((quotContraction φsΛ.eqTimeContractSet ⋯).sndFieldOfContract ⟨a, ⋯⟩)] → ¬timeOrderRel φs[uncontractedListEmd ((quotContraction φsΛ.eqTimeContractSet ⋯).sndFieldOfContract ⟨a, ⋯⟩)] φs[uncontractedListEmd ((quotContraction φsΛ.eqTimeContractSet ⋯).fstFieldOfContract ⟨a, ⋯⟩)] 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengtha:Finset (Fin [subContraction φsΛ.eqTimeContractSet ⋯]ᵘᶜ.length)ha:a ∈ ↑(quotContraction φsΛ.eqTimeContractSet ⋯)⊢ timeOrderRel φs[↑(φsΛ.fstFieldOfContract ⟨Finset.map uncontractedListEmd a, ⋯⟩)] φs[↑(φsΛ.sndFieldOfContract ⟨Finset.map uncontractedListEmd a, ⋯⟩)] → ¬timeOrderRel φs[↑(φsΛ.sndFieldOfContract ⟨Finset.map uncontractedListEmd a, ⋯⟩)] φs[↑(φsΛ.fstFieldOfContract ⟨Finset.map uncontractedListEmd a, ⋯⟩)] 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengtha:Finset (Fin [subContraction φsΛ.eqTimeContractSet ⋯]ᵘᶜ.length)ha✝:a ∈ ↑(quotContraction φsΛ.eqTimeContractSet ⋯)ha:Finset.map uncontractedListEmd a ∈ ↑φsΛ⊢ timeOrderRel φs[↑(φsΛ.fstFieldOfContract ⟨Finset.map uncontractedListEmd a, ⋯⟩)] φs[↑(φsΛ.sndFieldOfContract ⟨Finset.map uncontractedListEmd a, ⋯⟩)] → ¬timeOrderRel φs[↑(φsΛ.sndFieldOfContract ⟨Finset.map uncontractedListEmd a, ⋯⟩)] φs[↑(φsΛ.fstFieldOfContract ⟨Finset.map uncontractedListEmd a, ⋯⟩)] 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengtha:Finset (Fin [subContraction φsΛ.eqTimeContractSet ⋯]ᵘᶜ.length)ha✝:a ∈ ↑(quotContraction φsΛ.eqTimeContractSet ⋯)ha:Finset.map uncontractedListEmd a ∈ ↑φsΛhn':Finset.map uncontractedListEmd a ∉ ↑(subContraction φsΛ.eqTimeContractSet ⋯)⊢ timeOrderRel φs[↑(φsΛ.fstFieldOfContract ⟨Finset.map uncontractedListEmd a, ⋯⟩)] φs[↑(φsΛ.sndFieldOfContract ⟨Finset.map uncontractedListEmd a, ⋯⟩)] → ¬timeOrderRel φs[↑(φsΛ.sndFieldOfContract ⟨Finset.map uncontractedListEmd a, ⋯⟩)] φs[↑(φsΛ.fstFieldOfContract ⟨Finset.map uncontractedListEmd a, ⋯⟩)] 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengtha:Finset (Fin [subContraction φsΛ.eqTimeContractSet ⋯]ᵘᶜ.length)ha✝:a ∈ ↑(quotContraction φsΛ.eqTimeContractSet ⋯)ha:Finset.map uncontractedListEmd a ∈ ↑φsΛhn':Finset.map uncontractedListEmd a ∈ ↑φsΛ → ∃ (h : Finset.map uncontractedListEmd a ∈ ↑φsΛ), timeOrderRel φs[↑(φsΛ.fstFieldOfContract ⟨Finset.map uncontractedListEmd a, ⋯⟩)] φs[↑(φsΛ.sndFieldOfContract ⟨Finset.map uncontractedListEmd a, ⋯⟩)] → ¬timeOrderRel φs[↑(φsΛ.sndFieldOfContract ⟨Finset.map uncontractedListEmd a, ⋯⟩)] φs[↑(φsΛ.fstFieldOfContract ⟨Finset.map uncontractedListEmd a, ⋯⟩)]⊢ timeOrderRel φs[↑(φsΛ.fstFieldOfContract ⟨Finset.map uncontractedListEmd a, ⋯⟩)] φs[↑(φsΛ.sndFieldOfContract ⟨Finset.map uncontractedListEmd a, ⋯⟩)] → ¬timeOrderRel φs[↑(φsΛ.sndFieldOfContract ⟨Finset.map uncontractedListEmd a, ⋯⟩)] φs[↑(φsΛ.fstFieldOfContract ⟨Finset.map uncontractedListEmd a, ⋯⟩)] 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengtha:Finset (Fin [subContraction φsΛ.eqTimeContractSet ⋯]ᵘᶜ.length)ha✝:a ∈ ↑(quotContraction φsΛ.eqTimeContractSet ⋯)ha:Finset.map uncontractedListEmd a ∈ ↑φsΛhn':Finset.map uncontractedListEmd a ∈ ↑φsΛ → ∃ (h : Finset.map uncontractedListEmd a ∈ ↑φsΛ), timeOrderRel φs[↑(φsΛ.fstFieldOfContract ⟨Finset.map uncontractedListEmd a, ⋯⟩)] φs[↑(φsΛ.sndFieldOfContract ⟨Finset.map uncontractedListEmd a, ⋯⟩)] → ¬timeOrderRel φs[↑(φsΛ.sndFieldOfContract ⟨Finset.map uncontractedListEmd a, ⋯⟩)] φs[↑(φsΛ.fstFieldOfContract ⟨Finset.map uncontractedListEmd a, ⋯⟩)]h:Finset.map uncontractedListEmd a ∈ ↑φsΛh1:timeOrderRel φs[↑(φsΛ.fstFieldOfContract ⟨Finset.map uncontractedListEmd a, ⋯⟩)] φs[↑(φsΛ.sndFieldOfContract ⟨Finset.map uncontractedListEmd a, ⋯⟩)] → ¬timeOrderRel φs[↑(φsΛ.sndFieldOfContract ⟨Finset.map uncontractedListEmd a, ⋯⟩)] φs[↑(φsΛ.fstFieldOfContract ⟨Finset.map uncontractedListEmd a, ⋯⟩)]⊢ timeOrderRel φs[↑(φsΛ.fstFieldOfContract ⟨Finset.map uncontractedListEmd a, ⋯⟩)] φs[↑(φsΛ.sndFieldOfContract ⟨Finset.map uncontractedListEmd a, ⋯⟩)] → ¬timeOrderRel φs[↑(φsΛ.sndFieldOfContract ⟨Finset.map uncontractedListEmd a, ⋯⟩)] φs[↑(φsΛ.fstFieldOfContract ⟨Finset.map uncontractedListEmd a, ⋯⟩)] All goals completed! 🐙lemma join_haveEqTime_of_eqTimeOnly_nonEmpty {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) (h1 : φsΛ.EqTimeOnly) (h2 : φsΛ ≠ empty) (φsucΛ : WickContraction [φsΛ]ᵘᶜ.length) : HaveEqTime (join φsΛ φsucΛ) := 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthh1:φsΛ.EqTimeOnlyh2:φsΛ ≠ emptyφsucΛ:WickContraction [φsΛ]ᵘᶜ.length⊢ (φsΛ.join φsucΛ).HaveEqTime 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthh1:φsΛ.EqTimeOnlyh2:φsΛ ≠ emptyφsucΛ:WickContraction [φsΛ]ᵘᶜ.length⊢ ∃ i j, timeOrderRel φs[↑i] φs[↑j] ∧ ({i, j} ∈ ↑φsΛ ∨ ∃ a ∈ ↑φsucΛ, (Finset.mapEmbedding uncontractedListEmd) a = {i, j}) ∧ timeOrderRel φs[↑j] φs[↑i] 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthh1:∀ (i j : Fin φs.length), {i, j} ∈ ↑φsΛ → timeOrderRel φs[↑i] φs[↑j]h2:φsΛ ≠ emptyφsucΛ:WickContraction [φsΛ]ᵘᶜ.length⊢ ∃ i j, timeOrderRel φs[↑i] φs[↑j] ∧ ({i, j} ∈ ↑φsΛ ∨ ∃ a ∈ ↑φsucΛ, (Finset.mapEmbedding uncontractedListEmd) a = {i, j}) ∧ timeOrderRel φs[↑j] φs[↑i] 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthh1:∀ (i j : Fin φs.length), {i, j} ∈ ↑φsΛ → timeOrderRel φs[↑i] φs[↑j]h2:φsΛ ≠ emptyφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengthi:Fin φs.lengthj:Fin φs.lengthh:{i, j} ∈ ↑φsΛ⊢ ∃ i j, timeOrderRel φs[↑i] φs[↑j] ∧ ({i, j} ∈ ↑φsΛ ∨ ∃ a ∈ ↑φsucΛ, (Finset.mapEmbedding uncontractedListEmd) a = {i, j}) ∧ timeOrderRel φs[↑j] φs[↑i] 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthh1:∀ (i j : Fin φs.length), {i, j} ∈ ↑φsΛ → timeOrderRel φs[↑i] φs[↑j]h2:φsΛ ≠ emptyφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengthi:Fin φs.lengthj:Fin φs.lengthh:{i, j} ∈ ↑φsΛ⊢ timeOrderRel φs[↑i] φs[↑j] ∧ ({i, j} ∈ ↑φsΛ ∨ ∃ a ∈ ↑φsucΛ, (Finset.mapEmbedding uncontractedListEmd) a = {i, j}) ∧ timeOrderRel φs[↑j] φs[↑i] 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthh1:∀ (i j : Fin φs.length), {i, j} ∈ ↑φsΛ → timeOrderRel φs[↑i] φs[↑j]φsucΛ:WickContraction [φsΛ]ᵘᶜ.lengthi:Fin φs.lengthj:Fin φs.lengthh2:¬φsΛ = emptyh:{i, j} ∈ ↑φsΛ⊢ timeOrderRel φs[↑j] φs[↑i] exact h1 j i (𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthh1:∀ (i j : Fin φs.length), {i, j} ∈ ↑φsΛ → timeOrderRel φs[↑i] φs[↑j]φsucΛ:WickContraction [φsΛ]ᵘᶜ.lengthi:Fin φs.lengthj:Fin φs.lengthh2:¬φsΛ = emptyh:{i, j} ∈ ↑φsΛ⊢ {j, i} ∈ ↑φsΛ All goals completed! 🐙)lemma hasEqTimeEquiv_ext_sigma {φs : List 𝓕.FieldOp} {x1 x2 : Σ (φsΛ : {φsΛ : WickContraction φs.length // φsΛ.EqTimeOnly ∧ φsΛ ≠ empty}), {φssucΛ : WickContraction [φsΛ.1]ᵘᶜ.length // ¬ HaveEqTime φssucΛ}} (h1 : x1.1.1 = x2.1.1) (h2 : x1.2.1 = congr (𝓕:FieldSpecificationn:ℕc:WickContraction nφs:List 𝓕.FieldOpx1:(φsΛ : { φsΛ // φsΛ.EqTimeOnly ∧ φsΛ ≠ empty }) × { φssucΛ // ¬φssucΛ.HaveEqTime }x2:(φsΛ : { φsΛ // φsΛ.EqTimeOnly ∧ φsΛ ≠ empty }) × { φssucΛ // ¬φssucΛ.HaveEqTime }h1:↑x1.fst = ↑x2.fst⊢ [↑x2.fst]ᵘᶜ.length = [↑x1.fst]ᵘᶜ.length All goals completed! 🐙) x2.2.1) : x1 = x2 := 𝓕:FieldSpecificationφs:List 𝓕.FieldOpx1:(φsΛ : { φsΛ // φsΛ.EqTimeOnly ∧ φsΛ ≠ empty }) × { φssucΛ // ¬φssucΛ.HaveEqTime }x2:(φsΛ : { φsΛ // φsΛ.EqTimeOnly ∧ φsΛ ≠ empty }) × { φssucΛ // ¬φssucΛ.HaveEqTime }h1:↑x1.fst = ↑x2.fsth2:↑x1.snd = (congr ⋯) ↑x2.snd⊢ x1 = x2 𝓕:FieldSpecificationφs:List 𝓕.FieldOpx2:(φsΛ : { φsΛ // φsΛ.EqTimeOnly ∧ φsΛ ≠ empty }) × { φssucΛ // ¬φssucΛ.HaveEqTime }a1:WickContraction φs.lengthb1:a1.EqTimeOnly ∧ a1 ≠ emptyc1:WickContraction [↑⟨a1, b1⟩]ᵘᶜ.lengthd1:¬c1.HaveEqTimeh1:↑⟨⟨a1, b1⟩, ⟨c1, d1⟩⟩.fst = ↑x2.fsth2:↑⟨⟨a1, b1⟩, ⟨c1, d1⟩⟩.snd = (congr ⋯) ↑x2.snd⊢ ⟨⟨a1, b1⟩, ⟨c1, d1⟩⟩ = x2 𝓕:FieldSpecificationφs:List 𝓕.FieldOpa1:WickContraction φs.lengthb1:a1.EqTimeOnly ∧ a1 ≠ emptyc1:WickContraction [↑⟨a1, b1⟩]ᵘᶜ.lengthd1:¬c1.HaveEqTimeb2:{ φsΛ // φsΛ.EqTimeOnly ∧ φsΛ ≠ empty }h2✝:{ φssucΛ // ¬φssucΛ.HaveEqTime }h1:↑⟨⟨a1, b1⟩, ⟨c1, d1⟩⟩.fst = ↑⟨b2, h2✝⟩.fsth2:↑⟨⟨a1, b1⟩, ⟨c1, d1⟩⟩.snd = (congr ⋯) ↑⟨b2, h2✝⟩.snd⊢ ⟨⟨a1, b1⟩, ⟨c1, d1⟩⟩ = ⟨b2, h2✝⟩ 𝓕:FieldSpecificationφs:List 𝓕.FieldOpa1:WickContraction φs.lengthb1:a1.EqTimeOnly ∧ a1 ≠ emptyc1:WickContraction [↑⟨a1, b1⟩]ᵘᶜ.lengthd1:¬c1.HaveEqTimeb2:{ φsΛ // φsΛ.EqTimeOnly ∧ φsΛ ≠ empty }h2✝:{ φssucΛ // ¬φssucΛ.HaveEqTime }h1:a1 = ↑b2h2:↑⟨⟨a1, b1⟩, ⟨c1, d1⟩⟩.snd = (congr ⋯) ↑⟨b2, h2✝⟩.snd⊢ ⟨⟨a1, b1⟩, ⟨c1, d1⟩⟩ = ⟨b2, h2✝⟩ 𝓕:FieldSpecificationφs:List 𝓕.FieldOpb2:{ φsΛ // φsΛ.EqTimeOnly ∧ φsΛ ≠ empty }h2✝:{ φssucΛ // ¬φssucΛ.HaveEqTime }b1:(↑b2).EqTimeOnly ∧ ↑b2 ≠ emptyc1:WickContraction [↑⟨↑b2, b1⟩]ᵘᶜ.lengthd1:¬c1.HaveEqTimeh2:↑⟨⟨↑b2, b1⟩, ⟨c1, d1⟩⟩.snd = (congr ⋯) ↑⟨b2, h2✝⟩.snd⊢ ⟨⟨↑b2, b1⟩, ⟨c1, d1⟩⟩ = ⟨b2, h2✝⟩ 𝓕:FieldSpecificationφs:List 𝓕.FieldOpb2:{ φsΛ // φsΛ.EqTimeOnly ∧ φsΛ ≠ empty }h2✝:{ φssucΛ // ¬φssucΛ.HaveEqTime }b1:(↑b2).EqTimeOnly ∧ ↑b2 ≠ emptyc1:WickContraction [↑⟨↑b2, b1⟩]ᵘᶜ.lengthd1:¬c1.HaveEqTimeh2:c1 = ↑h2✝⊢ ⟨⟨↑b2, b1⟩, ⟨c1, d1⟩⟩ = ⟨b2, h2✝⟩ All goals completed! 🐙

The equivalence which separates a Wick contraction which has an equal time contraction into a non-empty contraction only between equal-time fields and a Wick contraction which does not have equal time contractions.

All goals completed! 🐙
𝓕:FieldSpecificationM:Type u_1φs:List 𝓕.FieldOpf:WickContraction φs.length → Minst✝:AddCommMonoid M⊢ ∑ i, f ↑((hasEqTimeEquiv φs).symm i) = ∑ φsΛ, ∑ φssucΛ, f ((↑φsΛ).join ↑φssucΛ) erw [𝓕:FieldSpecificationM:Type u_1φs:List 𝓕.FieldOpf:WickContraction φs.length → Minst✝:AddCommMonoid M⊢ ∑ a, ∑ s, f ↑((hasEqTimeEquiv φs).symm ⟨a, s⟩) = ∑ φsΛ, ∑ φssucΛ, f ((↑φsΛ).join ↑φssucΛ)𝓕:FieldSpecificationM:Type u_1φs:List 𝓕.FieldOpf:WickContraction φs.length → Minst✝:AddCommMonoid M⊢ ∑ a, ∑ s, f ↑((hasEqTimeEquiv φs).symm ⟨a, s⟩) = ∑ φsΛ, ∑ φssucΛ, f ((↑φsΛ).join ↑φssucΛ) All goals completed! 🐙