Physlib.QFT.PerturbationTheory.WickContraction.Basic

Given a natural number $n$, a Wick contraction is a finite collection $f$ of subsets of $\{0, 1, \dots, n-1\}$ such that: 1. Each subset $a \in f$ contains exactly two elements (i.e., it is a pair). 2. Any two distinct subsets $a, b \in f$ are disjoint, meaning no element of $\{0, 1, \dots, n-1\}$ is contained in more than one pair. This represents the set of pairings used to contract fields in Wick's theorem.

For any natural number $n$, it is decidable whether two Wick contractions of $n$ indices are equal. That is, given two Wick contractions $c_1, c_2$, there is an algorithmic procedure to determine if $c_1 = c_2$.

For a given natural number $n$, the empty Wick contraction is the contraction that contains no pairs of indices. It represents the case where none of the indices in $\{0, 1, \dots, n-1\}$ are contracted with each other.

Let $c$ be a Wick contraction of $n$ indices. The number of pairs in $c$ (its cardinality) is 0 if and only if $c$ is the empty Wick contraction.

Let $c$ be a Wick contraction of $n$ indices. If $c$ is not the empty contraction, then there exist indices $i$ and $j$ such that the pair $\{i, j\}$ is an element of $c$.

For any two natural numbers $n$ and $m$, an equality $n = m$ induces an equivalence (bijection) between the set of Wick contractions of $n$ indices and the set of Wick contractions of $m$ indices.

For any natural number $n$ and any Wick contraction $c$ of $n$ indices, the equivalence between the set of Wick contractions of $n$ indices and itself induced by the reflexivity of equality $n = n$ is the identity map. That is, applying the congruence map associated with $n = n$ to $c$ results in $c$ itself: $c.\text{congr}(\text{rfl}) = c$.

Let $n$ and $m$ be natural numbers such that $n = m$, and let $h$ denote this equality. Let $c$ be a Wick contraction of $n$ indices, which is defined as a collection of disjoint pairs of elements from the set $\{0, 1, \dots, n-1\}$. Let $\text{congr}(h)(c)$ be the Wick contraction of $m$ indices induced by the bijection of indices resulting from the equality $h$. Then the number of pairs (cardinality) in $\text{congr}(h)(c)$ is equal to the number of pairs in $c$.

Let $n$ and $m$ be natural numbers and $h: n = m$ be an equality. Let $c$ be a Wick contraction of $n$ indices, defined as a collection of disjoint pairs of elements from the set $\{0, 1, \dots, n-1\}$. Let $\text{congr}(h)$ be the equivalence between Wick contractions of $n$ indices and $m$ indices induced by the equality $h$. Then the collection of pairs in the Wick contraction $\text{congr}(h)(c)$ is equal to the collection obtained by mapping each pair in $c$ using the natural bijection between $\{0, 1, \dots, n-1\}$ and $\{0, 1, \dots, m-1\}$ induced by $h$.

Let $\text{WickContraction}(k)$ denote the set of Wick contractions of $k$ indices, which are collections of disjoint pairs of elements from the set $\{0, 1, \dots, k-1\}$. For any natural numbers $n, m,$ and $o$, and proofs of equality $h_1: n = m$ and $h_2: m = o$, let $\text{congr}(h)$ be the induced equivalence (bijection) between the corresponding sets of Wick contractions. Then, the composition of the equivalences $\text{congr}(h_1)$ and $\text{congr}(h_2)$ is equal to the equivalence $\text{congr}(h_1 \cdot h_2)$ induced by the transitivity of the equalities.

Let $\text{WickContraction}(k)$ denote the set of Wick contractions of $k$ indices, which are collections of disjoint pairs of elements from the set $\{0, 1, \dots, k-1\}$. For any natural numbers $n, m,$ and $o$, and proofs of equality $h_1: n = m$ and $h_2: m = o$, let $\text{congr}(h)$ be the induced equivalence (bijection) between the corresponding sets of Wick contractions. For any Wick contraction $c \in \text{WickContraction}(n)$, the composition of these bijections applied to $c$ satisfies $$\text{congr}(h_2)(\text{congr}(h_1)(c)) = \text{congr}(h_1 \cdot h_2)(c)$$ where $h_1 \cdot h_2$ is the equality $n = o$ obtained by the transitivity of $h_1$ and $h_2$.

