1. Physlib
  2. QFT
  3. PerturbationTheory
  4. WickAlgebra
  5. WickTerm
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.InsertNone public import Physlib.QFT.PerturbationTheory.WickContraction.Sign.InsertSome public import Physlib.QFT.PerturbationTheory.WickContraction.TimeContract public import Physlib.QFT.PerturbationTheory.WickAlgebra.NormalOrder.WickContractions

Wick term

@[expose] public section

For a list φs of 𝓕.FieldOp, and a Wick contraction φsΛ of φs, the element of 𝓕.WickAlgebra, φsΛ.wickTerm is defined as

φsΛ.sign • φsΛ.timeContract * 𝓝([φsΛ]ᵘᶜ).

This is a term which appears in the Wick's theorem.

def wickTerm {φs : List 𝓕.FieldOp} (φsΛ : WickContraction φs.length) : 𝓕.WickAlgebra := φsΛ.sign • φsΛ.timeContract * 𝓝(ofFieldOpList [φsΛ]ᵘᶜ)

For the empty list [] of 𝓕.FieldOp, the wickTerm of the Wick contraction corresponding to the empty set ∅ (the only Wick contraction of []) is 1.

𝓕:FieldSpecification⊢ sign [] empty • ↑empty.timeContract * normalOrder (ofFieldOpList [empty]ᵘᶜ) = 1 All goals completed! 🐙

For a list φs = φ₀…φₙ of 𝓕.FieldOp, a Wick contraction φsΛ of φs, an element φ of 𝓕.FieldOp, and i ≤ φs.length, then (φsΛ ↩Λ φ i none).wickTerm is equal to

𝓢(φ, φ₀…φᵢ₋₁) φsΛ.sign • φsΛ.timeContract * 𝓝(φ :: [φsΛ]ᵘᶜ)

The proof of this result relies on

    normalOrder_uncontracted_none to rewrite normal orderings.

    timeContract_insert_none to rewrite the time contract.

    sign_insert_none to rewrite the sign.

𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.lengthhg:¬GradingCompliant φs φsΛ⊢ sign (φs.insertIdx (↑i) φ) (φsΛ↩Λφ i none) • (↑0 * normalOrder (ofFieldOpList [φsΛ↩Λφ i none]ᵘᶜ)) = (exchangeSign (𝓕|>ₛφ)) (ofFinset 𝓕.fieldOpStatistic φs.get {k | i.succAbove k < i}) • sign φs φsΛ • (↑0 * normalOrder (ofFieldOpList (φ :: [φsΛ]ᵘᶜ)))𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.lengthhg:¬GradingCompliant φs φsΛ⊢ ¬GradingCompliant φs φsΛ 𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.lengthhg:¬GradingCompliant φs φsΛ⊢ ¬GradingCompliant φs φsΛ All goals completed! 🐙

For a list φs = φ₀…φₙ of 𝓕.FieldOp, a Wick contraction φsΛ of φs, an element φ of 𝓕.FieldOp, i ≤ φs.length and a k in φsΛ.uncontracted, such that all 𝓕.FieldOp in φ₀…φᵢ₋₁ have time strictly less than φ and φ has a time greater than or equal to all FieldOp in φ₀…φₙ, then (φsΛ ↩Λ φ i (some k)).staticWickTerm is equal to the product of

    the sign 𝓢(φ, φ₀…φᵢ₋₁)

    the sign φsΛ.sign

    φsΛ.timeContract

    s • [anPart φ, ofFieldOp φs[k]]ₛ where s is the sign associated with moving φ through uncontracted fields in φ₀…φₖ₋₁

    the normal ordering [φsΛ]ᵘᶜ with the field corresponding to k removed.

The proof of this result relies on

    timeContract_insert_some_of_not_lt and timeContract_insert_some_of_lt to rewrite time contractions.

    normalOrder_uncontracted_some to rewrite normal orderings.

    sign_insert_some_of_not_lt and sign_insert_some_of_lt to rewrite signs.

set_option backward.isDefEq.respectTransparency false in𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.lengthk:↥φsΛ.uncontractedhlt:∀ (k : Fin φs.length), timeOrderRel φ φs[k]hn:∀ (k : Fin φs.length), i.succAbove k < i → ¬timeOrderRel φs[k] φhg:GradingCompliant φs φsΛ → ¬(𝓕|>ₛφ) = 𝓕|>ₛφs[↑↑k]hg':¬GradingCompliant φs φsΛ⊢ sign (φs.insertIdx (↑i) φ) (φsΛ↩Λφ i some k) • ↑((if i < i.succAbove ↑k then ⟨WickAlgebra.timeContract φ φs[↑k], ⋯⟩ else ⟨WickAlgebra.timeContract φs[↑k] φ, ⋯⟩) * 0) * normalOrder (ofFieldOpList [φsΛ↩Λφ i some k]ᵘᶜ) = (exchangeSign (𝓕|>ₛφ)) (ofFinset 𝓕.fieldOpStatistic φs.get {x | i.succAbove x < i}) • (sign φs φsΛ • (contractStateAtIndex φ [φsΛ]ᵘᶜ ((uncontractedFieldOpEquiv φs φsΛ) (some k)) * ↑0) * normalOrder (ofFieldOpList (optionEraseZ [φsΛ]ᵘᶜ φ ((uncontractedFieldOpEquiv φs φsΛ) (some k)))))𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.lengthk:↥φsΛ.uncontractedhlt:∀ (k : Fin φs.length), timeOrderRel φ φs[k]hn:∀ (k : Fin φs.length), i.succAbove k < i → ¬timeOrderRel φs[k] φhg:GradingCompliant φs φsΛ → ¬(𝓕|>ₛφ) = 𝓕|>ₛφs[↑↑k]hg':¬GradingCompliant φs φsΛ⊢ ¬GradingCompliant φs φsΛ 𝓕:FieldSpecificationφ:𝓕.FieldOpφs:List 𝓕.FieldOpi:Fin φs.length.succφsΛ:WickContraction φs.lengthk:↥φsΛ.uncontractedhlt:∀ (k : Fin φs.length), timeOrderRel φ φs[k]hn:∀ (k : Fin φs.length), i.succAbove k < i → ¬timeOrderRel φs[k] φhg:GradingCompliant φs φsΛ → ¬(𝓕|>ₛφ) = 𝓕|>ₛφs[↑↑k]hg':¬GradingCompliant φs φsΛ⊢ ¬GradingCompliant φs φsΛ All goals completed! 🐙

For a list φs = φ₀…φₙ of 𝓕.FieldOp, a Wick contraction φsΛ of φs, an element φ of 𝓕.FieldOp, and i ≤ φs.length such that all 𝓕.FieldOp in φ₀…φᵢ₋₁ have time strictly less than φ and φ has a time greater than or equal to all FieldOp in φ₀…φₙ, then

φ * φsΛ.wickTerm = 𝓢(φ, φ₀…φᵢ₋₁) • ∑ k, (φsΛ ↩Λ φ i k).wickTerm

where the sum is over all k in Option φsΛ.uncontracted, so k is either none or some k.

The proof proceeds as follows:

    ofFieldOp_mul_normalOrder_ofFieldOpList_eq_sum is used to expand φ 𝓝([φsΛ]ᵘᶜ) as a sum over k in Option φsΛ.uncontracted of terms involving [anPart φ, φs[k]]ₛ.

    Then wickTerm_insert_none and wickTerm_insert_some are used to equate terms.

All goals completed! 🐙