PhysLean Documentation

PhysLean.QFT.PerturbationTheory.WickContraction.Perm

Permutations of Wick contractions #

We define two Wick contractions to be permutations of each other if the Wick term they produce is equal.

##Β TODO

The long term aim is to simplify this condition as much as possible, so that it can eventually be made decidable.

It should become apparent that two Wick contractions are permutations of each other if they correspond to the same Feynman diagram. Please speak to JTS before working in this direction.

source
def WickContraction.Perm {𝓕 : FieldSpecification} {Ο†s : List 𝓕.FieldOp} (Ο†sΛ₁ Ο†sΞ›β‚‚ : WickContraction Ο†s.length) :
Prop

For a list Ο†s of 𝓕.FieldOp, and two Wick contractions Ο†sΛ₁ and Ο†sΞ›β‚‚ of Ο†s, we say that Ο†sΛ₁ and Ο†sΞ›β‚‚ are permutations of each other if they have the same Wick term.

Equations
Instances For
    source
    theorem WickContraction.Perm.refl {𝓕 : FieldSpecification} {Ο†s : List 𝓕.FieldOp} {Ο†sΞ› : WickContraction Ο†s.length} :
    Ο†sΞ›.Perm Ο†sΞ›

    The reflexivity of the Perm relation.

    source
    theorem WickContraction.Perm.symm {𝓕 : FieldSpecification} {Ο†s : List 𝓕.FieldOp} {Ο†sΛ₁ Ο†sΞ›β‚‚ : WickContraction Ο†s.length} (h : Ο†sΛ₁.Perm Ο†sΞ›β‚‚) :
    Ο†sΞ›β‚‚.Perm Ο†sΛ₁

    The symmetry of the Perm relation.

    source
    theorem WickContraction.Perm.trans {𝓕 : FieldSpecification} {Ο†s : List 𝓕.FieldOp} {Ο†sΛ₁ Ο†sΞ›β‚‚ Ο†sΛ₃ : WickContraction Ο†s.length} (h12 : Ο†sΛ₁.Perm Ο†sΞ›β‚‚) (h23 : Ο†sΞ›β‚‚.Perm Ο†sΛ₃) :
    Ο†sΛ₁.Perm Ο†sΛ₃

    The transitivity of the Perm relation.

    source
    theorem WickContraction.Perm.isFull_of_isFull {𝓕 : FieldSpecification} {Ο†s : List 𝓕.FieldOp} {Ο†sΛ₁ Ο†sΞ›β‚‚ : WickContraction Ο†s.length} (h : Ο†sΛ₁.Perm Ο†sΞ›β‚‚) (hf : Ο†sΛ₁.IsFull) :
    Ο†sΞ›β‚‚.IsFull

    If Perm Ο†sΛ₁ Ο†sΞ›β‚‚ then if Ο†sΛ₁ is a full Wick contraction then Ο†sΞ›β‚‚ is a full Wick contraction..

    Implementation note: Please contact JTS before attempting this.

    source
    theorem WickContraction.Perm.perm_uncontractedList {𝓕 : FieldSpecification} {Ο†s : List 𝓕.FieldOp} {Ο†sΛ₁ Ο†sΞ›β‚‚ : WickContraction Ο†s.length} (h : Ο†sΛ₁.Perm Ο†sΞ›β‚‚) :
    Ο†sΛ₁.uncontractedListGet.Perm Ο†sΞ›β‚‚.uncontractedListGet

    If Perm Ο†sΛ₁ Ο†sΞ›β‚‚ then the uncontracted lists of Ο†sΛ₁ and Ο†sΞ›β‚‚ are permutations of each other.