Physlib.QFT.PerturbationTheory.WickContraction.InsertAndContractNat

Given a Wick contraction $c$ on $n$ elements, an index $i \in \{0, \dots, n\}$, and an optional element $j$ from the set of uncontracted indices of $c$, the function produces a new Wick contraction on $n+1$ elements. Let $f_i: \{0, \dots, n-1\} \to \{0, \dots, n\}$ be the increasing map that skips $i$ (i.e., $f_i(k) = k$ if $k < i$ and $f_i(k) = k+1$ if $k \geq i$). - If $j = \text{none}$, the new contraction consists of the pairs $\{f_i(a), f_i(b)\}$ for every pair $\{a, b\} \in c$. - If $j = \text{some } j'$, the new contraction consists of the pairs $\{f_i(a), f_i(b)\}$ for every $\{a, b\} \in c$, plus the additional pair $\{i, f_i(j')\}$.

Let $c$ be a Wick contraction on $n$ indices and $i \in \{0, \dots, n\}$ be a target index. Let $j$ be an uncontracted index of $c$ (provided as an optional value that is not `none`). Let $f_i: \{0, \dots, n-1\} \to \{0, \dots, n\}$ be the increasing map that skips $i$ (specifically, $f_i(k) = k$ if $k < i$ and $f_i(k) = k+1$ if $k \geq i$). Then the set of contraction pairs in the Wick contraction on $n+1$ indices obtained by inserting $i$ and contracting it with $j$ (via `insertAndContractNat`) is the union of: 1. The set of all pairs $\{f_i(a), f_i(b)\}$ for every pair $\{a, b\}$ in the original contraction $c$. 2. The new contraction pair $\{i, f_i(j)\}$.

For any Wick contraction $c$ on $n$ indices and any index $i \in \{0, \dots, n\}$, the index $i$ is an uncontracted index in the Wick contraction on $n+1$ indices obtained by inserting $i$ into $c$ without forming a new contraction pair (i.e., `insertAndContractNat c i none`).

Let $c$ be a Wick contraction on $n$ indices. For any index $i \in \{0, \dots, n\}$ and any uncontracted index $j$ of $c$, the index $i$ is not an uncontracted index in the Wick contraction on $n+1$ indices obtained by inserting $i$ and contracting it with $j$ (i.e., the contraction produced by `insertAndContractNat c i (some j)`).

Let $c$ be a Wick contraction on $n$ indices. Let $c'$ be the Wick contraction on $n+1$ indices obtained by inserting index $i$ and leaving it uncontracted (i.e., `insertAndContractNat c i none`). For any index $j \in \{0, \dots, n-1\}$, the shifted index $i.\text{succAbove}(j)$ is an uncontracted index in $c'$ if and only if $j$ is an uncontracted index in $c$.

Let $c$ be a Wick contraction on $n$ indices, and let $i \in \{0, \dots, n\}$. Let $f_i: \{0, \dots, n-1\} \to \{0, \dots, n\}$ be the increasing map that skips $i$, defined by $f_i(j) = j$ if $j < i$ and $f_i(j) = j + 1$ if $j \geq i$. An index $k \in \{0, \dots, n\}$ is uncontracted in the Wick contraction produced by `insertAndContractNat c i none` if and only if $k = i$ or $k = f_i(j)$ for some index $j$ that is uncontracted in $c$.

Let $c$ be a Wick contraction on $n$ indices, and let $U(c)$ denote the set of its uncontracted indices. For any index $i \in \{0, \dots, n\}$, let $f_i: \{0, \dots, n-1\} \to \{0, \dots, n\}$ be the increasing map that skips $i$, defined by $f_i(k) = k$ if $k < i$ and $f_i(k) = k+1$ if $k \geq i$. If a new Wick contraction on $n+1$ indices is formed by inserting $i$ into $c$ without contracting it (denoted by `insertAndContractNat c i none`), then its set of uncontracted indices is $\{i\} \cup \{f_i(j) \mid j \in U(c)\}$.

Let $c$ be a Wick contraction on $n$ elements. Let $i \in \{0, \dots, n\}$ be an index to be inserted, and let $j$ be an uncontracted index of $c$. Let $f_i: \{0, \dots, n-1\} \to \{0, \dots, n\}$ be the increasing map that skips $i$ (i.e., $f_i(z) = z$ if $z < i$ and $f_i(z) = z+1$ if $z \geq i$). For any index $k \in \{0, \dots, n\}$, $k$ is an uncontracted index of the Wick contraction formed by inserting $i$ and contracting it with $j$ if and only if $k = f_i(z)$ for some index $z$ that was uncontracted in $c$ and $z \neq j$.

