1. Physlib
  2. QFT
  3. PerturbationTheory
  4. WickContraction
  5. Card
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.WickContraction.ExtractEquiv

Cardinality of Wick contractions

@[expose] public sectionn:ℕe2:WickContraction n.succ ≃ { c // (c.getDual? 0).isSome = true } ⊕ { c // ¬(c.getDual? 0).isSome = true } := (Equiv.sumCompl fun c => (c.getDual? 0).isSome = true).symm⊢ Fintype.card ({ c // (c.getDual? 0).isSome = true } ⊕ { c // ¬(c.getDual? 0).isSome = true }) = Fintype.card { c // ¬(c.getDual? 0).isSome = true } + Fintype.card { c // (c.getDual? 0).isSome = true } All goals completed! 🐙lemma wickContraction_zero_none_card : Fintype.card {c : WickContraction n.succ // ¬ (c.getDual? 0).isSome} = Fintype.card (WickContraction n) := n:ℕ⊢ Fintype.card { c // ¬(c.getDual? 0).isSome = true } = Fintype.card (WickContraction n) n:ℕ⊢ Fintype.card { c // c.getDual? 0 = none } = Fintype.card (WickContraction n) n:ℕ⊢ Fintype.card (WickContraction n) = Fintype.card { c // c.getDual? 0 = none } All goals completed! 🐙n:ℕe1:{ c // (c.getDual? 0).isSome = true } ≃ (i : Fin n) × { c // (c.getDual? 0).isSome = true ∧ ∀ (h : (c.getDual? 0).isSome = true), (c.getDual? 0).get h = i.succ } := { toFun := fun c => ⟨(((↑c).getDual? 0).get ⋯).pred ⋯, ⟨↑c, ⋯⟩⟩, invFun := fun c => ⟨↑c.snd, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }⊢ Fintype.card ((i : Fin n) × { c // (c.getDual? 0).isSome = true ∧ ∀ (h : (c.getDual? 0).isSome = true), (c.getDual? 0).get h = i.succ }) = ∑ i, Fintype.card { c // (c.getDual? 0).isSome = true ∧ ∀ (h : (c.getDual? 0).isSome = true), (c.getDual? 0).get h = i.succ } All goals completed! 🐙lemma finset_succAbove_succ_disjoint (a : Finset (Fin n)) (i : Fin n.succ) : Disjoint ((Finset.map (Fin.succEmb (n + 1))) ((Finset.map i.succAboveEmb) a)) {0, i.succ} := n:ℕa:Finset (Fin n)i:Fin n.succ⊢ Disjoint (Finset.map (Fin.succEmb (n + 1)) (Finset.map i.succAboveEmb a)) {0, i.succ} n:ℕa:Finset (Fin n)i:Fin n.succ⊢ (∀ x ∈ a, ¬(i.succAbove x).succ = 0) ∧ ∀ x ∈ a, ¬i.succAbove x = i n:ℕa:Finset (Fin n)i:Fin n.succ⊢ ∀ x ∈ a, ¬(i.succAbove x).succ = 0n:ℕa:Finset (Fin n)i:Fin n.succ⊢ ∀ x ∈ a, ¬i.succAbove x = i n:ℕa:Finset (Fin n)i:Fin n.succ⊢ ∀ x ∈ a, ¬(i.succAbove x).succ = 0 All goals completed! 🐙 n:ℕa:Finset (Fin n)i:Fin n.succ⊢ ∀ x ∈ a, ¬i.succAbove x = i All goals completed! 🐙

The Wick contraction in WickContraction n.succ.succ formed by a Wick contraction WickContraction n by inserting at the 0 and i.succ and contracting these two.

𝓕:FieldSpecificationn:ℕc✝:WickContraction ni:Fin n.succc:WickContraction nb:Finset (Fin n)hb:b ∈ ↑c⊢ Disjoint {0, i.succ} (Finset.map (Fin.succEmb (n + 1)) (Finset.map i.succAboveEmb b)) All goals completed! 🐙 𝓕:FieldSpecificationn:ℕc✝:WickContraction ni:Fin n.succc:WickContraction na:Finset (Fin n.succ.succ)b:Finset (Fin n.succ.succ)ha:a = {0, i.succ}hb:b = {0, i.succ}⊢ a = b ∨ Disjoint a b 𝓕:FieldSpecificationn:ℕc✝:WickContraction ni:Fin n.succc:WickContraction n⊢ {0, i.succ} = {0, i.succ} ∨ Disjoint {0, i.succ} {0, i.succ} All goals completed! 🐙⟩
n:ℕi:Fin n.succc:WickContraction n⊢ {0, i.succ} ∈ ↑(consAddContract i c) All goals completed! 🐙n:ℕi:Fin n.succc:WickContraction n⊢ {i.succ, 0} ∈ ↑(consAddContract i c) All goals completed! 🐙n:ℕi:Fin n.succc:WickContraction na:Finset (Fin n)h:Finset.map (Fin.succEmb (n + 1)) (Finset.map i.succAboveEmb a) = {0, i.succ}h1:Disjoint {0, i.succ} {0, i.succ}⊢ a ∈ ↑c All goals completed! 🐙n:ℕi:Fin n.succc1:WickContraction nc2:WickContraction nh:consAddContract i c1 = consAddContract i c2a:Finset (Fin n)ha:a ∈ ↑c2ha':a ∈ ↑c1⊢ a ∈ ↑c1 All goals completed! 🐙n:ℕi:Fin n.succc:WickContraction n.succ.succh✝:(c.getDual? 0).isSome = truec':WickContraction n := ⟨{x | Finset.map (Fin.succEmb n.succ) (Finset.map i.succAboveEmb x) ∈ ↑c}, ⋯⟩h2:(c.getDual? 0).get h✝ = i.succx:Fin ny:Fin nhx:¬i.succAbove x = i.succAbove yh:{(i.succAbove x).succ, (i.succAbove y).succ} ∈ ↑cha:¬{(i.succAbove x).succ, (i.succAbove y).succ} = {0, i.succ}hd:(¬0 = (i.succAbove x).succ ∧ ¬0 = (i.succAbove y).succ) ∧ ¬i = i.succAbove x ∧ ¬i = i.succAbove y⊢ ∃ a ∈ ↑c', Finset.map (Fin.succEmb (n + 1)) (Finset.map i.succAboveEmb a) = {(i.succAbove x).succ, (i.succAbove y).succ} n:ℕi:Fin n.succc:WickContraction n.succ.succh✝:(c.getDual? 0).isSome = truec':WickContraction n := ⟨{x | Finset.map (Fin.succEmb n.succ) (Finset.map i.succAboveEmb x) ∈ ↑c}, ⋯⟩h2:(c.getDual? 0).get h✝ = i.succx:Fin ny:Fin nhx:¬i.succAbove x = i.succAbove yh:{(i.succAbove x).succ, (i.succAbove y).succ} ∈ ↑cha:¬{(i.succAbove x).succ, (i.succAbove y).succ} = {0, i.succ}hd:(¬0 = (i.succAbove x).succ ∧ ¬0 = (i.succAbove y).succ) ∧ ¬i = i.succAbove x ∧ ¬i = i.succAbove y⊢ {x, y} ∈ ↑c' ∧ Finset.map (Fin.succEmb (n + 1)) (Finset.map i.succAboveEmb {x, y}) = {(i.succAbove x).succ, (i.succAbove y).succ} n:ℕi:Fin n.succc:WickContraction n.succ.succh✝:(c.getDual? 0).isSome = truec':WickContraction n := ⟨{x | Finset.map (Fin.succEmb n.succ) (Finset.map i.succAboveEmb x) ∈ ↑c}, ⋯⟩h2:(c.getDual? 0).get h✝ = i.succx:Fin ny:Fin nhx:¬i.succAbove x = i.succAbove yh:{(i.succAbove x).succ, (i.succAbove y).succ} ∈ ↑cha:¬{(i.succAbove x).succ, (i.succAbove y).succ} = {0, i.succ}hd:(¬0 = (i.succAbove x).succ ∧ ¬0 = (i.succAbove y).succ) ∧ ¬i = i.succAbove x ∧ ¬i = i.succAbove y⊢ {x, y} ∈ {x | Finset.map (Fin.succEmb n.succ) (Finset.map i.succAboveEmb x) ∈ ↑c} ∧ Finset.map (Fin.succEmb (n + 1)) (Finset.map i.succAboveEmb {x, y}) = {(i.succAbove x).succ, (i.succAbove y).succ} All goals completed! 🐙lemma consAddContract_bijection (i : Fin n.succ) : Function.Bijective (fun c => (⟨(consAddContract i c), 𝓕:FieldSpecificationn:ℕc✝:WickContraction ni:Fin n.succc:WickContraction n⊢ ((consAddContract i c).getDual? 0).isSome = true ∧ ∀ (h : ((consAddContract i c).getDual? 0).isSome = true), ((consAddContract i c).getDual? 0).get h = i.succ All goals completed! 🐙⟩ : {c : WickContraction n.succ.succ // (c.getDual? 0).isSome ∧ ∀ (h : (c.getDual? 0).isSome), (c.getDual? 0).get h = Fin.succ i})) := n:ℕi:Fin n.succ⊢ Function.Bijective fun c => ⟨consAddContract i c, ⋯⟩ n:ℕi:Fin n.succ⊢ Function.Injective fun c => ⟨consAddContract i c, ⋯⟩n:ℕi:Fin n.succ⊢ Function.Surjective fun c => ⟨consAddContract i c, ⋯⟩ n:ℕi:Fin n.succ⊢ Function.Injective fun c => ⟨consAddContract i c, ⋯⟩ n:ℕi:Fin n.succc1:WickContraction nc2:WickContraction nh:(fun c => ⟨consAddContract i c, ⋯⟩) c1 = (fun c => ⟨consAddContract i c, ⋯⟩) c2⊢ c1 = c2 n:ℕi:Fin n.succc1:WickContraction nc2:WickContraction nh:consAddContract i c1 = consAddContract i c2⊢ c1 = c2 All goals completed! 🐙 n:ℕi:Fin n.succ⊢ Function.Surjective fun c => ⟨consAddContract i c, ⋯⟩ n:ℕi:Fin n.succc:{ c // (c.getDual? 0).isSome = true ∧ ∀ (h : (c.getDual? 0).isSome = true), (c.getDual? 0).get h = i.succ }⊢ ∃ a, (fun c => ⟨consAddContract i c, ⋯⟩) a = c n:ℕi:Fin n.succc:{ c // (c.getDual? 0).isSome = true ∧ ∀ (h : (c.getDual? 0).isSome = true), (c.getDual? 0).get h = i.succ }c':WickContraction nhc:consAddContract i c' = ↑c⊢ ∃ a, (fun c => ⟨consAddContract i c, ⋯⟩) a = c n:ℕi:Fin n.succc:{ c // (c.getDual? 0).isSome = true ∧ ∀ (h : (c.getDual? 0).isSome = true), (c.getDual? 0).get h = i.succ }c':WickContraction nhc:consAddContract i c' = ↑c⊢ (fun c => ⟨consAddContract i c, ⋯⟩) c' = c All goals completed! 🐙n:ℕ⊢ ∑ i, Fintype.card { c // (c.getDual? 0).isSome = true ∧ ∀ (h : (c.getDual? 0).isSome = true), (c.getDual? 0).get h = i.succ } = (n + 1) * Fintype.card (WickContraction n) conv_lhs => n:ℕi:Fin (n + 1)| Fintype.card { c // (c.getDual? 0).isSome = true ∧ ∀ (h : (c.getDual? 0).isSome = true), (c.getDual? 0).get h = i.succ } n:ℕi:Fin (n + 1)| Fintype.card (WickContraction n) All goals completed! 🐙

The cardinality of Wick's contractions as a recursive formula. This corresponds to OEIS:A000085.

def cardFun : ℕ → ℕ | 0 => 1 | 1 => 1 | Nat.succ (Nat.succ n) => cardFun (Nat.succ n) + (n + 1) * cardFun n

The number of Wick contractions in WickContraction n is equal to the terms in Online Encyclopedia of Integer Sequences (OEIS) A000085. That is: 1, 1, 2, 4, 10, 26, 76, 232, 764, 2620, 9496, ...

All goals completed! 🐙