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

Join of contractions

@[expose] public section

Given a list φs of 𝓕.FieldOp, a Wick contraction φsΛ of φs and a Wick contraction φsucΛ of [φsΛ]ᵘᶜ, join φsΛ φsucΛ is defined as the Wick contraction of φs consisting of the contractions in φsΛ and those in φsucΛ.

As an example, for φs = [φ1, φ2, φ3, φ4], φsΛ = {{0, 1}} corresponding to the contraction of φ1 and φ2 in φs and φsucΛ = {{0, 1}} corresponding to the contraction of φ3 and φ4 in [φsΛ]ᵘᶜ = [φ3, φ4], then join φsΛ φsucΛ is the contraction {{0, 1}, {2, 3}} of φs.

𝓕:FieldSpecificationn:c:WickContraction nφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:Finset (Fin [φsΛ]ᵘᶜ.length)ha:a φsucΛb:Finset (Fin [φsΛ]ᵘᶜ.length)hb:b φsucΛa = b Disjoint a b All goals completed! 🐙
lemma join_congr {φs : List 𝓕.FieldOp} {φsΛ : WickContraction φs.length} {φsucΛ : WickContraction [φsΛ]ᵘᶜ.length} {φsΛ' : WickContraction φs.length} (h1 : φsΛ = φsΛ') : join φsΛ φsucΛ = join φsΛ' (congr (𝓕:FieldSpecificationn:c:WickContraction nφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengthφsΛ':WickContraction φs.lengthh1:φsΛ = φsΛ'[φsΛ]ᵘᶜ.length = [φsΛ']ᵘᶜ.length All goals completed! 🐙) φsucΛ) := 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengthφsΛ':WickContraction φs.lengthh1:φsΛ = φsΛ'φsΛ.join φsucΛ = φsΛ'.join ((congr ) φsucΛ) 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengthφsΛ.join φsucΛ = φsΛ.join ((congr ) φsucΛ) All goals completed! 🐙

Given a contracting pair within φsΛ the corresponding contracting pair within (join φsΛ φsucΛ).

def joinLiftLeft {φs : List 𝓕.FieldOp} {φsΛ : WickContraction φs.length} {φsucΛ : WickContraction [φsΛ]ᵘᶜ.length} : φsΛ.1 (join φsΛ φsucΛ).1 := fun a => a, 𝓕:FieldSpecificationn:c:WickContraction nφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:φsΛa (φsΛ.join φsucΛ) All goals completed! 🐙
lemma jointLiftLeft_injective {φs : List 𝓕.FieldOp} {φsΛ : WickContraction φs.length} {φsucΛ : WickContraction [φsΛ]ᵘᶜ.length} : Function.Injective (@joinLiftLeft _ _ φsΛ φsucΛ) := 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengthFunction.Injective joinLiftLeft 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:φsΛb:φsΛh:joinLiftLeft a = joinLiftLeft ba = b 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:φsΛb:φsΛh:a = ba = b All goals completed! 🐙

Given a contracting pair within φsucΛ the corresponding contracting pair within (join φsΛ φsucΛ).

def joinLiftRight {φs : List 𝓕.FieldOp} {φsΛ : WickContraction φs.length} {φsucΛ : WickContraction [φsΛ]ᵘᶜ.length} : φsucΛ.1 (join φsΛ φsucΛ).1 := fun a => a.1.map uncontractedListEmd, 𝓕:FieldSpecificationn:c:WickContraction nφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:φsucΛFinset.map uncontractedListEmd a (φsΛ.join φsucΛ) 𝓕:FieldSpecificationn:c:WickContraction nφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:φsucΛFinset.map uncontractedListEmd a φsΛ a_1 φsucΛ, (Finset.mapEmbedding uncontractedListEmd) a_1 = Finset.map uncontractedListEmd a 𝓕:FieldSpecificationn:c:WickContraction nφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:φsucΛ a_1 φsucΛ, (Finset.mapEmbedding uncontractedListEmd) a_1 = Finset.map uncontractedListEmd a 𝓕:FieldSpecificationn:c:WickContraction nφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:φsucΛa φsucΛ (Finset.mapEmbedding uncontractedListEmd) a = Finset.map uncontractedListEmd a 𝓕:FieldSpecificationn:c:WickContraction nφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:φsucΛ(Finset.mapEmbedding uncontractedListEmd) a = Finset.map uncontractedListEmd a All goals completed! 🐙
lemma joinLiftRight_injective {φs : List 𝓕.FieldOp} {φsΛ : WickContraction φs.length} {φsucΛ : WickContraction [φsΛ]ᵘᶜ.length} : Function.Injective (@joinLiftRight _ _ φsΛ φsucΛ) := 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengthFunction.Injective joinLiftRight 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:φsucΛb:φsucΛh:joinLiftRight a = joinLiftRight ba = b 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:φsucΛb:φsucΛh:a = ba = b All goals completed! 🐙lemma jointLiftLeft_disjoint_joinLiftRight {φs : List 𝓕.FieldOp} {φsΛ : WickContraction φs.length} {φsucΛ : WickContraction [φsΛ]ᵘᶜ.length} (a : φsΛ.1) (b : φsucΛ.1) : Disjoint (@joinLiftLeft _ _ _ φsucΛ a).1 (joinLiftRight b).1 := (uncontractedListEmd_finset_disjoint_left b.1 a.1 a.2).symm𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:φsΛb:φsucΛhn:joinLiftLeft a = joinLiftRight bh1:(joinLiftRight b) = False 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:φsΛb:φsucΛhn:joinLiftLeft a = joinLiftRight bh1:(joinLiftRight b) = hj:(↑(joinLiftRight b)).card = 2False All goals completed! 🐙