Let $n$ and $m$ be natural numbers and let $h: n = m$ be an equality. Let $c$ be a Wick contraction of $n$ indices (a collection of disjoint pairs from the set $\{0, 1, \dots, n-1\}$), and let $\text{congr}(h, c)$ be the corresponding Wick contraction of $m$ indices induced by $h$. For any finite subset $a \subseteq \{0, 1, \dots, m-1\}$, $a$ is a pair in the contraction $\text{congr}(h, c)$ if and only if the image of $a$ under the index bijection $\phi: \{0, 1, \dots, m-1\} \to \{0, 1, \dots, n-1\}$ (induced by the equality $m = n$) is a pair in the original contraction $c$.

Let $n$ and $m$ be natural numbers and $h: n = m$ be an equality. Given a Wick contraction $c$ of $n$ indices (defined as a collection of disjoint pairs of elements from $\{0, 1, \dots, n-1\}$) and a specific contracted pair $a \in c$, this function returns the corresponding contracted pair in the induced Wick contraction $\text{congr}(h, c)$ of $m$ indices. The resulting pair is obtained by applying the index bijection $\phi: \{0, 1, \dots, n-1\} \xrightarrow{\cong} \{0, 1, \dots, m-1\}$ induced by the equality $h$ to the elements of $a$.

Let $n$ be a natural number and $c$ be a Wick contraction of $n$ indices (defined as a collection of disjoint pairs from the set $\{0, 1, \dots, n-1\}$). For the reflexivity equality $n = n$ (denoted as $\text{rfl}$), the function $\text{congrLift}$ that maps a contracted pair $a \in c$ to its corresponding pair in the induced Wick contraction is the identity function.

Let $n$ and $m$ be natural numbers and $h: n = m$ be an equality. Let $c$ be a Wick contraction of $n$ indices, which is a collection of disjoint pairs of elements from the set $\{0, 1, \dots, n-1\}$. The function $c.\text{congrLift}(h)$ maps each contracted pair $a \in c$ to its corresponding pair in the Wick contraction of $m$ indices induced by the equality $h$. This theorem states that the mapping $c.\text{congrLift}(h)$ is injective.

Let $n$ and $m$ be natural numbers and $h: n = m$ be an equality. Let $c$ be a Wick contraction of $n$ indices, defined as a collection of disjoint pairs from the set $\{0, 1, \dots, n-1\}$. The map $\text{congrLift}_h$, which sends each pair $a \in c$ to its corresponding pair in the induced Wick contraction of $m$ indices, is surjective.

Let $n$ and $m$ be natural numbers and let $h: n = m$ be an equality. For a Wick contraction $c$ of $n$ indices, which consists of a collection of disjoint pairs of elements from the set $\{0, 1, \dots, n-1\}$, the function $c.\text{congrLift}(h)$ maps each pair $a \in c$ to its corresponding pair in the Wick contraction of $m$ indices induced by the equality $h$. This theorem states that the mapping $c.\text{congrLift}(h)$ is bijective.

Let $n, m$ be natural numbers and $h: n = m$ be an equality. Let $c$ be a Wick contraction of $n$ indices, and let $c' = \text{congr}(h, c)$ be the corresponding Wick contraction of $m$ indices induced by the bijection between the index sets $\{0, 1, \dots, n-1\}$ and $\{0, 1, \dots, m-1\}$. For any pair of indices $a$ belonging to the contraction $c'$, this function returns the corresponding pair in the original contraction $c$ by applying the inverse index mapping.

For any natural number $n$ and any Wick contraction $c$ of $n$ indices, the inverse mapping of pairs induced by the reflexivity of equality $n=n$, denoted $c.\text{congrLiftInv}(\text{rfl})$, is the identity function. Here, a Wick contraction $c$ is a collection of disjoint pairs of indices from $\{0, 1, \dots, n-1\}$, and $\text{congrLiftInv}$ is the function that maps pairs from a transformed contraction back to the original pairs.

