Physlib

Physlib.QFT.PerturbationTheory.WickContraction.Join

43 declarations

definition

Join of a Wick contraction Λ\Lambda and a contraction Λ\Lambda' on the uncontracted operators of Λ\Lambda

#join

Given a list of field operators ϕs\phi_s, let Λ\Lambda be a Wick contraction on the indices of ϕs\phi_s. Let [Λ]uc[\Lambda]^{uc} be the sub-list of field operators in ϕs\phi_s that are not participating in any pairing in Λ\Lambda. Given a second Wick contraction Λ\Lambda' defined on the indices of this uncontracted list [Λ]uc[\Lambda]^{uc}, the function join(Λ,Λ)\text{join}(\Lambda, \Lambda') defines a new Wick contraction on the original list ϕs\phi_s. This contraction is the union of the set of pairings in Λ\Lambda and the set of pairings in Λ\Lambda', where the indices in Λ\Lambda' are mapped back to their original positions in ϕs\phi_s using the embedding f:{0,,length([Λ]uc)1}{0,,length(ϕs)1}f: \{0, \dots, \text{length}([\Lambda]^{uc})-1\} \hookrightarrow \{0, \dots, \text{length}(\phi_s)-1\}.

theorem

Λ=Λ    join(Λ,Λuc)=join(Λ,Λuc)\Lambda = \Lambda' \implies \text{join}(\Lambda, \Lambda_{uc}) = \text{join}(\Lambda', \Lambda_{uc})

#join_congr

Let ϕs\phi_s be a list of field operators. Let Λ\Lambda and Λ\Lambda' be two Wick contractions on the indices {0,,ϕs1}\{0, \dots, |\phi_s|-1\}. If Λ=Λ\Lambda = \Lambda', then for any Wick contraction Λuc\Lambda_{uc} on the indices of the list of uncontracted operators [Λ]uc[\Lambda]^{uc}, the joined contraction join(Λ,Λuc)\text{join}(\Lambda, \Lambda_{uc}) is equal to join(Λ,Λuc)\text{join}(\Lambda', \Lambda'_{uc}), where Λuc\Lambda'_{uc} is the contraction Λuc\Lambda_{uc} mapped to the indices of [Λ]uc[\Lambda']^{uc} via the equivalence induced by the equality of the base contractions.

definition

Inclusion of pairings from Λ\Lambda into join(Λ,Λ)\text{join}(\Lambda, \Lambda')

#joinLiftLeft

Let ϕs\phi_s be a list of field operators, Λ\Lambda be a Wick contraction on the indices of ϕs\phi_s, and Λ\Lambda' be a Wick contraction on the list of uncontracted operators [Λ]uc[\Lambda]^{uc}. This function maps any pairing aa belonging to the contraction Λ\Lambda to the corresponding pairing in the joined Wick contraction join(Λ,Λ)\text{join}(\Lambda, \Lambda').

theorem

joinLiftLeft\text{joinLiftLeft} is injective

#jointLiftLeft_injective

Let ϕs\phi_s be a list of field operators. Let Λ\Lambda be a Wick contraction on the indices of ϕs\phi_s, and let Λ\Lambda' be a Wick contraction on the sub-list of operators [Λ]uc[\Lambda]^{uc} that are not contracted by Λ\Lambda. The mapping joinLiftLeft\text{joinLiftLeft}, which sends each pairing in the original contraction Λ\Lambda to its corresponding pairing in the joined contraction join(Λ,Λ)\text{join}(\Lambda, \Lambda'), is injective.

definition

Lifting a pairing from the uncontracted contraction Λ\Lambda' to the joined contraction join(Λ,Λ)\text{join}(\Lambda, \Lambda')

#joinLiftRight

