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

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.

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

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
    theorem WickContraction.Perm.refl {𝓕 : FieldSpecification} {Ο†s : List 𝓕.FieldOp} {Ο†sΞ› : WickContraction Ο†s.length} :
    Ο†sΞ›.Perm Ο†sΞ›

    The reflexivity of the Perm relation.

    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.

    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.

    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.

    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.