1. Physlib
  2. QFT
  3. PerturbationTheory
  4. WickContraction
  5. Sign
  6. InsertNone
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.Sign.Basic public import Physlib.QFT.PerturbationTheory.WickContraction.InsertAndContract

Sign on inserting and not contracting

@[expose] public section๐“•:FieldSpecificationฯ†:๐“•.FieldOpฯ†s:List ๐“•.FieldOpฯ†sฮ›:WickContraction ฯ†s.lengthi:Fin ฯ†s.length.succi1:Fin ฯ†s.lengthi2:Fin ฯ†s.lengthk:Fin ฯ†s.lengthh1:(Fin.cast โ‹ฏ (i.succAbove k) โˆˆ if i.succAbove i1 < i โˆง i < i.succAbove i2 then insert ((finCongr โ‹ฏ) i) (insertAndContractLiftFinset ฯ† i (ฯ†sฮ›.signFinset i1 i2)) else insertAndContractLiftFinset ฯ† i (ฯ†sฮ›.signFinset i1 i2)) โ†” Fin.cast โ‹ฏ (i.succAbove k) โˆˆ insertAndContractLiftFinset ฯ† i (ฯ†sฮ›.signFinset i1 i2)โŠข i1 < k โˆง k < i2 โˆง (ฯ†sฮ›.getDual? k = none โˆจ โˆ€ (h : (ฯ†sฮ›.getDual? k).isSome = true), Fin.cast โ‹ฏ (i.succAbove i1) < Fin.cast โ‹ฏ (i.succAbove ((ฯ†sฮ›.getDual? k).get โ‹ฏ))) โ†” i1 < k โˆง k < i2 โˆง (ฯ†sฮ›.getDual? k = none โˆจ โˆ€ (h : (ฯ†sฮ›.getDual? k).isSome = true), i1 < (ฯ†sฮ›.getDual? k).get h) ๐“•:FieldSpecificationฯ†:๐“•.FieldOpฯ†s:List ๐“•.FieldOpฯ†sฮ›:WickContraction ฯ†s.lengthi:Fin ฯ†s.length.succi1:Fin ฯ†s.lengthi2:Fin ฯ†s.lengthk:Fin ฯ†s.lengthh1:(Fin.cast โ‹ฏ (i.succAbove k) โˆˆ if i.succAbove i1 < i โˆง i < i.succAbove i2 then insert ((finCongr โ‹ฏ) i) (insertAndContractLiftFinset ฯ† i (ฯ†sฮ›.signFinset i1 i2)) else insertAndContractLiftFinset ฯ† i (ฯ†sฮ›.signFinset i1 i2)) โ†” Fin.cast โ‹ฏ (i.succAbove k) โˆˆ insertAndContractLiftFinset ฯ† i (ฯ†sฮ›.signFinset i1 i2)โŠข i1 < k โ†’ k < i2 โ†’ ((ฯ†sฮ›.getDual? k = none โˆจ โˆ€ (h : (ฯ†sฮ›.getDual? k).isSome = true), Fin.cast โ‹ฏ (i.succAbove i1) < Fin.cast โ‹ฏ (i.succAbove ((ฯ†sฮ›.getDual? k).get โ‹ฏ))) โ†” ฯ†sฮ›.getDual? k = none โˆจ โˆ€ (h : (ฯ†sฮ›.getDual? k).isSome = true), i1 < (ฯ†sฮ›.getDual? k).get h) ๐“•:FieldSpecificationฯ†:๐“•.FieldOpฯ†s:List ๐“•.FieldOpฯ†sฮ›:WickContraction ฯ†s.lengthi:Fin ฯ†s.length.succi1:Fin ฯ†s.lengthi2:Fin ฯ†s.lengthk:Fin ฯ†s.lengthh1โœ:(Fin.cast โ‹ฏ (i.succAbove k) โˆˆ if i.succAbove i1 < i โˆง i < i.succAbove i2 then insert ((finCongr โ‹ฏ) i) (insertAndContractLiftFinset ฯ† i (ฯ†sฮ›.signFinset i1 i2)) else insertAndContractLiftFinset ฯ† i (ฯ†sฮ›.signFinset i1 i2)) โ†” Fin.cast โ‹ฏ (i.succAbove k) โˆˆ insertAndContractLiftFinset ฯ† i (ฯ†sฮ›.signFinset i1 i2)h1:i1 < kh2:k < i2โŠข (ฯ†sฮ›.getDual? k = none โˆจ โˆ€ (h : (ฯ†sฮ›.getDual? k).isSome = true), Fin.cast โ‹ฏ (i.succAbove i1) < Fin.cast โ‹ฏ (i.succAbove ((ฯ†sฮ›.getDual? k).get โ‹ฏ))) โ†” ฯ†sฮ›.getDual? k = none โˆจ โˆ€ (h : (ฯ†sฮ›.getDual? k).isSome = true), i1 < (ฯ†sฮ›.getDual? k).get h conv_lhs => ๐“•:FieldSpecificationฯ†:๐“•.FieldOpฯ†s:List ๐“•.FieldOpฯ†sฮ›:WickContraction ฯ†s.lengthi:Fin ฯ†s.length.succi1:Fin ฯ†s.lengthi2:Fin ฯ†s.lengthk:Fin ฯ†s.lengthh1โœ:(Fin.cast โ‹ฏ (i.succAbove k) โˆˆ if i.succAbove i1 < i โˆง i < i.succAbove i2 then insert ((finCongr โ‹ฏ) i) (insertAndContractLiftFinset ฯ† i (ฯ†sฮ›.signFinset i1 i2)) else insertAndContractLiftFinset ฯ† i (ฯ†sฮ›.signFinset i1 i2)) โ†” Fin.cast โ‹ฏ (i.succAbove k) โˆˆ insertAndContractLiftFinset ฯ† i (ฯ†sฮ›.signFinset i1 i2)h1:i1 < kh2:k < i2| โˆ€ (h : (ฯ†sฮ›.getDual? k).isSome = true), Fin.cast โ‹ฏ (i.succAbove i1) < Fin.cast โ‹ฏ (i.succAbove ((ฯ†sฮ›.getDual? k).get โ‹ฏ)) ๐“•:FieldSpecificationฯ†:๐“•.FieldOpฯ†s:List ๐“•.FieldOpฯ†sฮ›:WickContraction ฯ†s.lengthi:Fin ฯ†s.length.succi1:Fin ฯ†s.lengthi2:Fin ฯ†s.lengthk:Fin ฯ†s.lengthh1โœ:(Fin.cast โ‹ฏ (i.succAbove k) โˆˆ if i.succAbove i1 < i โˆง i < i.succAbove i2 then insert ((finCongr โ‹ฏ) i) (insertAndContractLiftFinset ฯ† i (ฯ†sฮ›.signFinset i1 i2)) else insertAndContractLiftFinset ฯ† i (ฯ†sฮ›.signFinset i1 i2)) โ†” Fin.cast โ‹ฏ (i.succAbove k) โˆˆ insertAndContractLiftFinset ฯ† i (ฯ†sฮ›.signFinset i1 i2)h1:i1 < kh2:k < i2h:(ฯ†sฮ›.getDual? k).isSome = true| Fin.cast โ‹ฏ (i.succAbove i1) < Fin.cast โ‹ฏ (i.succAbove ((ฯ†sฮ›.getDual? k).get โ‹ฏ)) ๐“•:FieldSpecificationฯ†:๐“•.FieldOpฯ†s:List ๐“•.FieldOpฯ†sฮ›:WickContraction ฯ†s.lengthi:Fin ฯ†s.length.succi1:Fin ฯ†s.lengthi2:Fin ฯ†s.lengthk:Fin ฯ†s.lengthh1โœ:(Fin.cast โ‹ฏ (i.succAbove k) โˆˆ if i.succAbove i1 < i โˆง i < i.succAbove i2 then insert ((finCongr โ‹ฏ) i) (insertAndContractLiftFinset ฯ† i (ฯ†sฮ›.signFinset i1 i2)) else insertAndContractLiftFinset ฯ† i (ฯ†sฮ›.signFinset i1 i2)) โ†” Fin.cast โ‹ฏ (i.succAbove k) โˆˆ insertAndContractLiftFinset ฯ† i (ฯ†sฮ›.signFinset i1 i2)h1:i1 < kh2:k < i2h:(ฯ†sฮ›.getDual? k).isSome = true| โ†‘(Fin.cast โ‹ฏ (i.succAbove i1)) < โ†‘(Fin.cast โ‹ฏ (i.succAbove ((ฯ†sฮ›.getDual? k).get โ‹ฏ))) ๐“•:FieldSpecificationฯ†:๐“•.FieldOpฯ†s:List ๐“•.FieldOpฯ†sฮ›:WickContraction ฯ†s.lengthi:Fin ฯ†s.length.succi1:Fin ฯ†s.lengthi2:Fin ฯ†s.lengthk:Fin ฯ†s.lengthh1โœ:(Fin.cast โ‹ฏ (i.succAbove k) โˆˆ if i.succAbove i1 < i โˆง i < i.succAbove i2 then insert ((finCongr โ‹ฏ) i) (insertAndContractLiftFinset ฯ† i (ฯ†sฮ›.signFinset i1 i2)) else insertAndContractLiftFinset ฯ† i (ฯ†sฮ›.signFinset i1 i2)) โ†” Fin.cast โ‹ฏ (i.succAbove k) โˆˆ insertAndContractLiftFinset ฯ† i (ฯ†sฮ›.signFinset i1 i2)h1:i1 < kh2:k < i2h:(ฯ†sฮ›.getDual? k).isSome = true| i.succAbove i1 < i.succAbove ((ฯ†sฮ›.getDual? k).get โ‹ฏ) ๐“•:FieldSpecificationฯ†:๐“•.FieldOpฯ†s:List ๐“•.FieldOpฯ†sฮ›:WickContraction ฯ†s.lengthi:Fin ฯ†s.length.succi1:Fin ฯ†s.lengthi2:Fin ฯ†s.lengthk:Fin ฯ†s.lengthh1โœ:(Fin.cast โ‹ฏ (i.succAbove k) โˆˆ if i.succAbove i1 < i โˆง i < i.succAbove i2 then insert ((finCongr โ‹ฏ) i) (insertAndContractLiftFinset ฯ† i (ฯ†sฮ›.signFinset i1 i2)) else insertAndContractLiftFinset ฯ† i (ฯ†sฮ›.signFinset i1 i2)) โ†” Fin.cast โ‹ฏ (i.succAbove k) โˆˆ insertAndContractLiftFinset ฯ† i (ฯ†sฮ›.signFinset i1 i2)h1:i1 < kh2:k < i2h:(ฯ†sฮ›.getDual? k).isSome = true| i1 < (ฯ†sฮ›.getDual? k).get โ‹ฏ

