Physlib.QFT.PerturbationTheory.WickContraction.IsFull

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.Mathematics.Fin.Involutions
public import Physlib.QFT.PerturbationTheory.WickContraction.ExtractEquiv
public import Physlib.QFT.PerturbationTheory.WickContraction.Involutions

Full contraction

We say that a contraction is full if it has no uncontracted fields.

@[expose] public section

A contraction is full if there are no uncontracted fields, i.e. the finite set of uncontracted fields is empty.

def IsFull : Prop := c.uncontracted = ∅

The condition on whether or not a contraction is full is decidable.

instance : Decidable (IsFull c) := decEq c.uncontracted ∅



lemma isFull_iff_equivInvolution_no_fixed_point :
    IsFull c ↔ ∀ (i : Fin n), (equivInvolution c).1 i ≠ i := byn:ℕc:WickContraction n⊢ c.IsFull ↔ ∀ (i : Fin n), ↑(equivInvolution c) i ≠ i
  simp only [IsFull, ne_eq]n:ℕc:WickContraction n⊢ c.uncontracted = ∅ ↔ ∀ (i : Fin n), ¬↑(equivInvolution c) i = i
  rw [Finset.eq_empty_iff_forall_notMemn:ℕc:WickContraction n⊢ (∀ (x : Fin n), x ∉ c.uncontracted) ↔ ∀ (i : Fin n), ¬↑(equivInvolution c) i = in:ℕc:WickContraction n⊢ (∀ (x : Fin n), x ∉ c.uncontracted) ↔ ∀ (i : Fin n), ¬↑(equivInvolution c) i = i]n:ℕc:WickContraction n⊢ (∀ (x : Fin n), x ∉ c.uncontracted) ↔ ∀ (i : Fin n), ¬↑(equivInvolution c) i = i
  simp [equivInvolution, toInvolution, uncontracted]All goals completed! 🐙

The equivalence between full contractions and fixed-point free involutions.


def isFullInvolutionEquiv : {c : WickContraction n // IsFull c} ≃
    {f : Fin n → Fin n // Function.Involutive f ∧ (∀ i, f i ≠ i)} where
  toFun c := ⟨equivInvolution c.1, by𝓕:FieldSpecificationn:ℕc✝:WickContraction nc:{ c // c.IsFull }⊢ Function.Involutive ↑(equivInvolution ↑c) ∧ ∀ (i : Fin n), ↑(equivInvolution ↑c) i ≠ i
    apply And.intro (equivInvolution c.1).2𝓕:FieldSpecificationn:ℕc✝:WickContraction nc:{ c // c.IsFull }⊢ ∀ (i : Fin n), ↑(equivInvolution ↑c) i ≠ i
    rw [← isFull_iff_equivInvolution_no_fixed_point𝓕:FieldSpecificationn:ℕc✝:WickContraction nc:{ c // c.IsFull }⊢ (↑c).IsFull𝓕:FieldSpecificationn:ℕc✝:WickContraction nc:{ c // c.IsFull }⊢ (↑c).IsFull]𝓕:FieldSpecificationn:ℕc✝:WickContraction nc:{ c // c.IsFull }⊢ (↑c).IsFull
    exact c.2All goals completed! 🐙⟩
  invFun f := ⟨equivInvolution.symm ⟨f.1, f.2.1⟩, by𝓕:FieldSpecificationn:ℕc:WickContraction nf:{ f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }⊢ (equivInvolution.symm ⟨↑f, ⋯⟩).IsFull
    rw [isFull_iff_equivInvolution_no_fixed_point𝓕:FieldSpecificationn:ℕc:WickContraction nf:{ f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }⊢ ∀ (i : Fin n), ↑(equivInvolution (equivInvolution.symm ⟨↑f, ⋯⟩)) i ≠ i𝓕:FieldSpecificationn:ℕc:WickContraction nf:{ f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }⊢ ∀ (i : Fin n), ↑(equivInvolution (equivInvolution.symm ⟨↑f, ⋯⟩)) i ≠ i]𝓕:FieldSpecificationn:ℕc:WickContraction nf:{ f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }⊢ ∀ (i : Fin n), ↑(equivInvolution (equivInvolution.symm ⟨↑f, ⋯⟩)) i ≠ i
    simpa using f.2.2All goals completed! 🐙⟩
  left_inv c := by𝓕:FieldSpecificationn:ℕc✝:WickContraction nc:{ c // c.IsFull }⊢ (fun f => ⟨equivInvolution.symm ⟨↑f, ⋯⟩, ⋯⟩) ((fun c => ⟨↑(equivInvolution ↑c), ⋯⟩) c) = c simpAll goals completed! 🐙
  right_inv f := by𝓕:FieldSpecificationn:ℕc:WickContraction nf:{ f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i }⊢ (fun c => ⟨↑(equivInvolution ↑c), ⋯⟩) ((fun f => ⟨equivInvolution.symm ⟨↑f, ⋯⟩, ⋯⟩) f) = f simpAll goals completed! 🐙

If n is even then the number of full contractions is (n-1)!!.


theorem card_of_isfull_even (he : Even n) :
    Fintype.card {c : WickContraction n // IsFull c} = (n - 1)‼ := byn:ℕhe:Even n⊢ Fintype.card { c // c.IsFull } = (n - 1)‼
  rw [Fintype.card_congr (isFullInvolutionEquiv)n:ℕhe:Even n⊢ Fintype.card { f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i } = (n - 1)‼n:ℕhe:Even n⊢ Fintype.card { f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i } = (n - 1)‼]n:ℕhe:Even n⊢ Fintype.card { f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i } = (n - 1)‼
  exact Physlib.Fin.involutionNoFixed_card_even n heAll goals completed! 🐙

If n is odd then there are no full contractions. This is because there will always be at least one element unpaired.


theorem card_of_isfull_odd (ho : Odd n) :
    Fintype.card {c : WickContraction n // IsFull c} = 0 := byn:ℕho:Odd n⊢ Fintype.card { c // c.IsFull } = 0
  rw [Fintype.card_congr (isFullInvolutionEquiv)n:ℕho:Odd n⊢ Fintype.card { f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i } = 0n:ℕho:Odd n⊢ Fintype.card { f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i } = 0]n:ℕho:Odd n⊢ Fintype.card { f // Function.Involutive f ∧ ∀ (i : Fin n), f i ≠ i } = 0
  exact Physlib.Fin.involutionNoFixed_card_odd n hoAll goals completed! 🐙