Let $c$ be a Wick contraction on $n$ elements, and let $U(c)$ denote the set of its uncontracted indices. Let $i \in \{0, \dots, n\}$ be a new index and $j \in U(c)$ be an index that was previously uncontracted in $c$. When $i$ is inserted into the system and specifically contracted with $j$ to form a new Wick contraction on $n+1$ elements, the set of uncontracted indices of this new contraction is obtained by removing $j$ from $U(c)$ and applying the increasing map $f_i: \{0, \dots, n-1\} \to \{0, \dots, n\}$ (which skips the value $i$) to the remaining indices. Mathematically, the new set of uncontracted indices is $\{f_i(k) \mid k \in U(c), k \neq j\}$.

Let $c$ be a Wick contraction on $n$ indices. For any index $i \in \{0, \dots, n\}$, let $c'$ be the Wick contraction on $n+1$ indices obtained by inserting $i$ into $c$ without contracting it with any other index (i.e., using `insertAndContractNat c i none`). In the resulting contraction $c'$, the index $i$ is uncontracted.

Let $c$ be a Wick contraction on $n$ elements and $i \in \{0, \dots, n\}$ be an index. If we form a new Wick contraction on $n+1$ elements by inserting the index $i$ without assigning it a contraction partner (using `insertAndContractNat c i none`), then the index $i$ is uncontracted in the resulting contraction, meaning its dual index is $\text{none}$.

Let $c$ be a Wick contraction on $n$ indices. For any index $i \in \{0, \dots, n\}$, let $c'$ be the Wick contraction on $n+1$ indices obtained by inserting the index $i$ and leaving it uncontracted (i.e., using `insertAndContractNat c i none`). For any index $j \in \{0, \dots, n-1\}$, the shifted index $i.\text{succAbove}(j)$ is uncontracted in $c'$ if and only if the index $j$ is uncontracted in $c$.

Let $c$ be a Wick contraction on $n$ elements. For any index $i \in \{0, \dots, n\}$, let $c'$ be the Wick contraction on $n+1$ elements obtained by inserting $i$ as an uncontracted index (using `insertAndContractNat c i none`). For any index $j \in \{0, \dots, n-1\}$, let $f_i(j)$ be the index $j$ shifted to skip $i$ (i.e., $f_i(j) = j$ if $j < i$ and $f_i(j) = j+1$ if $j \geq i$). Then, the index $f_i(j)$ is contracted in $c'$ if and only if the index $j$ is contracted in $c$.

Let $c$ be a Wick contraction on $n$ indices and $i \in \{0, \dots, n\}$ be an index. Let $c'$ be the Wick contraction on $n+1$ indices obtained by inserting $i$ into $c$ and leaving $i$ uncontracted (i.e., $c' = \text{insertAndContractNat}(c, i, \text{none})$). Let $f_i: \{0, \dots, n-1\} \to \{0, \dots, n\}$ be the strictly increasing map that skips $i$, defined by $f_i(k) = k$ if $k < i$ and $f_i(k) = k+1$ if $k \geq i$. For any index $j \in \{0, \dots, n-1\}$, if the index $f_i(j)$ is contracted in $c'$, then its dual (the index it is paired with) in $c'$ is $f_i(k)$, where $k$ is the dual of $j$ in $c$.

Let $c$ be a Wick contraction on $n$ indices. Let $i \in \{0, \dots, n\}$ be an index to be inserted and $j$ be an uncontracted index of $c$. If we form a new Wick contraction on $n+1$ indices by inserting $i$ and contracting it with $j$ (denoted as `insertAndContractNat c i (some j)`), then the index paired with $i$ in this new contraction is $i.\text{succAbove}(j)$, where $i.\text{succAbove}$ is the map that shifts indices to skip $i$.

Let $c$ be a Wick contraction on $n$ indices and let $i \in \{0, \dots, n\}$ be an index. Suppose $j$ is an index that is uncontracted in $c$. Let $c'$ be the Wick contraction on $n+1$ indices obtained by inserting $i$ and pairing it with $j$ (using the function `WickContraction.insertAndContractNat`). Let $f_i: \{0, \dots, n-1\} \to \{0, \dots, n\}$ be the increasing map that skips index $i$ (defined by $f_i(k) = k$ if $k < i$ and $f_i(k) = k+1$ if $k \geq i$). For any index $k \in \{0, \dots, n-1\}$ such that $k \neq j$, $f_i(k)$ is an uncontracted index in $c'$ if and only if $k$ is an uncontracted index in $c$.