Given a Wick contraction $c$ of $n$ indices and a specific index $i \in \{0, 1, \dots, n-1\}$, this function returns the index $j$ that is paired with $i$ in $c$. Specifically, if there exists a $j$ such that the set $\{i, j\}$ is a contracted pair in $c$, the function returns $\text{some } j$. If no such $j$ exists (meaning $i$ is not involved in any contraction), it returns $\text{none}$.

Let $n$ and $m$ be natural numbers such that $n = m$. Let $\phi: \{0, \dots, n-1\} \to \{0, \dots, m-1\}$ be the bijection induced by this equality, and let $c$ be a Wick contraction of $n$ indices. Let $c'$ be the corresponding Wick contraction of $m$ indices obtained via the equivalence $\text{WickContraction}(n) \simeq \text{WickContraction}(m)$. For any index $i \in \{0, \dots, m-1\}$, the partner of $i$ in $c'$ is equal to $\phi(j)$ if the partner of $\phi^{-1}(i)$ in $c$ is $j$. If $\phi^{-1}(i)$ is not involved in any contraction in $c$, then $i$ is not involved in any contraction in $c'$.

Let $n$ and $m$ be natural numbers such that $n = m$, and let $\phi: \{0, \dots, n-1\} \to \{0, \dots, m-1\}$ be the bijection induced by this equality. Let $c$ be a Wick contraction of $n$ indices, and let $c'$ be the corresponding Wick contraction of $m$ indices obtained via the equivalence $\text{WickContraction}(n) \simeq \text{WickContraction}(m)$. For any index $i \in \{0, \dots, m-1\}$, if $i$ has a contracted partner in $c'$, then that partner is equal to $\phi(j)$, where $j$ is the partner of $\phi^{-1}(i)$ in $c$.

For a Wick contraction $c$ of $n$ indices and any two indices $i, j \in \{0, 1, \dots, n-1\}$, the partner of $i$ in the contraction $c$ is $j$ if and only if the pair $\{i, j\}$ is an element of the collection of pairs defining $c$.

For any Wick contraction $c$ of $n = 1$ index and for any index $i \in \{0\}$, the partner of $i$ in the contraction $c$ is undefined (i.e., $c.\text{getDual?}(i) = \text{none}$).

Let $c$ be a Wick contraction of $n$ indices. For any index $i \in \{0, 1, \dots, n-1\}$, if $i$ is involved in a contraction (i.e., there exists a partner $j$ such that $c.\text{getDual?}(i) = \text{some } j$), then the pair $\{j, i\}$ is an element of the collection of pairs defining the contraction $c$.

Let $c$ be a Wick contraction of $n$ indices. For any index $i \in \{0, 1, \dots, n-1\}$, if $i$ is involved in a contraction (i.e., its partner exists), let $j$ be the partner of $i$ in $c$. Then the pair $\{i, j\}$ is an element of the collection of pairs defining the contraction $c$.

Let $c$ be a Wick contraction of $n$ indices. For any indices $i, j \in \{0, 1, \dots, n-1\}$, if the index $j$ is the contracted partner of $i$ in $c$ (meaning $c.\text{getDual?}(i) = \text{some } j$), then $i \neq j$.

Let $c$ be a Wick contraction of $n$ indices. For any index $i \in \{0, 1, \dots, n-1\}$, if $i$ is involved in a contraction with a partner index $j$, then $i \neq j$.

Let $c$ be a Wick contraction of $n$ indices. For any index $i \in \{0, 1, \dots, n-1\}$, if $i$ has a contracted partner $j$ (meaning the pair $\{i, j\}$ is in $c$), then $j \neq i$.

Let $c$ be a Wick contraction of $n$ indices. For any index $i \in \{0, 1, \dots, n-1\}$, the contracted partner of $i$ exists (i.e., `c.getDual? i` is not `none`) if and only if there exists a pair $a$ in the contraction $c$ such that $i \in a$.

Let $c$ be a Wick contraction of $n$ indices (a collection of disjoint pairs of indices from $\{0, 1, \dots, n-1\}$). For any pair $a$ in the contraction $c$, if an index $i$ is an element of $a$, then $i$ has a contracted partner in $c$ (i.e., the function $\text{getDual?}(i)$ returns a value).

