1. Physlib
  2. QFT
  3. PerturbationTheory
  4. WickContraction
  5. Sign
  6. Join
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

Sign associated with joining two Wick contractions

@[expose] public section𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengthi:Fin [φsΛ]ᵘᶜ.lengthj:Fin [φsΛ]ᵘᶜ.length⊢ List.map [φsΛ]ᵘᶜ.get ((φsucΛ.signFinset i j).sort fun x1 x2 => x1 ≤ x2) = List.map φs.get (List.map (⇑uncontractedListEmd) ((φsucΛ.signFinset i j).sort fun x1 x2 => x1 ≤ x2))𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengthi:Fin [φsΛ]ᵘᶜ.lengthj:Fin [φsΛ]ᵘᶜ.length⊢ StrictMono ⇑uncontractedListEmd 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengthi:Fin [φsΛ]ᵘᶜ.lengthj:Fin [φsΛ]ᵘᶜ.length⊢ StrictMono ⇑uncontractedListEmd 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengthi✝:Fin [φsΛ]ᵘᶜ.lengthj✝:Fin [φsΛ]ᵘᶜ.lengthi:Fin [φsΛ]ᵘᶜ.lengthj:Fin [φsΛ]ᵘᶜ.lengthh:i < j⊢ uncontractedListEmd i < uncontractedListEmd j All goals completed! 🐙𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengthi:Fin [φsΛ]ᵘᶜ.lengthj:Fin [φsΛ]ᵘᶜ.lengtha:Fin [φsΛ]ᵘᶜ.lengthh✝:uncontractedListEmd i < uncontractedListEmd a ∧ uncontractedListEmd a < uncontractedListEmd jh2:uncontractedListEmd a ∈ φsΛ.uncontractedh1:∀ (h : (φsucΛ.getDual? a).isSome = true), uncontractedListEmd i < (Option.map (⇑uncontractedListEmd) (φsucΛ.getDual? a)).get ⋯h:(φsucΛ.getDual? a).isSome = trueh1':uncontractedListEmd i < (Option.map (⇑uncontractedListEmd) (φsucΛ.getDual? a)).get ⋯hl:i < (φsucΛ.getDual? a).get h⊢ i < (φsucΛ.getDual? a).get h𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengthi:Fin [φsΛ]ᵘᶜ.lengthj:Fin [φsΛ]ᵘᶜ.lengtha:Fin [φsΛ]ᵘᶜ.lengthh✝:uncontractedListEmd i < uncontractedListEmd a ∧ uncontractedListEmd a < uncontractedListEmd jh2:uncontractedListEmd a ∈ φsΛ.uncontractedh1:∀ (h : (φsucΛ.getDual? a).isSome = true), uncontractedListEmd i < (Option.map (⇑uncontractedListEmd) (φsucΛ.getDual? a)).get ⋯h:(φsucΛ.getDual? a).isSome = trueh1':uncontractedListEmd i < (Option.map (⇑uncontractedListEmd) (φsucΛ.getDual? a)).get ⋯hl:uncontractedListEmd i < uncontractedListEmd ((φsucΛ.getDual? a).get h)⊢ StrictMono ⇑uncontractedListEmd 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengthi:Fin [φsΛ]ᵘᶜ.lengthj:Fin [φsΛ]ᵘᶜ.lengtha:Fin [φsΛ]ᵘᶜ.lengthh✝:uncontractedListEmd i < uncontractedListEmd a ∧ uncontractedListEmd a < uncontractedListEmd jh2:uncontractedListEmd a ∈ φsΛ.uncontractedh1:∀ (h : (φsucΛ.getDual? a).isSome = true), uncontractedListEmd i < (Option.map (⇑uncontractedListEmd) (φsucΛ.getDual? a)).get ⋯h:(φsucΛ.getDual? a).isSome = trueh1':uncontractedListEmd i < (Option.map (⇑uncontractedListEmd) (φsucΛ.getDual? a)).get ⋯hl:uncontractedListEmd i < uncontractedListEmd ((φsucΛ.getDual? a).get h)⊢ StrictMono ⇑uncontractedListEmd All goals completed! 🐙All goals completed! 🐙𝓕:FieldSpecificationφs:List 𝓕.FieldOpi:Fin φs.lengthj:Fin φs.lengthh:i < jφsucΛ:WickContraction [singleton h]ᵘᶜ.lengtha:Fin φs.lengthh1✝:i < ah2✝¹:a < jh1:(singleton h).getDual? a = noneh2✝:(((singleton h).join φsucΛ).getDual? a).isSome = true → ∃ (h_1 : (((singleton h).join φsucΛ).getDual? a).isSome = true), i ≤ (((singleton h).join φsucΛ).getDual? a).get ⋯h2':(((singleton h).join φsucΛ).getDual? a).isSome = truehb:(((singleton h).join φsucΛ).getDual? a).isSome = trueh2:i ≤ (((singleton h).join φsucΛ).getDual? a).get ⋯hl:(((singleton h).join φsucΛ).getDual? a).isSome = truehn:i = (((singleton h).join φsucΛ).getDual? a).get ⋯hij:((singleton h).join φsucΛ).getDual? i = some j⊢ False 𝓕:FieldSpecificationφs:List 𝓕.FieldOpi:Fin φs.lengthj:Fin φs.lengthh:i < jφsucΛ:WickContraction [singleton h]ᵘᶜ.lengtha:Fin φs.lengthh1✝:i < ah2✝¹:a < jh1:(singleton h).getDual? a = noneh2✝:(((singleton h).join φsucΛ).getDual? a).isSome = true → ∃ (h_1 : (((singleton h).join φsucΛ).getDual? a).isSome = true), i ≤ (((singleton h).join φsucΛ).getDual? a).get ⋯h2':(((singleton h).join φsucΛ).getDual? a).isSome = truehb:(((singleton h).join φsucΛ).getDual? a).isSome = trueh2:i ≤ (((singleton h).join φsucΛ).getDual? a).get ⋯hl:(((singleton h).join φsucΛ).getDual? a).isSome = truehn:i = (((singleton h).join φsucΛ).getDual? a).get ⋯hij:a = j⊢ False All goals completed! 🐙 𝓕:FieldSpecificationφs:List 𝓕.FieldOpi:Fin φs.lengthj:Fin φs.lengthh:i < jφsucΛ:WickContraction [singleton h]ᵘᶜ.lengtha:Fin φs.lengthh1✝:i < ah2✝:a < jh1:(singleton h).getDual? a = noneh2:(((singleton h).join φsucΛ).getDual? a).isSome = true → ∃ (h_1 : (((singleton h).join φsucΛ).getDual? a).isSome = true), i ≤ (((singleton h).join φsucΛ).getDual? a).get ⋯h2':¬(((singleton h).join φsucΛ).getDual? a).isSome = true⊢ ((singleton h).join φsucΛ).getDual? a = none ∨ ∀ (h_1 : (((singleton h).join φsucΛ).getDual? a).isSome = true), i < (((singleton h).join φsucΛ).getDual? a).get h_1 𝓕:FieldSpecificationφs:List 𝓕.FieldOpi:Fin φs.lengthj:Fin φs.lengthh:i < jφsucΛ:WickContraction [singleton h]ᵘᶜ.lengtha:Fin φs.lengthh1✝:i < ah2✝:a < jh1:(singleton h).getDual? a = noneh2:(((singleton h).join φsucΛ).getDual? a).isSome = true → ∃ (h_1 : (((singleton h).join φsucΛ).getDual? a).isSome = true), i ≤ (((singleton h).join φsucΛ).getDual? a).get ⋯h2':(((singleton h).join φsucΛ).getDual? a).isSome = false⊢ ((singleton h).join φsucΛ).getDual? a = none ∨ ∀ (h_1 : (((singleton h).join φsucΛ).getDual? a).isSome = true), i < (((singleton h).join φsucΛ).getDual? a).get h_1 All goals completed! 🐙𝓕:FieldSpecificationφs:List 𝓕.FieldOpi:Fin φs.lengthj:Fin φs.lengthh:i < jφsucΛ:WickContraction [singleton h]ᵘᶜ.length⊢ ofFinset 𝓕.fieldOpStatistic φs.get ((singleton h).signFinset i j) = ofFinset 𝓕.fieldOpStatistic φs.get ({c ∈ (singleton h).signFinset i j | (((singleton h).join φsucΛ).getDual? c).isSome = true ∧ ∀ (h1 : (((singleton h).join φsucΛ).getDual? c).isSome = true), (((singleton h).join φsucΛ).getDual? c).get h1 < i}) * ofFinset 𝓕.fieldOpStatistic φs.get ({c ∈ (singleton h).signFinset i j | ¬((((singleton h).join φsucΛ).getDual? c).isSome = true ∧ ∀ (h1 : (((singleton h).join φsucΛ).getDual? c).isSome = true), (((singleton h).join φsucΛ).getDual? c).get h1 < i)}) All goals completed! 🐙

The difference in sign between φsucΛ.sign and the direct contribution of φsucΛ to (join (singleton h) φsucΛ).