Let $c$ be a Wick contraction on $n$ indices and let $i \in \{0, \dots, n\}$ be an index. Suppose $j$ is an index that is uncontracted in $c$. Let $c'$ be the Wick contraction on $n+1$ indices obtained by inserting $i$ and pairing it with $j$ (using the function `WickContraction.insertAndContractNat`). Let $f_i: \{0, \dots, n-1\} \to \{0, \dots, n\}$ be the increasing map that skips index $i$ (defined by $f_i(k) = k$ if $k < i$ and $f_i(k) = k+1$ if $k \geq i$). For any index $k \in \{0, \dots, n-1\}$ such that $k \neq j$, $f_i(k)$ is a contracted index in $c'$ if and only if $k$ is a contracted index in $c$.

Let $c$ be a Wick contraction on $n$ indices and $i \in \{0, \dots, n\}$ be an index. Let $j$ be an index that is uncontracted in $c$, and let $c'$ be the Wick contraction on $n+1$ indices obtained by inserting $i$ and pairing it with $j$ (using the function `WickContraction.insertAndContractNat c i (some j)`). Let $f_i: \{0, \dots, n-1\} \to \{0, \dots, n\}$ be the increasing map that skips index $i$ (defined by $f_i(k) = k$ if $k < i$ and $f_i(k) = k+1$ if $k \geq i$). For any index $k \in \{0, \dots, n-1\}$ such that $k \neq j$, if $f_i(k)$ is a contracted index in $c'$, then the index it is paired with in $c'$ is $f_i(m)$, where $m$ is the index paired with $k$ in $c$.

Let $c$ be a Wick contraction on $n$ indices and $i \in \{0, \dots, n\}$ be an index. Let $j$ be an index that is uncontracted in $c$, and let $c'$ be the Wick contraction on $n+1$ indices obtained by inserting $i$ and pairing it with $j$ (using the function $\text{insertAndContractNat}(c, i, \text{some } j)$). Let $f_i: \{0, \dots, n-1\} \to \{0, \dots, n\}$ be the increasing map that skips index $i$ (defined by $f_i(k) = k$ if $k < i$ and $f_i(k) = k+1$ if $k \geq i$). For any index $k \in \{0, \dots, n-1\}$ such that $k \neq j$, the index paired with $f_i(k)$ in $c'$ is the image under $f_i$ of the index paired with $k$ in $c$. Specifically, $$\text{getDual?}_{c'}(f_i(k)) = \text{Option.map}(f_i, \text{getDual?}_c(k))$$ where $\text{getDual?}$ returns the partner of an index or $\text{none}$ if it is uncontracted.

Let $c$ be a Wick contraction on $n$ elements. For any index $i \in \{0, \dots, n\}$ and any optional uncontracted element $j$ of $c$, if we form a new Wick contraction on $n+1$ elements by inserting index $i$ and optionally contracting it with $j$, and then subsequently erase the index $i$ from this new contraction, the result is the original contraction $c$. Mathematically, this is expressed as: $$\text{erase}(\text{insertAndContractNat}(c, i, j), i) = c$$ where $\text{insertAndContractNat}$ is the operation that inserts index $i$ into $c$ and handles the optional contraction with $j$, and $\text{erase}$ is the operation that removes index $i$ and shifts the remaining indices to restore a contraction on $n$ elements.

Let $c$ be a Wick contraction on $n$ elements. Given an index $i \in \{0, \dots, n\}$ and an optional uncontracted index $j$ of $c$ (where $j = \text{none}$ if $i$ is to remain uncontracted, and $j = \text{some } j'$ if $i$ is to be contracted with $j'$), let $c' = \text{insertAndContractNat}(c, i, j)$ be the resulting Wick contraction on $n+1$ elements. The theorem states that: $$\text{getDualErase}(c', i) = j$$ where $\text{getDualErase}$ is the operation that identifies the index paired with $i$ in $c'$ as an optional uncontracted index of the contraction $\text{erase}(c', i)$. Since $\text{erase}(\text{insertAndContractNat}(c, i, j), i) = c$, the result of $\text{getDualErase}$ is identified with the original optional index $j$ via the equivalence of their respective sets of uncontracted indices.