The map from contracted pairs of φsΛ and φsucΛ to contracted pairs in (join φsΛ φsucΛ).

def joinLift {φs : List 𝓕.FieldOp} {φsΛ : WickContraction φs.length} {φsucΛ : WickContraction [φsΛ]ᵘᶜ.length} : φsΛ.1 φsucΛ.1 (join φsΛ φsucΛ).1 := fun a => match a with | Sum.inl a => joinLiftLeft a | Sum.inr a => joinLiftRight a
lemma joinLift_injective {φs : List 𝓕.FieldOp} {φsΛ : WickContraction φs.length} {φsucΛ : WickContraction [φsΛ]ᵘᶜ.length} : Function.Injective (@joinLift _ _ φsΛ φsucΛ) := 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengthFunction.Injective joinLift 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:φsΛ φsucΛb:φsΛ φsucΛh:joinLift a = joinLift ba = b match a, b with 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha✝:φsΛ φsucΛb✝:φsΛ φsucΛa:φsΛb:φsΛh:joinLift (Sum.inl a) = joinLift (Sum.inl b)Sum.inl a = Sum.inl b All goals completed! 🐙 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha✝:φsΛ φsucΛb✝:φsΛ φsucΛa:φsucΛb:φsucΛh:joinLift (Sum.inr a) = joinLift (Sum.inr b)Sum.inr a = Sum.inr b All goals completed! 🐙 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha✝:φsΛ φsucΛb✝:φsΛ φsucΛa:φsΛb:φsucΛh:joinLift (Sum.inl a) = joinLift (Sum.inr b)Sum.inl a = Sum.inr b All goals completed! 🐙 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha✝:φsΛ φsucΛb✝:φsΛ φsucΛa:φsucΛb:φsΛh:joinLift (Sum.inr a) = joinLift (Sum.inl b)Sum.inr a = Sum.inl b All goals completed! 🐙𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:(φsΛ.join φsucΛ)a2:Finset (Fin [φsΛ]ᵘᶜ.length)ha3:a2 φsucΛ Finset.map uncontractedListEmd a2 = a a_1, joinLift a_1 = a 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:(φsΛ.join φsucΛ)a2:Finset (Fin [φsΛ]ᵘᶜ.length)ha3:a2 φsucΛ Finset.map uncontractedListEmd a2 = ajoinLift (Sum.inr a2, ) = a 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:(φsΛ.join φsucΛ)a2:Finset (Fin [φsΛ]ᵘᶜ.length)ha3:a2 φsucΛ Finset.map uncontractedListEmd a2 = aFinset.map uncontractedListEmd a2, = a 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:(φsΛ.join φsucΛ)a2:Finset (Fin [φsΛ]ᵘᶜ.length)ha3:a2 φsucΛ Finset.map uncontractedListEmd a2 = aFinset.map uncontractedListEmd a2, = a All goals completed! 🐙lemma joinLift_bijective {φs : List 𝓕.FieldOp} {φsΛ : WickContraction φs.length} {φsucΛ : WickContraction [φsΛ]ᵘᶜ.length} : Function.Bijective (@joinLift _ _ φsΛ φsucΛ) := joinLift_injective, joinLift_surjective𝓕:FieldSpecificationM:Type u_1φs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengthf:(φsΛ.join φsucΛ) Minst✝:CommMonoid M i, f ((Equiv.ofBijective joinLift ) i) = (∏ a, f (joinLiftLeft a)) * a, f (joinLiftRight a) 𝓕:FieldSpecificationM:Type u_1φs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengthf:(φsΛ.join φsucΛ) Minst✝:CommMonoid M(∏ a₁ (↑φsΛ).attach, f ((Equiv.ofBijective joinLift ) (Sum.inl a₁))) * a₂ (↑φsucΛ).attach, f ((Equiv.ofBijective joinLift ) (Sum.inr a₂)) = (∏ a (↑φsΛ).attach, f (joinLiftLeft a)) * a (↑φsucΛ).attach, f (joinLiftRight a) All goals completed! 🐙lemma joinLiftLeft_or_joinLiftRight_of_mem_join {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) (φsucΛ : WickContraction [φsΛ]ᵘᶜ.length) {a : Finset (Fin φs.length)} (ha : a (join φsΛ φsucΛ).1) : ( b, a = (joinLiftLeft (φsucΛ := φsucΛ) b).1) ( b, a = (joinLiftRight (φsucΛ := φsucΛ) b).1) := 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:Finset (Fin φs.length)ha:a (φsΛ.join φsucΛ)(∃ b, a = (joinLiftLeft b)) b, a = (joinLiftRight b) 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:Finset (Fin φs.length)ha:a φsΛ a_1 φsucΛ, (Finset.mapEmbedding uncontractedListEmd) a_1 = a(∃ b, a = (joinLiftLeft b)) b, a = (joinLiftRight b) 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:Finset (Fin φs.length)ha:a φsΛ(∃ b, a = (joinLiftLeft b)) b, a = (joinLiftRight b)𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:Finset (Fin [φsΛ]ᵘᶜ.length)ha:a φsucΛ(∃ b, (Finset.mapEmbedding uncontractedListEmd) a = (joinLiftLeft b)) b, (Finset.mapEmbedding uncontractedListEmd) a = (joinLiftRight b) 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:Finset (Fin φs.length)ha:a φsΛ(∃ b, a = (joinLiftLeft b)) b, a = (joinLiftRight b) All goals completed! 🐙 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:Finset (Fin [φsΛ]ᵘᶜ.length)ha:a φsucΛ(∃ b, (Finset.mapEmbedding uncontractedListEmd) a = (joinLiftLeft b)) b, (Finset.mapEmbedding uncontractedListEmd) a = (joinLiftRight b) All goals completed! 🐙@[simp] lemma join_fstFieldOfContract_joinLiftRight {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) (φsucΛ : WickContraction [φsΛ]ᵘᶜ.length) (a : φsucΛ.1) : (join φsΛ φsucΛ).fstFieldOfContract (joinLiftRight a) = uncontractedListEmd (φsucΛ.fstFieldOfContract a) := 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:φsucΛ(φsΛ.join φsucΛ).fstFieldOfContract (joinLiftRight a) = uncontractedListEmd (φsucΛ.fstFieldOfContract a) 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:φsucΛuncontractedListEmd (φsucΛ.fstFieldOfContract a) (joinLiftRight a)𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:φsucΛuncontractedListEmd (φsucΛ.sndFieldOfContract a) (joinLiftRight a)𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:φsucΛuncontractedListEmd (φsucΛ.fstFieldOfContract a) < uncontractedListEmd (φsucΛ.sndFieldOfContract a) 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:φsucΛuncontractedListEmd (φsucΛ.fstFieldOfContract a) (joinLiftRight a) All goals completed! 🐙 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:φsucΛuncontractedListEmd (φsucΛ.sndFieldOfContract a) (joinLiftRight a) All goals completed! 🐙 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:φsucΛuncontractedListEmd (φsucΛ.fstFieldOfContract a) < uncontractedListEmd (φsucΛ.sndFieldOfContract a) 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:φsucΛφsucΛ.fstFieldOfContract a < φsucΛ.sndFieldOfContract a All goals completed! 🐙@[simp] lemma join_sndFieldOfContract_joinLiftRight {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) (φsucΛ : WickContraction [φsΛ]ᵘᶜ.length) (a : φsucΛ.1) : (join φsΛ φsucΛ).sndFieldOfContract (joinLiftRight a) = uncontractedListEmd (φsucΛ.sndFieldOfContract a) := 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:φsucΛ(φsΛ.join φsucΛ).sndFieldOfContract (joinLiftRight a) = uncontractedListEmd (φsucΛ.sndFieldOfContract a) 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:φsucΛuncontractedListEmd (φsucΛ.fstFieldOfContract a) (joinLiftRight a)𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:φsucΛuncontractedListEmd (φsucΛ.sndFieldOfContract a) (joinLiftRight a)𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:φsucΛuncontractedListEmd (φsucΛ.fstFieldOfContract a) < uncontractedListEmd (φsucΛ.sndFieldOfContract a) 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:φsucΛuncontractedListEmd (φsucΛ.fstFieldOfContract a) (joinLiftRight a) All goals completed! 🐙 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:φsucΛuncontractedListEmd (φsucΛ.sndFieldOfContract a) (joinLiftRight a) All goals completed! 🐙 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:φsucΛuncontractedListEmd (φsucΛ.fstFieldOfContract a) < uncontractedListEmd (φsucΛ.sndFieldOfContract a) 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:φsucΛφsucΛ.fstFieldOfContract a < φsucΛ.sndFieldOfContract a All goals completed! 🐙@[simp] lemma join_fstFieldOfContract_joinLiftLeft {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) (φsucΛ : WickContraction [φsΛ]ᵘᶜ.length) (a : φsΛ.1) : (join φsΛ φsucΛ).fstFieldOfContract (joinLiftLeft a) = (φsΛ.fstFieldOfContract a) := 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:φsΛ(φsΛ.join φsucΛ).fstFieldOfContract (joinLiftLeft a) = φsΛ.fstFieldOfContract a 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:φsΛφsΛ.fstFieldOfContract a (joinLiftLeft a)𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:φsΛφsΛ.sndFieldOfContract a (joinLiftLeft a)𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:φsΛφsΛ.fstFieldOfContract a < φsΛ.sndFieldOfContract a 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:φsΛφsΛ.fstFieldOfContract a (joinLiftLeft a) All goals completed! 🐙 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:φsΛφsΛ.sndFieldOfContract a (joinLiftLeft a) All goals completed! 🐙 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:φsΛφsΛ.fstFieldOfContract a < φsΛ.sndFieldOfContract a All goals completed! 🐙@[simp] lemma join_sndFieldOfContract_joinLift {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) (φsucΛ : WickContraction [φsΛ]ᵘᶜ.length) (a : φsΛ.1) : (join φsΛ φsucΛ).sndFieldOfContract (joinLiftLeft a) = (φsΛ.sndFieldOfContract a) := 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:φsΛ(φsΛ.join φsucΛ).sndFieldOfContract (joinLiftLeft a) = φsΛ.sndFieldOfContract a 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:φsΛφsΛ.fstFieldOfContract a (joinLiftLeft a)𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:φsΛφsΛ.sndFieldOfContract a (joinLiftLeft a)𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:φsΛφsΛ.fstFieldOfContract a < φsΛ.sndFieldOfContract a 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:φsΛφsΛ.fstFieldOfContract a (joinLiftLeft a) All goals completed! 🐙 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:φsΛφsΛ.sndFieldOfContract a (joinLiftLeft a) All goals completed! 🐙 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:φsΛφsΛ.fstFieldOfContract a < φsΛ.sndFieldOfContract a All goals completed! 🐙𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha✝:Finset (Fin [φsΛ]ᵘᶜ.length)h1':Finset.map uncontractedListEmd a φsΛa:Finset (Fin [φsΛ]ᵘᶜ.length)ha:a φsucΛh2:a = a✝a φsucΛ All goals completed! 🐙𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:Finset (Fin φs.length)ha:a φsΛx:Finset (Fin [φsΛ]ᵘᶜ.length)hx:x φsucΛhn:Finset.map uncontractedListEmd x = ahdis:Disjoint a aFalse 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:Finset (Fin φs.length)ha:a φsΛx:Finset (Fin [φsΛ]ᵘᶜ.length)hx:x φsucΛhn:Finset.map uncontractedListEmd x = ahdis:Disjoint a ahcard:a.card = 2False All goals completed! 🐙𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction [empty]ᵘᶜ.lengtha:Finset (Fin φs.length)h:Finset.map (finCongr ).toEmbedding a φsΛFinset.map ((finCongr ).toEmbedding.trans (finCongr ).toEmbedding) a = a All goals completed! 🐙@[simp] lemma join_empty {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) : join φsΛ empty = φsΛ := 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsΛ.join empty = φsΛ 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.length(φsΛ.join empty) = φsΛ 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengtha:Finset (Fin φs.length)a (φsΛ.join empty) a φsΛ All goals completed! 🐙𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.length(∏ a, WickAlgebra.timeContract φs[((φsΛ.join φsucΛ).fstFieldOfContract (joinLiftLeft a))] φs[((φsΛ.join φsucΛ).sndFieldOfContract (joinLiftLeft a))], ) * a, WickAlgebra.timeContract φs[((φsΛ.join φsucΛ).fstFieldOfContract (joinLiftRight a))] φs[((φsΛ.join φsucΛ).sndFieldOfContract (joinLiftRight a))], = (∏ x, WickAlgebra.timeContract φs[(φsΛ.fstFieldOfContract x)] φs[(φsΛ.sndFieldOfContract x)], ) * x, WickAlgebra.timeContract [φsΛ]ᵘᶜ[(φsucΛ.fstFieldOfContract x)] [φsΛ]ᵘᶜ[(φsucΛ.sndFieldOfContract x)], 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.length a, WickAlgebra.timeContract φs[((φsΛ.join φsucΛ).fstFieldOfContract (joinLiftRight a))] φs[((φsΛ.join φsucΛ).sndFieldOfContract (joinLiftRight a))], = x, WickAlgebra.timeContract [φsΛ]ᵘᶜ[(φsucΛ.fstFieldOfContract x)] [φsΛ]ᵘᶜ[(φsucΛ.sndFieldOfContract x)], exact Finset.prod_congr rfl fun a _ => 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:φsucΛx✝:a Finset.univWickAlgebra.timeContract φs[((φsΛ.join φsucΛ).fstFieldOfContract (joinLiftRight a))] φs[((φsΛ.join φsucΛ).sndFieldOfContract (joinLiftRight a))], = WickAlgebra.timeContract [φsΛ]ᵘᶜ[(φsucΛ.fstFieldOfContract a)] [φsΛ]ᵘᶜ[(φsucΛ.sndFieldOfContract a)], All goals completed! 🐙𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.length(∏ a, (superCommute (anPart φs[((φsΛ.join φsucΛ).fstFieldOfContract (joinLiftLeft a))])) (ofFieldOp φs[((φsΛ.join φsucΛ).sndFieldOfContract (joinLiftLeft a))]), ) * a, (superCommute (anPart φs[((φsΛ.join φsucΛ).fstFieldOfContract (joinLiftRight a))])) (ofFieldOp φs[((φsΛ.join φsucΛ).sndFieldOfContract (joinLiftRight a))]), = (∏ x, (superCommute (anPart φs[(φsΛ.fstFieldOfContract x)])) (ofFieldOp φs[(φsΛ.sndFieldOfContract x)]), ) * x, (superCommute (anPart [φsΛ]ᵘᶜ[(φsucΛ.fstFieldOfContract x)])) (ofFieldOp [φsΛ]ᵘᶜ[(φsucΛ.sndFieldOfContract x)]), 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.length a, (superCommute (anPart φs[((φsΛ.join φsucΛ).fstFieldOfContract (joinLiftRight a))])) (ofFieldOp φs[((φsΛ.join φsucΛ).sndFieldOfContract (joinLiftRight a))]), = x, (superCommute (anPart [φsΛ]ᵘᶜ[(φsucΛ.fstFieldOfContract x)])) (ofFieldOp [φsΛ]ᵘᶜ[(φsucΛ.sndFieldOfContract x)]), exact Finset.prod_congr rfl fun a _ => 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:φsucΛx✝:a Finset.univ(superCommute (anPart φs[((φsΛ.join φsucΛ).fstFieldOfContract (joinLiftRight a))])) (ofFieldOp φs[((φsΛ.join φsucΛ).sndFieldOfContract (joinLiftRight a))]), = (superCommute (anPart [φsΛ]ᵘᶜ[(φsucΛ.fstFieldOfContract a)])) (ofFieldOp [φsΛ]ᵘᶜ[(φsucΛ.sndFieldOfContract a)]), All goals completed! 🐙𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengthi:Fin [φsΛ]ᵘᶜ.lengthha: p φsucΛ, i pp:Finset (Fin [φsΛ]ᵘᶜ.length)hp:p φsucΛi p All goals completed! 🐙𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengthi:Fin φs.lengthha: p (φsΛ.join φsucΛ), i p p φsΛ, i p 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengthi:Fin φs.lengthha: (p : Finset (Fin φs.length)), (p φsΛ a φsucΛ, (Finset.mapEmbedding uncontractedListEmd) a = p) i p p φsΛ, i p 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengthi:Fin φs.lengthha: (p : Finset (Fin φs.length)), (p φsΛ a φsucΛ, (Finset.mapEmbedding uncontractedListEmd) a = p) i pp:Finset (Fin φs.length)hp:p φsΛi p All goals completed! 🐙𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengthj:Fin [φsΛ]ᵘᶜ.lengthhi: p (φsΛ.join φsucΛ), uncontractedListEmd j phi':uncontractedListEmd j φsΛ.uncontractedp:Finset (Fin [φsΛ]ᵘᶜ.length)hp:p φsucΛhip:uncontractedListEmd j Finset.map uncontractedListEmd pj p All goals completed! 🐙𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.length((φsΛ.join φsucΛ).uncontracted.sort fun x1 x2 => x1 x2) = (Finset.map uncontractedListEmd φsucΛ.uncontracted).sort fun x1 x2 => x1 x2𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengthStrictMono uncontractedListEmd 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.length(φsΛ.join φsucΛ).uncontracted = Finset.map uncontractedListEmd φsucΛ.uncontracted𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengthStrictMono uncontractedListEmd 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:Fin φs.lengtha (φsΛ.join φsucΛ).uncontracted a Finset.map uncontractedListEmd φsucΛ.uncontracted𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengthStrictMono uncontractedListEmd 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:Fin φs.lengtha (φsΛ.join φsucΛ).uncontracted a_1 φsucΛ.uncontracted, uncontractedListEmd a_1 = a𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengthStrictMono uncontractedListEmd 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:Fin φs.lengtha (φsΛ.join φsucΛ).uncontracted a_2 φsucΛ.uncontracted, uncontractedListEmd a_2 = a𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:Fin φs.length(∃ a_1 φsucΛ.uncontracted, uncontractedListEmd a_1 = a) a (φsΛ.join φsucΛ).uncontracted𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengthStrictMono uncontractedListEmd 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:Fin φs.lengtha (φsΛ.join φsucΛ).uncontracted a_2 φsucΛ.uncontracted, uncontractedListEmd a_2 = a 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:Fin φs.lengthh:a (φsΛ.join φsucΛ).uncontracted a_1 φsucΛ.uncontracted, uncontractedListEmd a_1 = a 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:Fin [φsΛ]ᵘᶜ.lengthha:a φsucΛ.uncontractedh:uncontractedListEmd a (φsΛ.join φsucΛ).uncontracted a_1 φsucΛ.uncontracted, uncontractedListEmd a_1 = uncontractedListEmd a All goals completed! 🐙 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:Fin φs.length(∃ a_1 φsucΛ.uncontracted, uncontractedListEmd a_1 = a) a (φsΛ.join φsucΛ).uncontracted 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:Fin φs.lengthh: a_1 φsucΛ.uncontracted, uncontractedListEmd a_1 = aa (φsΛ.join φsucΛ).uncontracted 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:Fin [φsΛ]ᵘᶜ.lengthha:a φsucΛ.uncontracteduncontractedListEmd a (φsΛ.join φsucΛ).uncontracted All goals completed! 🐙 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengthStrictMono uncontractedListEmd 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:Fin [φsΛ]ᵘᶜ.lengthb:Fin [φsΛ]ᵘᶜ.lengthh:a < buncontractedListEmd a < uncontractedListEmd b All goals completed! 🐙𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengthh1: {n : } (l1 l2 : List (Fin n)) (h : l1 = l2), l1.get = l2.get Fin.cast (φsΛ.join φsucΛ).uncontractedList.get = uncontractedListEmd φsucΛ.uncontractedList.get Fin.cast conv_lhs => 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengthh1: {n : } (l1 l2 : List (Fin n)) (h : l1 = l2), l1.get = l2.get Fin.cast | (List.map (⇑uncontractedListEmd) φsucΛ.uncontractedList).get Fin.cast 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengthh1: {n : } (l1 l2 : List (Fin n)) (h : l1 = l2), l1.get = l2.get Fin.cast i:Fin (φsΛ.join φsucΛ).uncontractedList.length(((List.map (⇑uncontractedListEmd) φsucΛ.uncontractedList).get Fin.cast ) i) = ((uncontractedListEmd φsucΛ.uncontractedList.get Fin.cast ) i) All goals completed! 🐙lemma join_uncontractedListGet {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) (φsucΛ : WickContraction [φsΛ]ᵘᶜ.length) : (join φsΛ φsucΛ).uncontractedListGet = φsucΛ.uncontractedListGet := 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.length[φsΛ.join φsucΛ]ᵘᶜ = [φsucΛ]ᵘᶜ 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.length a φsucΛ.uncontractedList, φs[(uncontractedListEmd a)] = φs[φsΛ.uncontractedList[a]] 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:Fin (List.map φs.get φsΛ.uncontractedList).lengthha:a φsucΛ.uncontractedListφs[(uncontractedListEmd a)] = φs[φsΛ.uncontractedList[a]] 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:Fin (List.map φs.get φsΛ.uncontractedList).lengthha:a φsucΛ.uncontractedListφs[((((finCongr ).toEmbedding.trans { toFun := fun i => φsΛ.uncontractedList[i], , invFun := fun i => List.idxOf (↑i) φsΛ.uncontractedList, , left_inv := , right_inv := }.toEmbedding).trans (Function.Embedding.subtype fun x => x φsΛ.uncontracted)) a)] = φs[φsΛ.uncontractedList[a]] All goals completed! 🐙𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.length(uncontractedListEmd φsucΛ.uncontractedList.get Fin.cast ) (finCongr ) = (((finCongr ).toEmbedding.trans uncontractedListEmd).trans uncontractedListEmd) All goals completed! 🐙𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengthφsucΛ':WickContraction [φsΛ.join φsucΛ]ᵘᶜ.lengtha:Finset (Fin [φsucΛ]ᵘᶜ.length)ha':a ((congr ) φsucΛ')ha:(Finset.mapEmbedding uncontractedListEmd) ((Finset.mapEmbedding uncontractedListEmd) a) φsΛa':φsucΛ' := congrLiftInv a, ha'Finset.map ((finCongr ).toEmbedding.trans (finCongr ).toEmbedding) a = a 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengthφsucΛ':WickContraction [φsΛ.join φsucΛ]ᵘᶜ.lengtha:Finset (Fin [φsucΛ]ᵘᶜ.length)ha':a ((congr ) φsucΛ')ha:(Finset.mapEmbedding uncontractedListEmd) ((Finset.mapEmbedding uncontractedListEmd) a) φsΛa':φsucΛ' := congrLiftInv a, ha'Finset.map (Equiv.refl (Fin [φsucΛ]ᵘᶜ.length)).toEmbedding a = a All goals completed! 🐙𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengthi:Fin [φsΛ]ᵘᶜ.lengthuncontractedListEmd i (φsΛ.join φsucΛ).uncontracted i φsucΛ.uncontracted 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengthi:Fin [φsΛ]ᵘᶜ.lengthuncontractedListEmd i (φsΛ.join φsucΛ).uncontracted i φsucΛ.uncontracted𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengthi:Fin [φsΛ]ᵘᶜ.lengthi φsucΛ.uncontracted uncontractedListEmd i (φsΛ.join φsucΛ).uncontracted 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengthi:Fin [φsΛ]ᵘᶜ.lengthuncontractedListEmd i (φsΛ.join φsucΛ).uncontracted i φsucΛ.uncontracted 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengthi:Fin [φsΛ]ᵘᶜ.lengthh:uncontractedListEmd i (φsΛ.join φsucΛ).uncontractedi φsucΛ.uncontracted 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengthi:Fin [φsΛ]ᵘᶜ.lengthh:uncontractedListEmd i (φsΛ.join φsucΛ).uncontracteda:Fin [φsΛ]ᵘᶜ.lengthha':uncontractedListEmd a = uncontractedListEmd iha:a φsucΛ.uncontractedi φsucΛ.uncontracted 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengthi:Fin [φsΛ]ᵘᶜ.lengthh:uncontractedListEmd i (φsΛ.join φsucΛ).uncontracteda:Fin [φsΛ]ᵘᶜ.lengthha:a φsucΛ.uncontractedha':a = ii φsucΛ.uncontracted All goals completed! 🐙 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengthi:Fin [φsΛ]ᵘᶜ.lengthi φsucΛ.uncontracted uncontractedListEmd i (φsΛ.join φsucΛ).uncontracted 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengthi:Fin [φsΛ]ᵘᶜ.lengthh:i φsucΛ.uncontracteduncontractedListEmd i (φsΛ.join φsucΛ).uncontracted All goals completed! 🐙𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengthi:Fin [φsΛ]ᵘᶜ.length¬((φsΛ.join φsucΛ).getDual? (uncontractedListEmd i)).isSome = true ¬(φsucΛ.getDual? i).isSome = true All goals completed! 🐙𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengthi:Fin [φsΛ]ᵘᶜ.lengthhi:((φsΛ.join φsucΛ).getDual? (uncontractedListEmd i)).isSome = trueFinset.map uncontractedListEmd {i, (φsucΛ.getDual? i).get } = {uncontractedListEmd i, uncontractedListEmd ((φsucΛ.getDual? i).get )} All goals completed! 🐙𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengthi:Fin [φsΛ]ᵘᶜ.lengthh:(φsucΛ.getDual? i).isSome = truesome (uncontractedListEmd ((φsucΛ.getDual? i).get )) = Option.map (⇑uncontractedListEmd) (φsucΛ.getDual? i)𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengthi:Fin [φsΛ]ᵘᶜ.lengthh:(φsucΛ.getDual? i).isSome = true((φsΛ.join φsucΛ).getDual? (uncontractedListEmd i)).isSome = true conv_rhs => 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengthi:Fin [φsΛ]ᵘᶜ.lengthh:(φsucΛ.getDual? i).isSome = true| Option.map (⇑uncontractedListEmd) (some ((φsucΛ.getDual? i).get h)) 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengthi:Fin [φsΛ]ᵘᶜ.lengthh:(φsucΛ.getDual? i).isSome = true((φsΛ.join φsucΛ).getDual? (uncontractedListEmd i)).isSome = true All goals completed! 🐙 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengthi:Fin [φsΛ]ᵘᶜ.lengthh:¬(φsucΛ.getDual? i).isSome = true(φsΛ.join φsucΛ).getDual? (uncontractedListEmd i) = Option.map (⇑uncontractedListEmd) (φsucΛ.getDual? i) 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengthi:Fin [φsΛ]ᵘᶜ.lengthh:φsucΛ.getDual? i = none(φsΛ.join φsucΛ).getDual? (uncontractedListEmd i) = Option.map (⇑uncontractedListEmd) (φsucΛ.getDual? i) All goals completed! 🐙

Subcontractions and quotient contractions

lemma join_sub_quot (S : Finset (Finset (Fin φs.length))) (ha : S φsΛ.1) : join (subContraction S ha) (quotContraction S ha) = φsΛ := 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))ha:S φsΛ(subContraction S ha).join (quotContraction S ha) = φsΛ 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))ha:S φsΛ((subContraction S ha).join (quotContraction S ha)) = φsΛ 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))ha:S φsΛa:Finset (Fin φs.length)a ((subContraction S ha).join (quotContraction S ha)) a φsΛ 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))ha:S φsΛa:Finset (Fin φs.length)(a (subContraction S ha) a_1 (quotContraction S ha), (Finset.mapEmbedding uncontractedListEmd) a_1 = a) a φsΛ 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))ha:S φsΛa:Finset (Fin φs.length)(a (subContraction S ha) a_1 (quotContraction S ha), (Finset.mapEmbedding uncontractedListEmd) a_1 = a) a φsΛ𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))ha:S φsΛa:Finset (Fin φs.length)a φsΛ a (subContraction S ha) a_2 (quotContraction S ha), (Finset.mapEmbedding uncontractedListEmd) a_2 = a 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))ha:S φsΛa:Finset (Fin φs.length)(a (subContraction S ha) a_1 (quotContraction S ha), (Finset.mapEmbedding uncontractedListEmd) a_1 = a) a φsΛ 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))ha:S φsΛa:Finset (Fin φs.length)h:a (subContraction S ha) a_1 (quotContraction S ha), (Finset.mapEmbedding uncontractedListEmd) a_1 = aa φsΛ 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))ha:S φsΛa:Finset (Fin φs.length)h:a (subContraction S ha)a φsΛ𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))ha:S φsΛa:Finset (Fin φs.length)h: a_1 (quotContraction S ha), (Finset.mapEmbedding uncontractedListEmd) a_1 = aa φsΛ 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))ha:S φsΛa:Finset (Fin φs.length)h:a (subContraction S ha)a φsΛ All goals completed! 🐙 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))ha:S φsΛa:Finset (Fin φs.length)h: a_1 (quotContraction S ha), (Finset.mapEmbedding uncontractedListEmd) a_1 = aa φsΛ 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))ha✝:S φsΛa:Finset (Fin [subContraction S ha✝]ᵘᶜ.length)ha:a (quotContraction S ha✝)(Finset.mapEmbedding uncontractedListEmd) a φsΛ All goals completed! 🐙 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))ha:S φsΛa:Finset (Fin φs.length)a φsΛ a (subContraction S ha) a_2 (quotContraction S ha), (Finset.mapEmbedding uncontractedListEmd) a_2 = a 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))ha:S φsΛa:Finset (Fin φs.length)h:a φsΛa (subContraction S ha) a_1 (quotContraction S ha), (Finset.mapEmbedding uncontractedListEmd) a_1 = a 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))ha:S φsΛa:Finset (Fin φs.length)h:a φsΛh1:a (subContraction S ha) a', Finset.map uncontractedListEmd a' = a a' (quotContraction S ha)a (subContraction S ha) a_1 (quotContraction S ha), (Finset.mapEmbedding uncontractedListEmd) a_1 = a 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))ha:S φsΛa:Finset (Fin φs.length)h:a φsΛh1:a (subContraction S ha)a (subContraction S ha) a_1 (quotContraction S ha), (Finset.mapEmbedding uncontractedListEmd) a_1 = a𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))ha:S φsΛa:Finset (Fin φs.length)h:a φsΛh1: a', Finset.map uncontractedListEmd a' = a a' (quotContraction S ha)a (subContraction S ha) a_1 (quotContraction S ha), (Finset.mapEmbedding uncontractedListEmd) a_1 = a 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))ha:S φsΛa:Finset (Fin φs.length)h:a φsΛh1:a (subContraction S ha)a (subContraction S ha) a_1 (quotContraction S ha), (Finset.mapEmbedding uncontractedListEmd) a_1 = a All goals completed! 🐙 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))ha:S φsΛa:Finset (Fin φs.length)h:a φsΛh1: a', Finset.map uncontractedListEmd a' = a a' (quotContraction S ha)a (subContraction S ha) a_1 (quotContraction S ha), (Finset.mapEmbedding uncontractedListEmd) a_1 = a 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))ha:S φsΛa:Finset (Fin φs.length)h:a φsΛh1: a', Finset.map uncontractedListEmd a' = a a' (quotContraction S ha) a_1 (quotContraction S ha), (Finset.mapEmbedding uncontractedListEmd) a_1 = a 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))ha✝:S φsΛa:Finset (Fin [subContraction S ha✝]ᵘᶜ.length)ha:a (quotContraction S ha✝)h:Finset.map uncontractedListEmd a φsΛ a_1 (quotContraction S ha✝), (Finset.mapEmbedding uncontractedListEmd) a_1 = Finset.map uncontractedListEmd a All goals completed! 🐙𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthS:Finset (Finset (Fin φs.length))ha:S φsΛ(↑((subContraction S ha).join (quotContraction S ha))).card = (↑φsΛ).card All goals completed! 🐙𝓕:FieldSpecificationφs:List 𝓕.FieldOpi:Fin φs.lengthj:Fin φs.lengthh:i < jφsucΛ:WickContraction [singleton h]ᵘᶜ.length{i, j} ((singleton h).join φsucΛ) All goals completed! 🐙𝓕:FieldSpecificationφs:List 𝓕.FieldOpi:Fin φs.lengthj:Fin φs.lengthh:i < jφsucΛ:WickContraction [singleton h]ᵘᶜ.length{j, i} ((singleton h).join φsucΛ) 𝓕:FieldSpecificationφs:List 𝓕.FieldOpi:Fin φs.lengthj:Fin φs.lengthh:i < jφsucΛ:WickContraction [singleton h]ᵘᶜ.length{j, i} = {i, j} a φsucΛ, (Finset.mapEmbedding uncontractedListEmd) a = {j, i} 𝓕:FieldSpecificationφs:List 𝓕.FieldOpi:Fin φs.lengthj:Fin φs.lengthh:i < jφsucΛ:WickContraction [singleton h]ᵘᶜ.length{j, i} = {i, j} All goals completed! 🐙lemma exists_contraction_pair_of_card_ge_zero {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) (h : 0 < φsΛ.1.card) : a, a φsΛ.1 := Finset.card_pos.mp h𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthh:0 < (↑φsΛ).cardhc:GradingCompliant φs φsΛa: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Λ).cardhc:GradingCompliant φs φsΛa: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! 🐙lemma join_not_gradingCompliant_of_left_not_gradingCompliant {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) (φsucΛ : WickContraction [φsΛ]ᵘᶜ.length) (hc : ¬ φsΛ.GradingCompliant) : ¬ (join φsΛ φsucΛ).GradingCompliant := 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengthhc:¬GradingCompliant φs φsΛ¬GradingCompliant φs (φsΛ.join φsucΛ) 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengthhc: x, (x_1 : x φsΛ), ¬(𝓕|>ₛφs[(φsΛ.fstFieldOfContract x, x_1)]) = 𝓕|>ₛφs[(φsΛ.sndFieldOfContract x, x_1)] x, (x_1 : x (φsΛ.join φsucΛ)), ¬(𝓕|>ₛφs[((φsΛ.join φsucΛ).fstFieldOfContract x, x_1)]) = 𝓕|>ₛφs[((φsΛ.join φsucΛ).sndFieldOfContract x, x_1)] 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:Finset (Fin φs.length)ha:a φsΛha2:¬(𝓕|>ₛφs[(φsΛ.fstFieldOfContract a, ha)]) = 𝓕|>ₛφs[(φsΛ.sndFieldOfContract a, ha)] x, (x_1 : x (φsΛ.join φsucΛ)), ¬(𝓕|>ₛφs[((φsΛ.join φsucΛ).fstFieldOfContract x, x_1)]) = 𝓕|>ₛφs[((φsΛ.join φsucΛ).sndFieldOfContract x, x_1)] 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:Finset (Fin φs.length)ha:a φsΛha2:¬(𝓕|>ₛφs[(φsΛ.fstFieldOfContract a, ha)]) = 𝓕|>ₛφs[(φsΛ.sndFieldOfContract a, ha)] (x : (joinLiftLeft a, ha) (φsΛ.join φsucΛ)), ¬(𝓕|>ₛφs[((φsΛ.join φsucΛ).fstFieldOfContract (joinLiftLeft a, ha), x)]) = 𝓕|>ₛφs[((φsΛ.join φsucΛ).sndFieldOfContract (joinLiftLeft a, ha), x)] 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:Finset (Fin φs.length)ha:a φsΛha2:¬(𝓕|>ₛφs[(φsΛ.fstFieldOfContract a, ha)]) = 𝓕|>ₛφs[(φsΛ.sndFieldOfContract a, ha)]¬(𝓕|>ₛφs[((φsΛ.join φsucΛ).fstFieldOfContract (joinLiftLeft a, ha), )]) = 𝓕|>ₛφs[((φsΛ.join φsucΛ).sndFieldOfContract (joinLiftLeft a, ha), )] 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengtha:Finset (Fin φs.length)ha:a φsΛha2:¬(𝓕|>ₛφs[(φsΛ.fstFieldOfContract a, ha)]) = 𝓕|>ₛφs[(φsΛ.sndFieldOfContract a, ha)]¬(𝓕|>ₛφs[(φsΛ.fstFieldOfContract a, ha)]) = 𝓕|>ₛφs[(φsΛ.sndFieldOfContract a, ha)] All goals completed! 🐙