def joinSignRightExtra {φs : List 𝓕.FieldOp} {i j : Fin φs.length} (h : i < j) (φsucΛ : WickContraction [singleton h]ᵘᶜ.length) : ℂ := ∏ a, 𝓢(𝓕|>ₛ [singleton h]ᵘᶜ[φsucΛ.sndFieldOfContract a], 𝓕|>ₛ ⟨φs.get, ((join (singleton h) φsucΛ).signFinset (uncontractedListEmd (φsucΛ.fstFieldOfContract a)) (uncontractedListEmd (φsucΛ.sndFieldOfContract a))).filter (fun c => ¬ c ∈ (singleton h).uncontracted)⟩)

The difference in sign between (singleton h).sign and the direct contribution of (singleton h) to (join (singleton h) φsucΛ).

def joinSignLeftExtra {φs : List 𝓕.FieldOp} {i j : Fin φs.length} (h : i < j) (φsucΛ : WickContraction [singleton h]ᵘᶜ.length) : ℂ := 𝓢(𝓕 |>ₛ φs[j], (𝓕 |>ₛ ⟨φs.get, ((singleton h).signFinset i j).filter (fun c => (((join (singleton h) φsucΛ).getDual? c).isSome ∧ ((h1 : ((join (singleton h) φsucΛ).getDual? c).isSome) → (((join (singleton h) φsucΛ).getDual? c).get h1) < i)))⟩))
𝓕:FieldSpecificationφs:List 𝓕.FieldOpi:Fin φs.lengthj:Fin φs.lengthh:i < jφsucΛ:WickContraction [singleton h]ᵘᶜ.length⊢ (exchangeSign (𝓕|>ₛφs[j])) (ofFinset 𝓕.fieldOpStatistic φs.get (((singleton h).join φsucΛ).signFinset i j)) * (exchangeSign (𝓕|>ₛφs[j])) (ofFinset 𝓕.fieldOpStatistic φs.get ({c ∈ (singleton h).signFinset i j | (((singleton h).join φsucΛ).getDual? c).isSome = true ∧ ∀ (h1 : (((singleton h).join φsucΛ).getDual? c).isSome = true), (((singleton h).join φsucΛ).getDual? c).get h1 < i})) = (exchangeSign (𝓕|>ₛφs[j])) (ofFinset 𝓕.fieldOpStatistic φs.get (((singleton h).join φsucΛ).signFinset i j)) * joinSignLeftExtra h φsucΛ All goals completed! 🐙𝓕:FieldSpecificationφs:List 𝓕.FieldOpi:Fin φs.lengthj:Fin φs.lengthh:i < jφsucΛ:WickContraction [singleton h]ᵘᶜ.length⊢ (∏ a, (exchangeSign (𝓕|>ₛ[singleton h]ᵘᶜ[φsucΛ.sndFieldOfContract a])) (ofFinset 𝓕.fieldOpStatistic φs.get ({c ∈ ((singleton h).join φsucΛ).signFinset (uncontractedListEmd (φsucΛ.fstFieldOfContract a)) (uncontractedListEmd (φsucΛ.sndFieldOfContract a)) | c ∉ (singleton h).uncontracted}))) * ∏ a, (exchangeSign (𝓕|>ₛ[singleton h]ᵘᶜ[φsucΛ.sndFieldOfContract a])) (ofFinset 𝓕.fieldOpStatistic φs.get (((singleton h).join φsucΛ).signFinset (uncontractedListEmd (φsucΛ.fstFieldOfContract a)) (uncontractedListEmd (φsucΛ.sndFieldOfContract a)))) = joinSignRightExtra h φsucΛ * ∏ a, (exchangeSign (𝓕|>ₛ[singleton h]ᵘᶜ[φsucΛ.sndFieldOfContract a])) (ofFinset 𝓕.fieldOpStatistic φs.get (((singleton h).join φsucΛ).signFinset (uncontractedListEmd (φsucΛ.fstFieldOfContract a)) (uncontractedListEmd (φsucΛ.sndFieldOfContract a)))) All goals completed! 🐙𝓕:FieldSpecificationφs:List 𝓕.FieldOpi:Fin φs.lengthj:Fin φs.lengthh:i < jφsucΛ:WickContraction [singleton h]ᵘᶜ.lengtha:↥↑φsucΛh11:{c | c ∉ (singleton h).uncontracted} = {i, j}x:Fin φs.lengthhjneqfst:uncontractedListEmd (φsucΛ.fstFieldOfContract a) ≠ jhjneqsnd:uncontractedListEmd (φsucΛ.sndFieldOfContract a) ≠ jhineqfst:uncontractedListEmd (φsucΛ.fstFieldOfContract a) ≠ ihineqsnd:uncontractedListEmd (φsucΛ.sndFieldOfContract a) ≠ ihj1✝:¬¬uncontractedListEmd (φsucΛ.fstFieldOfContract a) < jhj1:uncontractedListEmd (φsucΛ.fstFieldOfContract a) < jhi1✝:¬¬i < uncontractedListEmd (φsucΛ.sndFieldOfContract a)hi1:i < uncontractedListEmd (φsucΛ.sndFieldOfContract a)hi2✝:¬¬uncontractedListEmd (φsucΛ.fstFieldOfContract a) < ihi2:uncontractedListEmd (φsucΛ.fstFieldOfContract a) < ihj3✝:¬¬j < uncontractedListEmd (φsucΛ.sndFieldOfContract a)hj3:j < uncontractedListEmd (φsucΛ.sndFieldOfContract a)⊢ (x = i ∨ x = j) ∧ uncontractedListEmd (φsucΛ.fstFieldOfContract a) < x ∧ x < uncontractedListEmd (φsucΛ.sndFieldOfContract a) ∧ (((singleton h).join φsucΛ).getDual? x = none ∨ ∀ (h_1 : (((singleton h).join φsucΛ).getDual? x).isSome = true), uncontractedListEmd (φsucΛ.fstFieldOfContract a) < (((singleton h).join φsucΛ).getDual? x).get h_1) ↔ (x ∈ if j < uncontractedListEmd (φsucΛ.sndFieldOfContract a) then {j} else ∅) ∨ x = i 𝓕:FieldSpecificationφs:List 𝓕.FieldOpi:Fin φs.lengthj:Fin φs.lengthh:i < jφsucΛ:WickContraction [singleton h]ᵘᶜ.lengtha:↥↑φsucΛh11:{c | c ∉ (singleton h).uncontracted} = {i, j}x:Fin φs.lengthhjneqfst:uncontractedListEmd (φsucΛ.fstFieldOfContract a) ≠ jhjneqsnd:uncontractedListEmd (φsucΛ.sndFieldOfContract a) ≠ jhineqfst:uncontractedListEmd (φsucΛ.fstFieldOfContract a) ≠ ihineqsnd:uncontractedListEmd (φsucΛ.sndFieldOfContract a) ≠ ihj1✝:¬¬uncontractedListEmd (φsucΛ.fstFieldOfContract a) < jhj1:uncontractedListEmd (φsucΛ.fstFieldOfContract a) < jhi1✝:¬¬i < uncontractedListEmd (φsucΛ.sndFieldOfContract a)hi1:i < uncontractedListEmd (φsucΛ.sndFieldOfContract a)hi2✝:¬¬uncontractedListEmd (φsucΛ.fstFieldOfContract a) < ihi2:uncontractedListEmd (φsucΛ.fstFieldOfContract a) < ihj3✝:¬¬j < uncontractedListEmd (φsucΛ.sndFieldOfContract a)hj3:j < uncontractedListEmd (φsucΛ.sndFieldOfContract a)⊢ (x = i ∨ x = j) ∧ uncontractedListEmd (φsucΛ.fstFieldOfContract a) < x ∧ x < uncontractedListEmd (φsucΛ.sndFieldOfContract a) ∧ (((singleton h).join φsucΛ).getDual? x = none ∨ ∀ (h_1 : (((singleton h).join φsucΛ).getDual? x).isSome = true), uncontractedListEmd (φsucΛ.fstFieldOfContract a) < (((singleton h).join φsucΛ).getDual? x).get h_1) ↔ x = j ∨ x = i 𝓕:FieldSpecificationφs:List 𝓕.FieldOpi:Fin φs.lengthj:Fin φs.lengthh:i < jφsucΛ:WickContraction [singleton h]ᵘᶜ.lengtha:↥↑φsucΛh11:{c | c ∉ (singleton h).uncontracted} = {i, j}x:Fin φs.lengthhjneqfst:uncontractedListEmd (φsucΛ.fstFieldOfContract a) ≠ jhjneqsnd:uncontractedListEmd (φsucΛ.sndFieldOfContract a) ≠ jhineqfst:uncontractedListEmd (φsucΛ.fstFieldOfContract a) ≠ ihineqsnd:uncontractedListEmd (φsucΛ.sndFieldOfContract a) ≠ ihj1✝:¬¬uncontractedListEmd (φsucΛ.fstFieldOfContract a) < jhj1:uncontractedListEmd (φsucΛ.fstFieldOfContract a) < jhi1✝:¬¬i < uncontractedListEmd (φsucΛ.sndFieldOfContract a)hi1:i < uncontractedListEmd (φsucΛ.sndFieldOfContract a)hi2✝:¬¬uncontractedListEmd (φsucΛ.fstFieldOfContract a) < ihi2:uncontractedListEmd (φsucΛ.fstFieldOfContract a) < ihj3✝:¬¬j < uncontractedListEmd (φsucΛ.sndFieldOfContract a)hj3:j < uncontractedListEmd (φsucΛ.sndFieldOfContract a)⊢ (x = i ∨ x = j) ∧ uncontractedListEmd (φsucΛ.fstFieldOfContract a) < x ∧ x < uncontractedListEmd (φsucΛ.sndFieldOfContract a) ∧ (((singleton h).join φsucΛ).getDual? x = none ∨ ∀ (h_1 : (((singleton h).join φsucΛ).getDual? x).isSome = true), uncontractedListEmd (φsucΛ.fstFieldOfContract a) < (((singleton h).join φsucΛ).getDual? x).get h_1) → x = j ∨ x = i𝓕:FieldSpecificationφs:List 𝓕.FieldOpi:Fin φs.lengthj:Fin φs.lengthh:i < jφsucΛ:WickContraction [singleton h]ᵘᶜ.lengtha:↥↑φsucΛh11:{c | c ∉ (singleton h).uncontracted} = {i, j}x:Fin φs.lengthhjneqfst:uncontractedListEmd (φsucΛ.fstFieldOfContract a) ≠ jhjneqsnd:uncontractedListEmd (φsucΛ.sndFieldOfContract a) ≠ jhineqfst:uncontractedListEmd (φsucΛ.fstFieldOfContract a) ≠ ihineqsnd:uncontractedListEmd (φsucΛ.sndFieldOfContract a) ≠ ihj1✝:¬¬uncontractedListEmd (φsucΛ.fstFieldOfContract a) < jhj1:uncontractedListEmd (φsucΛ.fstFieldOfContract a) < jhi1✝:¬¬i < uncontractedListEmd (φsucΛ.sndFieldOfContract a)hi1:i < uncontractedListEmd (φsucΛ.sndFieldOfContract a)hi2✝:¬¬uncontractedListEmd (φsucΛ.fstFieldOfContract a) < ihi2:uncontractedListEmd (φsucΛ.fstFieldOfContract a) < ihj3✝:¬¬j < uncontractedListEmd (φsucΛ.sndFieldOfContract a)hj3:j < uncontractedListEmd (φsucΛ.sndFieldOfContract a)⊢ x = j ∨ x = i → (x = i ∨ x = j) ∧ uncontractedListEmd (φsucΛ.fstFieldOfContract a) < x ∧ x < uncontractedListEmd (φsucΛ.sndFieldOfContract a) ∧ (((singleton h).join φsucΛ).getDual? x = none ∨ ∀ (h_1 : (((singleton h).join φsucΛ).getDual? x).isSome = true), uncontractedListEmd (φsucΛ.fstFieldOfContract a) < (((singleton h).join φsucΛ).getDual? x).get h_1) 𝓕:FieldSpecificationφs:List 𝓕.FieldOpi:Fin φs.lengthj:Fin φs.lengthh:i < jφsucΛ:WickContraction [singleton h]ᵘᶜ.lengtha:↥↑φsucΛh11:{c | c ∉ (singleton h).uncontracted} = {i, j}x:Fin φs.lengthhjneqfst:uncontractedListEmd (φsucΛ.fstFieldOfContract a) ≠ jhjneqsnd:uncontractedListEmd (φsucΛ.sndFieldOfContract a) ≠ jhineqfst:uncontractedListEmd (φsucΛ.fstFieldOfContract a) ≠ ihineqsnd:uncontractedListEmd (φsucΛ.sndFieldOfContract a) ≠ ihj1✝:¬¬uncontractedListEmd (φsucΛ.fstFieldOfContract a) < jhj1:uncontractedListEmd (φsucΛ.fstFieldOfContract a) < jhi1✝:¬¬i < uncontractedListEmd (φsucΛ.sndFieldOfContract a)hi1:i < uncontractedListEmd (φsucΛ.sndFieldOfContract a)hi2✝:¬¬uncontractedListEmd (φsucΛ.fstFieldOfContract a) < ihi2:uncontractedListEmd (φsucΛ.fstFieldOfContract a) < ihj3✝:¬¬j < uncontractedListEmd (φsucΛ.sndFieldOfContract a)hj3:j < uncontractedListEmd (φsucΛ.sndFieldOfContract a)⊢ (x = i ∨ x = j) ∧ uncontractedListEmd (φsucΛ.fstFieldOfContract a) < x ∧ x < uncontractedListEmd (φsucΛ.sndFieldOfContract a) ∧ (((singleton h).join φsucΛ).getDual? x = none ∨ ∀ (h_1 : (((singleton h).join φsucΛ).getDual? x).isSome = true), uncontractedListEmd (φsucΛ.fstFieldOfContract a) < (((singleton h).join φsucΛ).getDual? x).get h_1) → x = j ∨ x = i 𝓕:FieldSpecificationφs:List 𝓕.FieldOpi:Fin φs.lengthj:Fin φs.lengthh✝:i < jφsucΛ:WickContraction [singleton h]ᵘᶜ.lengtha:↥↑φsucΛh11:{c | c ∉ (singleton h).uncontracted} = {i, j}x:Fin φs.lengthhjneqfst:uncontractedListEmd (φsucΛ.fstFieldOfContract a) ≠ jhjneqsnd:uncontractedListEmd (φsucΛ.sndFieldOfContract a) ≠ jhineqfst:uncontractedListEmd (φsucΛ.fstFieldOfContract a) ≠ ihineqsnd:uncontractedListEmd (φsucΛ.sndFieldOfContract a) ≠ ihj1✝:¬¬uncontractedListEmd (φsucΛ.fstFieldOfContract a) < jhj1:uncontractedListEmd (φsucΛ.fstFieldOfContract a) < jhi1✝:¬¬i < uncontractedListEmd (φsucΛ.sndFieldOfContract a)hi1:i < uncontractedListEmd (φsucΛ.sndFieldOfContract a)hi2✝:¬¬uncontractedListEmd (φsucΛ.fstFieldOfContract a) < ihi2:uncontractedListEmd (φsucΛ.fstFieldOfContract a) < ihj3✝:¬¬j < uncontractedListEmd (φsucΛ.sndFieldOfContract a)hj3:j < uncontractedListEmd (φsucΛ.sndFieldOfContract a)h:(x = i ∨ x = j) ∧ uncontractedListEmd (φsucΛ.fstFieldOfContract a) < x ∧ x < uncontractedListEmd (φsucΛ.sndFieldOfContract a) ∧ (((singleton h✝).join φsucΛ).getDual? x = none ∨ ∀ (h : (((singleton h✝).join φsucΛ).getDual? x).isSome = true), uncontractedListEmd (φsucΛ.fstFieldOfContract a) < (((singleton h✝).join φsucΛ).getDual? x).get h)⊢ x = j ∨ x = i All goals completed! 🐙 𝓕:FieldSpecificationφs:List 𝓕.FieldOpi:Fin φs.lengthj:Fin φs.lengthh:i < jφsucΛ:WickContraction [singleton h]ᵘᶜ.lengtha:↥↑φsucΛh11:{c | c ∉ (singleton h).uncontracted} = {i, j}x:Fin φs.lengthhjneqfst:uncontractedListEmd (φsucΛ.fstFieldOfContract a) ≠ jhjneqsnd:uncontractedListEmd (φsucΛ.sndFieldOfContract a) ≠ jhineqfst:uncontractedListEmd (φsucΛ.fstFieldOfContract a) ≠ ihineqsnd:uncontractedListEmd (φsucΛ.sndFieldOfContract a) ≠ ihj1✝:¬¬uncontractedListEmd (φsucΛ.fstFieldOfContract a) < jhj1:uncontractedListEmd (φsucΛ.fstFieldOfContract a) < jhi1✝:¬¬i < uncontractedListEmd (φsucΛ.sndFieldOfContract a)hi1:i < uncontractedListEmd (φsucΛ.sndFieldOfContract a)hi2✝:¬¬uncontractedListEmd (φsucΛ.fstFieldOfContract a) < ihi2:uncontractedListEmd (φsucΛ.fstFieldOfContract a) < ihj3✝:¬¬j < uncontractedListEmd (φsucΛ.sndFieldOfContract a)hj3:j < uncontractedListEmd (φsucΛ.sndFieldOfContract a)⊢ x = j ∨ x = i → (x = i ∨ x = j) ∧ uncontractedListEmd (φsucΛ.fstFieldOfContract a) < x ∧ x < uncontractedListEmd (φsucΛ.sndFieldOfContract a) ∧ (((singleton h).join φsucΛ).getDual? x = none ∨ ∀ (h_1 : (((singleton h).join φsucΛ).getDual? x).isSome = true), uncontractedListEmd (φsucΛ.fstFieldOfContract a) < (((singleton h).join φsucΛ).getDual? x).get h_1) 𝓕:FieldSpecificationφs:List 𝓕.FieldOpi:Fin φs.lengthj:Fin φs.lengthh✝:i < jφsucΛ:WickContraction [singleton h]ᵘᶜ.lengtha:↥↑φsucΛh11:{c | c ∉ (singleton h).uncontracted} = {i, j}x:Fin φs.lengthhjneqfst:uncontractedListEmd (φsucΛ.fstFieldOfContract a) ≠ jhjneqsnd:uncontractedListEmd (φsucΛ.sndFieldOfContract a) ≠ jhineqfst:uncontractedListEmd (φsucΛ.fstFieldOfContract a) ≠ ihineqsnd:uncontractedListEmd (φsucΛ.sndFieldOfContract a) ≠ ihj1✝:¬¬uncontractedListEmd (φsucΛ.fstFieldOfContract a) < jhj1:uncontractedListEmd (φsucΛ.fstFieldOfContract a) < jhi1✝:¬¬i < uncontractedListEmd (φsucΛ.sndFieldOfContract a)hi1:i < uncontractedListEmd (φsucΛ.sndFieldOfContract a)hi2✝:¬¬uncontractedListEmd (φsucΛ.fstFieldOfContract a) < ihi2:uncontractedListEmd (φsucΛ.fstFieldOfContract a) < ihj3✝:¬¬j < uncontractedListEmd (φsucΛ.sndFieldOfContract a)hj3:j < uncontractedListEmd (φsucΛ.sndFieldOfContract a)h:x = j ∨ x = i⊢ (x = i ∨ x = j) ∧ uncontractedListEmd (φsucΛ.fstFieldOfContract a) < x ∧ x < uncontractedListEmd (φsucΛ.sndFieldOfContract a) ∧ (((singleton h✝).join φsucΛ).getDual? x = none ∨ ∀ (h : (((singleton h✝).join φsucΛ).getDual? x).isSome = true), uncontractedListEmd (φsucΛ.fstFieldOfContract a) < (((singleton h✝).join φsucΛ).getDual? x).get h) 𝓕:FieldSpecificationφs:List 𝓕.FieldOpi:Fin φs.lengthj:Fin φs.lengthh:i < jφsucΛ:WickContraction [singleton h]ᵘᶜ.lengtha:↥↑φsucΛh11:{c | c ∉ (singleton h).uncontracted} = {i, j}x:Fin φs.lengthhjneqfst:uncontractedListEmd (φsucΛ.fstFieldOfContract a) ≠ jhjneqsnd:uncontractedListEmd (φsucΛ.sndFieldOfContract a) ≠ jhineqfst:uncontractedListEmd (φsucΛ.fstFieldOfContract a) ≠ ihineqsnd:uncontractedListEmd (φsucΛ.sndFieldOfContract a) ≠ ihj1✝:¬¬uncontractedListEmd (φsucΛ.fstFieldOfContract a) < jhj1:uncontractedListEmd (φsucΛ.fstFieldOfContract a) < jhi1✝:¬¬i < uncontractedListEmd (φsucΛ.sndFieldOfContract a)hi1:i < uncontractedListEmd (φsucΛ.sndFieldOfContract a)hi2✝:¬¬uncontractedListEmd (φsucΛ.fstFieldOfContract a) < ihi2:uncontractedListEmd (φsucΛ.fstFieldOfContract a) < ihj3✝:¬¬j < uncontractedListEmd (φsucΛ.sndFieldOfContract a)hj3:j < uncontractedListEmd (φsucΛ.sndFieldOfContract a)h1:x = j⊢ (x = i ∨ x = j) ∧ uncontractedListEmd (φsucΛ.fstFieldOfContract a) < x ∧ x < uncontractedListEmd (φsucΛ.sndFieldOfContract a) ∧ (((singleton h✝).join φsucΛ).getDual? x = none ∨ ∀ (h : (((singleton h✝).join φsucΛ).getDual? x).isSome = true), uncontractedListEmd (φsucΛ.fstFieldOfContract a) < (((singleton h✝).join φsucΛ).getDual? x).get h)𝓕:FieldSpecificationφs:List 𝓕.FieldOpi:Fin φs.lengthj:Fin φs.lengthh:i < jφsucΛ:WickContraction [singleton h]ᵘᶜ.lengtha:↥↑φsucΛh11:{c | c ∉ (singleton h).uncontracted} = {i, j}x:Fin φs.lengthhjneqfst:uncontractedListEmd (φsucΛ.fstFieldOfContract a) ≠ jhjneqsnd:uncontractedListEmd (φsucΛ.sndFieldOfContract a) ≠ jhineqfst:uncontractedListEmd (φsucΛ.fstFieldOfContract a) ≠ ihineqsnd:uncontractedListEmd (φsucΛ.sndFieldOfContract a) ≠ ihj1✝:¬¬uncontractedListEmd (φsucΛ.fstFieldOfContract a) < jhj1:uncontractedListEmd (φsucΛ.fstFieldOfContract a) < jhi1✝:¬¬i < uncontractedListEmd (φsucΛ.sndFieldOfContract a)hi1:i < uncontractedListEmd (φsucΛ.sndFieldOfContract a)hi2✝:¬¬uncontractedListEmd (φsucΛ.fstFieldOfContract a) < ihi2:uncontractedListEmd (φsucΛ.fstFieldOfContract a) < ihj3✝:¬¬j < uncontractedListEmd (φsucΛ.sndFieldOfContract a)hj3:j < uncontractedListEmd (φsucΛ.sndFieldOfContract a)h1:x = i⊢ (x = i ∨ x = j) ∧ uncontractedListEmd (φsucΛ.fstFieldOfContract a) < x ∧ x < uncontractedListEmd (φsucΛ.sndFieldOfContract a) ∧ (((singleton h✝).join φsucΛ).getDual? x = none ∨ ∀ (h : (((singleton h✝).join φsucΛ).getDual? x).isSome = true), uncontractedListEmd (φsucΛ.fstFieldOfContract a) < (((singleton h✝).join φsucΛ).getDual? x).get h) 𝓕:FieldSpecificationφs:List 𝓕.FieldOpi:Fin φs.lengthj:Fin φs.lengthh:i < jφsucΛ:WickContraction [singleton h]ᵘᶜ.lengtha:↥↑φsucΛh11:{c | c ∉ (singleton h).uncontracted} = {i, j}x:Fin φs.lengthhjneqfst:uncontractedListEmd (φsucΛ.fstFieldOfContract a) ≠ jhjneqsnd:uncontractedListEmd (φsucΛ.sndFieldOfContract a) ≠ jhineqfst:uncontractedListEmd (φsucΛ.fstFieldOfContract a) ≠ ihineqsnd:uncontractedListEmd (φsucΛ.sndFieldOfContract a) ≠ ihj1✝:¬¬uncontractedListEmd (φsucΛ.fstFieldOfContract a) < jhj1:uncontractedListEmd (φsucΛ.fstFieldOfContract a) < jhi1✝:¬¬i < uncontractedListEmd (φsucΛ.sndFieldOfContract a)hi1:i < uncontractedListEmd (φsucΛ.sndFieldOfContract a)hi2✝:¬¬uncontractedListEmd (φsucΛ.fstFieldOfContract a) < ihi2:uncontractedListEmd (φsucΛ.fstFieldOfContract a) < ihj3✝:¬¬j < uncontractedListEmd (φsucΛ.sndFieldOfContract a)hj3:j < uncontractedListEmd (φsucΛ.sndFieldOfContract a)h1:x = j⊢ (x = i ∨ x = j) ∧ uncontractedListEmd (φsucΛ.fstFieldOfContract a) < x ∧ x < uncontractedListEmd (φsucΛ.sndFieldOfContract a) ∧ (((singleton h✝).join φsucΛ).getDual? x = none ∨ ∀ (h : (((singleton h✝).join φsucΛ).getDual? x).isSome = true), uncontractedListEmd (φsucΛ.fstFieldOfContract a) < (((singleton h✝).join φsucΛ).getDual? x).get h) 𝓕:FieldSpecificationφs:List 𝓕.FieldOpi:Fin φs.lengthx:Fin φs.lengthh:i < xφsucΛ:WickContraction [singleton h]ᵘᶜ.lengtha:↥↑φsucΛh11:{c | c ∉ (singleton h).uncontracted} = {i, x}hjneqfst:uncontractedListEmd (φsucΛ.fstFieldOfContract a) ≠ xhjneqsnd:uncontractedListEmd (φsucΛ.sndFieldOfContract a) ≠ xhineqfst:uncontractedListEmd (φsucΛ.fstFieldOfContract a) ≠ ihineqsnd:uncontractedListEmd (φsucΛ.sndFieldOfContract a) ≠ ihj1✝:¬¬uncontractedListEmd (φsucΛ.fstFieldOfContract a) < xhj1:uncontractedListEmd (φsucΛ.fstFieldOfContract a) < xhi1✝:¬¬i < uncontractedListEmd (φsucΛ.sndFieldOfContract a)hi1:i < uncontractedListEmd (φsucΛ.sndFieldOfContract a)hi2✝:¬¬uncontractedListEmd (φsucΛ.fstFieldOfContract a) < ihi2:uncontractedListEmd (φsucΛ.fstFieldOfContract a) < ihj3✝:¬¬x < uncontractedListEmd (φsucΛ.sndFieldOfContract a)hj3:x < uncontractedListEmd (φsucΛ.sndFieldOfContract a)⊢ (x = i ∨ x = x) ∧ uncontractedListEmd (φsucΛ.fstFieldOfContract a) < x ∧ x < uncontractedListEmd (φsucΛ.sndFieldOfContract a) ∧ (((singleton h).join φsucΛ).getDual? x = none ∨ ∀ (h_1 : (((singleton h).join φsucΛ).getDual? x).isSome = true), uncontractedListEmd (φsucΛ.fstFieldOfContract a) < (((singleton h).join φsucΛ).getDual? x).get h_1) 𝓕:FieldSpecificationφs:List 𝓕.FieldOpi:Fin φs.lengthx:Fin φs.lengthh:i < xφsucΛ:WickContraction [singleton h]ᵘᶜ.lengtha:↥↑φsucΛh11:{c | c ∉ (singleton h).uncontracted} = {i, x}hjneqfst:uncontractedListEmd (φsucΛ.fstFieldOfContract a) ≠ xhjneqsnd:uncontractedListEmd (φsucΛ.sndFieldOfContract a) ≠ xhineqfst:uncontractedListEmd (φsucΛ.fstFieldOfContract a) ≠ ihineqsnd:uncontractedListEmd (φsucΛ.sndFieldOfContract a) ≠ ihj1✝:¬¬uncontractedListEmd (φsucΛ.fstFieldOfContract a) < xhj1:uncontractedListEmd (φsucΛ.fstFieldOfContract a) < xhi1✝:¬¬i < uncontractedListEmd (φsucΛ.sndFieldOfContract a)hi1:i < uncontractedListEmd (φsucΛ.sndFieldOfContract a)hi2✝:¬¬uncontractedListEmd (φsucΛ.fstFieldOfContract a) < ihi2:uncontractedListEmd (φsucΛ.fstFieldOfContract a) < ihj3✝:¬¬x < uncontractedListEmd (φsucΛ.sndFieldOfContract a)hj3:x < uncontractedListEmd (φsucΛ.sndFieldOfContract a)⊢ uncontractedListEmd (φsucΛ.fstFieldOfContract a) < x ∧ x < uncontractedListEmd (φsucΛ.sndFieldOfContract a) ∧ uncontractedListEmd (φsucΛ.fstFieldOfContract a) < i All goals completed! 🐙 𝓕:FieldSpecificationφs:List 𝓕.FieldOpi:Fin φs.lengthj:Fin φs.lengthh:i < jφsucΛ:WickContraction [singleton h]ᵘᶜ.lengtha:↥↑φsucΛh11:{c | c ∉ (singleton h).uncontracted} = {i, j}x:Fin φs.lengthhjneqfst:uncontractedListEmd (φsucΛ.fstFieldOfContract a) ≠ jhjneqsnd:uncontractedListEmd (φsucΛ.sndFieldOfContract a) ≠ jhineqfst:uncontractedListEmd (φsucΛ.fstFieldOfContract a) ≠ ihineqsnd:uncontractedListEmd (φsucΛ.sndFieldOfContract a) ≠ ihj1✝:¬¬uncontractedListEmd (φsucΛ.fstFieldOfContract a) < jhj1:uncontractedListEmd (φsucΛ.fstFieldOfContract a) < jhi1✝:¬¬i < uncontractedListEmd (φsucΛ.sndFieldOfContract a)hi1:i < uncontractedListEmd (φsucΛ.sndFieldOfContract a)hi2✝:¬¬uncontractedListEmd (φsucΛ.fstFieldOfContract a) < ihi2:uncontractedListEmd (φsucΛ.fstFieldOfContract a) < ihj3✝:¬¬j < uncontractedListEmd (φsucΛ.sndFieldOfContract a)hj3:j < uncontractedListEmd (φsucΛ.sndFieldOfContract a)h1:x = i⊢ (x = i ∨ x = j) ∧ uncontractedListEmd (φsucΛ.fstFieldOfContract a) < x ∧ x < uncontractedListEmd (φsucΛ.sndFieldOfContract a) ∧ (((singleton h✝).join φsucΛ).getDual? x = none ∨ ∀ (h : (((singleton h✝).join φsucΛ).getDual? x).isSome = true), uncontractedListEmd (φsucΛ.fstFieldOfContract a) < (((singleton h✝).join φsucΛ).getDual? x).get h) 𝓕:FieldSpecificationφs:List 𝓕.FieldOpj:Fin φs.lengthx:Fin φs.lengthh:x < jφsucΛ:WickContraction [singleton h]ᵘᶜ.lengtha:↥↑φsucΛh11:{c | c ∉ (singleton h).uncontracted} = {x, j}hjneqfst:uncontractedListEmd (φsucΛ.fstFieldOfContract a) ≠ jhjneqsnd:uncontractedListEmd (φsucΛ.sndFieldOfContract a) ≠ jhineqfst:uncontractedListEmd (φsucΛ.fstFieldOfContract a) ≠ xhineqsnd:uncontractedListEmd (φsucΛ.sndFieldOfContract a) ≠ xhj1✝:¬¬uncontractedListEmd (φsucΛ.fstFieldOfContract a) < jhj1:uncontractedListEmd (φsucΛ.fstFieldOfContract a) < jhi1✝:¬¬x < uncontractedListEmd (φsucΛ.sndFieldOfContract a)hi1:x < uncontractedListEmd (φsucΛ.sndFieldOfContract a)hi2✝:¬¬uncontractedListEmd (φsucΛ.fstFieldOfContract a) < xhi2:uncontractedListEmd (φsucΛ.fstFieldOfContract a) < xhj3✝:¬¬j < uncontractedListEmd (φsucΛ.sndFieldOfContract a)hj3:j < uncontractedListEmd (φsucΛ.sndFieldOfContract a)⊢ (x = x ∨ x = j) ∧ uncontractedListEmd (φsucΛ.fstFieldOfContract a) < x ∧ x < uncontractedListEmd (φsucΛ.sndFieldOfContract a) ∧ (((singleton h).join φsucΛ).getDual? x = none ∨ ∀ (h_1 : (((singleton h).join φsucΛ).getDual? x).isSome = true), uncontractedListEmd (φsucΛ.fstFieldOfContract a) < (((singleton h).join φsucΛ).getDual? x).get h_1) 𝓕:FieldSpecificationφs:List 𝓕.FieldOpj:Fin φs.lengthx:Fin φs.lengthh:x < jφsucΛ:WickContraction [singleton h]ᵘᶜ.lengtha:↥↑φsucΛh11:{c | c ∉ (singleton h).uncontracted} = {x, j}hjneqfst:uncontractedListEmd (φsucΛ.fstFieldOfContract a) ≠ jhjneqsnd:uncontractedListEmd (φsucΛ.sndFieldOfContract a) ≠ jhineqfst:uncontractedListEmd (φsucΛ.fstFieldOfContract a) ≠ xhineqsnd:uncontractedListEmd (φsucΛ.sndFieldOfContract a) ≠ xhj1✝:¬¬uncontractedListEmd (φsucΛ.fstFieldOfContract a) < jhj1:uncontractedListEmd (φsucΛ.fstFieldOfContract a) < jhi1✝:¬¬x < uncontractedListEmd (φsucΛ.sndFieldOfContract a)hi1:x < uncontractedListEmd (φsucΛ.sndFieldOfContract a)hi2✝:¬¬uncontractedListEmd (φsucΛ.fstFieldOfContract a) < xhi2:uncontractedListEmd (φsucΛ.fstFieldOfContract a) < xhj3✝:¬¬j < uncontractedListEmd (φsucΛ.sndFieldOfContract a)hj3:j < uncontractedListEmd (φsucΛ.sndFieldOfContract a)⊢ uncontractedListEmd (φsucΛ.fstFieldOfContract a) < x ∧ x < uncontractedListEmd (φsucΛ.sndFieldOfContract a) ∧ uncontractedListEmd (φsucΛ.fstFieldOfContract a) < j All goals completed! 🐙𝓕:FieldSpecificationφs:List 𝓕.FieldOpi:Fin φs.lengthj:Fin φs.lengthh:i < jhs:(𝓕|>ₛφs[i]) = 𝓕|>ₛφs[j]φsucΛ:WickContraction [singleton h]ᵘᶜ.lengthe2:Fin φs.length ≃ { x // (((singleton h).join φsucΛ).getDual? x).isSome = true } ⊕ { x // ¬(((singleton h).join φsucΛ).getDual? x).isSome = true } := (Equiv.sumCompl fun a => (((singleton h).join φsucΛ).getDual? a).isSome = true).symma:↥↑φsucΛhjneqsnd:uncontractedListEmd (φsucΛ.sndFieldOfContract a) ≠ jhl:uncontractedListEmd (φsucΛ.fstFieldOfContract a) < uncontractedListEmd (φsucΛ.sndFieldOfContract a)hj1✝:¬¬uncontractedListEmd (φsucΛ.fstFieldOfContract a) < jhj1:uncontractedListEmd (φsucΛ.fstFieldOfContract a) < jhi2✝:¬¬i < uncontractedListEmd (φsucΛ.sndFieldOfContract a)hi2:i < uncontractedListEmd (φsucΛ.sndFieldOfContract a)hi2n:¬uncontractedListEmd (φsucΛ.sndFieldOfContract a) < ihj2✝:j < uncontractedListEmd (φsucΛ.sndFieldOfContract a)hi1✝:¬¬uncontractedListEmd (φsucΛ.fstFieldOfContract a) < ihi1:uncontractedListEmd (φsucΛ.fstFieldOfContract a) < ihj2:¬uncontractedListEmd (φsucΛ.sndFieldOfContract a) < j⊢ 1 = (exchangeSign (𝓕|>ₛ[singleton h]ᵘᶜ[↑(φsucΛ.sndFieldOfContract a)])) (ofFinset 𝓕.fieldOpStatistic φs.get {j} * ofFinset 𝓕.fieldOpStatistic φs.get {i})𝓕:FieldSpecificationφs:List 𝓕.FieldOpi:Fin φs.lengthj:Fin φs.lengthh:i < jhs:(𝓕|>ₛφs[i]) = 𝓕|>ₛφs[j]φsucΛ:WickContraction [singleton h]ᵘᶜ.lengthe2:Fin φs.length ≃ { x // (((singleton h).join φsucΛ).getDual? x).isSome = true } ⊕ { x // ¬(((singleton h).join φsucΛ).getDual? x).isSome = true } := (Equiv.sumCompl fun a => (((singleton h).join φsucΛ).getDual? a).isSome = true).symma:↥↑φsucΛhjneqsnd:uncontractedListEmd (φsucΛ.sndFieldOfContract a) ≠ jhl:uncontractedListEmd (φsucΛ.fstFieldOfContract a) < uncontractedListEmd (φsucΛ.sndFieldOfContract a)hj1✝:¬¬uncontractedListEmd (φsucΛ.fstFieldOfContract a) < jhj1:uncontractedListEmd (φsucΛ.fstFieldOfContract a) < jhi2✝:¬¬i < uncontractedListEmd (φsucΛ.sndFieldOfContract a)hi2:i < uncontractedListEmd (φsucΛ.sndFieldOfContract a)hi2n:¬uncontractedListEmd (φsucΛ.sndFieldOfContract a) < ihj2✝:j < uncontractedListEmd (φsucΛ.sndFieldOfContract a)hi1✝:¬¬uncontractedListEmd (φsucΛ.fstFieldOfContract a) < ihi1:uncontractedListEmd (φsucΛ.fstFieldOfContract a) < ihj2:¬uncontractedListEmd (φsucΛ.sndFieldOfContract a) < j⊢ Disjoint {j} {i} 𝓕:FieldSpecificationφs:List 𝓕.FieldOpi:Fin φs.lengthj:Fin φs.lengthh:i < jhs:(𝓕|>ₛφs[i]) = 𝓕|>ₛφs[j]φsucΛ:WickContraction [singleton h]ᵘᶜ.lengthe2:Fin φs.length ≃ { x // (((singleton h).join φsucΛ).getDual? x).isSome = true } ⊕ { x // ¬(((singleton h).join φsucΛ).getDual? x).isSome = true } := (Equiv.sumCompl fun a => (((singleton h).join φsucΛ).getDual? a).isSome = true).symma:↥↑φsucΛhjneqsnd:uncontractedListEmd (φsucΛ.sndFieldOfContract a) ≠ jhl:uncontractedListEmd (φsucΛ.fstFieldOfContract a) < uncontractedListEmd (φsucΛ.sndFieldOfContract a)hj1✝:¬¬uncontractedListEmd (φsucΛ.fstFieldOfContract a) < jhj1:uncontractedListEmd (φsucΛ.fstFieldOfContract a) < jhi2✝:¬¬i < uncontractedListEmd (φsucΛ.sndFieldOfContract a)hi2:i < uncontractedListEmd (φsucΛ.sndFieldOfContract a)hi2n:¬uncontractedListEmd (φsucΛ.sndFieldOfContract a) < ihj2✝:j < uncontractedListEmd (φsucΛ.sndFieldOfContract a)hi1✝:¬¬uncontractedListEmd (φsucΛ.fstFieldOfContract a) < ihi1:uncontractedListEmd (φsucΛ.fstFieldOfContract a) < ihj2:¬uncontractedListEmd (φsucΛ.sndFieldOfContract a) < j⊢ 1 = (exchangeSign (𝓕|>ₛ[singleton h]ᵘᶜ[↑(φsucΛ.sndFieldOfContract a)])) ((𝓕|>ₛφs[↑j]) * 𝓕|>ₛφs[↑i])𝓕:FieldSpecificationφs:List 𝓕.FieldOpi:Fin φs.lengthj:Fin φs.lengthh:i < jhs:(𝓕|>ₛφs[i]) = 𝓕|>ₛφs[j]φsucΛ:WickContraction [singleton h]ᵘᶜ.lengthe2:Fin φs.length ≃ { x // (((singleton h).join φsucΛ).getDual? x).isSome = true } ⊕ { x // ¬(((singleton h).join φsucΛ).getDual? x).isSome = true } := (Equiv.sumCompl fun a => (((singleton h).join φsucΛ).getDual? a).isSome = true).symma:↥↑φsucΛhjneqsnd:uncontractedListEmd (φsucΛ.sndFieldOfContract a) ≠ jhl:uncontractedListEmd (φsucΛ.fstFieldOfContract a) < uncontractedListEmd (φsucΛ.sndFieldOfContract a)hj1✝:¬¬uncontractedListEmd (φsucΛ.fstFieldOfContract a) < jhj1:uncontractedListEmd (φsucΛ.fstFieldOfContract a) < jhi2✝:¬¬i < uncontractedListEmd (φsucΛ.sndFieldOfContract a)hi2:i < uncontractedListEmd (φsucΛ.sndFieldOfContract a)hi2n:¬uncontractedListEmd (φsucΛ.sndFieldOfContract a) < ihj2✝:j < uncontractedListEmd (φsucΛ.sndFieldOfContract a)hi1✝:¬¬uncontractedListEmd (φsucΛ.fstFieldOfContract a) < ihi1:uncontractedListEmd (φsucΛ.fstFieldOfContract a) < ihj2:¬uncontractedListEmd (φsucΛ.sndFieldOfContract a) < j⊢ Disjoint {j} {i} erw [𝓕:FieldSpecificationφs:List 𝓕.FieldOpi:Fin φs.lengthj:Fin φs.lengthh:i < jhs:(𝓕|>ₛφs[i]) = 𝓕|>ₛφs[j]φsucΛ:WickContraction [singleton h]ᵘᶜ.lengthe2:Fin φs.length ≃ { x // (((singleton h).join φsucΛ).getDual? x).isSome = true } ⊕ { x // ¬(((singleton h).join φsucΛ).getDual? x).isSome = true } := (Equiv.sumCompl fun a => (((singleton h).join φsucΛ).getDual? a).isSome = true).symma:↥↑φsucΛhjneqsnd:uncontractedListEmd (φsucΛ.sndFieldOfContract a) ≠ jhl:uncontractedListEmd (φsucΛ.fstFieldOfContract a) < uncontractedListEmd (φsucΛ.sndFieldOfContract a)hj1✝:¬¬uncontractedListEmd (φsucΛ.fstFieldOfContract a) < jhj1:uncontractedListEmd (φsucΛ.fstFieldOfContract a) < jhi2✝:¬¬i < uncontractedListEmd (φsucΛ.sndFieldOfContract a)hi2:i < uncontractedListEmd (φsucΛ.sndFieldOfContract a)hi2n:¬uncontractedListEmd (φsucΛ.sndFieldOfContract a) < ihj2✝:j < uncontractedListEmd (φsucΛ.sndFieldOfContract a)hi1✝:¬¬uncontractedListEmd (φsucΛ.fstFieldOfContract a) < ihi1:uncontractedListEmd (φsucΛ.fstFieldOfContract a) < ihj2:¬uncontractedListEmd (φsucΛ.sndFieldOfContract a) < j⊢ 1 = (exchangeSign (𝓕|>ₛ[singleton h]ᵘᶜ[↑(φsucΛ.sndFieldOfContract a)])) ((𝓕|>ₛφs[↑j]) * 𝓕|>ₛφs[j])𝓕:FieldSpecificationφs:List 𝓕.FieldOpi:Fin φs.lengthj:Fin φs.lengthh:i < jhs:(𝓕|>ₛφs[i]) = 𝓕|>ₛφs[j]φsucΛ:WickContraction [singleton h]ᵘᶜ.lengthe2:Fin φs.length ≃ { x // (((singleton h).join φsucΛ).getDual? x).isSome = true } ⊕ { x // ¬(((singleton h).join φsucΛ).getDual? x).isSome = true } := (Equiv.sumCompl fun a => (((singleton h).join φsucΛ).getDual? a).isSome = true).symma:↥↑φsucΛhjneqsnd:uncontractedListEmd (φsucΛ.sndFieldOfContract a) ≠ jhl:uncontractedListEmd (φsucΛ.fstFieldOfContract a) < uncontractedListEmd (φsucΛ.sndFieldOfContract a)hj1✝:¬¬uncontractedListEmd (φsucΛ.fstFieldOfContract a) < jhj1:uncontractedListEmd (φsucΛ.fstFieldOfContract a) < jhi2✝:¬¬i < uncontractedListEmd (φsucΛ.sndFieldOfContract a)hi2:i < uncontractedListEmd (φsucΛ.sndFieldOfContract a)hi2n:¬uncontractedListEmd (φsucΛ.sndFieldOfContract a) < ihj2✝:j < uncontractedListEmd (φsucΛ.sndFieldOfContract a)hi1✝:¬¬uncontractedListEmd (φsucΛ.fstFieldOfContract a) < ihi1:uncontractedListEmd (φsucΛ.fstFieldOfContract a) < ihj2:¬uncontractedListEmd (φsucΛ.sndFieldOfContract a) < j⊢ Disjoint {j} {i}𝓕:FieldSpecificationφs:List 𝓕.FieldOpi:Fin φs.lengthj:Fin φs.lengthh:i < jhs:(𝓕|>ₛφs[i]) = 𝓕|>ₛφs[j]φsucΛ:WickContraction [singleton h]ᵘᶜ.lengthe2:Fin φs.length ≃ { x // (((singleton h).join φsucΛ).getDual? x).isSome = true } ⊕ { x // ¬(((singleton h).join φsucΛ).getDual? x).isSome = true } := (Equiv.sumCompl fun a => (((singleton h).join φsucΛ).getDual? a).isSome = true).symma:↥↑φsucΛhjneqsnd:uncontractedListEmd (φsucΛ.sndFieldOfContract a) ≠ jhl:uncontractedListEmd (φsucΛ.fstFieldOfContract a) < uncontractedListEmd (φsucΛ.sndFieldOfContract a)hj1✝:¬¬uncontractedListEmd (φsucΛ.fstFieldOfContract a) < jhj1:uncontractedListEmd (φsucΛ.fstFieldOfContract a) < jhi2✝:¬¬i < uncontractedListEmd (φsucΛ.sndFieldOfContract a)hi2:i < uncontractedListEmd (φsucΛ.sndFieldOfContract a)hi2n:¬uncontractedListEmd (φsucΛ.sndFieldOfContract a) < ihj2✝:j < uncontractedListEmd (φsucΛ.sndFieldOfContract a)hi1✝:¬¬uncontractedListEmd (φsucΛ.fstFieldOfContract a) < ihi1:uncontractedListEmd (φsucΛ.fstFieldOfContract a) < ihj2:¬uncontractedListEmd (φsucΛ.sndFieldOfContract a) < j⊢ 1 = (exchangeSign (𝓕|>ₛ[singleton h]ᵘᶜ[↑(φsucΛ.sndFieldOfContract a)])) ((𝓕|>ₛφs[↑j]) * 𝓕|>ₛφs[j])𝓕:FieldSpecificationφs:List 𝓕.FieldOpi:Fin φs.lengthj:Fin φs.lengthh:i < jhs:(𝓕|>ₛφs[i]) = 𝓕|>ₛφs[j]φsucΛ:WickContraction [singleton h]ᵘᶜ.lengthe2:Fin φs.length ≃ { x // (((singleton h).join φsucΛ).getDual? x).isSome = true } ⊕ { x // ¬(((singleton h).join φsucΛ).getDual? x).isSome = true } := (Equiv.sumCompl fun a => (((singleton h).join φsucΛ).getDual? a).isSome = true).symma:↥↑φsucΛhjneqsnd:uncontractedListEmd (φsucΛ.sndFieldOfContract a) ≠ jhl:uncontractedListEmd (φsucΛ.fstFieldOfContract a) < uncontractedListEmd (φsucΛ.sndFieldOfContract a)hj1✝:¬¬uncontractedListEmd (φsucΛ.fstFieldOfContract a) < jhj1:uncontractedListEmd (φsucΛ.fstFieldOfContract a) < jhi2✝:¬¬i < uncontractedListEmd (φsucΛ.sndFieldOfContract a)hi2:i < uncontractedListEmd (φsucΛ.sndFieldOfContract a)hi2n:¬uncontractedListEmd (φsucΛ.sndFieldOfContract a) < ihj2✝:j < uncontractedListEmd (φsucΛ.sndFieldOfContract a)hi1✝:¬¬uncontractedListEmd (φsucΛ.fstFieldOfContract a) < ihi1:uncontractedListEmd (φsucΛ.fstFieldOfContract a) < ihj2:¬uncontractedListEmd (φsucΛ.sndFieldOfContract a) < j⊢ Disjoint {j} {i} 𝓕:FieldSpecificationφs:List 𝓕.FieldOpi:Fin φs.lengthj:Fin φs.lengthh:i < jhs:(𝓕|>ₛφs[i]) = 𝓕|>ₛφs[j]φsucΛ:WickContraction [singleton h]ᵘᶜ.lengthe2:Fin φs.length ≃ { x // (((singleton h).join φsucΛ).getDual? x).isSome = true } ⊕ { x // ¬(((singleton h).join φsucΛ).getDual? x).isSome = true } := (Equiv.sumCompl fun a => (((singleton h).join φsucΛ).getDual? a).isSome = true).symma:↥↑φsucΛhjneqsnd:uncontractedListEmd (φsucΛ.sndFieldOfContract a) ≠ jhl:uncontractedListEmd (φsucΛ.fstFieldOfContract a) < uncontractedListEmd (φsucΛ.sndFieldOfContract a)hj1✝:¬¬uncontractedListEmd (φsucΛ.fstFieldOfContract a) < jhj1:uncontractedListEmd (φsucΛ.fstFieldOfContract a) < jhi2✝:¬¬i < uncontractedListEmd (φsucΛ.sndFieldOfContract a)hi2:i < uncontractedListEmd (φsucΛ.sndFieldOfContract a)hi2n:¬uncontractedListEmd (φsucΛ.sndFieldOfContract a) < ihj2✝:j < uncontractedListEmd (φsucΛ.sndFieldOfContract a)hi1✝:¬¬uncontractedListEmd (φsucΛ.fstFieldOfContract a) < ihi1:uncontractedListEmd (φsucΛ.fstFieldOfContract a) < ihj2:¬uncontractedListEmd (φsucΛ.sndFieldOfContract a) < j⊢ Disjoint {j} {i} 𝓕:FieldSpecificationφs:List 𝓕.FieldOpi:Fin φs.lengthj:Fin φs.lengthh:i < jhs:(𝓕|>ₛφs[i]) = 𝓕|>ₛφs[j]φsucΛ:WickContraction [singleton h]ᵘᶜ.lengthe2:Fin φs.length ≃ { x // (((singleton h).join φsucΛ).getDual? x).isSome = true } ⊕ { x // ¬(((singleton h).join φsucΛ).getDual? x).isSome = true } := (Equiv.sumCompl fun a => (((singleton h).join φsucΛ).getDual? a).isSome = true).symma:↥↑φsucΛhjneqsnd:uncontractedListEmd (φsucΛ.sndFieldOfContract a) ≠ jhl:uncontractedListEmd (φsucΛ.fstFieldOfContract a) < uncontractedListEmd (φsucΛ.sndFieldOfContract a)hj1✝:¬¬uncontractedListEmd (φsucΛ.fstFieldOfContract a) < jhj1:uncontractedListEmd (φsucΛ.fstFieldOfContract a) < jhi2✝:¬¬i < uncontractedListEmd (φsucΛ.sndFieldOfContract a)hi2:i < uncontractedListEmd (φsucΛ.sndFieldOfContract a)hi2n:¬uncontractedListEmd (φsucΛ.sndFieldOfContract a) < ihj2✝:j < uncontractedListEmd (φsucΛ.sndFieldOfContract a)hi1✝:¬¬uncontractedListEmd (φsucΛ.fstFieldOfContract a) < ihi1:uncontractedListEmd (φsucΛ.fstFieldOfContract a) < ihj2:¬uncontractedListEmd (φsucΛ.sndFieldOfContract a) < j⊢ ¬i = j All goals completed! 🐙𝓕:FieldSpecificationφs:List 𝓕.FieldOpi:Fin φs.lengthj:Fin φs.lengthh:i < jhs:(𝓕|>ₛφs[i]) = 𝓕|>ₛφs[j]φsucΛ:WickContraction [singleton h]ᵘᶜ.lengthh1:joinSignRightExtra h φsucΛ * joinSignRightExtra h φsucΛ = 1⊢ (exchangeSign (𝓕|>ₛφs[((singleton h).join φsucΛ).sndFieldOfContract (joinLiftLeft ⟨{i, j}, ⋯⟩)])) (ofFinset 𝓕.fieldOpStatistic φs.get (((singleton h).join φsucΛ).signFinset (((singleton h).join φsucΛ).fstFieldOfContract (joinLiftLeft ⟨{i, j}, ⋯⟩)) (((singleton h).join φsucΛ).sndFieldOfContract (joinLiftLeft ⟨{i, j}, ⋯⟩)))) = (exchangeSign (𝓕|>ₛφs[↑j])) (ofFinset 𝓕.fieldOpStatistic φs.get (((singleton h).join φsucΛ).signFinset i j)) All goals completed! 🐙 𝓕:FieldSpecificationφs:List 𝓕.FieldOpi:Fin φs.lengthj:Fin φs.lengthh:i < jhs:(𝓕|>ₛφs[i]) = 𝓕|>ₛφs[j]φsucΛ:WickContraction [singleton h]ᵘᶜ.lengthh1:joinSignRightExtra h φsucΛ * joinSignRightExtra h φsucΛ = 1⊢ (fun a => (exchangeSign (𝓕|>ₛφs[((singleton h).join φsucΛ).sndFieldOfContract (joinLiftRight a)])) (ofFinset 𝓕.fieldOpStatistic φs.get (((singleton h).join φsucΛ).signFinset (((singleton h).join φsucΛ).fstFieldOfContract (joinLiftRight a)) (((singleton h).join φsucΛ).sndFieldOfContract (joinLiftRight a))))) = fun x => (exchangeSign (𝓕|>ₛ[singleton h]ᵘᶜ[↑(φsucΛ.sndFieldOfContract x)])) (ofFinset 𝓕.fieldOpStatistic φs.get (((singleton h).join φsucΛ).signFinset (uncontractedListEmd (φsucΛ.fstFieldOfContract x)) (uncontractedListEmd (φsucΛ.sndFieldOfContract x)))) 𝓕:FieldSpecificationφs:List 𝓕.FieldOpi:Fin φs.lengthj:Fin φs.lengthh:i < jhs:(𝓕|>ₛφs[i]) = 𝓕|>ₛφs[j]φsucΛ:WickContraction [singleton h]ᵘᶜ.lengthh1:joinSignRightExtra h φsucΛ * joinSignRightExtra h φsucΛ = 1a:↥↑φsucΛ⊢ (exchangeSign (𝓕|>ₛφs[((singleton h).join φsucΛ).sndFieldOfContract (joinLiftRight a)])) (ofFinset 𝓕.fieldOpStatistic φs.get (((singleton h).join φsucΛ).signFinset (((singleton h).join φsucΛ).fstFieldOfContract (joinLiftRight a)) (((singleton h).join φsucΛ).sndFieldOfContract (joinLiftRight a)))) = (exchangeSign (𝓕|>ₛ[singleton h]ᵘᶜ[↑(φsucΛ.sndFieldOfContract a)])) (ofFinset 𝓕.fieldOpStatistic φs.get (((singleton h).join φsucΛ).signFinset (uncontractedListEmd (φsucΛ.fstFieldOfContract a)) (uncontractedListEmd (φsucΛ.sndFieldOfContract a)))) All goals completed! 🐙𝓕:FieldSpecificationφs:List 𝓕.FieldOpn:ℕi:Fin φs.lengthj:Fin φs.lengthhij:i < jφsucΛ':WickContraction [singleton hij]ᵘᶜ.lengthφsucΛ:WickContraction [(singleton hij).join φsucΛ']ᵘᶜ.lengthhc:GradingCompliant φs ((singleton hij).join φsucΛ')hn✝:(↑((singleton hij).join φsucΛ')).card = n.succh1:(𝓕|>ₛφs[i]) = 𝓕|>ₛφs[j]h2:GradingCompliant [singleton hij]ᵘᶜ φsucΛ'h3:(↑φsucΛ').card + 1 = (↑((singleton hij).join φsucΛ')).cardhn:(↑φsucΛ').card = n⊢ sign φs (singleton hij) * (sign [singleton hij]ᵘᶜ φsucΛ' * sign [φsucΛ']ᵘᶜ ((congr ⋯) φsucΛ)) = sign φs (singleton hij) * (sign [singleton hij]ᵘᶜ φsucΛ' * sign [(singleton hij).join φsucΛ']ᵘᶜ φsucΛ) 𝓕:FieldSpecificationφs:List 𝓕.FieldOpn:ℕi:Fin φs.lengthj:Fin φs.lengthhij:i < jφsucΛ':WickContraction [singleton hij]ᵘᶜ.lengthφsucΛ:WickContraction [(singleton hij).join φsucΛ']ᵘᶜ.lengthhc:GradingCompliant φs ((singleton hij).join φsucΛ')hn✝:(↑((singleton hij).join φsucΛ')).card = n.succh1:(𝓕|>ₛφs[i]) = 𝓕|>ₛφs[j]h2:GradingCompliant [singleton hij]ᵘᶜ φsucΛ'h3:(↑φsucΛ').card + 1 = (↑((singleton hij).join φsucΛ')).cardhn:(↑φsucΛ').card = n⊢ (sign [φsucΛ']ᵘᶜ ((congr ⋯) φsucΛ) = sign [(singleton hij).join φsucΛ']ᵘᶜ φsucΛ ∨ sign [singleton hij]ᵘᶜ φsucΛ' = 0) ∨ sign φs (singleton hij) = 0 𝓕:FieldSpecificationφs:List 𝓕.FieldOpn:ℕi:Fin φs.lengthj:Fin φs.lengthhij:i < jφsucΛ':WickContraction [singleton hij]ᵘᶜ.lengthφsucΛ:WickContraction [(singleton hij).join φsucΛ']ᵘᶜ.lengthhc:GradingCompliant φs ((singleton hij).join φsucΛ')hn✝:(↑((singleton hij).join φsucΛ')).card = n.succh1:(𝓕|>ₛφs[i]) = 𝓕|>ₛφs[j]h2:GradingCompliant [singleton hij]ᵘᶜ φsucΛ'h3:(↑φsucΛ').card + 1 = (↑((singleton hij).join φsucΛ')).cardhn:(↑φsucΛ').card = n⊢ sign [φsucΛ']ᵘᶜ ((congr ⋯) φsucΛ) = sign [(singleton hij).join φsucΛ']ᵘᶜ φsucΛ ∨ sign [singleton hij]ᵘᶜ φsucΛ' = 0 𝓕:FieldSpecificationφs:List 𝓕.FieldOpn:ℕi:Fin φs.lengthj:Fin φs.lengthhij:i < jφsucΛ':WickContraction [singleton hij]ᵘᶜ.lengthφsucΛ:WickContraction [(singleton hij).join φsucΛ']ᵘᶜ.lengthhc:GradingCompliant φs ((singleton hij).join φsucΛ')hn✝:(↑((singleton hij).join φsucΛ')).card = n.succh1:(𝓕|>ₛφs[i]) = 𝓕|>ₛφs[j]h2:GradingCompliant [singleton hij]ᵘᶜ φsucΛ'h3:(↑φsucΛ').card + 1 = (↑((singleton hij).join φsucΛ')).cardhn:(↑φsucΛ').card = n⊢ sign [φsucΛ']ᵘᶜ ((congr ⋯) φsucΛ) = sign [(singleton hij).join φsucΛ']ᵘᶜ φsucΛ 𝓕:FieldSpecificationφs:List 𝓕.FieldOpn:ℕi:Fin φs.lengthj:Fin φs.lengthhij:i < jφsucΛ':WickContraction [singleton hij]ᵘᶜ.lengthφsucΛ:WickContraction [(singleton hij).join φsucΛ']ᵘᶜ.lengthhc:GradingCompliant φs ((singleton hij).join φsucΛ')hn✝:(↑((singleton hij).join φsucΛ')).card = n.succh1:(𝓕|>ₛφs[i]) = 𝓕|>ₛφs[j]h2:GradingCompliant [singleton hij]ᵘᶜ φsucΛ'h3:(↑φsucΛ').card + 1 = (↑((singleton hij).join φsucΛ')).cardhn:(↑φsucΛ').card = n⊢ [(singleton hij).join φsucΛ']ᵘᶜ = [φsucΛ']ᵘᶜ All goals completed! 🐙

For a list φs of 𝓕.FieldOp, a grading compliant Wick contraction φsΛ of φs, and a Wick contraction φsucΛ of [φsΛ]ᵘᶜ, the following relation holds (join φsΛ φsucΛ).sign = φsΛ.sign * φsucΛ.sign.

In φsΛ.sign the sign is determined by starting with the contracted pair whose first element occurs at the left-most position. This lemma manifests that this choice does not matter, and that contracted pairs can be brought together in any order.

lemma join_sign {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) (φsucΛ : WickContraction [φsΛ]ᵘᶜ.length) (hc : φsΛ.GradingCompliant) : (join φsΛ φsucΛ).sign = φsΛ.sign * φsucΛ.sign := join_sign_induction φsΛ φsucΛ hc (φsΛ).1.card rfl

For a list φs of 𝓕.FieldOp, a Wick contraction φsΛ of φs, and a Wick contraction φsucΛ of [φsΛ]ᵘᶜ, (join φsΛ φsucΛ).sign • (join φsΛ φsucΛ).timeContract is equal to the product of

    φsΛ.sign • φsΛ.timeContract and

    φsucΛ.sign • φsucΛ.timeContract.

𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ:WickContraction φs.lengthφsucΛ:WickContraction [φsΛ]ᵘᶜ.lengthh:¬GradingCompliant φs φsΛ⊢ sign φs (φsΛ.join φsucΛ) • ↑(0 * φsucΛ.timeContract) = sign φs φsΛ • ↑0 * sign [φsΛ]ᵘᶜ φsucΛ • ↑φsucΛ.timeContract All goals completed! 🐙