Let $c$ be a Wick contraction on $n+1$ elements and $i \in \{0, \dots, n\}$ be an index. Let $\text{erase}(c, i)$ be the Wick contraction on $n$ elements obtained by removing index $i$ from $c$ and shifting the remaining indices. Let $\text{getDualErase}(c, i)$ be the partner of index $i$ in $c$, represented as an optional uncontracted index of $\text{erase}(c, i)$ (which is `none` if $i$ was uncontracted in $c$). Then, re-inserting $i$ and contracting it with its original partner via $\text{insertAndContractNat}$ recovers the original contraction: $$\text{insertAndContractNat}(\text{erase}(c, i), i, \text{getDualErase}(c, i)) = c$$

Given a Wick contraction $c$ on $n$ elements, an index $i \in \{0, \dots, n\}$, and an optional index $j$ to be contracted with $i$, this function maps an existing contraction (a pair of indices) $a \in c$ to its corresponding contraction in the augmented Wick contraction on $n+1$ elements. Specifically, if $a = \{u, v\}$, the function returns the pair $\{f_i(u), f_i(v)\}$, where $f_i: \{0, \dots, n-1\} \to \{0, \dots, n\}$ is the strictly increasing map that skips $i$.

Let $c$ be a Wick contraction on $n$ elements and $i \in \{0, \dots, n\}$ be an insertion index. For any optional uncontracted index $j$ of $c$, the lifting map $\text{insertLift}_i : c \to (c.\text{insertAndContractNat}(i, j))$ is injective. This map sends each pair of contracted indices $\{u, v\} \in c$ to the pair $\{f_i(u), f_i(v)\}$, where $f_i: \{0, \dots, n-1\} \to \{0, \dots, n\}$ is the strictly increasing map that skips $i$ (defined by $f_i(k) = k$ if $k < i$ and $f_i(k) = k+1$ if $k \geq i$).

Let $c$ be a Wick contraction on $n$ elements and $i \in \{0, \dots, n\}$ be an insertion index. Let $c'$ be the Wick contraction on $n+1$ elements obtained by inserting index $i$ without forming a new contraction (i.e., using the `insertAndContractNat` function with $j = \text{none}$). Then the lifting map $\text{insertLift}_i : c \to c'$, which maps each pair $\{u, v\} \in c$ to the pair $\{f_i(u), f_i(v)\}$ in $c'$ (where $f_i: \{0, \dots, n-1\} \to \{0, \dots, n\}$ is the strictly increasing map that skips $i$), is surjective.

Let $c$ be a Wick contraction on $n$ elements and $i \in \{0, \dots, n\}$ be an insertion index. Let $c'$ be the Wick contraction on $n+1$ elements obtained by inserting the index $i$ without forming a new contraction (i.e., using the `insertAndContractNat` function with $j = \text{none}$). The lifting map $\text{insertLift}_i : c \to c'$, which maps each pair of contracted indices $\{u, v\} \in c$ to the pair $\{f_i(u), f_i(v)\}$ in $c'$ (where $f_i: \{0, \dots, n-1\} \to \{0, \dots, n\}$ is the strictly increasing map that skips $i$), is bijective.

Let $c$ be a Wick contraction on $n$ elements and $a \in c$ be a pair in that contraction. Let $i \in \{0, \dots, n\}$ be an insertion index and $j$ be an optional index from the uncontracted indices of $c$ to be paired with $i$. Let $f_i: \{0, \dots, n-1\} \to \{0, \dots, n\}$ be the strictly increasing map that skips $i$ (i.e., $f_i(k) = k$ if $k < i$ and $f_i(k) = k+1$ if $k \geq i$). Then, the first index of the lifted contraction $\text{insertLift}(i, j, a)$ in the new augmented Wick contraction is equal to the image of the first index of $a$ under $f_i$. Mathematically, this is expressed as: $$\text{fstFieldOfContract}(\text{insertLift}(i, j, a)) = f_i(\text{fstFieldOfContract}(a))$$ where $\text{fstFieldOfContract}$ denotes the first index of a given contraction pair.

Let $c$ be a Wick contraction on $n$ elements and $a \in c$ be a pair in that contraction. Let $i \in \{0, \dots, n\}$ be an insertion index and $j$ be an optional index from the uncontracted indices of $c$ to be paired with $i$. Let $f_i: \{0, \dots, n-1\} \to \{0, \dots, n\}$ be the strictly increasing map that skips $i$ (defined as $f_i(k) = k$ if $k < i$ and $f_i(k) = k+1$ if $k \geq i$). Then, the second index of the lifted contraction $\text{insertLift}(i, j, a)$ in the new augmented Wick contraction is equal to the image of the second index of $a$ under $f_i$. Mathematically, this is expressed as: $$\text{sndFieldOfContract}(\text{insertLift}(i, j, a)) = f_i(\text{sndFieldOfContract}(a))$$ where $\text{sndFieldOfContract}$ denotes the second (larger) index of a given contraction pair.