Let ϕs\phi_s be a list of field operators and Λ\Lambda be a Wick contraction on the indices of ϕs\phi_s. Let [Λ]uc[\Lambda]^{uc} denote the sub-list of field operators that remain uncontracted by Λ\Lambda. Given a second Wick contraction Λ\Lambda' acting on the indices of [Λ]uc[\Lambda]^{uc}, the function `joinLiftRight` maps a pairing (a set of two indices) aΛa \in \Lambda' to its corresponding pairing in the joined contraction join(Λ,Λ)\text{join}(\Lambda, \Lambda'). This mapping is defined by applying the embedding f:{0,,length([Λ]uc)1}{0,,length(ϕs)1}f: \{0, \dots, \text{length}([\Lambda]^{uc})-1\} \hookrightarrow \{0, \dots, \text{length}(\phi_s)-1\} to the indices in aa, which translates the local indices of the uncontracted list back to their original positions in ϕs\phi_s.

theorem

The mapping `joinLiftRight` is injective

#joinLiftRight_injective

Let ϕs\phi_s be a list of field operators and let Λ\Lambda be a Wick contraction on the indices of ϕs\phi_s. Let [Λ]uc[\Lambda]^{uc} denote the sub-list of field operators from ϕs\phi_s that are not participating in any pairing in Λ\Lambda. Given a second Wick contraction Λ\Lambda' defined on the indices of the list [Λ]uc[\Lambda]^{uc}, the mapping joinLiftRight\text{joinLiftRight}—which maps each pairing aΛa \in \Lambda' to its corresponding pairing in the joined contraction join(Λ,Λ)\text{join}(\Lambda, \Lambda') by translating the indices of [Λ]uc[\Lambda]^{uc} back to their original positions in ϕs\phi_s—is injective.

theorem

Pairings from Λ\Lambda and Λ\Lambda' are Disjoint in join(Λ,Λ)\text{join}(\Lambda, \Lambda')

#jointLiftLeft_disjoint_joinLiftRight

Let ϕs\phi_s be a list of field operators, Λ\Lambda be a Wick contraction on the indices of ϕs\phi_s, and Λ\Lambda' be a Wick contraction on the sub-list of uncontracted operators [Λ]uc[\Lambda]^{uc}. For any pairing aΛa \in \Lambda and any pairing bΛb \in \Lambda', the set of indices in the original list ϕs\phi_s associated with aa and the set of indices in ϕs\phi_s associated with bb (after mapping the indices of bb from the uncontracted list back to their original positions in ϕs\phi_s) are disjoint.

theorem

joinLiftLeft(a)joinLiftRight(b)\text{joinLiftLeft}(a) \neq \text{joinLiftRight}(b) for joined Wick contractions

#jointLiftLeft_ne_joinLiftRight

Let ϕs\phi_s be a list of field operators. Let Λ\Lambda be a Wick contraction on the indices of ϕs\phi_s, and let Λ\Lambda' be a Wick contraction on the list of operators [Λ]uc[\Lambda]^{uc} that remain uncontracted by Λ\Lambda. For any pairing aΛa \in \Lambda and any pairing bΛb \in \Lambda', the pairings in the joined contraction join(Λ,Λ)\text{join}(\Lambda, \Lambda') obtained by lifting aa (via joinLiftLeft\text{joinLiftLeft}) and bb (via joinLiftRight\text{joinLiftRight}) are distinct; that is, joinLiftLeft(a)joinLiftRight(b)\text{joinLiftLeft}(a) \neq \text{joinLiftRight}(b).

definition

Lifting pairings from ΛΛ\Lambda \oplus \Lambda' to join(Λ,Λ)\text{join}(\Lambda, \Lambda')

#joinLift

Let ϕs\phi_s be a list of field operators. Let Λ\Lambda be a Wick contraction on the indices of ϕs\phi_s, and let Λ\Lambda' be a Wick contraction on the indices of the sub-list of operators [Λ]uc[\Lambda]^{uc} that remain uncontracted by Λ\Lambda. The function maps an element of the disjoint union of the pairings in Λ\Lambda and the pairings in Λ\Lambda' to its corresponding pairing in the joined contraction join(Λ,Λ)\text{join}(\Lambda, \Lambda'). Specifically, a pairing originating from Λ\Lambda is mapped using `joinLiftLeft`, and a pairing originating from Λ\Lambda' is mapped using `joinLiftRight`.

theorem

The mapping joinLift\text{joinLift} is injective

#joinLift_injective

Let ϕs\phi_s be a list of field operators and Λ\Lambda be a Wick contraction on the indices of ϕs\phi_s. Let [Λ]uc[\Lambda]^{uc} denote the sub-list of field operators in ϕs\phi_s that are not participating in any pairing in Λ\Lambda. Given a Wick contraction Λ\Lambda' on the indices of [Λ]uc[\Lambda]^{uc}, the function joinLift\text{joinLift} maps the pairings from the disjoint union of Λ\Lambda and Λ\Lambda' to the pairings in the joined contraction join(Λ,Λ)\text{join}(\Lambda, \Lambda'). This mapping joinLift\text{joinLift} is injective.

theorem

The map joinLift\text{joinLift} is surjective

#joinLift_surjective

Let ϕs\phi_s be a list of field operators and Λ\Lambda be a Wick contraction on the indices of ϕs\phi_s. Let [Λ]uc[\Lambda]^{uc} denote the sub-list of field operators in ϕs\phi_s that are not participating in any pairing in Λ\Lambda. Given a Wick contraction Λ\Lambda' on the indices of [Λ]uc[\Lambda]^{uc}, the function joinLift\text{joinLift} maps the pairings from the disjoint union of Λ\Lambda and Λ\Lambda' to the pairings in the joined contraction join(Λ,Λ)\text{join}(\Lambda, \Lambda'). This mapping joinLift\text{joinLift} is surjective.

theorem

The mapping joinLift\text{joinLift} is bijective

#joinLift_bijective

Let ϕs\phi_s be a list of field operators and Λ\Lambda be a Wick contraction on the indices of ϕs\phi_s. Let [Λ]uc[\Lambda]^{uc} denote the sub-list of field operators in ϕs\phi_s that are not participating in any pairing in Λ\Lambda. Given a Wick contraction Λ\Lambda' on the indices of [Λ]uc[\Lambda]^{uc}, the function joinLift\text{joinLift} maps the pairings from the disjoint union of the set of pairings in Λ\Lambda and the set of pairings in Λ\Lambda' to the pairings in the joined contraction join(Λ,Λ)\text{join}(\Lambda, \Lambda'). This mapping joinLift\text{joinLift} is bijective.

theorem

join(Λ,Λ)=ΛΛ\prod \text{join}(\Lambda, \Lambda') = \prod \Lambda \cdot \prod \Lambda'

#prod_join

Let ϕs\phi_s be a list of field operators and MM be a commutative monoid. Let Λ\Lambda be a Wick contraction on the indices of ϕs\phi_s, and let Λ\Lambda' be a Wick contraction on the indices of the sub-list of operators [Λ]uc[\Lambda]^{uc} that remain uncontracted by Λ\Lambda. For any function ff mapping the pairings of the joined contraction join(Λ,Λ)\text{join}(\Lambda, \Lambda') to MM, the product over all pairings in the joined contraction satisfies: ajoin(Λ,Λ)f(a)=(aΛf(joinLiftLeft(a)))(aΛf(joinLiftRight(a)))\prod_{a \in \text{join}(\Lambda, \Lambda')} f(a) = \left( \prod_{a \in \Lambda} f(\text{joinLiftLeft}(a)) \right) \cdot \left( \prod_{a \in \Lambda'} f(\text{joinLiftRight}(a)) \right) where joinLiftLeft\text{joinLiftLeft} and joinLiftRight\text{joinLiftRight} are the natural inclusions of the pairings from Λ\Lambda and Λ\Lambda' into join(Λ,Λ)\text{join}(\Lambda, \Lambda'), respectively.

theorem

Any pairing in join(Λ,Λ)\text{join}(\Lambda, \Lambda') originates from Λ\Lambda or Λ\Lambda'

#joinLiftLeft_or_joinLiftRight_of_mem_join

Let ϕs\phi_s be a list of field operators. Let Λ\Lambda be a Wick contraction on the indices of ϕs\phi_s, and let Λ\Lambda' be a Wick contraction on the sub-list of operators [Λ]uc[\Lambda]^{uc} that remain uncontracted by Λ\Lambda. For any pairing aa (a set of two indices) in the joined Wick contraction join(Λ,Λ)\text{join}(\Lambda, \Lambda'), there exists either a pairing bΛb \in \Lambda such that a=joinLiftLeft(b)a = \text{joinLiftLeft}(b), or a pairing bΛb' \in \Lambda' such that a=joinLiftRight(b)a = \text{joinLiftRight}(b').

theorem

The first index of a lifted pair in join(Λ,Λ)\text{join}(\Lambda, \Lambda') is the image of the first index in Λ\Lambda' under the uncontracted list embedding.

#join_fstFieldOfContract_joinLiftRight

Let ϕs\phi_s be a list of field operators and Λ\Lambda be a Wick contraction on the indices of ϕs\phi_s. Let [Λ]uc[\Lambda]^{uc} denote the sub-list of field operators in ϕs\phi_s that are not contracted by Λ\Lambda. Let f:{0,,length([Λ]uc)1}{0,,length(ϕs)1}f: \{0, \dots, \text{length}([\Lambda]^{uc})-1\} \hookrightarrow \{0, \dots, \text{length}(\phi_s)-1\} be the embedding (the function `uncontractedListEmd`) that maps the index of an operator in the uncontracted list to its original position in ϕs\phi_s. For any Wick contraction Λ\Lambda' defined on the indices of [Λ]uc[\Lambda]^{uc} and any contracted pair aΛa \in \Lambda', the first index (the smaller of the two indices) of the corresponding pair in the joined contraction join(Λ,Λ)\text{join}(\Lambda, \Lambda') is equal to the image under ff of the first index of the pair aa in Λ\Lambda'.

theorem

The larger index of a right-lifted pairing in a joined Wick contraction

#join_sndFieldOfContract_joinLiftRight

Let ϕs\phi_s be a list of field operators. Let Λ\Lambda be a Wick contraction on ϕs\phi_s, and let [Λ]uc[\Lambda]^{uc} denote the sub-list of field operators that remain uncontracted. Suppose Λ\Lambda' is a second Wick contraction acting on the indices of the uncontracted list [Λ]uc[\Lambda]^{uc}. Let f:{0,1,,length([Λ]uc)1}{0,1,,length(ϕs)1}f: \{0, 1, \dots, \text{length}([\Lambda]^{uc}) - 1\} \hookrightarrow \{0, 1, \dots, \text{length}(\phi_s) - 1\} be the embedding that maps the index of an operator in the uncontracted list back to its original index in ϕs\phi_s. For any contracted pair aΛa \in \Lambda', the larger index of the lifted pairing in the joined contraction join(Λ,Λ)\text{join}(\Lambda, \Lambda') is equal to the image under ff of the larger index of aa in Λ\Lambda': \[ \text{snd}(\text{joinLiftRight}(a)) = f(\text{snd}(a)) \] where snd\text{snd} denotes the function that returns the larger index of a contracted pair.

theorem

The first index of a pair in Λ\Lambda is preserved in join(Λ,Λ)\text{join}(\Lambda, \Lambda')

#join_fstFieldOfContract_joinLiftLeft

Let ϕs\phi_s be a list of field operators belonging to a field specification F\mathcal{F}. Let Λ\Lambda be a Wick contraction on the indices of ϕs\phi_s, and let Λ\Lambda' be a Wick contraction on the indices of the list of uncontracted operators [Λ]uc[\Lambda]^{uc}. For any contracted pair aΛa \in \Lambda, the first index (the smaller of the two indices) of the corresponding pair in the joined Wick contraction join(Λ,Λ)\text{join}(\Lambda, \Lambda') is equal to the first index of aa in the original contraction Λ\Lambda.

theorem

The larger index of aΛa \in \Lambda is invariant in join(Λ,Λ)\text{join}(\Lambda, \Lambda')

#join_sndFieldOfContract_joinLift

Let ϕs\phi_s be a list of field operators. Let Λ\Lambda be a Wick contraction on the indices of ϕs\phi_s, and let Λ\Lambda' be a Wick contraction on the list of uncontracted operators [Λ]uc[\Lambda]^{uc}. For any contracted pair aΛa \in \Lambda, the larger index of the corresponding pair in the joined contraction join(Λ,Λ)\text{join}(\Lambda, \Lambda') is equal to the larger index of aa in the original contraction Λ\Lambda.

theorem

aΛ    f(a)join(Λ,Λ)a \in \Lambda' \iff f(a) \in \text{join}(\Lambda, \Lambda') for Wick contractions

#mem_join_right_iff

Let ϕs\phi_s be a list of field operators from a field specification F\mathcal{F}. Let Λ\Lambda be a Wick contraction on the indices of ϕs\phi_s, and let Λ\Lambda' be a Wick contraction on the indices of the list of operators [Λ]uc[\Lambda]^{uc} that remain uncontracted by Λ\Lambda. Let ff be the embedding (`uncontractedListEmd`) that maps an index of the uncontracted list to its corresponding original index in ϕs\phi_s. For any finite set of indices aa from the uncontracted list, aa is a contracted pair in Λ\Lambda' if and only if the image of aa under ff, denoted {f(i)ia}\{f(i) \mid i \in a\}, is a contracted pair in the joined Wick contraction join(Λ,Λ)\text{join}(\Lambda, \Lambda').

theorem

join(Λ,Λ)=Λ+Λ|\text{join}(\Lambda, \Lambda')| = |\Lambda| + |\Lambda'| for Wick contractions

#join_card

Let ϕs\phi_s be a list of field operators. Let Λ\Lambda be a Wick contraction on the indices of ϕs\phi_s, and let [Λ]uc[\Lambda]^{uc} denote the list of operators remaining uncontracted by Λ\Lambda. If Λ\Lambda' is a Wick contraction on the indices of [Λ]uc[\Lambda]^{uc}, then the number of pairings in the joined Wick contraction join(Λ,Λ)\text{join}(\Lambda, \Lambda') is equal to the sum of the number of pairings in Λ\Lambda and Λ\Lambda': join(Λ,Λ)=Λ+Λ|\text{join}(\Lambda, \Lambda')| = |\Lambda| + |\Lambda'|

theorem

join(empty,Λ)=Λ\text{join}(\text{empty}, \Lambda) = \Lambda for Wick contractions

#empty_join

For any list of field operators ϕs\phi_s, let Λ\Lambda_\emptyset be the empty Wick contraction on the indices of ϕs\phi_s. Let [Λ]uc[\Lambda_\emptyset]^{uc} be the list of field operators in ϕs\phi_s that are not participating in any pairing in Λ\Lambda_\emptyset (which is identically ϕs\phi_s). For any Wick contraction Λ\Lambda defined on the indices of [Λ]uc[\Lambda_\emptyset]^{uc}, the join of Λ\Lambda_\emptyset and Λ\Lambda is equal to the Wick contraction Λ\Lambda (under the canonical equivalence induced by the identification of indices).

theorem

join(Λ,empty)=Λ\text{join}(\Lambda, \text{empty}) = \Lambda for Wick contractions

#join_empty

Let ϕs\phi_s be a list of field operators and Λ\Lambda be a Wick contraction on the indices of ϕs\phi_s. The join of Λ\Lambda with the empty Wick contraction (defined on the set of indices uncontracted by Λ\Lambda) is equal to Λ\Lambda.

theorem

timeContract(join(Λ,Λ))=timeContract(Λ)timeContract(Λ)\text{timeContract}(\text{join}(\Lambda, \Lambda')) = \text{timeContract}(\Lambda) \cdot \text{timeContract}(\Lambda')

#join_timeContract

Let ϕs\phi_s be a list of field operators. Let Λ\Lambda be a Wick contraction on the indices of ϕs\phi_s, and let [Λ]uc[\Lambda]^{uc} be the sub-list of field operators in ϕs\phi_s that remain uncontracted by Λ\Lambda. For any Wick contraction Λ\Lambda' defined on the indices of the uncontracted list [Λ]uc[\Lambda]^{uc}, the time contraction of the joined contraction join(Λ,Λ)\text{join}(\Lambda, \Lambda') is equal to the product of the time contraction of Λ\Lambda and the time contraction of Λ\Lambda': \[ \text{timeContract}(\text{join}(\Lambda, \Lambda')) = \text{timeContract}(\Lambda) \cdot \text{timeContract}(\Lambda') \] where the time contraction of a Wick contraction Λ\Lambda is defined as the product of the pairwise contractions of the field operators corresponding to the indices paired in Λ\Lambda.

theorem

staticContract(join(Λ,Λ))=staticContract(Λ)staticContract(Λ)\text{staticContract}(\text{join}(\Lambda, \Lambda')) = \text{staticContract}(\Lambda) \cdot \text{staticContract}(\Lambda')

#join_staticContract

Let ϕs\phi_s be a list of field operators. Let Λ\Lambda be a Wick contraction on the indices of ϕs\phi_s, and let [Λ]uc[\Lambda]^{uc} be the list of field operators that remain uncontracted by Λ\Lambda. Given a second Wick contraction Λ\Lambda' defined on the indices of [Λ]uc[\Lambda]^{uc}, the static contraction of the joined contraction join(Λ,Λ)\text{join}(\Lambda, \Lambda') is equal to the product of the static contractions of Λ\Lambda and Λ\Lambda': staticContract(join(Λ,Λ))=staticContract(Λ)staticContract(Λ)\text{staticContract}(\text{join}(\Lambda, \Lambda')) = \text{staticContract}(\Lambda) \cdot \text{staticContract}(\Lambda') where the static contraction of a contraction cc is defined as the product {j,k}c,j<k[ϕj,ϕk]s\prod_{\{j, k\} \in c, j < k} [\phi_j^-, \phi_k]_s of super-commutators of the annihilation parts of the field operators.

theorem

iΛ.uncontracted    f(i)join(Λ,Λ).uncontractedi \in \Lambda'.\text{uncontracted} \implies f(i) \in \text{join}(\Lambda, \Lambda').\text{uncontracted}

#mem_join_uncontracted_of_mem_right_uncontracted

Let ϕs\phi_s be a list of field operators and Λ\Lambda be a Wick contraction on the indices of ϕs\phi_s. Let [Λ]uc[\Lambda]^{uc} be the sub-list of field operators that are uncontracted by Λ\Lambda. Given a second Wick contraction Λ\Lambda' on the indices of [Λ]uc[\Lambda]^{uc}, let join(Λ,Λ)\text{join}(\Lambda, \Lambda') be the union of these two contractions. If an index ii is uncontracted in Λ\Lambda', then the corresponding original index in ϕs\phi_s, given by the embedding f:{0,,length([Λ]uc)1}{0,,length(ϕs)1}f: \{0, \dots, \text{length}([\Lambda]^{uc})-1\} \hookrightarrow \{0, \dots, \text{length}(\phi_s)-1\}, is uncontracted in the combined contraction join(Λ,Λ)\text{join}(\Lambda, \Lambda').

theorem

iuncontracted(join(Λ,Λ))    iuncontracted(Λ)i \in \text{uncontracted}(\text{join}(\Lambda, \Lambda')) \implies i \in \text{uncontracted}(\Lambda)

#exists_mem_left_uncontracted_of_mem_join_uncontracted

Let ϕs\phi_s be a list of field operators and let Λ\Lambda be a Wick contraction on the indices of ϕs\phi_s. Let [Λ]uc[\Lambda]^{uc} be the list of field operators remaining uncontracted by Λ\Lambda, and let Λ\Lambda' be a Wick contraction on the indices of [Λ]uc[\Lambda]^{uc}. For any index i{0,,length(ϕs)1}i \in \{0, \dots, \text{length}(\phi_s)-1\}, if ii is uncontracted in the joined contraction join(Λ,Λ)\text{join}(\Lambda, \Lambda'), then ii is necessarily uncontracted in the initial contraction Λ\Lambda.

theorem

iuncontracted(join(Λ,Λ))    auncontracted(Λ),f(a)=ii \in \text{uncontracted}(\text{join}(\Lambda, \Lambda')) \implies \exists a \in \text{uncontracted}(\Lambda'), f(a) = i

#exists_mem_right_uncontracted_of_mem_join_uncontracted

Let ϕs\phi_s be a list of field operators. Let Λ\Lambda be a Wick contraction on the indices of ϕs\phi_s, and let [Λ]uc[\Lambda]^{uc} be the sub-list of field operators that are uncontracted by Λ\Lambda. Let Λ\Lambda' be a Wick contraction on the indices of [Λ]uc[\Lambda]^{uc}. If an index i{0,,length(ϕs)1}i \in \{0, \dots, \text{length}(\phi_s)-1\} is uncontracted in the joined contraction join(Λ,Λ)\text{join}(\Lambda, \Lambda'), then there exists an index a{0,,length([Λ]uc)1}a \in \{0, \dots, \text{length}([\Lambda]^{uc})-1\} such that ii is the original index corresponding to aa via the embedding f:{0,,length([Λ]uc)1}{0,,length(ϕs)1}f: \{0, \dots, \text{length}([\Lambda]^{uc})-1\} \hookrightarrow \{0, \dots, \text{length}(\phi_s)-1\}, and aa is uncontracted in the second contraction Λ\Lambda'.

theorem

uncontractedList(join(Λ,Λ))=map f(Λ.uncontractedList)\text{uncontractedList}(\text{join}(\Lambda, \Lambda')) = \text{map } f (\Lambda'.\text{uncontractedList})

#join_uncontractedList

Let ϕs\phi_s be a list of field operators. Let Λ\Lambda be a Wick contraction on the indices of ϕs\phi_s, and let Λ\Lambda' be a Wick contraction on the sub-list of operators [Λ]uc[\Lambda]^{uc} that are uncontracted by Λ\Lambda. The sorted list of indices in ϕs\phi_s that remain uncontracted under the joined contraction join(Λ,Λ)\text{join}(\Lambda, \Lambda') is equal to the list obtained by applying the embedding f:{0,,length([Λ]uc)1}{0,,length(ϕs)1}f: \{0, \dots, \text{length}([\Lambda]^{uc})-1\} \hookrightarrow \{0, \dots, \text{length}(\phi_s)-1\} to each element of the sorted list of indices uncontracted by Λ\Lambda'.

theorem

uncontractedList(join(Λ,Λ))[j]=f(uncontractedList(Λ)[j])\text{uncontractedList}(\text{join}(\Lambda, \Lambda'))[j] = f(\text{uncontractedList}(\Lambda')[j])

#join_uncontractedList_get

Let ϕs\phi_s be a list of field operators. Let Λ\Lambda be a Wick contraction on the indices of ϕs\phi_s, and let Λ\Lambda' be a Wick contraction on the indices of the sub-list [Λ]uc[\Lambda]^{uc} consisting of operators uncontracted by Λ\Lambda. Let f:{0,,length([Λ]uc)1}{0,,length(ϕs)1}f: \{0, \dots, \text{length}([\Lambda]^{uc})-1\} \hookrightarrow \{0, \dots, \text{length}(\phi_s)-1\} be the embedding (`uncontractedListEmd`) that maps an index in the uncontracted sub-list to its original position in ϕs\phi_s. Then, the jj-th element of the sorted list of indices uncontracted by the joined contraction join(Λ,Λ)\text{join}(\Lambda, \Lambda') is equal to f(k)f(k), where kk is the jj-th element of the sorted list of indices uncontracted by Λ\Lambda'.

theorem

[join(Λ,Λ)]uc=[Λ]uc[\text{join}(\Lambda, \Lambda')]^{uc} = [\Lambda']^{uc} for uncontracted field operators

#join_uncontractedListGet

Let ϕs\phi_s be a list of field operators. Let Λ\Lambda be a Wick contraction on the indices of ϕs\phi_s, and let [Λ]uc[\Lambda]^{uc} denote the sub-list of field operators in ϕs\phi_s that are uncontracted by Λ\Lambda. Given a second Wick contraction Λ\Lambda' defined on the indices of the list [Λ]uc[\Lambda]^{uc}, the list of field operators that remain uncontracted under the joined contraction join(Λ,Λ)\text{join}(\Lambda, \Lambda') is equal to the list of operators in [Λ]uc[\Lambda]^{uc} that are uncontracted by Λ\Lambda'.

theorem

fjoin(Λ,Λ)=fΛfΛf_{\text{join}(\Lambda, \Lambda')} = f_{\Lambda} \circ f_{\Lambda'} for uncontracted index embeddings

#join_uncontractedListEmb

Let ϕs\phi_s be a list of field operators. Let Λ\Lambda be a Wick contraction on the indices of ϕs\phi_s, and let [Λ]uc[\Lambda]^{uc} denote the sub-list of field operators that are uncontracted by Λ\Lambda. Given a second Wick contraction Λ\Lambda' on the indices of [Λ]uc[\Lambda]^{uc}, let fΛ:{0,,[Λ]uc1}{0,,ϕs1}f_{\Lambda} : \{0, \dots, |[\Lambda]^{uc}|-1\} \hookrightarrow \{0, \dots, |\phi_s|-1\} be the embedding that maps an index in the uncontracted list of Λ\Lambda to its original position in ϕs\phi_s, and let fΛ:{0,,[Λ]uc1}{0,,[Λ]uc1}f_{\Lambda'} : \{0, \dots, |[\Lambda']^{uc}|-1\} \hookrightarrow \{0, \dots, |[\Lambda]^{uc}|-1\} be the embedding that maps an index in the uncontracted list of Λ\Lambda' to its position in [Λ]uc[\Lambda]^{uc}. Then the embedding for the joined contraction fjoin(Λ,Λ):{0,,[join(Λ,Λ)]uc1}{0,,ϕs1}f_{\text{join}(\Lambda, \Lambda')} : \{0, \dots, |[\text{join}(\Lambda, \Lambda')]^{uc}|-1\} \hookrightarrow \{0, \dots, |\phi_s|-1\} is equal to the composition of these embeddings: fjoin(Λ,Λ)=fΛfΛ f_{\text{join}(\Lambda, \Lambda')} = f_{\Lambda} \circ f_{\Lambda'} (where the domains are identified using the fact that the uncontracted operators of the joined contraction are exactly those of Λ\Lambda').

theorem

join(join(Λ,Λ),Λ)=join(Λ,join(Λ,Λ))\text{join}(\text{join}(\Lambda, \Lambda'), \Lambda'') = \text{join}(\Lambda, \text{join}(\Lambda', \Lambda'')) for Wick contractions

#join_assoc

Let ϕs\phi_s be a list of field operators. Let Λ\Lambda be a Wick contraction on the indices of ϕs\phi_s, and let [Λ]uc[\Lambda]^{uc} denote the sub-list of operators in ϕs\phi_s that remain uncontracted by Λ\Lambda. Let Λ\Lambda' be a second Wick contraction acting on the indices of [Λ]uc[\Lambda]^{uc}, and let Λ\Lambda'' be a third Wick contraction acting on the indices of the operators uncontracted by the joined contraction join(Λ,Λ)\text{join}(\Lambda, \Lambda'). Since the list of uncontracted operators of the joined contraction join(Λ,Λ)\text{join}(\Lambda, \Lambda') is identical to the list of uncontracted operators of Λ\Lambda' (i.e., [join(Λ,Λ)]uc=[Λ]uc[\text{join}(\Lambda, \Lambda')]^{uc} = [\Lambda']^{uc}), the contraction Λ\Lambda'' can be identified as a contraction acting on the uncontracted indices of Λ\Lambda'. Under this identification, the operation of joining Wick contractions is associative: join(join(Λ,Λ),Λ)=join(Λ,join(Λ,Λ)) \text{join}(\text{join}(\Lambda, \Lambda'), \Lambda'') = \text{join}(\Lambda, \text{join}(\Lambda', \Lambda''))

theorem

Index f(i)f(i) is uncontracted in join(Λ,Λ)    i\text{join}(\Lambda, \Lambda') \iff i is uncontracted in Λ\Lambda'

#join_getDual?_apply_uncontractedListEmb_eq_none_iff

Let ϕs\phi_s be a list of field operators and Λ\Lambda be a Wick contraction on the indices of ϕs\phi_s. Let [Λ]uc[\Lambda]^{uc} denote the list of field operators that are not contracted by Λ\Lambda, and let f:{0,1,,length([Λ]uc)1}{0,1,,length(ϕs)1}f: \{0, 1, \dots, \text{length}([\Lambda]^{uc}) - 1\} \hookrightarrow \{0, 1, \dots, \text{length}(\phi_s) - 1\} be the embedding that maps the index of an operator in the uncontracted list back to its original position in ϕs\phi_s. Given a second Wick contraction Λ\Lambda' on the indices of [Λ]uc[\Lambda]^{uc}, the index f(i)f(i) is uncontracted in the joined contraction join(Λ,Λ)\text{join}(\Lambda, \Lambda') if and only if the index ii is uncontracted in Λ\Lambda'.

theorem

Index f(i)f(i) is contracted in join(Λ,Λ)    i\text{join}(\Lambda, \Lambda') \iff i is contracted in Λ\Lambda'

#join_getDual?_apply_uncontractedListEmb_isSome_iff

Let ϕs\phi_s be a list of field operators and Λ\Lambda be a Wick contraction on the indices of ϕs\phi_s. Let [Λ]uc[\Lambda]^{uc} denote the list of field operators that are not contracted by Λ\Lambda, and let f:{0,1,,length([Λ]uc)1}{0,1,,length(ϕs)1}f: \{0, 1, \dots, \text{length}([\Lambda]^{uc}) - 1\} \hookrightarrow \{0, 1, \dots, \text{length}(\phi_s) - 1\} be the embedding that maps the index of an operator in the uncontracted list back to its original position in ϕs\phi_s. Given a second Wick contraction Λ\Lambda' on the indices of [Λ]uc[\Lambda]^{uc}, the index f(i)f(i) is contracted in the joined contraction join(Λ,Λ)\text{join}(\Lambda, \Lambda') if and only if the index ii is contracted in Λ\Lambda'.

theorem

Partner of an uncontracted index in the join ΛΛ\Lambda \cup \Lambda'

#join_getDual?_apply_uncontractedListEmb_some

Let ϕs\phi_s be a list of field operators and let Λ\Lambda be a Wick contraction on the indices of ϕs\phi_s. Let [Λ]uc[\Lambda]^{uc} be the list of operators in ϕs\phi_s that are not contracted by Λ\Lambda, and let f:{0,,length([Λ]uc)1}{0,,length(ϕs)1}f: \{0, \dots, \text{length}([\Lambda]^{uc}) - 1\} \hookrightarrow \{0, \dots, \text{length}(\phi_s) - 1\} be the embedding that maps an index in the uncontracted list to its original position in ϕs\phi_s. Suppose Λ\Lambda' is a second Wick contraction defined on the indices of [Λ]uc[\Lambda]^{uc}. For any index ii in the uncontracted list, if the index f(i)f(i) has a partner in the joined contraction join(Λ,Λ)\text{join}(\Lambda, \Lambda'), then this partner is given by f(j)f(j), where jj is the partner of ii in the contraction Λ\Lambda'.

theorem

The partner of f(i)f(i) in join(Λ,Λ)\text{join}(\Lambda, \Lambda') is the image of the partner of ii in Λ\Lambda'

#join_getDual?_apply_uncontractedListEmb

Let ϕs\phi_s be a list of field operators and Λ\Lambda be a Wick contraction on the indices of ϕs\phi_s. Let [Λ]uc[\Lambda]^{uc} be the sub-list of operators in ϕs\phi_s that are not contracted by Λ\Lambda, and let f:{0,,length([Λ]uc)1}{0,,length(ϕs)1}f: \{0, \dots, \text{length}([\Lambda]^{uc}) - 1\} \hookrightarrow \{0, \dots, \text{length}(\phi_s) - 1\} be the embedding that maps an index in the uncontracted list back to its original position in ϕs\phi_s. Given a second Wick contraction Λ\Lambda' on the indices of [Λ]uc[\Lambda]^{uc}, the contraction partner of the index f(i)f(i) in the joined contraction join(Λ,Λ)\text{join}(\Lambda, \Lambda') is the image under ff of the contraction partner of ii in Λ\Lambda'. That is, getDual?(join(Λ,Λ),f(i))=Option.map(f,getDual?(Λ,i))\text{getDual?}(\text{join}(\Lambda, \Lambda'), f(i)) = \text{Option.map}(f, \text{getDual?}(\Lambda', i)) where getDual?(c,k)\text{getDual?}(c, k) returns the index paired with kk in contraction cc, or none\text{none} if kk is unpaired.

theorem

join(ΛS,Λ/S)=Λ\text{join}(\Lambda|_S, \Lambda/S) = \Lambda

#join_sub_quot

Let ϕs\phi_s be a sequence of field operators and Λ\Lambda be a Wick contraction on ϕs\phi_s. For any subset SΛS \subseteq \Lambda of the contracted pairs, let ΛS\Lambda|_S be the sub-contraction containing only the pairs in SS, and let Λ/S\Lambda/S be the quotient contraction containing the pairs in Λ\Lambda that are not in SS. Then the join of the sub-contraction and the quotient contraction recovers the original contraction: join(ΛS,Λ/S)=Λ\text{join}(\Lambda|_S, \Lambda/S) = \Lambda

theorem

ΛS+Λ/S=Λ|\Lambda|_S| + |\Lambda/S| = |\Lambda| for Wick contractions

#subContraction_card_plus_quotContraction_card_eq

Let ϕs\phi_s be a sequence of field operators and Λ\Lambda be a Wick contraction on ϕs\phi_s. For any subset of contracted pairs SΛS \subseteq \Lambda, let ΛS\Lambda|_S be the sub-contraction containing only the pairs in SS, and let Λ/S\Lambda/S be the quotient contraction containing the pairs in Λ\Lambda that are not in SS (relabeled to correspond to the indices of the operators left uncontracted by ΛS\Lambda|_S). The sum of the number of pairings in the sub-contraction and the number of pairings in the quotient contraction is equal to the total number of pairings in the original contraction Λ\Lambda: ΛS+Λ/S=Λ|\Lambda|_S| + |\Lambda/S| = |\Lambda|

theorem

In the joined Wick contraction join(singleton(i,j),Λ)\text{join}(\text{singleton}(i, j), \Lambda'), the partner of ii is jj

#join_singleton_getDual?_left

Let ϕs\phi_s be a list of field operators and let ii and jj be indices in the list such that i<ji < j. Let singleton(i,j)\text{singleton}(i, j) be the Wick contraction consisting of the single pair {i,j}\{i, j\}. Given any Wick contraction Λ\Lambda' defined on the sub-list of field operators [singleton(i,j)]uc[\text{singleton}(i, j)]^{uc} (the operators not involved in the pairing {i,j}\{i, j\}), let Λ=join(singleton(i,j),Λ)\Lambda = \text{join}(\text{singleton}(i, j), \Lambda') be the combined Wick contraction on the original list ϕs\phi_s. Then, the index ii is paired with jj in Λ\Lambda.

theorem

The partner of jj in join({i,j},Λ)\text{join}(\{i, j\}, \Lambda') is ii

#join_singleton_getDual?_right

Let ϕs\phi_s be a list of field operators. For any two indices i,j{0,,ϕs1}i, j \in \{0, \dots, |\phi_s|-1\} such that i<ji < j, let Λ{i,j}\Lambda_{\{i, j\}} be the Wick contraction consisting only of the pair {i,j}\{i, j\}. Let Λ\Lambda' be a Wick contraction defined on the list of uncontracted operators [Λ{i,j}]uc[\Lambda_{\{i, j\}}]^{uc} (which consists of the operators in ϕs\phi_s excluding those at indices ii and jj). If Λ=join(Λ{i,j},Λ)\Lambda = \text{join}(\Lambda_{\{i, j\}}, \Lambda') is the Wick contraction formed by joining these two, then the contracted partner of the index jj in Λ\Lambda is ii.

theorem

A Wick contraction with Λ>0|\Lambda| > 0 contains at least one pair

#exists_contraction_pair_of_card_ge_zero

Let ϕs\phi_s be a list of field operators associated with a field specification F\mathcal{F}. Let Λ\Lambda be a Wick contraction on the indices {0,1,,n1}\{0, 1, \dots, n-1\} where nn is the length of ϕs\phi_s. If the number of pairs in the contraction satisfies Λ>0|\Lambda| > 0, then there exists a pair aa such that aΛa \in \Lambda.

theorem

Decomposition of non-empty grading-compliant Wick contractions into a singleton and a compliant remainder

#exists_join_singleton_of_card_ge_zero

Let F\mathcal{F} be a field specification and ϕs\phi_s be a list of field operators. Let Λ\Lambda be a Wick contraction on the indices of ϕs\phi_s such that its cardinality is greater than zero (Λ>0|\Lambda| > 0) and it is grading compliant. Then there exist indices i,j{0,,ϕs1}i, j \in \{0, \dots, |\phi_s|-1\} with i<ji < j and a Wick contraction Λ\Lambda' on the list of operators remaining after the indices ii and jj are removed (denoted [singleton(i,j)]uc[\text{singleton}(i, j)]^{uc}) such that: 1. Λ\Lambda is equal to the join of the singleton contraction {i,j}\{i, j\} and Λ\Lambda'. 2. The field statistics of the ii-th and jj-th operators are equal, i.e., Fsϕi=Fsϕj\mathcal{F} \triangleright_s \phi_i = \mathcal{F} \triangleright_s \phi_j. 3. The contraction Λ\Lambda' is grading compliant. 4. The number of pairs in Λ\Lambda' satisfies Λ+1=Λ|\Lambda'| + 1 = |\Lambda|.

theorem

Λ\Lambda not grading compliant     join(Λ,Λ)\implies \text{join}(\Lambda, \Lambda') not grading compliant

#join_not_gradingCompliant_of_left_not_gradingCompliant

Let ϕs\phi_s be a list of field operators associated with a field specification F\mathcal{F}. Let Λ\Lambda be a Wick contraction on the indices of ϕs\phi_s, and let Λ\Lambda' be a Wick contraction on the indices of the list of uncontracted operators [Λ]uc[\Lambda]^{uc}. If Λ\Lambda is not grading compliant (meaning there exists at least one contracted pair in Λ\Lambda whose operators have different field statistics), then the joined Wick contraction join(Λ,Λ)\text{join}(\Lambda, \Lambda') is also not grading compliant.