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 = itimeOrderRel φ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Λ)).cardtimeOrderRel φ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Λ)).cardtimeOrderRel φ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Λ)).cardtimeOrderRel φ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Λ)).cardtimeOrderRel φ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Λ).EqTimeOnlytimeOrder (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Λ).EqTimeOnlytimeOrder (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Λ.eqTimeContractSeta φ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Λ.eqTimeContractSetFalse 𝓕: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 < itimeOrderRel φ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.sndx1 = 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.snda1, 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✝.snda1, 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✝.snda1, 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✝.sndb2, 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! 🐙