Physlib.QFT.PerturbationTheory.WickContraction.Uncontracted

For a Wick contraction $c$ on the set of indices $\{0, 1, \dots, n-1\}$, the set of uncontracted elements is the finite set (finset) of indices $i \in \{0, 1, \dots, n-1\}$ that are not part of any contracted pair in $c$. Formally, this is defined as the subset of indices for which the dual element function `getDual?` returns no value (none).

Let $n$ and $m$ be natural numbers such that $n = m$. For any Wick contraction $c$ on the set of indices $\{0, 1, \dots, n-1\}$, let $c'$ be the Wick contraction on $\{0, 1, \dots, m-1\}$ induced by the equality $n = m$. Then, the set of uncontracted indices of $c'$ is equal to the image of the set of uncontracted indices of $c$ under the natural bijection between $\{0, 1, \dots, n-1\}$ and $\{0, 1, \dots, m-1\}$.

Let $c$ be a Wick contraction on the set of indices $\{0, 1, \dots, n-1\}$. For any index $i \in \{0, 1, \dots, n-1\}$, the partner (dual) of $i$ under the contraction $c$ is undefined (denoted by `none`) if and only if $i$ belongs to the set of uncontracted indices of $c$.

Given two Wick contractions $c$ and $c'$ on a set of $n$ indices, if $c = c'$, there exists an equivalence (a bijection) between the sets of their uncontracted indices, each augmented with an additional "none" element. Formally, for $c = c'$, this is the bijection between $\text{Option}(U_c)$ and $\text{Option}(U_{c'})$, where $U_c \subset \{0, 1, \dots, n-1\}$ is the set of indices that are not part of any contracted pair in $c$.

Let $c$ and $c'$ be Wick contractions on the set of indices $\{0, 1, \dots, n-1\}$, and let $U_c$ and $U_{c'}$ be the sets of uncontracted indices for $c$ and $c'$ respectively. Given a proof $h : c = c'$, let $f : \text{Option}(U_c) \simeq \text{Option}(U_{c'})$ be the equivalence (bijection) between the augmented sets of uncontracted indices defined by `uncontractedCongr h`. Then the bijection maps the element $\text{none}$ in $\text{Option}(U_c)$ to the element $\text{none}$ in $\text{Option}(U_{c'})$.

Let $c$ and $c'$ be Wick contractions on the set of indices $\{0, 1, \dots, n-1\}$, and let $U_c$ and $U_{c'}$ denote their respective sets of uncontracted indices. Given a proof $h: c = c'$, let $f: \text{Option}(U_c) \simeq \text{Option}(U_{c'})$ be the equivalence between the sets of uncontracted indices (each augmented with a "none" element) defined by `uncontractedCongr h`. For any uncontracted index $i \in U_c$, the equivalence maps the element $\text{some}(i)$ to the element $\text{some}(i)$, where the latter is interpreted as an element of the set $U_{c'}$.

For a Wick contraction $c$ on the set of indices $\{0, 1, \dots, n-1\}$, an index $i$ belongs to the set of uncontracted indices of $c$ if and only if $i$ is not contained in any pair $p$ that belongs to the contraction $c$.

For any index $i \in \{0, 1, \dots, n-1\}$, $i$ belongs to the set of uncontracted indices of the empty Wick contraction.

For any index $i \in \{0, 1, \dots, n-1\}$, the dual element function $\text{getDual?}$ of the empty Wick contraction returns $\text{none}$ for $i$. This indicates that in the empty Wick contraction, no index is paired with a dual element.

For the empty Wick contraction on $n$ indices, the set of uncontracted indices is the universal set of all indices $\{0, 1, \dots, n-1\}$.

For any Wick contraction $c$ on a set of $n$ indices, the number of uncontracted indices is less than or equal to $n$.

For any Wick contraction $c$ on a set of $n$ indices, the number of uncontracted indices is equal to $n$ if and only if $c$ is the empty contraction.