Physlib.QFT.PerturbationTheory.WickContraction.UncontractedList

For any natural numbers $n$ and $m$, let $l$ be a list of elements of the finite set $\text{Fin } n = \{0, 1, \dots, n-1\}$. If the list $l$ is sorted in non-decreasing order (i.e., it is pairwise $\le$) and $f: \text{Fin } n \to \text{Fin } m$ is a strictly monotonic function, then the list obtained by applying $f$ to each element of $l$ is also sorted in non-decreasing order.

Let $n$ be a natural number and let $l$ be a list of elements from the set $\text{Fin } n = \{0, 1, \dots, n-1\}$. If the list $l$ is sorted in non-decreasing order (i.e., its elements are pairwise $\le$), then for any $i \in \text{Fin}(n+1)$, the list obtained by applying the embedding $i.\text{succAboveEmb}: \text{Fin } n \hookrightarrow \text{Fin}(n+1)$ to each element of $l$ is also sorted in non-decreasing order. The embedding $i.\text{succAboveEmb}$ maps an element $x$ to $x$ if $x < i$ and to $x+1$ if $x \ge i$.

Let $n, m \in \mathbb{N}$ and let $A$ be a finite subset of $\text{Fin } n = \{0, 1, \dots, n-1\}$. Let $f: \text{Fin } n \hookrightarrow \text{Fin } m$ be a strictly monotone embedding. Then the list obtained by sorting the elements of $A$ in non-decreasing order and applying $f$ to each element is equal to the list obtained by sorting the image set $f(A) = \{f(x) \mid x \in A\}$. That is, $(\text{sort } A). \text{map } f = \text{sort}(f(A))$.

Let $l$ be a list of elements from the set $\{0, 1, \dots, n-1\}$. If $l$ is sorted in non-decreasing order, then for any natural number $i$, the list $l$ is equal to the concatenation of two sublists: the sublist of elements $x \in l$ such that $x < i$ and the sublist of elements $x \in l$ such that $x \geq i$. That is, $l = [x \in l \mid x < i] \text{ ++ } [x \in l \mid x \geq i]$.

Let $l$ be a list of elements in $\{0, 1, \dots, n-1\}$ that is sorted in non-decreasing order. Let $i$ be an element belonging to $l$. If $l'$ is the sublist of $l$ containing only those elements $x$ such that $i \le x$, then the index of the first occurrence of $i$ in $l'$ is 0.

Let $l$ be a list of elements from the set $\{0, 1, \dots, n-1\}$ that is sorted in non-decreasing order. For any element $i$ belonging to $l$, the index of the first occurrence of $i$ in $l$ is equal to the length of the sublist containing all elements $x \in l$ such that $x < i$.

Let $l$ be a list of elements from the set $\{0, 1, \dots, n-1\}$. Suppose $l$ is sorted in non-decreasing order. For any $i \in \{0, 1, \dots, n-1\}$, the ordered insertion of $i$ into $l$ (preserving the non-decreasing order) is equal to the concatenation of the sublist of elements $x \in l$ such that $x < i$, the element $i$ itself, and the sublist of elements $x \in l$ such that $x \geq i$. In symbols, if $l_{< i} = [x \in l \mid x < i]$ and $l_{\ge i} = [x \in l \mid x \ge i]$, then $$\text{orderedInsert}(\le, i, l) = l_{< i} \text{ ++ } [i] \text{ ++ } l_{\ge i}$$

Let $l$ be a list of elements from the set $\{0, 1, \dots, n-1\}$ that is sorted in non-decreasing order. For any $i \in \{0, 1, \dots, n-1\}$, the ordered insertion of $i$ into $l$ (preserving the $\le$ order) is equal to the result of inserting $i$ into $l$ at the specific index corresponding to the number of elements in $l$ that are strictly less than $i$. In symbols, if $l_{< i}$ denotes the sublist of elements $x \in l$ such that $x < i$, then: $$\text{orderedInsert}(\le, i, l) = \text{insertIdx}(\text{length}(l_{< i}), i, l)$$

Given a Wick contraction $c$ on $n$ indices, the uncontracted list is the list of all indices $i \in \{0, 1, \dots, n-1\}$ that are not part of any contracted pair in $c$, ordered such that the indices are in strictly increasing order.

For a Wick contraction $c$ on $n$ indices, an index $i \in \{0, 1, \dots, n-1\}$ belongs to the sorted list of uncontracted indices $c.\text{uncontractedList}$ if and only if it belongs to the set of uncontracted indices $c.\text{uncontracted}$.