Given a Wick contraction $c$ on $n$ elements, an insertion index $i \in \{0, \dots, n\}$, and an index $j$ that is uncontracted in $c$, let $c'$ be the augmented Wick contraction on $n+1$ elements obtained by contracting $i$ with $j$ (specifically, the contraction produced by `WickContraction.insertAndContractNat c i (some j)`). This function provides the mapping from the set of pairs in $c$ plus one additional element to the set of contracted pairs in $c'$. Let $f_i: \{0, \dots, n-1\} \to \{0, \dots, n\}$ be the strictly increasing map that skips $i$ (i.e., $f_i(k) = k$ if $k < i$ and $f_i(k) = k+1$ if $k \geq i$). The function is defined as follows: - The element `Sum.inl ()` (representing the new contraction) maps to the pair $\{i, f_i(j)\}$. - An existing contraction pair $p \in c$ (represented by `Sum.inr p`) maps to the lifted pair $\{f_i(u), f_i(v)\}$, where $\{u, v\} = p$.

Let $c$ be a Wick contraction on $n$ elements, $i \in \{0, \dots, n\}$ be an insertion index, and $j$ be an uncontracted index of $c$. Let $f_i: \{0, \dots, n-1\} \to \{0, \dots, n\}$ be the strictly increasing map that skips $i$ (defined as $f_i(k) = k$ if $k < i$ and $f_i(k) = k+1$ if $k \geq i$). The lifting map $\text{insertLiftSome}_{i,j}$, which maps the set of contracted pairs in $c$ augmented by a new element (representing the pair $\{i, f_i(j)\}$) to the set of contracted pairs in the new Wick contraction on $n+1$ elements, is injective.

Let $c$ be a Wick contraction on $n$ elements, $i \in \{0, \dots, n\}$ be an insertion index, and $j$ be an index that is uncontracted in $c$. Let $f_i: \{0, \dots, n-1\} \to \{0, \dots, n\}$ be the strictly increasing map that skips $i$ (defined as $f_i(k) = k$ if $k < i$ and $f_i(k) = k+1$ if $k \geq i$). Let $c'$ be the Wick contraction on $n+1$ elements obtained by contracting $i$ with $f_i(j)$ and shifting existing pairs in $c$ via $f_i$. The lifting map $\text{insertLiftSome}_{i,j}$, which maps the set of contracted pairs in $c$ augmented by a new element to the set of contracted pairs in $c'$, is surjective.

Let $c$ be a Wick contraction on $n$ elements, $i \in \{0, \dots, n\}$ be an insertion index, and $j$ be an index that is uncontracted in $c$. Let $f_i: \{0, \dots, n-1\} \to \{0, \dots, n\}$ be the strictly increasing map that skips $i$ (defined as $f_i(k) = k$ if $k < i$ and $f_i(k) = k+1$ if $k \geq i$). Let $c'$ be the Wick contraction on $n+1$ elements obtained by contracting $i$ with $f_i(j)$ and shifting existing pairs in $c$ via $f_i$ (specifically, the contraction produced by `WickContraction.insertAndContractNat c i (some j)`). The lifting map $\text{insertLiftSome}_{i,j}$, which maps the set of contracted pairs in $c$ augmented by a new element (representing the pair $\{i, f_i(j)\}$) to the set of contracted pairs in $c'$, is bijective.

For any natural number $n$ and any index $i \in \{0, \dots, n\}$, let $\Phi_i$ be the map that takes a Wick contraction $c$ on $n$ elements and produces a Wick contraction on $n+1$ elements by inserting $i$ as an uncontracted index. Specifically, $\Phi_i(c)$ contains the pairs $\{f_i(a), f_i(b)\}$ for every pair $\{a, b\} \in c$, where $f_i: \{0, \dots, n-1\} \to \{0, \dots, n\}$ is the unique increasing map that skips $i$. The map $\Phi_i$ is injective.

For a natural number $n$ and an index $i \in \{0, \dots, n\}$, if $c$ is a Wick contraction on $n+1$ elements where $i$ is uncontracted (meaning its dual $c.\text{getDual?}(i)$ is $\text{none}$), then there exists a Wick contraction $c'$ on $n$ elements such that $c = \text{insertAndContractNat}(c', i, \text{none})$. The function $\text{insertAndContractNat}(c', i, \text{none})$ constructs a new contraction on $n+1$ elements by shifting the indices of all existing pairs in $c'$ to skip the index $i$, leaving $i$ itself uncontracted.