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.

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.