Let $c$ be a Wick contraction of $n$ indices. For any index $i \in \{0, 1, \dots, n-1\}$, if $i$ has a contracted partner $j$ (meaning the function `c.getDual? i` returns $j$), then the contracted partner of $j$ is $i$ (meaning `c.getDual? j = some i`).

Let $c$ be a Wick contraction of $n$ indices, defined as a collection of disjoint pairs of indices from the set $\{0, 1, \dots, n-1\}$. For any index $i \in \{0, 1, \dots, n-1\}$, let $\text{getDual?}(i)$ be the function that returns the index $j$ paired with $i$ in $c$, or $\text{none}$ if $i$ is not part of any pair. If $i$ has a contracted partner $j$ (i.e., $\text{getDual?}(i)$ returns a value), then $j$ also has a contracted partner (i.e., $\text{getDual?}(j)$ returns a value).

Let $c$ be a Wick contraction of $n$ indices. For any index $i \in \{0, 1, \dots, n-1\}$, if $i$ has a contracted partner $j$ (meaning the function $\text{getDual?}(i)$ returns $\text{some } j$), then the contracted partner of $j$ is not $\text{none}$ (i.e., $\text{getDual?}(j) \neq \text{none}$).

For a Wick contraction $c$ of $n$ indices, let $a \in c$ be a contracted pair consisting of two indices $\{i, j\} \subset \{0, 1, \dots, n-1\}$. This function returns the smaller of the two indices in the pair $a$, i.e., $\min \{i, j\}$.

Given natural numbers $n$ and $m$ such that $n = m$, let $c$ be a Wick contraction of $n$ indices and let $a \in c$ be a contracted pair. The smaller index of the corresponding pair in the induced Wick contraction of $m$ indices is equal to the image of the smaller index of $a$ under the natural bijection between index sets $\{0, 1, \dots, n-1\}$ and $\{0, 1, \dots, m-1\}$ induced by the equality $n = m$.

Given a Wick contraction $c$ of $n$ indices and a contracted pair $a \in c$, where $a$ consists of two distinct indices $\{i, j\} \subset \{0, 1, \dots, n-1\}$, this function returns the larger of the two indices. Specifically, if the pair is ordered such that $i < j$, the function returns $j$.

Let $n$ and $m$ be natural numbers and $h: n = m$ be an equality. Let $c$ be a Wick contraction of $n$ indices (a collection of disjoint pairs of indices from $\{0, 1, \dots, n-1\}$) and let $a \in c$ be a specific contracted pair. Then the larger index (the second field) of the corresponding pair in the induced Wick contraction of $m$ indices is equal to the image of the larger index of $a$ under the index bijection $\phi: \{0, 1, \dots, n-1\} \xrightarrow{\cong} \{0, 1, \dots, m-1\}$ induced by $h$.

For a Wick contraction $c$ of $n$ indices, let $a \in c$ be a contracted pair. The set of indices constituting the pair $a$ is equal to $\{i, j\}$, where $i$ is the smaller index in the pair (the first field of the contract) and $j$ is the larger index in the pair (the second field of the contract).

For a Wick contraction $c$ of $n$ indices and a contracted pair $a \in c$, the smaller index of the pair (the first field of the contract) is not equal to the larger index of the pair (the second field of the contract).

For any Wick contraction $c$ of $n$ indices and any contracted pair $a \in c$, the smaller index of the pair (denoted as the first field of the contract) is less than or equal to the larger index of the pair (denoted as the second field of the contract).

For a Wick contraction $c$ of $n$ indices and any contracted pair $a \in c$, the smaller index of the pair (the first field of the contract) is strictly less than the larger index of the pair (the second field of the contract).

Let $c$ be a Wick contraction of $n$ indices. For any pair $a \in c$ within the contraction, the smaller of the two indices in $a$ (referred to as the first field of the contract) is an element of the set of indices that constitute the pair $a$.

Let $c$ be a Wick contraction of $n$ indices and let $a \in c$ be a pair in the contraction. Let $i = \min(a)$ be the smaller of the two indices in the pair $a$. Then the contracted partner of $i$ in the contraction $c$ exists (i.e., $c.\text{getDual?}(i)$ is not $\text{none}$).