For the empty Wick contraction on $n$ indices, where no elements are paired, the sorted list of uncontracted indices is equal to the list of all indices from $0$ to $n-1$ in strictly increasing order, denoted as `List.finRange n`.

For an empty Wick contraction on a set of $n = 0$ indices, the list of uncontracted indices is the empty list $[ ]$.

Let $n, m \in \mathbb{N}$ be such that $n = m$, and let $c$ be a Wick contraction on $n$ indices. The uncontracted list of the Wick contraction $c$ when re-indexed to $m$ indices (via the equality $h: n = m$) is equal to the list obtained by applying the index transformation mapping $\text{finCongr}(h)$ to each element of the uncontracted list of $c$.

Let $c$ be a Wick contraction on $n$ indices $\{0, 1, \dots, n-1\}$. Let $c.\text{uncontractedList}$ be the sorted list of uncontracted indices and $c.\text{uncontracted}$ be the set of uncontracted indices. For any valid index $i$ into the list (i.e., $0 \le i < \text{length}(c.\text{uncontractedList})$), the $i$-th element of $c.\text{uncontractedList}$ is an element of the set $c.\text{uncontracted}$.

For a Wick contraction $c$ on $n$ indices, the list of uncontracted indices is non-decreasing. That is, for any two elements in the list, the element appearing at an earlier position is less than or equal to any element appearing at a subsequent position.

For a Wick contraction $c$ on $n$ indices $\{0, 1, \dots, n-1\}$, the list of uncontracted indices is strictly increasing. That is, for any two indices in the list, the element at the earlier position is strictly less than the element at any subsequent position.

For a Wick contraction $c$ on the set of indices $\{0, 1, \dots, n-1\}$, the list of uncontracted indices contains no duplicate elements.

For a Wick contraction $c$ on $n$ indices $\{0, 1, \dots, n-1\}$, the set of elements contained in the sorted list of uncontracted indices is equal to the set of uncontracted indices of $c$.

For a Wick contraction $c$ on the set of indices $\{0, 1, \dots, n-1\}$, the list of uncontracted indices $c.\text{uncontractedList}$ is equal to the list obtained by sorting the set of uncontracted indices $c.\text{uncontracted}$ in non-decreasing order with respect to $\le$.

For a Wick contraction $c$ on the set of indices $\{0, 1, \dots, n-1\}$, the length of the sorted list of uncontracted indices $c.\text{uncontractedList}$ is equal to the cardinality of the set of uncontracted indices, denoted as $|c.\text{uncontracted}|$.

For a Wick contraction $c$ on $n$ indices $\{0, 1, \dots, n-1\}$ and a decidable predicate $p$ on these indices, filtering the sorted list of uncontracted indices $c.\text{uncontractedList}$ by $p$ results in the same list as sorting the set of uncontracted indices that satisfy $p$ (i.e., $\{i \in c.\text{uncontracted} \mid p(i)\}$) in non-decreasing order with respect to $\le$.

For a Wick contraction $c$ on $n$ indices, let $c.\text{uncontractedList}$ be the list of indices not involved in any contracted pair, sorted in increasing order, and let $c.\text{uncontracted}$ be the set of these same indices. The equivalence `uncontractedIndexEquiv` is the bijection between the set of positions in the list, represented by the finite type $\{0, 1, \dots, \text{length}(c.\text{uncontractedList}) - 1\}$, and the set of uncontracted indices. Under this bijection, an index $i$ is mapped to the $i$-th element of the sorted list $c.\text{uncontractedList}$.

For a Wick contraction $c$ on $n$ indices, let $c.\text{uncontractedList}$ be the list of indices not part of any contracted pair, sorted in strictly increasing order, and let $c.\text{uncontracted}$ be the set of these indices. For any uncontracted index $k \in c.\text{uncontracted}$, the element at the position in $c.\text{uncontractedList}$ corresponding to $k$ under the inverse bijection $c.\text{uncontractedIndexEquiv}^{-1}$ is equal to $k$ itself.

Let $c$ be a Wick contraction on $n$ indices. Let $c.\text{uncontracted}$ be the set of indices not involved in any contracted pair, and let $c.\text{uncontractedList}$ be the list containing these indices sorted in strictly increasing order. For any uncontracted index $k \in c.\text{uncontracted}$, the position (index) of $k$ in $c.\text{uncontractedList}$ is equal to the number of elements in $c.\text{uncontractedList}$ that are strictly less than $k$.

