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.WickAlgebra.WickTerm
public import Physlib.QFT.PerturbationTheory.WickContraction.IsFull
public import Physlib.Meta.Linters.SorryPermutations 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.
@[expose] public section
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.
def Perm {φs : List 𝓕.FieldOp} (φsΛ₁ φsΛ₂ : WickContraction φs.length) : Prop :=
φsΛ₁.wickTerm = φsΛ₂.wickTerm
The reflexivity of the Perm relation.
All goals completed! 🐙
The symmetry of the Perm relation.
𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ₁:WickContraction φs.lengthφsΛ₂:WickContraction φs.lengthh:φsΛ₁.wickTerm = φsΛ₂.wickTerm⊢ φsΛ₂.wickTerm = φsΛ₁.wickTerm
All goals completed! 🐙
The transitivity of the Perm relation.
𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ₁:WickContraction φs.lengthφsΛ₂:WickContraction φs.lengthφsΛ₃:WickContraction φs.lengthh12:φsΛ₁.wickTerm = φsΛ₂.wickTermh23:φsΛ₂.wickTerm = φsΛ₃.wickTerm⊢ φsΛ₁.wickTerm = φsΛ₃.wickTerm
All goals completed! 🐙
If Perm φsΛ₁ φsΛ₂ and both contractions are grading-compliant,
then if φsΛ₁ is a full Wick contraction, so is φsΛ₂.
@[sorryful]
lemma isFull_of_isFull (h : Perm φsΛ₁ φsΛ₂)
(h₁ : GradingCompliant φs φsΛ₁) (h₂ : GradingCompliant φs φsΛ₂)
(hf : IsFull φsΛ₁) : IsFull φsΛ₂ := 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ₁:WickContraction φs.lengthφsΛ₂:WickContraction φs.lengthh:φsΛ₁.Perm φsΛ₂h₁:GradingCompliant φs φsΛ₁h₂:GradingCompliant φs φsΛ₂hf:φsΛ₁.IsFull⊢ φsΛ₂.IsFull
All goals completed! 🐙
If Perm φsΛ₁ φsΛ₂ and both contractions are grading-compliant,
then their uncontracted lists are permutations of each other.
@[sorryful]
lemma perm_uncontractedList (h : Perm φsΛ₁ φsΛ₂)
(h₁ : GradingCompliant φs φsΛ₁) (h₂ : GradingCompliant φs φsΛ₂) :
[φsΛ₁]ᵘᶜ.Perm [φsΛ₂]ᵘᶜ := 𝓕:FieldSpecificationφs:List 𝓕.FieldOpφsΛ₁:WickContraction φs.lengthφsΛ₂:WickContraction φs.lengthh:φsΛ₁.Perm φsΛ₂h₁:GradingCompliant φs φsΛ₁h₂:GradingCompliant φs φsΛ₂⊢ [φsΛ₁]ᵘᶜ.Perm [φsΛ₂]ᵘᶜ
All goals completed! 🐙