Let $c$ be a Wick contraction of $n$ indices and let $a \in c$ be a pair in the contraction. Let $i = \min(a)$ and $j = \max(a)$ be the smaller and larger indices of the pair $a$, respectively. Then the contracted partner of $i$ in the contraction $c$ is $j$.

Let $c$ be a Wick contraction of $n$ indices and let $a \in c$ be a contracted pair. Then the larger index of the pair $a$ is an element of $a$.

Let $c$ be a Wick contraction of $n$ indices and let $a \in c$ be a pair in the contraction. Let $j$ be the larger index of the pair $a$ (the second field of the contract). Then $j$ has a contracted partner in $c$ (i.e., the result of the partner lookup `getDual?` is not empty).

For a Wick contraction $c$ of $n$ indices and any contracted pair $a \in c$, let $j$ be the larger index in $a$ (the second field of the contract) and $i$ be the smaller index in $a$ (the first field of the contract). Then the partner of $j$ in the contraction $c$ is $i$.

Given a Wick contraction $c$ of $n$ indices and a contracted pair $a \in c$ (which consists of two distinct indices $\{i, j\} \subset \{0, 1, \dots, n-1\}$), this definition establishes an equivalence (a bijection) between the set $a$ and the set $\{0, 1\}$. Under this equivalence, the smaller index in the pair $a$ (the first field of the contract) is mapped to $0$, and the larger index (the second field of the contract) is mapped to $1$.

Let $c$ be a Wick contraction of $n$ indices and let $a \in c$ be a contracted pair within it. For any function $f$ mapping the indices in $a$ to a commutative monoid $M$, the product of the values of $f$ over the pair $a$ is equal to the product of $f$ evaluated at the smaller index and $f$ evaluated at the larger index in $a$. That is, $$\prod_{x \in a} f(x) = f(i) \cdot f(j)$$ where $i$ is the smaller index ($\min a$) and $j$ is the larger index ($\max a$) of the pair.

Let $\mathcal{F}$ be a field specification. Given a list of field operators $\phi_s = [\phi_0, \phi_1, \dots, \phi_{n-1}]$ and a Wick contraction $\Lambda$ (a set of disjoint pairs of indices from $\{0, 1, \dots, n-1\}$), the contraction $\Lambda$ is said to be **grading compliant** if for every pair $\{i, j\} \in \Lambda$, the field operators at those positions have the same field statistic. That is, the condition $\mathcal{F} \triangleright_s \phi_i = \mathcal{F} \triangleright_s \phi_j$ must hold for every contracted pair, ensuring that bosonic fields are only paired with bosonic fields and fermionic fields are only paired with fermionic fields.

Let $\mathcal{F}$ be a field specification. Suppose $\phi_s$ and $\phi_s'$ are two lists of field operators such that $\phi_s = \phi_s'$. A Wick contraction $\Lambda$ of the indices $\{0, 1, \dots, |\phi_s|-1\}$ is grading compliant with respect to $\phi_s$ if and only if the congruent Wick contraction $\Lambda'$ (of the indices $\{0, 1, \dots, |\phi_s'|-1\}$) is grading compliant with respect to $\phi_s'$. A contraction is said to be grading compliant if for every contracted pair of indices $\{i, j\} \in \Lambda$, the field operators at those positions have the same field statistic (meaning bosonic fields are paired with bosonic fields and fermionic fields with fermionic fields).

Given a Wick contraction $c$ of $n$ indices (represented as a collection of disjoint pairs of indices from $\{0, 1, \dots, n-1\}$), this equivalence defines a bijection between the sigma type $\sum_{a \in c} a$ and the set of indices $x \in \{0, 1, \dots, n-1\}$ that are contracted. The sigma type $\sum_{a \in c} a$ consists of all pairs $(a, i)$ where $a$ is a contracted pair in $c$ and $i$ is an index contained in $a$. The bijection maps such a pair $(a, i)$ to the index $i$ itself. Conversely, it maps a contracted index $x$ to the pair $(a, x)$, where $a$ is the unique pair in $c$ containing $x$.