For a Wick contraction $c$ on $n$ indices, let $c.\text{uncontractedList}$ be the list of indices not involved in any contracted pair, sorted in strictly increasing order. For any uncontracted index $k \in c.\text{uncontracted}$, the sublist consisting of the first $m$ elements of $c.\text{uncontractedList}$, where $m$ is the position (index) of $k$ in the list, is equal to the sublist of elements in $c.\text{uncontractedList}$ that are strictly less than $k$.

Given a list of field operators $\phi_s$ and a Wick contraction $\Lambda$ on that list, the function returns the sub-list of operators in $\phi_s$ whose indices are uncontracted by $\Lambda$. Specifically, if $\{i_1, i_2, \dots, i_k\}$ is the sorted list of indices in $\{0, \dots, |\phi_s|-1\}$ that do not participate in any contraction in $\Lambda$, the function returns the list $[\phi_s[i_1], \phi_s[i_2], \dots, \phi_s[i_k]]$. This list is denoted by the notation $[\Lambda]^{uc}$.

Given a Wick contraction $\Lambda$ on a sequence of field operators $\phi_s$, the notation $[\Lambda]^{uc}$ denotes the sub-list of field operators in $\phi_s$ that remain uncontracted (i.e., those operators not paired with another by the contraction $\Lambda$).

For a list of field operators $\phi_s$, let $\Lambda_{\emptyset}$ be the empty Wick contraction (where no operators are paired). The list of uncontracted field operators $[\Lambda_{\emptyset}]^{uc}$ is equal to the original list $\phi_s$.

For a list of field operators $\phi_s$ and a Wick contraction $\Lambda$ acting on those operators, let $\mathcal{U}$ be the set of indices not involved in any contraction, and let $[\Lambda]^{uc}$ be the list of field operators corresponding to these uncontracted indices (sorted by their original positions). This definition establishes a bijection (equivalence) between $\mathcal{U} \cup \{\text{none}\}$ and the set of positions in the list $[\Lambda]^{uc}$ plus a "none" element, i.e., $\{0, 1, \dots, |[\Lambda]^{uc}| - 1\} \cup \{\text{none}\}$. Under this bijection, an index $i \in \mathcal{U}$ is mapped to its position in the sorted list, and the value `none` is mapped to `none`.

For a list of field operators $\phi_s$ and a Wick contraction $\Lambda$ on those operators, let $E$ be the equivalence `uncontractedFieldOpEquiv` that maps between the optional uncontracted indices $\mathcal{U} \cup \{\text{none}\}$ and the optional positions in the sorted list of uncontracted field operators $\{0, 1, \dots, |[\Lambda]^{uc}| - 1\} \cup \{\text{none}\}$. The mapping satisfies $E(\text{none}) = \text{none}$.

Let $\phi_s$ be a list of field operators and $\Lambda$ a Wick contraction on its indices. Let $\mathcal{U}$ be the set of indices in $\{0, \dots, |\phi_s|-1\}$ that are uncontracted by $\Lambda$, and let $[\Lambda]^{uc}$ be the list of field operators corresponding to these uncontracted indices (sorted by their original positions). Let $\psi$ be the bijection `uncontractedFieldOpEquiv` that maps the set $\mathcal{U} \cup \{\text{none}\}$ to the set of positions in $[\Lambda]^{uc}$ plus a "none" element, i.e., $\{0, \dots, |[\Lambda]^{uc}| - 1\} \cup \{\text{none}\}$. For any function $f$ mapping from $\{0, \dots, |[\Lambda]^{uc}| - 1\} \cup \{\text{none}\}$ to an additive commutative monoid $\alpha$, the sum of $f$ over its domain is equal to the sum of $f \circ \psi$ over the set $\mathcal{U} \cup \{\text{none}\}$: $$\sum_{i \in \{0, \dots, |[\Lambda]^{uc}| - 1\} \cup \{\text{none}\}} f(i) = \sum_{j \in \mathcal{U} \cup \{\text{none}\}} f(\psi(j))$$

For a list of field operators $\phi_s$ and a Wick contraction $\Lambda$ acting on them, let $[\Lambda]^{uc}$ denote the list of field operators that remain uncontracted, sorted by their original positions. This function is an embedding $f: \{0, 1, \dots, \text{length}([\Lambda]^{uc}) - 1\} \hookrightarrow \{0, 1, \dots, \text{length}(\phi_s) - 1\}$ that maps the index of an operator in the uncontracted list to its corresponding original index in the list $\phi_s$.