Given a Wick contraction ฯ†sฮ› associated with a list of states ฯ†s and an i : Fin ฯ†s.length.succ, the change in sign of the contraction associated with inserting ฯ† into ฯ†s at position i without contracting it.

For each contracted pair {a1, a2} in ฯ†sฮ› if a1 < a2 such that i is within the range a1 < i < a2 we pick up a sign equal to ๐“ข(ฯ†, ฯ†s[a2]).

def signInsertNone (ฯ† : ๐“•.FieldOp) (ฯ†s : List ๐“•.FieldOp) (ฯ†sฮ› : WickContraction ฯ†s.length) (i : Fin ฯ†s.length.succ) : โ„‚ := โˆ (a : ฯ†sฮ›.1), if i.succAbove (ฯ†sฮ›.fstFieldOfContract a) < i โˆง i < i.succAbove (ฯ†sฮ›.sndFieldOfContract a) then ๐“ข(๐“• |>โ‚› ฯ†, ๐“• |>โ‚› ฯ†s[ฯ†sฮ›.sndFieldOfContract a]) else 1
All goals completed! ๐Ÿ™๐“•:FieldSpecificationฯ†:๐“•.FieldOpฯ†s:List ๐“•.FieldOpฯ†sฮ›:WickContraction ฯ†s.lengthi:Fin ฯ†s.length.succa:โ†ฅโ†‘ฯ†sฮ›h:i.succAbove (ฯ†sฮ›.fstFieldOfContract a) < i โ†’ i.succAbove (ฯ†sฮ›.sndFieldOfContract a) โ‰ค ih1:i โ‰ค i.succAbove (ฯ†sฮ›.fstFieldOfContract a)โŠข 1 = 1 * 1๐“•:FieldSpecificationฯ†:๐“•.FieldOpฯ†s:List ๐“•.FieldOpฯ†sฮ›:WickContraction ฯ†s.lengthi:Fin ฯ†s.length.succa:โ†ฅโ†‘ฯ†sฮ›h:i.succAbove (ฯ†sฮ›.fstFieldOfContract a) < i โ†’ i.succAbove (ฯ†sฮ›.sndFieldOfContract a) โ‰ค ih1:i โ‰ค i.succAbove (ฯ†sฮ›.fstFieldOfContract a)โŠข ยฌi.succAbove (ฯ†sฮ›.sndFieldOfContract a) < i ๐“•:FieldSpecificationฯ†:๐“•.FieldOpฯ†s:List ๐“•.FieldOpฯ†sฮ›:WickContraction ฯ†s.lengthi:Fin ฯ†s.length.succa:โ†ฅโ†‘ฯ†sฮ›h:i.succAbove (ฯ†sฮ›.fstFieldOfContract a) < i โ†’ i.succAbove (ฯ†sฮ›.sndFieldOfContract a) โ‰ค ih1:i โ‰ค i.succAbove (ฯ†sฮ›.fstFieldOfContract a)โŠข ยฌi.succAbove (ฯ†sฮ›.sndFieldOfContract a) < i ๐“•:FieldSpecificationฯ†:๐“•.FieldOpฯ†s:List ๐“•.FieldOpฯ†sฮ›:WickContraction ฯ†s.lengthi:Fin ฯ†s.length.succa:โ†ฅโ†‘ฯ†sฮ›h:i.succAbove (ฯ†sฮ›.fstFieldOfContract a) < i โ†’ i.succAbove (ฯ†sฮ›.sndFieldOfContract a) โ‰ค ih1:i โ‰ค i.succAbove (ฯ†sฮ›.fstFieldOfContract a)hn:ฯ†sฮ›.fstFieldOfContract a < ฯ†sฮ›.sndFieldOfContract aโŠข ยฌi.succAbove (ฯ†sฮ›.sndFieldOfContract a) < i ๐“•:FieldSpecificationฯ†:๐“•.FieldOpฯ†s:List ๐“•.FieldOpฯ†sฮ›:WickContraction ฯ†s.lengthi:Fin ฯ†s.length.succa:โ†ฅโ†‘ฯ†sฮ›h:i.succAbove (ฯ†sฮ›.fstFieldOfContract a) < i โ†’ i.succAbove (ฯ†sฮ›.sndFieldOfContract a) โ‰ค ih1:i โ‰ค i.succAbove (ฯ†sฮ›.fstFieldOfContract a)hn:ฯ†sฮ›.fstFieldOfContract a < ฯ†sฮ›.sndFieldOfContract ahx:i.succAbove (ฯ†sฮ›.fstFieldOfContract a) < i.succAbove (ฯ†sฮ›.sndFieldOfContract a)โŠข ยฌi.succAbove (ฯ†sฮ›.sndFieldOfContract a) < i All goals completed! ๐Ÿ™All goals completed! ๐Ÿ™๐“•:FieldSpecificationฯ†:๐“•.FieldOpฯ†s:List ๐“•.FieldOpฯ†sฮ›:WickContraction ฯ†s.lengthi:Fin ฯ†s.length.succhG:GradingCompliant ฯ†s ฯ†sฮ›e2:Fin ฯ†s.length โ‰ƒ { x // (ฯ†sฮ›.getDual? x).isSome = true } โŠ• { x // ยฌ(ฯ†sฮ›.getDual? x).isSome = true } := (Equiv.sumCompl fun a => (ฯ†sฮ›.getDual? a).isSome = true).symmโŠข (โˆ i_1, if i.succAbove โ†‘(ฯ†sฮ›.sigmaContractedEquiv.symm i_1).snd < i then (exchangeSign (๐“•|>โ‚›ฯ†)) (๐“•|>โ‚›ฯ†s[โ†‘(ฯ†sฮ›.sigmaContractedEquiv.symm i_1).snd]) else 1) = โˆ i_1, if (ฯ†sฮ›.getDual? (e2.symm i_1)).isSome = true then if i.succAbove (e2.symm i_1) < i then (exchangeSign (๐“•|>โ‚›ฯ†)) (๐“•|>โ‚›ฯ†s[โ†‘(e2.symm i_1)]) else 1 else 1๐“•:FieldSpecificationฯ†:๐“•.FieldOpฯ†s:List ๐“•.FieldOpฯ†sฮ›:WickContraction ฯ†s.lengthi:Fin ฯ†s.length.succhG:GradingCompliant ฯ†s ฯ†sฮ›โŠข GradingCompliant ฯ†s ฯ†sฮ› ๐“•:FieldSpecificationฯ†:๐“•.FieldOpฯ†s:List ๐“•.FieldOpฯ†sฮ›:WickContraction ฯ†s.lengthi:Fin ฯ†s.length.succhG:GradingCompliant ฯ†s ฯ†sฮ›e2:Fin ฯ†s.length โ‰ƒ { x // (ฯ†sฮ›.getDual? x).isSome = true } โŠ• { x // ยฌ(ฯ†sฮ›.getDual? x).isSome = true } := (Equiv.sumCompl fun a => (ฯ†sฮ›.getDual? a).isSome = true).symmโŠข (โˆ x, if i.succAbove โ†‘(ฯ†sฮ›.sigmaContractedEquiv.symm x).snd < i then (exchangeSign (๐“•|>โ‚›ฯ†)) (๐“•|>โ‚›ฯ†s[โ†‘โ†‘(ฯ†sฮ›.sigmaContractedEquiv.symm x).snd]) else 1) = (โˆ aโ‚, if (ฯ†sฮ›.getDual? (e2.symm (Sum.inl aโ‚))).isSome = true then if i.succAbove (e2.symm (Sum.inl aโ‚)) < i then (exchangeSign (๐“•|>โ‚›ฯ†)) (๐“•|>โ‚›ฯ†s[โ†‘(e2.symm (Sum.inl aโ‚))]) else 1 else 1) * โˆ aโ‚‚, if (ฯ†sฮ›.getDual? (e2.symm (Sum.inr aโ‚‚))).isSome = true then if i.succAbove (e2.symm (Sum.inr aโ‚‚)) < i then (exchangeSign (๐“•|>โ‚›ฯ†)) (๐“•|>โ‚›ฯ†s[โ†‘(e2.symm (Sum.inr aโ‚‚))]) else 1 else 1๐“•:FieldSpecificationฯ†:๐“•.FieldOpฯ†s:List ๐“•.FieldOpฯ†sฮ›:WickContraction ฯ†s.lengthi:Fin ฯ†s.length.succhG:GradingCompliant ฯ†s ฯ†sฮ›โŠข GradingCompliant ฯ†s ฯ†sฮ› conv_rhs => ๐“•:FieldSpecificationฯ†:๐“•.FieldOpฯ†s:List ๐“•.FieldOpฯ†sฮ›:WickContraction ฯ†s.lengthi:Fin ฯ†s.length.succhG:GradingCompliant ฯ†s ฯ†sฮ›e2:Fin ฯ†s.length โ‰ƒ { x // (ฯ†sฮ›.getDual? x).isSome = true } โŠ• { x // ยฌ(ฯ†sฮ›.getDual? x).isSome = true } := (Equiv.sumCompl fun a => (ฯ†sฮ›.getDual? a).isSome = true).symm| โˆ aโ‚‚, if (ฯ†sฮ›.getDual? (e2.symm (Sum.inr aโ‚‚))).isSome = true then if i.succAbove (e2.symm (Sum.inr aโ‚‚)) < i then (exchangeSign (๐“•|>โ‚›ฯ†)) (๐“•|>โ‚›ฯ†s[โ†‘(e2.symm (Sum.inr aโ‚‚))]) else 1 else 1 ๐“•:FieldSpecificationฯ†:๐“•.FieldOpฯ†s:List ๐“•.FieldOpฯ†sฮ›:WickContraction ฯ†s.lengthi:Fin ฯ†s.length.succhG:GradingCompliant ฯ†s ฯ†sฮ›e2:Fin ฯ†s.length โ‰ƒ { x // (ฯ†sฮ›.getDual? x).isSome = true } โŠ• { x // ยฌ(ฯ†sฮ›.getDual? x).isSome = true } := (Equiv.sumCompl fun a => (ฯ†sฮ›.getDual? a).isSome = true).symma:{ x // ยฌ(ฯ†sฮ›.getDual? x).isSome = true }| if (ฯ†sฮ›.getDual? (e2.symm (Sum.inr a))).isSome = true then if i.succAbove (e2.symm (Sum.inr a)) < i then (exchangeSign (๐“•|>โ‚›ฯ†)) (๐“•|>โ‚›ฯ†s[โ†‘(e2.symm (Sum.inr a))]) else 1 else 1 rw [if_neg (๐“•:FieldSpecificationฯ†:๐“•.FieldOpฯ†s:List ๐“•.FieldOpฯ†sฮ›:WickContraction ฯ†s.lengthi:Fin ฯ†s.length.succhG:GradingCompliant ฯ†s ฯ†sฮ›e2:Fin ฯ†s.length โ‰ƒ { x // (ฯ†sฮ›.getDual? x).isSome = true } โŠ• { x // ยฌ(ฯ†sฮ›.getDual? x).isSome = true } := (Equiv.sumCompl fun a => (ฯ†sฮ›.getDual? a).isSome = true).symma:{ x // ยฌ(ฯ†sฮ›.getDual? x).isSome = true }โŠข ยฌ(ฯ†sฮ›.getDual? (e2.symm (Sum.inr a))).isSome = true All goals completed! ๐Ÿ™)] conv_rhs => ๐“•:FieldSpecificationฯ†:๐“•.FieldOpฯ†s:List ๐“•.FieldOpฯ†sฮ›:WickContraction ฯ†s.lengthi:Fin ฯ†s.length.succhG:GradingCompliant ฯ†s ฯ†sฮ›e2:Fin ฯ†s.length โ‰ƒ { x // (ฯ†sฮ›.getDual? x).isSome = true } โŠ• { x // ยฌ(ฯ†sฮ›.getDual? x).isSome = true } := (Equiv.sumCompl fun a => (ฯ†sฮ›.getDual? a).isSome = true).symm| โˆ aโ‚, if (ฯ†sฮ›.getDual? (e2.symm (Sum.inl aโ‚))).isSome = true then if i.succAbove (e2.symm (Sum.inl aโ‚)) < i then (exchangeSign (๐“•|>โ‚›ฯ†)) (๐“•|>โ‚›ฯ†s[โ†‘(e2.symm (Sum.inl aโ‚))]) else 1 else 1 ๐“•:FieldSpecificationฯ†:๐“•.FieldOpฯ†s:List ๐“•.FieldOpฯ†sฮ›:WickContraction ฯ†s.lengthi:Fin ฯ†s.length.succhG:GradingCompliant ฯ†s ฯ†sฮ›e2:Fin ฯ†s.length โ‰ƒ { x // (ฯ†sฮ›.getDual? x).isSome = true } โŠ• { x // ยฌ(ฯ†sฮ›.getDual? x).isSome = true } := (Equiv.sumCompl fun a => (ฯ†sฮ›.getDual? a).isSome = true).symma:{ x // (ฯ†sฮ›.getDual? x).isSome = true }| if (ฯ†sฮ›.getDual? (e2.symm (Sum.inl a))).isSome = true then if i.succAbove (e2.symm (Sum.inl a)) < i then (exchangeSign (๐“•|>โ‚›ฯ†)) (๐“•|>โ‚›ฯ†s[โ†‘(e2.symm (Sum.inl a))]) else 1 else 1 rw [if_pos (๐“•:FieldSpecificationฯ†:๐“•.FieldOpฯ†s:List ๐“•.FieldOpฯ†sฮ›:WickContraction ฯ†s.lengthi:Fin ฯ†s.length.succhG:GradingCompliant ฯ†s ฯ†sฮ›e2:Fin ฯ†s.length โ‰ƒ { x // (ฯ†sฮ›.getDual? x).isSome = true } โŠ• { x // ยฌ(ฯ†sฮ›.getDual? x).isSome = true } := (Equiv.sumCompl fun a => (ฯ†sฮ›.getDual? a).isSome = true).symma:{ x // (ฯ†sฮ›.getDual? x).isSome = true }โŠข (ฯ†sฮ›.getDual? (e2.symm (Sum.inl a))).isSome = true All goals completed! ๐Ÿ™)] ๐“•:FieldSpecificationฯ†:๐“•.FieldOpฯ†s:List ๐“•.FieldOpฯ†sฮ›:WickContraction ฯ†s.lengthi:Fin ฯ†s.length.succhG:GradingCompliant ฯ†s ฯ†sฮ›e2:Fin ฯ†s.length โ‰ƒ { x // (ฯ†sฮ›.getDual? x).isSome = true } โŠ• { x // ยฌ(ฯ†sฮ›.getDual? x).isSome = true } := (Equiv.sumCompl fun a => (ฯ†sฮ›.getDual? a).isSome = true).symmโŠข (โˆ x, if i.succAbove โ†‘(ฯ†sฮ›.sigmaContractedEquiv.symm x).snd < i then (exchangeSign (๐“•|>โ‚›ฯ†)) (๐“•|>โ‚›ฯ†s[โ†‘โ†‘(ฯ†sฮ›.sigmaContractedEquiv.symm x).snd]) else 1) = โˆ x, if i.succAbove โ†‘x < i then (exchangeSign (๐“•|>โ‚›ฯ†)) (๐“•|>โ‚›ฯ†s[โ†‘โ†‘x]) else 1๐“•:FieldSpecificationฯ†:๐“•.FieldOpฯ†s:List ๐“•.FieldOpฯ†sฮ›:WickContraction ฯ†s.lengthi:Fin ฯ†s.length.succhG:GradingCompliant ฯ†s ฯ†sฮ›โŠข GradingCompliant ฯ†s ฯ†sฮ› ๐“•:FieldSpecificationฯ†:๐“•.FieldOpฯ†s:List ๐“•.FieldOpฯ†sฮ›:WickContraction ฯ†s.lengthi:Fin ฯ†s.length.succhG:GradingCompliant ฯ†s ฯ†sฮ›โŠข GradingCompliant ฯ†s ฯ†sฮ› All goals completed! ๐Ÿ™๐“•:FieldSpecificationฯ†:๐“•.FieldOpฯ†s:List ๐“•.FieldOpฯ†sฮ›:WickContraction ฯ†s.lengthi:Fin ฯ†s.length.succhG:GradingCompliant ฯ†s ฯ†sฮ›โŠข (โˆ x, if (ฯ†sฮ›.getDual? x).isSome = true then if i.succAbove x < i then (exchangeSign (๐“•|>โ‚›ฯ†)) (๐“•|>โ‚›ฯ†s[โ†‘x]) else 1 else 1) = โˆ x, (exchangeSign (๐“•|>โ‚›ฯ†)) (if x โˆˆ List.filter (fun x => decide ((ฯ†sฮ›.getDual? x).isSome = true โˆง i.succAbove x < i)) (List.finRange ฯ†s.length) then ๐“•|>โ‚›ฯ†s[x] else 1)๐“•:FieldSpecificationฯ†:๐“•.FieldOpฯ†s:List ๐“•.FieldOpฯ†sฮ›:WickContraction ฯ†s.lengthi:Fin ฯ†s.length.succhG:GradingCompliant ฯ†s ฯ†sฮ›โŠข (List.filter (fun x => decide ((ฯ†sฮ›.getDual? x).isSome = true โˆง i.succAbove x < i)) (List.finRange ฯ†s.length)).Nodup๐“•:FieldSpecificationฯ†:๐“•.FieldOpฯ†s:List ๐“•.FieldOpฯ†sฮ›:WickContraction ฯ†s.lengthi:Fin ฯ†s.length.succhG:GradingCompliant ฯ†s ฯ†sฮ›โŠข GradingCompliant ฯ†s ฯ†sฮ› ๐“•:FieldSpecificationฯ†:๐“•.FieldOpฯ†s:List ๐“•.FieldOpฯ†sฮ›:WickContraction ฯ†s.lengthi:Fin ฯ†s.length.succhG:GradingCompliant ฯ†s ฯ†sฮ›โŠข (fun x => if (ฯ†sฮ›.getDual? x).isSome = true then if i.succAbove x < i then (exchangeSign (๐“•|>โ‚›ฯ†)) (๐“•|>โ‚›ฯ†s[โ†‘x]) else 1 else 1) = fun x => (exchangeSign (๐“•|>โ‚›ฯ†)) (if x โˆˆ List.filter (fun x => decide ((ฯ†sฮ›.getDual? x).isSome = true โˆง i.succAbove x < i)) (List.finRange ฯ†s.length) then ๐“•|>โ‚›ฯ†s[x] else 1)๐“•:FieldSpecificationฯ†:๐“•.FieldOpฯ†s:List ๐“•.FieldOpฯ†sฮ›:WickContraction ฯ†s.lengthi:Fin ฯ†s.length.succhG:GradingCompliant ฯ†s ฯ†sฮ›โŠข (List.filter (fun x => decide ((ฯ†sฮ›.getDual? x).isSome = true โˆง i.succAbove x < i)) (List.finRange ฯ†s.length)).Nodup๐“•:FieldSpecificationฯ†:๐“•.FieldOpฯ†s:List ๐“•.FieldOpฯ†sฮ›:WickContraction ฯ†s.lengthi:Fin ฯ†s.length.succhG:GradingCompliant ฯ†s ฯ†sฮ›โŠข GradingCompliant ฯ†s ฯ†sฮ› ๐“•:FieldSpecificationฯ†:๐“•.FieldOpฯ†s:List ๐“•.FieldOpฯ†sฮ›:WickContraction ฯ†s.lengthi:Fin ฯ†s.length.succhG:GradingCompliant ฯ†s ฯ†sฮ›a:Fin ฯ†s.lengthโŠข (if (ฯ†sฮ›.getDual? a).isSome = true then if i.succAbove a < i then (exchangeSign (๐“•|>โ‚›ฯ†)) (๐“•|>โ‚›ฯ†s[โ†‘a]) else 1 else 1) = (exchangeSign (๐“•|>โ‚›ฯ†)) (if a โˆˆ List.filter (fun x => decide ((ฯ†sฮ›.getDual? x).isSome = true โˆง i.succAbove x < i)) (List.finRange ฯ†s.length) then ๐“•|>โ‚›ฯ†s[a] else 1)๐“•:FieldSpecificationฯ†:๐“•.FieldOpฯ†s:List ๐“•.FieldOpฯ†sฮ›:WickContraction ฯ†s.lengthi:Fin ฯ†s.length.succhG:GradingCompliant ฯ†s ฯ†sฮ›โŠข (List.filter (fun x => decide ((ฯ†sฮ›.getDual? x).isSome = true โˆง i.succAbove x < i)) (List.finRange ฯ†s.length)).Nodup๐“•:FieldSpecificationฯ†:๐“•.FieldOpฯ†s:List ๐“•.FieldOpฯ†sฮ›:WickContraction ฯ†s.lengthi:Fin ฯ†s.length.succhG:GradingCompliant ฯ†s ฯ†sฮ›โŠข GradingCompliant ฯ†s ฯ†sฮ› ๐“•:FieldSpecificationฯ†:๐“•.FieldOpฯ†s:List ๐“•.FieldOpฯ†sฮ›:WickContraction ฯ†s.lengthi:Fin ฯ†s.length.succhG:GradingCompliant ฯ†s ฯ†sฮ›a:Fin ฯ†s.lengthโŠข (if (ฯ†sฮ›.getDual? a).isSome = true then if i.succAbove a < i then (exchangeSign (๐“•|>โ‚›ฯ†)) (๐“•|>โ‚›ฯ†s[โ†‘a]) else 1 else 1) = (exchangeSign (๐“•|>โ‚›ฯ†)) (if (ฯ†sฮ›.getDual? a).isSome = true โˆง i.succAbove a < i then ๐“•|>โ‚›ฯ†s[โ†‘a] else 1)๐“•:FieldSpecificationฯ†:๐“•.FieldOpฯ†s:List ๐“•.FieldOpฯ†sฮ›:WickContraction ฯ†s.lengthi:Fin ฯ†s.length.succhG:GradingCompliant ฯ†s ฯ†sฮ›โŠข (List.filter (fun x => decide ((ฯ†sฮ›.getDual? x).isSome = true โˆง i.succAbove x < i)) (List.finRange ฯ†s.length)).Nodup๐“•:FieldSpecificationฯ†:๐“•.FieldOpฯ†s:List ๐“•.FieldOpฯ†sฮ›:WickContraction ฯ†s.lengthi:Fin ฯ†s.length.succhG:GradingCompliant ฯ†s ฯ†sฮ›โŠข GradingCompliant ฯ†s ฯ†sฮ› ๐“•:FieldSpecificationฯ†:๐“•.FieldOpฯ†s:List ๐“•.FieldOpฯ†sฮ›:WickContraction ฯ†s.lengthi:Fin ฯ†s.length.succhG:GradingCompliant ฯ†s ฯ†sฮ›a:Fin ฯ†s.lengthhโœ:(ฯ†sฮ›.getDual? a).isSome = trueโŠข (if i.succAbove a < i then (exchangeSign (๐“•|>โ‚›ฯ†)) (๐“•|>โ‚›ฯ†s[โ†‘a]) else 1) = (exchangeSign (๐“•|>โ‚›ฯ†)) (if (ฯ†sฮ›.getDual? a).isSome = true โˆง i.succAbove a < i then ๐“•|>โ‚›ฯ†s[โ†‘a] else 1)๐“•:FieldSpecificationฯ†:๐“•.FieldOpฯ†s:List ๐“•.FieldOpฯ†sฮ›:WickContraction ฯ†s.lengthi:Fin ฯ†s.length.succhG:GradingCompliant ฯ†s ฯ†sฮ›a:Fin ฯ†s.lengthhโœ:ยฌ(ฯ†sฮ›.getDual? a).isSome = trueโŠข 1 = (exchangeSign (๐“•|>โ‚›ฯ†)) (if (ฯ†sฮ›.getDual? a).isSome = true โˆง i.succAbove a < i then ๐“•|>โ‚›ฯ†s[โ†‘a] else 1)๐“•:FieldSpecificationฯ†:๐“•.FieldOpฯ†s:List ๐“•.FieldOpฯ†sฮ›:WickContraction ฯ†s.lengthi:Fin ฯ†s.length.succhG:GradingCompliant ฯ†s ฯ†sฮ›โŠข (List.filter (fun x => decide ((ฯ†sฮ›.getDual? x).isSome = true โˆง i.succAbove x < i)) (List.finRange ฯ†s.length)).Nodup๐“•:FieldSpecificationฯ†:๐“•.FieldOpฯ†s:List ๐“•.FieldOpฯ†sฮ›:WickContraction ฯ†s.lengthi:Fin ฯ†s.length.succhG:GradingCompliant ฯ†s ฯ†sฮ›โŠข GradingCompliant ฯ†s ฯ†sฮ› ๐“•:FieldSpecificationฯ†:๐“•.FieldOpฯ†s:List ๐“•.FieldOpฯ†sฮ›:WickContraction ฯ†s.lengthi:Fin ฯ†s.length.succhG:GradingCompliant ฯ†s ฯ†sฮ›a:Fin ฯ†s.lengthhโœ:(ฯ†sฮ›.getDual? a).isSome = trueโŠข (if i.succAbove a < i then (exchangeSign (๐“•|>โ‚›ฯ†)) (๐“•|>โ‚›ฯ†s[โ†‘a]) else 1) = (exchangeSign (๐“•|>โ‚›ฯ†)) (if (ฯ†sฮ›.getDual? a).isSome = true โˆง i.succAbove a < i then ๐“•|>โ‚›ฯ†s[โ†‘a] else 1) ๐“•:FieldSpecificationฯ†:๐“•.FieldOpฯ†s:List ๐“•.FieldOpฯ†sฮ›:WickContraction ฯ†s.lengthi:Fin ฯ†s.length.succhG:GradingCompliant ฯ†s ฯ†sฮ›a:Fin ฯ†s.lengthh:(ฯ†sฮ›.getDual? a).isSome = trueโŠข (if i.succAbove a < i then (exchangeSign (๐“•|>โ‚›ฯ†)) (๐“•|>โ‚›ฯ†s[โ†‘a]) else 1) = (exchangeSign (๐“•|>โ‚›ฯ†)) (if (ฯ†sฮ›.getDual? a).isSome = true โˆง i.succAbove a < i then ๐“•|>โ‚›ฯ†s[โ†‘a] else 1) ๐“•:FieldSpecificationฯ†:๐“•.FieldOpฯ†s:List ๐“•.FieldOpฯ†sฮ›:WickContraction ฯ†s.lengthi:Fin ฯ†s.length.succhG:GradingCompliant ฯ†s ฯ†sฮ›a:Fin ฯ†s.lengthh:(ฯ†sฮ›.getDual? a).isSome = trueโŠข (if i.succAbove a < i then (exchangeSign (๐“•|>โ‚›ฯ†)) (๐“•|>โ‚›ฯ†s[โ†‘a]) else 1) = (exchangeSign (๐“•|>โ‚›ฯ†)) (if i.succAbove a < i then ๐“•|>โ‚›ฯ†s[โ†‘a] else 1) ๐“•:FieldSpecificationฯ†:๐“•.FieldOpฯ†s:List ๐“•.FieldOpฯ†sฮ›:WickContraction ฯ†s.lengthi:Fin ฯ†s.length.succhG:GradingCompliant ฯ†s ฯ†sฮ›a:Fin ฯ†s.lengthh:(ฯ†sฮ›.getDual? a).isSome = truehโœ:i.succAbove a < iโŠข (exchangeSign (๐“•|>โ‚›ฯ†)) (๐“•|>โ‚›ฯ†s[โ†‘a]) = (exchangeSign (๐“•|>โ‚›ฯ†)) (๐“•|>โ‚›ฯ†s[โ†‘a])๐“•:FieldSpecificationฯ†:๐“•.FieldOpฯ†s:List ๐“•.FieldOpฯ†sฮ›:WickContraction ฯ†s.lengthi:Fin ฯ†s.length.succhG:GradingCompliant ฯ†s ฯ†sฮ›a:Fin ฯ†s.lengthh:(ฯ†sฮ›.getDual? a).isSome = truehโœ:ยฌi.succAbove a < iโŠข 1 = (exchangeSign (๐“•|>โ‚›ฯ†)) 1 ๐“•:FieldSpecificationฯ†:๐“•.FieldOpฯ†s:List ๐“•.FieldOpฯ†sฮ›:WickContraction ฯ†s.lengthi:Fin ฯ†s.length.succhG:GradingCompliant ฯ†s ฯ†sฮ›a:Fin ฯ†s.lengthh:(ฯ†sฮ›.getDual? a).isSome = truehโœ:i.succAbove a < iโŠข (exchangeSign (๐“•|>โ‚›ฯ†)) (๐“•|>โ‚›ฯ†s[โ†‘a]) = (exchangeSign (๐“•|>โ‚›ฯ†)) (๐“•|>โ‚›ฯ†s[โ†‘a]) All goals completed! ๐Ÿ™ ๐“•:FieldSpecificationฯ†:๐“•.FieldOpฯ†s:List ๐“•.FieldOpฯ†sฮ›:WickContraction ฯ†s.lengthi:Fin ฯ†s.length.succhG:GradingCompliant ฯ†s ฯ†sฮ›a:Fin ฯ†s.lengthh:(ฯ†sฮ›.getDual? a).isSome = truehโœ:ยฌi.succAbove a < iโŠข 1 = (exchangeSign (๐“•|>โ‚›ฯ†)) 1 All goals completed! ๐Ÿ™ ๐“•:FieldSpecificationฯ†:๐“•.FieldOpฯ†s:List ๐“•.FieldOpฯ†sฮ›:WickContraction ฯ†s.lengthi:Fin ฯ†s.length.succhG:GradingCompliant ฯ†s ฯ†sฮ›a:Fin ฯ†s.lengthhโœ:ยฌ(ฯ†sฮ›.getDual? a).isSome = trueโŠข 1 = (exchangeSign (๐“•|>โ‚›ฯ†)) (if (ฯ†sฮ›.getDual? a).isSome = true โˆง i.succAbove a < i then ๐“•|>โ‚›ฯ†s[โ†‘a] else 1) ๐“•:FieldSpecificationฯ†:๐“•.FieldOpฯ†s:List ๐“•.FieldOpฯ†sฮ›:WickContraction ฯ†s.lengthi:Fin ฯ†s.length.succhG:GradingCompliant ฯ†s ฯ†sฮ›a:Fin ฯ†s.lengthh:ยฌ(ฯ†sฮ›.getDual? a).isSome = trueโŠข 1 = (exchangeSign (๐“•|>โ‚›ฯ†)) (if (ฯ†sฮ›.getDual? a).isSome = true โˆง i.succAbove a < i then ๐“•|>โ‚›ฯ†s[โ†‘a] else 1) All goals completed! ๐Ÿ™ ๐“•:FieldSpecificationฯ†:๐“•.FieldOpฯ†s:List ๐“•.FieldOpฯ†sฮ›:WickContraction ฯ†s.lengthi:Fin ฯ†s.length.succhG:GradingCompliant ฯ†s ฯ†sฮ›โŠข (List.filter (fun x => decide ((ฯ†sฮ›.getDual? x).isSome = true โˆง i.succAbove x < i)) (List.finRange ฯ†s.length)).Nodup ๐“•:FieldSpecificationฯ†:๐“•.FieldOpฯ†s:List ๐“•.FieldOpฯ†sฮ›:WickContraction ฯ†s.lengthi:Fin ฯ†s.length.succhG:GradingCompliant ฯ†s ฯ†sฮ›โŠข (List.finRange ฯ†s.length).Nodup All goals completed! ๐Ÿ™ ๐“•:FieldSpecificationฯ†:๐“•.FieldOpฯ†s:List ๐“•.FieldOpฯ†sฮ›:WickContraction ฯ†s.lengthi:Fin ฯ†s.length.succhG:GradingCompliant ฯ†s ฯ†sฮ›โŠข GradingCompliant ฯ†s ฯ†sฮ› All goals completed! ๐Ÿ™

The following signs for a grading compliant Wick contraction are equal:

    The sign ฯ†sฮ›.signInsertNone ฯ† ฯ†s i which is given by the following: For each contracted pair {a1, a2} in ฯ†sฮ› if a1 < a2 such that i is within the range a1 < i < a2 we pick up a sign equal to ๐“ข(ฯ†, ฯ†s[a2]).

    The sign got by moving ฯ† through ฯ†โ‚€โ€ฆฯ†แตขโ‚‹โ‚ and only picking up a sign when ฯ†แตข has a dual. These are equal since: Both ignore uncontracted fields, and for a contracted pair {a1, a2} with a1 < a2

    if i < a1 < a2 then we don't pick up a sign from either ฯ†โ‚โ‚ or ฯ†โ‚โ‚‚.

    if a1 < i < a2 then we pick up a sign from ฯ†โ‚โ‚ cases which is equal to ๐“ข(ฯ†, ฯ†s[a2]) (since ฯ†sฮ› is grading compliant).

    if a1 < a2 < i then we pick up a sign from both ฯ†โ‚โ‚ and ฯ†โ‚โ‚‚ which cancel each other out.

๐“•:FieldSpecificationฯ†:๐“•.FieldOpฯ†s:List ๐“•.FieldOpฯ†sฮ›:WickContraction ฯ†s.lengthi:Fin ฯ†s.length.succhG:GradingCompliant ฯ†s ฯ†sฮ›โŠข (โˆ x, if (ฯ†sฮ›.getDual? x).isSome = true then if i.succAbove x < i then (exchangeSign (๐“•|>โ‚›ฯ†)) (๐“•|>โ‚›ฯ†s[โ†‘x]) else 1 else 1) = โˆ x, (exchangeSign (๐“•|>โ‚›ฯ†)) (if x โˆˆ {x | (ฯ†sฮ›.getDual? x).isSome = true โˆง i.succAbove x < i} then ๐“•|>โ‚›ฯ†s[x] else 1)๐“•:FieldSpecificationฯ†:๐“•.FieldOpฯ†s:List ๐“•.FieldOpฯ†sฮ›:WickContraction ฯ†s.lengthi:Fin ฯ†s.length.succhG:GradingCompliant ฯ†s ฯ†sฮ›โŠข GradingCompliant ฯ†s ฯ†sฮ› ๐“•:FieldSpecificationฯ†:๐“•.FieldOpฯ†s:List ๐“•.FieldOpฯ†sฮ›:WickContraction ฯ†s.lengthi:Fin ฯ†s.length.succhG:GradingCompliant ฯ†s ฯ†sฮ›โŠข (fun x => if (ฯ†sฮ›.getDual? x).isSome = true then if i.succAbove x < i then (exchangeSign (๐“•|>โ‚›ฯ†)) (๐“•|>โ‚›ฯ†s[โ†‘x]) else 1 else 1) = fun x => (exchangeSign (๐“•|>โ‚›ฯ†)) (if x โˆˆ {x | (ฯ†sฮ›.getDual? x).isSome = true โˆง i.succAbove x < i} then ๐“•|>โ‚›ฯ†s[x] else 1)๐“•:FieldSpecificationฯ†:๐“•.FieldOpฯ†s:List ๐“•.FieldOpฯ†sฮ›:WickContraction ฯ†s.lengthi:Fin ฯ†s.length.succhG:GradingCompliant ฯ†s ฯ†sฮ›โŠข GradingCompliant ฯ†s ฯ†sฮ› ๐“•:FieldSpecificationฯ†:๐“•.FieldOpฯ†s:List ๐“•.FieldOpฯ†sฮ›:WickContraction ฯ†s.lengthi:Fin ฯ†s.length.succhG:GradingCompliant ฯ†s ฯ†sฮ›a:Fin ฯ†s.lengthโŠข (if (ฯ†sฮ›.getDual? a).isSome = true then if i.succAbove a < i then (exchangeSign (๐“•|>โ‚›ฯ†)) (๐“•|>โ‚›ฯ†s[โ†‘a]) else 1 else 1) = (exchangeSign (๐“•|>โ‚›ฯ†)) (if a โˆˆ {x | (ฯ†sฮ›.getDual? x).isSome = true โˆง i.succAbove x < i} then ๐“•|>โ‚›ฯ†s[a] else 1)๐“•:FieldSpecificationฯ†:๐“•.FieldOpฯ†s:List ๐“•.FieldOpฯ†sฮ›:WickContraction ฯ†s.lengthi:Fin ฯ†s.length.succhG:GradingCompliant ฯ†s ฯ†sฮ›โŠข GradingCompliant ฯ†s ฯ†sฮ› ๐“•:FieldSpecificationฯ†:๐“•.FieldOpฯ†s:List ๐“•.FieldOpฯ†sฮ›:WickContraction ฯ†s.lengthi:Fin ฯ†s.length.succhG:GradingCompliant ฯ†s ฯ†sฮ›a:Fin ฯ†s.lengthโŠข (if (ฯ†sฮ›.getDual? a).isSome = true then if i.succAbove a < i then (exchangeSign (๐“•|>โ‚›ฯ†)) (๐“•|>โ‚›ฯ†s[โ†‘a]) else 1 else 1) = (exchangeSign (๐“•|>โ‚›ฯ†)) (if (ฯ†sฮ›.getDual? a).isSome = true โˆง i.succAbove a < i then ๐“•|>โ‚›ฯ†s[โ†‘a] else 1)๐“•:FieldSpecificationฯ†:๐“•.FieldOpฯ†s:List ๐“•.FieldOpฯ†sฮ›:WickContraction ฯ†s.lengthi:Fin ฯ†s.length.succhG:GradingCompliant ฯ†s ฯ†sฮ›โŠข GradingCompliant ฯ†s ฯ†sฮ› ๐“•:FieldSpecificationฯ†:๐“•.FieldOpฯ†s:List ๐“•.FieldOpฯ†sฮ›:WickContraction ฯ†s.lengthi:Fin ฯ†s.length.succhG:GradingCompliant ฯ†s ฯ†sฮ›a:Fin ฯ†s.lengthhโœ:(ฯ†sฮ›.getDual? a).isSome = trueโŠข (if i.succAbove a < i then (exchangeSign (๐“•|>โ‚›ฯ†)) (๐“•|>โ‚›ฯ†s[โ†‘a]) else 1) = (exchangeSign (๐“•|>โ‚›ฯ†)) (if (ฯ†sฮ›.getDual? a).isSome = true โˆง i.succAbove a < i then ๐“•|>โ‚›ฯ†s[โ†‘a] else 1)๐“•:FieldSpecificationฯ†:๐“•.FieldOpฯ†s:List ๐“•.FieldOpฯ†sฮ›:WickContraction ฯ†s.lengthi:Fin ฯ†s.length.succhG:GradingCompliant ฯ†s ฯ†sฮ›a:Fin ฯ†s.lengthhโœ:ยฌ(ฯ†sฮ›.getDual? a).isSome = trueโŠข 1 = (exchangeSign (๐“•|>โ‚›ฯ†)) (if (ฯ†sฮ›.getDual? a).isSome = true โˆง i.succAbove a < i then ๐“•|>โ‚›ฯ†s[โ†‘a] else 1)๐“•:FieldSpecificationฯ†:๐“•.FieldOpฯ†s:List ๐“•.FieldOpฯ†sฮ›:WickContraction ฯ†s.lengthi:Fin ฯ†s.length.succhG:GradingCompliant ฯ†s ฯ†sฮ›โŠข GradingCompliant ฯ†s ฯ†sฮ› ๐“•:FieldSpecificationฯ†:๐“•.FieldOpฯ†s:List ๐“•.FieldOpฯ†sฮ›:WickContraction ฯ†s.lengthi:Fin ฯ†s.length.succhG:GradingCompliant ฯ†s ฯ†sฮ›a:Fin ฯ†s.lengthhโœ:(ฯ†sฮ›.getDual? a).isSome = trueโŠข (if i.succAbove a < i then (exchangeSign (๐“•|>โ‚›ฯ†)) (๐“•|>โ‚›ฯ†s[โ†‘a]) else 1) = (exchangeSign (๐“•|>โ‚›ฯ†)) (if (ฯ†sฮ›.getDual? a).isSome = true โˆง i.succAbove a < i then ๐“•|>โ‚›ฯ†s[โ†‘a] else 1) ๐“•:FieldSpecificationฯ†:๐“•.FieldOpฯ†s:List ๐“•.FieldOpฯ†sฮ›:WickContraction ฯ†s.lengthi:Fin ฯ†s.length.succhG:GradingCompliant ฯ†s ฯ†sฮ›a:Fin ฯ†s.lengthh:(ฯ†sฮ›.getDual? a).isSome = trueโŠข (if i.succAbove a < i then (exchangeSign (๐“•|>โ‚›ฯ†)) (๐“•|>โ‚›ฯ†s[โ†‘a]) else 1) = (exchangeSign (๐“•|>โ‚›ฯ†)) (if (ฯ†sฮ›.getDual? a).isSome = true โˆง i.succAbove a < i then ๐“•|>โ‚›ฯ†s[โ†‘a] else 1) ๐“•:FieldSpecificationฯ†:๐“•.FieldOpฯ†s:List ๐“•.FieldOpฯ†sฮ›:WickContraction ฯ†s.lengthi:Fin ฯ†s.length.succhG:GradingCompliant ฯ†s ฯ†sฮ›a:Fin ฯ†s.lengthh:(ฯ†sฮ›.getDual? a).isSome = trueโŠข (if i.succAbove a < i then (exchangeSign (๐“•|>โ‚›ฯ†)) (๐“•|>โ‚›ฯ†s[โ†‘a]) else 1) = (exchangeSign (๐“•|>โ‚›ฯ†)) (if i.succAbove a < i then ๐“•|>โ‚›ฯ†s[โ†‘a] else 1) ๐“•:FieldSpecificationฯ†:๐“•.FieldOpฯ†s:List ๐“•.FieldOpฯ†sฮ›:WickContraction ฯ†s.lengthi:Fin ฯ†s.length.succhG:GradingCompliant ฯ†s ฯ†sฮ›a:Fin ฯ†s.lengthh:(ฯ†sฮ›.getDual? a).isSome = truehโœ:i.succAbove a < iโŠข (exchangeSign (๐“•|>โ‚›ฯ†)) (๐“•|>โ‚›ฯ†s[โ†‘a]) = (exchangeSign (๐“•|>โ‚›ฯ†)) (๐“•|>โ‚›ฯ†s[โ†‘a])๐“•:FieldSpecificationฯ†:๐“•.FieldOpฯ†s:List ๐“•.FieldOpฯ†sฮ›:WickContraction ฯ†s.lengthi:Fin ฯ†s.length.succhG:GradingCompliant ฯ†s ฯ†sฮ›a:Fin ฯ†s.lengthh:(ฯ†sฮ›.getDual? a).isSome = truehโœ:ยฌi.succAbove a < iโŠข 1 = (exchangeSign (๐“•|>โ‚›ฯ†)) 1 ๐“•:FieldSpecificationฯ†:๐“•.FieldOpฯ†s:List ๐“•.FieldOpฯ†sฮ›:WickContraction ฯ†s.lengthi:Fin ฯ†s.length.succhG:GradingCompliant ฯ†s ฯ†sฮ›a:Fin ฯ†s.lengthh:(ฯ†sฮ›.getDual? a).isSome = truehโœ:i.succAbove a < iโŠข (exchangeSign (๐“•|>โ‚›ฯ†)) (๐“•|>โ‚›ฯ†s[โ†‘a]) = (exchangeSign (๐“•|>โ‚›ฯ†)) (๐“•|>โ‚›ฯ†s[โ†‘a]) All goals completed! ๐Ÿ™ ๐“•:FieldSpecificationฯ†:๐“•.FieldOpฯ†s:List ๐“•.FieldOpฯ†sฮ›:WickContraction ฯ†s.lengthi:Fin ฯ†s.length.succhG:GradingCompliant ฯ†s ฯ†sฮ›a:Fin ฯ†s.lengthh:(ฯ†sฮ›.getDual? a).isSome = truehโœ:ยฌi.succAbove a < iโŠข 1 = (exchangeSign (๐“•|>โ‚›ฯ†)) 1 All goals completed! ๐Ÿ™ ๐“•:FieldSpecificationฯ†:๐“•.FieldOpฯ†s:List ๐“•.FieldOpฯ†sฮ›:WickContraction ฯ†s.lengthi:Fin ฯ†s.length.succhG:GradingCompliant ฯ†s ฯ†sฮ›a:Fin ฯ†s.lengthhโœ:ยฌ(ฯ†sฮ›.getDual? a).isSome = trueโŠข 1 = (exchangeSign (๐“•|>โ‚›ฯ†)) (if (ฯ†sฮ›.getDual? a).isSome = true โˆง i.succAbove a < i then ๐“•|>โ‚›ฯ†s[โ†‘a] else 1) ๐“•:FieldSpecificationฯ†:๐“•.FieldOpฯ†s:List ๐“•.FieldOpฯ†sฮ›:WickContraction ฯ†s.lengthi:Fin ฯ†s.length.succhG:GradingCompliant ฯ†s ฯ†sฮ›a:Fin ฯ†s.lengthh:ยฌ(ฯ†sฮ›.getDual? a).isSome = trueโŠข 1 = (exchangeSign (๐“•|>โ‚›ฯ†)) (if (ฯ†sฮ›.getDual? a).isSome = true โˆง i.succAbove a < i then ๐“•|>โ‚›ฯ†s[โ†‘a] else 1) All goals completed! ๐Ÿ™ ๐“•:FieldSpecificationฯ†:๐“•.FieldOpฯ†s:List ๐“•.FieldOpฯ†sฮ›:WickContraction ฯ†s.lengthi:Fin ฯ†s.length.succhG:GradingCompliant ฯ†s ฯ†sฮ›โŠข GradingCompliant ฯ†s ฯ†sฮ› All goals completed! ๐Ÿ™

For a list ฯ†s = ฯ†โ‚€โ€ฆฯ†โ‚™ of ๐“•.FieldOp, a graded compliant Wick contraction ฯ†sฮ› of ฯ†s, an i โ‰ค ฯ†s.length, and a ฯ† in ๐“•.FieldOp, then (ฯ†sฮ› โ†ฉฮ› ฯ† i none).sign = s * ฯ†sฮ›.sign where s is the sign arrived at by moving ฯ† through the elements of ฯ†โ‚€โ€ฆฯ†แตขโ‚‹โ‚ which are contracted with some element.

The proof of this result involves a careful consideration of the contributions of different FieldOps in ฯ†s to the sign of ฯ†sฮ› โ†ฉฮ› ฯ† i none.

๐“•:FieldSpecificationฯ†:๐“•.FieldOpฯ†s:List ๐“•.FieldOpฯ†sฮ›:WickContraction ฯ†s.lengthi:Fin ฯ†s.length.succhG:GradingCompliant ฯ†s ฯ†sฮ›โŠข GradingCompliant ฯ†s ฯ†sฮ› All goals completed! ๐Ÿ™

For a list ฯ†s = ฯ†โ‚€โ€ฆฯ†โ‚™ of ๐“•.FieldOp, a graded compliant Wick contraction ฯ†sฮ› of ฯ†s, and a ฯ† in ๐“•.FieldOp, then (ฯ†sฮ› โ†ฉฮ› ฯ† 0 none).sign = ฯ†sฮ›.sign.

This is a direct corollary of sign_insert_none.

๐“•:FieldSpecificationฯ†:๐“•.FieldOpฯ†s:List ๐“•.FieldOpฯ†sฮ›:WickContraction ฯ†s.lengthโŠข signInsertNone ฯ† ฯ†s ฯ†sฮ› 0 * sign ฯ†s ฯ†sฮ› = sign ฯ†s ฯ†sฮ› All goals completed! ๐Ÿ™