Let $\phi_s$ be a list of field operators and let $\Lambda$ and $\Lambda'$ be two Wick contractions on $\phi_s$. If $\Lambda = \Lambda'$, then the embedding $f_{\Lambda} : \{0, 1, \dots, |[\Lambda]^{uc}| - 1\} \hookrightarrow \{0, 1, \dots, |\phi_s| - 1\}$, which maps the index of an operator in the uncontracted list $[\Lambda]^{uc}$ to its original index in $\phi_s$, is equal to the composition of the index congruence map (identifying the index sets of the two identical uncontracted lists) and the embedding $f_{\Lambda'}$.

For a list of field operators $\phi_s$ and a Wick contraction $\Lambda$ acting on them, let $L$ be the list of indices in $\{0, 1, \dots, \text{length}(\phi_s) - 1\}$ that are not part of any contracted pair in $\Lambda$, ordered such that they are strictly increasing. The embedding function $f$ (defined by `uncontractedListEmd`), which maps an index $i$ from the set $\{0, 1, \dots, \text{length}([\Lambda]^{uc}) - 1\}$ to its original index in $\phi_s$, is equal to the function that retrieves the $i$-th element of the list $L$. Here, $[\Lambda]^{uc}$ denotes the list of field operators that remain uncontracted.

For a list of field operators $\phi_s$ and a Wick contraction $\Lambda$ acting on them, let $[\Lambda]^{uc}$ be the list of uncontracted field operators sorted by their original positions. Let $f$ be the embedding (the function `uncontractedListEmd`) that maps the index $i$ of an operator in the uncontracted list $[\Lambda]^{uc}$ to its corresponding original index in the list $\phi_s$. Then $f$ is strictly increasing: for any two indices $i, j$ in the domain of $f$, if $i < j$, then $f(i) < f(j)$.

For a field specification $\mathcal{F}$, a list of field operators $\phi_s$, and a Wick contraction $\Lambda$ acting on $\phi_s$, let $[\Lambda]^{uc}$ be the list of field operators that remain uncontracted. For any index $i \in \{0, 1, \dots, \text{length}([\Lambda]^{uc}) - 1\}$, the original index in $\phi_s$ corresponding to the $i$-th uncontracted operator (given by the embedding $\text{uncontractedListEmd}(i)$) is an element of the set of uncontracted indices of the contraction $\Lambda$.

For a list of field operators $\phi_s$ and a Wick contraction $\Lambda$ acting on them, let $i \in \{0, 1, \dots, |\phi_s|-1\}$ be an index that is uncontracted under $\Lambda$. Then there exists an index $j \in \{0, 1, \dots, |[\Lambda]^{uc}|-1\}$ in the list of uncontracted field operators $[\Lambda]^{uc}$ such that the embedding function $\text{uncontractedListEmd}$ maps $j$ to $i$.

For a list of field operators $\phi_s$ and a Wick contraction $\Lambda$ on $\phi_s$, let $[\Lambda]^{uc}$ be the list of field operators remaining uncontracted and $f$ be the embedding (`uncontractedListEmd`) that maps an index of the uncontracted list to its original index in $\phi_s$. For any finite set of indices $a$ of the uncontracted list and any pair $b$ that is part of the contraction $\Lambda$ ($b \in \Lambda$), the set of original indices $\{f(i) \mid i \in a\}$ and the set $b$ are disjoint.

For a list of field operators $\phi_s$ and a Wick contraction $\Lambda$ on that list, let $[\Lambda]^{uc}$ denote the list of field operators that remain uncontracted. Let $f$ be the embedding (`uncontractedListEmd`) that maps an index of the uncontracted list to its corresponding original index in $\phi_s$. For any finite set of indices $a$ from the uncontracted list, the set of mapped indices $\{f(i) \mid i \in a\}$ is not a member of the set of contracted pairs in $\Lambda$.

For a list of field operators $\phi_s$ and a Wick contraction $\Lambda$ acting on them, let $[\Lambda]^{uc}$ be the list of uncontracted field operators and $f$ be the embedding (the `uncontractedListEmd`) that maps an index $k$ in the list $[\Lambda]^{uc}$ to its original index in $\phi_s$. For any index $k \in \{0, \dots, \text{length}([\Lambda]^{uc}) - 1\}$, the $k$-th element of the uncontracted list is equal to the element of the original list $\phi_s$ at index $f(k)$: $$[\Lambda]^{uc}[k] = \phi_s[f(k)]$$

For a list of field operators $\phi_s$ of length $n$, let $\text{empty}$ be the Wick contraction where no operators are paired. The embedding $f: \{0, 1, \dots, n-1\} \hookrightarrow \{0, 1, \dots, n-1\}$ that maps the index of an operator in the uncontracted list to its original index in $\phi_s$ is the canonical identity embedding.

For a Wick contraction $c$ on $n$ indices, let $c.\text{uncontractedList}$ be the list of indices in $\{0, 1, \dots, n-1\}$ that are not part of any contracted pair, ordered in strictly increasing order. For any index $i \in \{0, 1, \dots, n\}$, the list obtained by applying the embedding $i.\text{succAboveEmb} : \text{Fin } n \hookrightarrow \text{Fin } (n+1)$ to each element of $c.\text{uncontractedList}$ is non-decreasingly sorted (i.e., its elements are pairwise $\le$). The embedding $i.\text{succAboveEmb}$ maps an index $x$ to $x$ if $x < i$ and to $x+1$ if $x \ge i$.

For a Wick contraction $c$ on $n$ indices, let $c.\text{uncontractedList}$ be the list of indices in $\{0, 1, \dots, n-1\}$ that are not part of any contracted pair in $c$, ordered in strictly increasing order. For any index $i \in \{0, 1, \dots, n\}$, let $i.\text{succAboveEmb} : \{0, 1, \dots, n-1\} \hookrightarrow \{0, 1, \dots, n\}$ be the embedding that maps an index $x$ to $x$ if $x < i$ and to $x+1$ if $x \ge i$. Then the list obtained by applying $i.\text{succAboveEmb}$ to each element of $c.\text{uncontractedList}$ contains no duplicate elements.

For a Wick contraction $c$ on $n$ indices, let $c.\text{uncontractedList}$ be the list of all indices in $\{0, 1, \dots, n-1\}$ that are not part of any contracted pair, ordered in strictly increasing order. For any index $i \in \{0, 1, \dots, n\}$, let $i.\text{succAboveEmb} : \{0, 1, \dots, n-1\} \hookrightarrow \{0, 1, \dots, n\}$ be the embedding that maps an index $x$ to $x$ if $x < i$ and to $x+1$ if $x \ge i$. Then, the list obtained by performing an ordered insertion of $i$ (with respect to the $\le$ relation) into the list formed by applying $i.\text{succAboveEmb}$ to each element of $c.\text{uncontractedList}$ contains no duplicate elements.

For a Wick contraction $c$ on $n$ indices, let $c.\text{uncontractedList}$ be the strictly increasing list of indices in $\{0, 1, \dots, n-1\}$ that are not part of any contracted pair. For any index $i \in \{0, 1, \dots, n\}$, let $i.\text{succAboveEmb} : \{0, \dots, n-1\} \to \{0, \dots, n\}$ be the embedding that maps $x$ to $x$ if $x < i$ and to $x+1$ if $x \ge i$. Then the list formed by performing an ordered insertion of $i$ (maintaining the $\le$ relation) into the list obtained by applying $i.\text{succAboveEmb}$ to each element of $c.\text{uncontractedList}$ is sorted non-decreasingly.

For a Wick contraction $c$ on $n$ indices, let $c.\text{uncontractedList}$ be the sorted list of indices that are not part of any contracted pair, and let $c.\text{uncontracted}$ be the set of these indices. Given an index $i \in \{0, 1, \dots, n\}$, let $i.\text{succAboveEmb}: \{0, \dots, n-1\} \to \{0, \dots, n\}$ be the embedding that "skips" $i$ (mapping $j < i$ to $j$ and $j \ge i$ to $j+1$). Then, the set of elements in the list formed by an ordered insertion of $i$ into the list of mapped uncontracted indices is equal to the set formed by inserting $i$ into the set of mapped uncontracted indices.

For a Wick contraction $c$ on $n$ indices, let $c.\text{uncontractedList}$ be the list of uncontracted indices in strictly increasing order, and let $c.\text{uncontracted}$ be the set of these indices. For any index $i \in \{0, 1, \dots, n\}$, let $f_i: \{0, 1, \dots, n-1\} \hookrightarrow \{0, 1, \dots, n\}$ be the embedding (known as `succAboveEmb`) that maps $x$ to $x$ if $x < i$ and to $x+1$ if $x \ge i$. Then, the list obtained by performing an ordered insertion of $i$ (maintaining the $\le$ relation) into the list formed by applying $f_i$ to each element of $c.\text{uncontractedList}$ is equal to the list obtained by sorting the set $\{f_i(u) \mid u \in c.\text{uncontracted}\} \cup \{i\}$ in non-decreasing order.

For a Wick contraction $c$ on $n$ indices, let $L(c)$ be the list of its uncontracted indices sorted in strictly increasing order. Let $\phi_i : \mathcal{W}_{n+1} \cong \sum_{c \in \mathcal{W}_n} \text{Option}(U(c))$ be the equivalence defined by extracting the index $i \in \{0, \dots, n\}$, and let $c' = \phi_i^{-1}(c, \text{none})$ be the Wick contraction on $n+1$ indices formed by inserting $i$ as an uncontracted index. Then the sorted list of uncontracted indices of $c'$ is given by: \[ L(c') = \text{ordered\_insert}_{\le}(i, [f_i(j) \mid j \in L(c)]) \] where $f_i: \{0, \dots, n-1\} \to \{0, \dots, n\}$ is the increasing embedding that skips $i$ (mapping $j$ to $j$ if $j < i$ and to $j+1$ if $j \geq i$), and $\text{ordered\_insert}_{\le}$ denotes the operation of inserting an element into a list while maintaining non-decreasing order.

For a Wick contraction $c$ on $n$ indices, let $c.\text{uncontracted}$ be the set of indices that are not part of any contracted pair, and let $c.\text{uncontractedList}$ be the list of these indices sorted in strictly increasing order. For any index $i \in \{0, 1, \dots, n\}$, let $f_i: \{0, 1, \dots, n-1\} \hookrightarrow \{0, 1, \dots, n\}$ be the embedding (known as `succAboveEmb`) that maps $x$ to $x$ if $x < i$ and to $x+1$ if $x \ge i$. For any natural number $k$ less than the number of uncontracted indices, the set of elements in the list obtained by applying $f_i$ to $c.\text{uncontractedList}$ and then removing the element at position $k$ is equal to the set $\{f_i(u) \mid u \in c.\text{uncontracted}\}$ with the element $f_i(c.\text{uncontractedList}[k])$ removed.

Let $c$ be a Wick contraction on $n$ indices and let $c.\text{uncontractedList}$ be the list of indices in $\{0, 1, \dots, n-1\}$ that are not part of any contracted pair, ordered in strictly increasing order. For any index $i \in \{0, 1, \dots, n\}$, let $i.\text{succAboveEmb} : \text{Fin } n \hookrightarrow \text{Fin } (n+1)$ be the embedding that maps an index $x$ to $x$ if $x < i$ and to $x+1$ if $x \ge i$. For any $k \in \mathbb{N}$, the list formed by applying $i.\text{succAboveEmb}$ to each element of $c.\text{uncontractedList}$ and then removing the element at index $k$ is sorted in non-decreasing order (i.e., its elements are pairwise $\le$).

For a Wick contraction $c$ on $n$ indices, let $c.\text{uncontractedList}$ be the list of uncontracted indices in $\{0, 1, \dots, n-1\}$ sorted in strictly increasing order. For any index $i \in \{0, 1, \dots, n\}$, let $i.\text{succAboveEmb} : \{0, 1, \dots, n-1\} \hookrightarrow \{0, 1, \dots, n\}$ be the embedding that maps $x$ to $x$ if $x < i$ and to $x+1$ if $x \ge i$. For any natural number $k$, the list obtained by applying $i.\text{succAboveEmb}$ to each element of $c.\text{uncontractedList}$ and then removing the element at position $k$ contains no duplicate elements.

Let $c$ be a Wick contraction on $n$ indices $\{0, 1, \dots, n-1\}$. Let $U_c \subset \{0, 1, \dots, n-1\}$ be the set of uncontracted indices of $c$, and let $L_c$ be the list of these indices sorted in strictly increasing order. For any index $i \in \{0, 1, \dots, n\}$, let $f_i: \{0, 1, \dots, n-1\} \hookrightarrow \{0, 1, \dots, n\}$ be the "successor-above" embedding defined by $f_i(x) = x$ if $x < i$ and $f_i(x) = x + 1$ if $x \ge i$. For any natural number $k$ less than the length of $L_c$, the list obtained by applying $f_i$ to each element of $L_c$ and then removing the element at position $k$ is equal to the list obtained by taking the image of the set $U_c$ under $f_i$, removing the element $f_i(L_c[k])$, and sorting the resulting set in non-decreasing order.