Physlib.QFT.PerturbationTheory.FieldSpecification.CrAnSection

For a given field specification $\mathcal{F}$ and a list of field operators $\varphi_s = [\phi_1, \phi_2, \dots, \phi_n] \in \text{List}(\mathcal{F}.\text{FieldOp})$, the type $\text{CrAnSection}(\varphi_s)$ is defined as the set of lists of creation and annihilation operators $\psi_s = [\psi_1, \psi_2, \dots, \psi_n] \in \text{List}(\mathcal{F}.\text{CrAnFieldOp})$ such that mapping each $\psi_i$ through the projection function $\mathcal{F}.\text{crAnFieldOpToFieldOp}$ yields the original list $\varphi_s$. Physically, this represents all possible ways to associate each field operator in a product with either a creation or an annihilation component.

Let $\mathcal{F}$ be a field specification and $\varphi_s$ be a list of field operators. For any creation and annihilation section $\psi_s \in \text{CrAnSection}(\varphi_s)$, the length of the list of operators in $\psi_s$ is equal to the length of the list $\varphi_s$.

Given a list of field operators $\varphi_s = [\phi_1, \phi_2, \dots, \phi_n]$ and a creation and annihilation section $\psi_s = [\psi_1, \psi_2, \dots, \psi_n] \in \text{CrAnSection}(\varphi_s)$ (where each $\psi_i$ is a creation or annihilation component of the corresponding field operator $\phi_i$), this function returns the tail of the section $[\psi_2, \dots, \psi_n]$. This resulting list is a valid creation and annihilation section for the tail of the original field operator list, $\text{tail}(\varphi_s) = [\phi_2, \dots, \phi_n]$.

Let $\mathcal{F}$ be a field specification. For any field operator $\phi \in \mathcal{F}.\text{FieldOp}$ and any list of field operators $\varphi_s$, let $\psi_s \in \text{CrAnSection}(\phi :: \varphi_s)$ be a creation and annihilation section of the list starting with $\phi$. Then, the projection of the first element (the head) of $\psi_s$ to its underlying field operator is equal to $\phi$.

For a given field specification $\mathcal{F}$, let $\varphi_s = [\phi_1, \phi_2, \dots, \phi_n]$ be a list of field operators and let $\psi_s = [\psi_1, \psi_2, \dots, \psi_n]$ be a section of creation and annihilation operators such that each $\psi_i$ is a component of $\phi_i$ (that is, $\psi_s \in \text{CrAnSection}(\varphi_s)$). Then the list of field statistics (identifying each operator as bosonic or fermionic) associated with the creation and annihilation operators $\psi_s$ is equal to the list of field statistics associated with the original field operators $\varphi_s$. In symbols, $(\mathcal{F} \triangleright_s \psi_s) = (\mathcal{F} \triangleright_s \varphi_s)$.

Given a field specification $\mathcal{F}$, let $\varphi_s$ be a list of field operators and $\psi_s$ be a creation and annihilation section of $\varphi_s$ (that is, a list of creation or annihilation components $\psi_i$ whose underlying field operators are the $\phi_i$ in $\varphi_s$). For any natural number $n$, the sequence of field statistics associated with the first $n$ elements of $\psi_s$ is identical to the sequence of field statistics associated with the first $n$ field operators in $\varphi_s$.

Given a field specification $\mathcal{F}$ and a list of field operators starting with $\phi$, denoted as $\phi :: \phi_s$, let $\psi_s$ be a creation and annihilation section for this list. The function `head` extracts the specific mode (the creation or annihilation label) associated with the first field operator $\phi$ in the section, returning an element of the type $\mathcal{F}.\text{fieldOpToCrAnType}(\phi)$.

For a given field specification $\mathcal{F}$, let $\phi \in \mathcal{F}.\text{FieldOp}$ be a field operator and $\phi_s$ be a list of field operators. Given a creation or annihilation label $\psi \in \mathcal{F}.\text{fieldOpToCrAnType}(\phi)$ and a section $\psi_s \in \text{CrAnSection}(\phi_s)$, the function constructs a new section for the extended list $\phi :: \phi_s$ by prepending the creation/annihilation operator pair $\langle \phi, \psi \rangle$ to the list representing $\psi_s$.

For a given field specification $\mathcal{F}$, the type of creation and annihilation sections $\text{CrAnSection}([])$ associated with the empty list of field operators is equivalent to the unit type $\text{Unit}$. This implies that there is exactly one such section, which corresponds to the empty list of creation and annihilation operators.

For a given field specification $\mathcal{F}$ and a field operator $\phi \in \mathcal{F}.\text{FieldOp}$, the type of creation and annihilation sections for the singleton list $[\phi]$, denoted as $\text{CrAnSection}([\phi])$, is equivalent to the type of creation and annihilation labels $\mathcal{F}.\text{fieldOpToCrAnType}(\phi)$ associated with $\phi$. Physically, this means that specifying a section for a single operator $\phi$ is uniquely determined by choosing its mode (creation or annihilation); if $\phi$ is an asymptotic state, this choice is unique (singleton), whereas if $\phi$ is a position-space operator, there are two choices.

For a given field specification $\mathcal{F}$, a field operator $\phi \in \mathcal{F}.\text{FieldOp}$, and a list of field operators $\phi_s$, there is a natural equivalence: $$\text{CrAnSection}(\phi :: \phi_s) \simeq \mathcal{F}.\text{fieldOpToCrAnType}(\phi) \times \text{CrAnSection}(\phi_s)$$ This equivalence decomposes a creation and annihilation section of the list $\phi :: \phi_s$ into a pair consisting of the specific mode (creation or annihilation label) of the first operator $\phi$ and the remaining section for the tail of the list $\phi_s$.

For a given field specification $\mathcal{F}$ and a list of field operators $\varphi_s = [\phi_1, \phi_2, \dots, \phi_n] \in \text{List}(\mathcal{F}.\text{FieldOp})$, the type of creation and annihilation sections $\text{CrAnSection}(\varphi_s)$ is finite. This finiteness is defined recursively: the section for an empty list is equivalent to the finite unit type, and the section for a list $\phi :: \varphi_s$ is equivalent to the product of the finite set of modes $\mathcal{F}.\text{fieldOpToCrAnType}(\phi)$ and the (inductively finite) set $\text{CrAnSection}(\varphi_s)$.

For a given field specification $\mathcal{F}$, the cardinality of the set of creation and annihilation sections $\text{CrAnSection}([])$ corresponding to the empty list of field operators is equal to $1$, denoted as: $$|\text{CrAnSection}([])| = 1$$ This reflects the fact that the only creation and annihilation section for an empty list of field operators is the empty list of creation and annihilation operators.

For a given field specification $\mathcal{F}$, let $\phi$ be a field operator and $\phi_s$ be a list of field operators. The number of creation and annihilation sections for the list formed by prepending $\phi$ to $\phi_s$ is equal to the product of the number of allowed creation or annihilation modes for $\phi$ and the number of sections for $\phi_s$: $$|\text{CrAnSection}(\phi :: \phi_s)| = |\mathcal{F}.\text{fieldOpToCrAnType}(\phi)| \times |\text{CrAnSection}(\phi_s)|$$ Here, $\mathcal{F}.\text{fieldOpToCrAnType}(\phi)$ represents the finite set of modes (such as $\{\text{create}, \text{annihilate}\}$ for position-space operators) associated with the operator $\phi$.

For a given field specification $\mathcal{F}$ and a list of field operators $\varphi_s = [\phi_1, \phi_2, \dots, \phi_n]$, let $\text{CrAnSection}(\varphi_s)$ be the set of all possible sequences of creation and annihilation components corresponding to $\varphi_s$. The cardinality of this set is given by: $$|\text{CrAnSection}(\varphi_s)| = 2^k$$ where $k$ is the number of position-space field operators in the list $\varphi_s$ (determined by the predicate $\mathcal{F}.\text{statesIsPosition}$). This follows from the fact that position-space operators possess two modes (creation and annihilation), while asymptotic operators possess only one.

For a given field specification $\mathcal{F}$, let $\varphi_s$ and $\varphi_s'$ be two lists of field operators. If $\varphi_s'$ is a permutation of $\varphi_s$, then the cardinality of the set of creation and annihilation sections for $\varphi_s$ is equal to the cardinality of the set of creation and annihilation sections for $\varphi_s'$: $$|\text{CrAnSection}(\varphi_s)| = |\text{CrAnSection}(\varphi_s')|$$

For a given field specification $\mathcal{F}$ and an additive commutative monoid $M$, let $\text{CrAnSection}([])$ be the type of creation and annihilation sections associated with the empty list of field operators. For any function $f : \text{CrAnSection}([]) \to M$, the sum of $f$ over all sections $s \in \text{CrAnSection}([])$ is equal to the value of $f$ at the unique empty section $\langle [], \text{rfl} \rangle$: $$\sum_{s \in \text{CrAnSection}([])} f(s) = f(\langle [], \text{rfl} \rangle)$$ where $\langle [], \text{rfl} \rangle$ denotes the section containing an empty list of creation/annihilation operators.

Let $\mathcal{F}$ be a field specification, $\phi \in \mathcal{F}.\text{FieldOp}$ be a field operator, and $\varphi_s$ be a list of field operators. For any function $f: \text{CrAnSection}(\phi :: \varphi_s) \to M$ mapping into an additive commutative monoid $M$, the sum over all possible creation and annihilation sections $s$ of the prepended list $\phi :: \varphi_s$ is equal to the iterated sum over the possible modes $a \in \mathcal{F}.\text{fieldOpToCrAnType}(\phi)$ of the first operator and the sections $s' \in \text{CrAnSection}(\varphi_s)$ of the remaining list: $$\sum_{s \in \text{CrAnSection}(\phi :: \varphi_s)} f(s) = \sum_{a \in \mathcal{F}.\text{fieldOpToCrAnType}(\phi)} \sum_{s' \in \text{CrAnSection}(\varphi_s)} f(\text{cons}(a, s'))$$ where $\text{cons}(a, s')$ denotes the section constructed by prepending the mode label $a$ to the section $s'$.

Let $\mathcal{F}$ be a field specification and $\varphi_s$ be a list of field operators. For any creation and annihilation section $s \in \text{CrAnSection}(\varphi_s)$ and any function $f$ mapping the indices of the list $s$ to an additive commutative monoid $M$, the sum over the indices of $s$ is equal to the sum over the indices of $\varphi_s$: $$\sum_{n \in \text{Fin}(|s|)} f(n) = \sum_{n \in \text{Fin}(|\varphi_s|)} f(n)$$ where $|s|$ and $|\varphi_s|$ denote the lengths of the respective lists, and the equality of indices is justified by the property that $|s| = |\varphi_s|$ for any section $s$ of $\varphi_s$.

For a field specification $\mathcal{F}$ and two lists of field operators $\varphi_s$ and $\varphi_s'$, an equality $\varphi_s = \varphi_s'$ induces an equivalence (a bijection) between the sets of creation and annihilation sections $\text{CrAnSection}(\varphi_s)$ and $\text{CrAnSection}(\varphi_s')$. This equivalence is the identity map when the two lists are equal by definition.

Let $\mathcal{F}$ be a field specification. Given two lists of field operators $\varphi_s, \varphi_s' \in \text{List}(\mathcal{F}.\text{FieldOp})$ such that there is an equality $h: \varphi_s = \varphi_s'$, let $\text{congr}(h)$ be the induced equivalence between the types of creation and annihilation sections $\text{CrAnSection}(\varphi_s)$ and $\text{CrAnSection}(\varphi_s')$. For any section $\psi_s \in \text{CrAnSection}(\varphi_s)$, the underlying list of creation and annihilation operators of the transformed section $\text{congr}(h, \psi_s)$ is equal to the underlying list of operators in $\psi_s$.

For a field specification $\mathcal{F}$ and two lists of field operators $\varphi_s$ and $\varphi_s'$, let $h : \varphi_s = \varphi_s'$ be an equality between them. Let $\text{congr}(h) : \text{CrAnSection}(\varphi_s) \simeq \text{CrAnSection}(\varphi_s')$ be the equivalence (bijection) between the sets of creation and annihilation sections induced by this equality. Then the inverse of this equivalence, $(\text{congr}(h))^{-1}$, is equal to the equivalence $\text{congr}(h^{-1})$ induced by the symmetric equality $h^{-1} : \varphi_s' = \varphi_s$.

Let $\mathcal{F}$ be a field specification. Suppose we have three lists of field operators $\varphi_s, \varphi_s', \varphi_s'' \in \text{List}(\mathcal{F}.\text{FieldOp})$ and two equalities $h_1 : \varphi_s = \varphi_s'$ and $h_2 : \varphi_s' = \varphi_s''$. Let $\text{congr}(h, \cdot)$ denote the equivalence between the types of creation and annihilation sections $\text{CrAnSection}(\text{source})$ and $\text{CrAnSection}(\text{target})$ induced by an equality $h$. For any creation and annihilation section $\psi_s \in \text{CrAnSection}(\varphi_s)$, the composition of these induced maps satisfies: $$\text{congr}(h_2, \text{congr}(h_1, \psi_s)) = \text{congr}(h, \psi_s)$$ where $h: \varphi_s = \varphi_s''$ is the equality obtained by the transitivity of $h_1$ and $h_2$.

Given a natural number $n$ and a creation-annihilation section $\psi_s \in \text{CrAnSection}(\varphi_s)$ corresponding to a list of field operators $\varphi_s = [\phi_1, \phi_2, \dots, \phi_m]$, this function returns the prefix of the section consisting of its first $n$ elements. The resulting list is a valid section for the truncated list of field operators $\varphi_s|_{n} = [\phi_1, \dots, \phi_{\min(n, m)}]$.

Let $\mathcal{F}$ be a field specification and $\varphi_s, \varphi_s'$ be lists of field operators such that $\varphi_s = \varphi_s'$. For any natural number $n$ and any creation and annihilation section $\psi_s \in \text{CrAnSection}(\varphi_s)$, taking the first $n$ elements of the section cast by the equality $\varphi_s = \varphi_s'$ is equal to casting the first $n$ elements of the original section $\psi_s$ via the induced equality $\varphi_s.\text{take}(n) = \varphi_s'.\text{take}(n)$. Mathematically, this is expressed as: $$\text{take}_n (\text{congr}(h, \psi_s)) = \text{congr}(h', \text{take}_n \psi_s)$$ where $h$ is the proof of $\varphi_s = \varphi_s'$ and $h'$ is the proof of $\varphi_s.\text{take}(n) = \varphi_s'.\text{take}(n)$.

For a given field specification $\mathcal{F}$, let $\varphi_s$ be a list of field operators and $\psi_s \in \text{CrAnSection}(\varphi_s)$ be a corresponding section of creation and annihilation operators. For any natural number $n$, the function $\text{drop}$ produces a new section by removing the first $n$ elements of the list $\psi_s$. This resulting list is a valid creation and annihilation section for the truncated list of field operators obtained by removing the first $n$ elements of $\varphi_s$.

Given a field specification $\mathcal{F}$ and two lists of field operators $\varphi_s$ and $\varphi_s'$ that are equal ($h: \varphi_s = \varphi_s'$), let $\text{congr}_h$ be the induced equivalence between the sets of creation and annihilation sections $\text{CrAnSection}(\varphi_s) \simeq \text{CrAnSection}(\varphi_s')$. For any natural number $n$ and any section $\psi_s \in \text{CrAnSection}(\varphi_s)$, the operation of dropping the first $n$ elements commutes with this congruence. Specifically, removing the first $n$ elements from the section $\text{congr}_h(\psi_s)$ is identical to removing the first $n$ elements from $\psi_s$ and then applying the congruence map associated with the equality of the truncated lists $\varphi_s.\text{drop}(n) = \varphi_s'.\text{drop}(n)$. Mathematically, this is expressed as: $$\text{drop}(n, \text{congr}(h, \psi_s)) = \text{congr}(h', \text{drop}(n, \psi_s))$$ where $h'$ is the proof that $\varphi_s.\text{drop}(n) = \varphi_s'.\text{drop}(n)$ follows from $h$.

Given a field specification $\mathcal{F}$ and two lists of field operators $\varphi_s, \varphi_s' \in \text{List}(\mathcal{F}.\text{FieldOp})$, let $\psi_s$ be a creation and annihilation section of $\varphi_s$ and $\psi_s'$ be a creation and annihilation section of $\varphi_s'$. The `append` operation constructs a new section of the concatenated list $\varphi_s \text{ ++ } \varphi_s'$ by concatenating the underlying lists of creation and annihilation operators $\psi_s$ and $\psi_s'$.

For a field specification $\mathcal{F}$ and three lists of field operators $\varphi_s, \varphi_s', \varphi_s'' \in \text{List}(\mathcal{F}.\text{FieldOp})$, let $\psi_s \in \text{CrAnSection}(\varphi_s)$, $\psi_s' \in \text{CrAnSection}(\varphi_s')$, and $\psi_s'' \in \text{CrAnSection}(\varphi_s'')$ be their respective creation and annihilation sections. The concatenation operation `append` for these sections is associative: $$\text{append}(\psi_s, \text{append}(\psi_s', \psi_s'')) = \text{congr}(h, \text{append}(\text{append}(\psi_s, \psi_s'), \psi_s''))$$ where $\text{congr}(h)$ is the equivalence between the types of creation and annihilation sections induced by the proof $h$ of the associativity of list concatenation, i.e., $\varphi_s \text{ ++ } (\varphi_s' \text{ ++ } \varphi_s'') = (\varphi_s \text{ ++ } \varphi_s') \text{ ++ } \varphi_s''$.

Let $\mathcal{F}$ be a field specification and $\varphi_s, \varphi_s', \varphi_s''$ be three lists of field operators in $\mathcal{F}.\text{FieldOp}$. Let $\psi_s \in \text{CrAnSection}(\varphi_s)$, $\psi_s' \in \text{CrAnSection}(\varphi_s')$, and $\psi_s'' \in \text{CrAnSection}(\varphi_s'')$ be their respective creation and annihilation sections. The concatenation operation $append$ for these sections is associative, such that: $$append(append(\psi_s, \psi_s'), \psi_s'') = \text{congr}(h, append(\psi_s, append(\psi_s', \psi_s'')))$$ where $h$ is the proof of associativity for list concatenation $(\varphi_s \text{ ++ } \varphi_s') \text{ ++ } \varphi_s'' = \varphi_s \text{ ++ } (\varphi_s' \text{ ++ } \varphi_s'')$, and $\text{congr}(h, \cdot)$ is the equivalence between the types $\text{CrAnSection}((\varphi_s \text{ ++ } \varphi_s') \text{ ++ } \varphi_s'')$ and $\text{CrAnSection}(\varphi_s \text{ ++ } (\varphi_s' \text{ ++ } \varphi_s''))$ induced by that equality.

For a given field specification $\mathcal{F}$, let $\phi \in \mathcal{F}.\text{FieldOp}$ be a field operator and $\varphi_s$ be a list of field operators. Let $\psi \in \mathcal{F}.\text{fieldOpToCrAnType}(\phi)$ be a creation or annihilation label for $\phi$, and let $\psi_s \in \text{CrAnSection}(\varphi_s)$ be a section of the list $\varphi_s$. The theorem states that: $$\text{append}(\text{singletonEquiv}^{-1}(\psi), \psi_s) = \text{cons}(\psi, \psi_s)$$ where $\text{singletonEquiv}^{-1}(\psi)$ is the creation/annihilation section of the singleton list $[\phi]$ corresponding to the label $\psi$, $\text{append}$ is the concatenation of sections, and $\text{cons}$ is the operation of prepending a label to a section.

For a field specification $\mathcal{F}$, let $\varphi_s$ be a list of field operators and $\psi_s \in \text{CrAnSection}(\varphi_s)$ be a creation and annihilation section. For any natural number $n$, the concatenation of the first $n$ elements of the section, $\text{take}(n, \psi_s)$, and the remaining elements, $\text{drop}(n, \psi_s)$, is equal to the original section $\psi_s$ after applying the type-level congruence induced by the list identity $\varphi_s = \text{take}(n, \varphi_s) \text{ ++ } \text{drop}(n, \varphi_s)$. That is: $$\text{append}(\text{take}(n, \psi_s), \text{drop}(n, \psi_s)) = \text{congr}(h, \psi_s)$$ where $h$ is the equality $\varphi_s = \text{take}(n, \varphi_s) \text{ ++ } \text{drop}(n, \varphi_s)$.

For a field specification $\mathcal{F}$, let $\varphi_{s1}, \varphi_{s1}', \varphi_{s2}, \varphi_{s2}'$ be lists of field operators such that $\varphi_{s1} = \varphi_{s1}'$ and $\varphi_{s2} = \varphi_{s2}'$. Given creation and annihilation sections $\psi_{s1} \in \text{CrAnSection}(\varphi_{s1})$ and $\psi_{s2} \in \text{CrAnSection}(\varphi_{s2})$, the concatenation of the sections after applying the type-level congruences induced by these equalities is equal to the type-level congruence applied to the concatenation of the original sections. That is: $$\text{append}(\text{congr}(h_1, \psi_{s1}), \text{congr}(h_2, \psi_{s2})) = \text{congr}(h, \text{append}(\psi_{s1}, \psi_{s2}))$$ where $\text{congr}$ is the equivalence between section types induced by an equality of the underlying field operator lists, and $h$ is the equality $\varphi_{s1} \text{ ++ } \varphi_{s2} = \varphi_{s1}' \text{ ++ } \varphi_{s2}'$ derived from $h_1$ and $h_2$.

For a field specification $\mathcal{F}$, let $\varphi_{s1}, \varphi_{s1'}, \varphi_{s2} \in \text{List}(\mathcal{F}.\text{FieldOp})$ be lists of field operators such that $h_1 : \varphi_{s1} = \varphi_{s1'}$. Given a creation and annihilation section $\psi_{s1}$ of $\varphi_{s1}$ and a section $\psi_{s2}$ of $\varphi_{s2}$, the concatenation of the section $\text{congr}(h_1, \psi_{s1})$ (which is $\psi_{s1}$ cast to the type $\text{CrAnSection}(\varphi_{s1'})$) with $\psi_{s2}$ is equal to casting the concatenated section $\text{append}(\psi_{s1}, \psi_{s2})$ using the equality $\varphi_{s1} \text{ ++ } \varphi_{s2} = \varphi_{s1'} \text{ ++ } \varphi_{s2}$ induced by $h_1$. In terms of the projection to the underlying lists of creation and annihilation operators, this states that: $$\text{append}(\text{congr}(h_1, \psi_{s1}), \psi_{s2}) = \text{congr}(h_1', \text{append}(\psi_{s1}, \psi_{s2}))$$ where $h_1'$ is the equality between concatenated lists of field operators.

For a field specification $\mathcal{F}$, let $\varphi_{s1}, \varphi_{s2}$, and $\varphi_{s2}'$ be lists of field operators, and let $h_2 : \varphi_{s2} = \varphi_{s2}'$ be an equality between the second and third lists. Given a creation and annihilation section $\psi_{s1}$ of $\varphi_{s1}$ and a section $\psi_{s2}$ of $\varphi_{s2}$, the result of concatenating $\psi_{s1}$ with the section $\psi_{s2}$ (adjusted to $\text{CrAnSection}(\varphi_{s2}')$ via the equality $h_2$) is equal to the concatenated section $\text{append}(\psi_{s1}, \psi_{s2})$ adjusted to $\text{CrAnSection}(\varphi_{s1} \text{ ++ } \varphi_{s2}')$ by the induced equality $\varphi_{s1} \text{ ++ } \varphi_{s2} = \varphi_{s1} \text{ ++ } \varphi_{s2}'$. Here, $\text{congr}$ denotes the equivalence between section types induced by an equality of their underlying field operator lists.

Let $\mathcal{F}$ be a field specification. For any two lists of field operators $\varphi_s, \varphi_s' \in \text{List}(\mathcal{F}.\text{FieldOp})$, let $\psi_s \in \text{CrAnSection}(\varphi_s)$ and $\psi_s' \in \text{CrAnSection}(\varphi_s')$ be their respective creation and annihilation sections. Then, taking the first $n$ elements of the concatenated section $\text{append}(\psi_s, \psi_s')$, where $n = \text{length}(\varphi_s)$, is equal to the original section $\psi_s$. This equality holds under the type-casting equivalence $\text{congr}$ induced by the list identity $\text{take}(|\varphi_s|, \varphi_s \mathbin{+\!+} \varphi_s') = \varphi_s$.

For a given field specification $\mathcal{F}$, let $\varphi_s$ and $\varphi_s'$ be lists of field operators. Let $\psi_s \in \text{CrAnSection}(\varphi_s)$ and $\psi_s' \in \text{CrAnSection}(\varphi_s')$ be their corresponding sections of creation and annihilation operators. Then, dropping the first $n$ elements of the concatenated section $\text{append}(\psi_s, \psi_s')$, where $n$ is the length of the list $\varphi_s$, is equal to the section $\psi_s'$. This equality is defined via the equivalence $\text{congr}$ induced by the list identity $(\varphi_s \mathbin{+\!+} \varphi_s').\text{drop}(\text{length}(\varphi_s)) = \varphi_s'$.

Given a field specification $\mathcal{F}$ and two lists of field operators $\varphi_s, \varphi_s' \in \text{List}(\mathcal{F}.\text{FieldOp})$, there exists an equivalence (bijection) between the type of creation and annihilation sections of the concatenated list, $\text{CrAnSection}(\varphi_s \mathbin{+\!+} \varphi_s')$, and the Cartesian product of the types of sections for the individual lists, $\text{CrAnSection}(\varphi_s) \times \text{CrAnSection}(\varphi_s')$. Specifically, the equivalence is defined by: - The forward map (splitting): A section of the concatenated list $\psi \in \text{CrAnSection}(\varphi_s \mathbin{+\!+} \varphi_s')$ is decomposed into a pair of sections $(\psi_1, \psi_2)$ by taking the first $n$ elements and dropping the first $n$ elements of $\psi$, respectively, where $n$ is the length of the list $\varphi_s$. - The inverse map (joining): A pair of sections $(\psi_s, \psi_s') \in \text{CrAnSection}(\varphi_s) \times \text{CrAnSection}(\varphi_s')$ is mapped to their concatenation $\psi_s \mathbin{+\!+} \psi_s'$.

Let $\alpha$ and $\beta$ be types, $f: \alpha \to \beta$ be a function, $l$ be a list of elements in $\alpha$, and $n$ be a natural number representing an index. The operation of mapping the function $f$ over the list $l$ after removing the element at index $n$ is equivalent to removing the element at index $n$ from the list after mapping $f$ over $l$. That is, $$\text{map}(f, \text{eraseIdx}(l, n)) = \text{eraseIdx}(\text{map}(f, l), n)$$ where $\text{map}(f, l)$ is the list obtained by applying $f$ to each element of $l$, and $\text{eraseIdx}(l, n)$ is the list $l$ with the element at position $n$ removed.

Given a natural number $n$ and a creation and annihilation section $\psi_s \in \text{CrAnSection}(\varphi_s)$ associated with a list of field operators $\varphi_s$, this function removes the $n$-th element from the underlying list of $\psi_s$. The resulting list is a valid section of the list of field operators $\text{eraseIdx}(\varphi_s, n)$, which represents the original list $\varphi_s$ with the element at index $n$ removed.

For a field specification $\mathcal{F}$ and a list of field operators $\varphi_s \in \text{List}(\mathcal{F}.\text{FieldOp})$, let $n$ be a natural number such that $n < \text{length}(\varphi_s)$. There exists an equivalence (bijection) between the type of creation and annihilation sections of the full list, $\text{CrAnSection}(\varphi_s)$, and the Cartesian product of: 1. The type of creation and annihilation labels associated with the $n$-th field operator in the list, $\mathcal{F}.\text{fieldOpToCrAnType}(\varphi_s[n])$. 2. The type of sections for the list obtained by removing the $n$-th operator, $\text{CrAnSection}(\varphi_s.\text{eraseIdx } n)$. This equivalence allows for the extraction of the creation/annihilation mode of a specific operator at index $n$ from a complete section of a product of field operators.

For a field specification $\mathcal{F}$, a list of field operators $\varphi_s$, and a natural number $n < \text{length}(\varphi_s)$, let $\psi_s$ be a creation and annihilation section in $\text{CrAnSection}(\varphi_s)$. The second component of the image of $\psi_s$ under the equivalence $\text{eraseIdxEquiv}$ (which decomposes a section into the $n$-th mode and the remaining section) is equal to the section obtained by directly removing the $n$-th element from $\psi_s$, denoted $\text{eraseIdx}(n, \psi_s)$.

For a field specification $\mathcal{F}$, let $\varphi_s$ be a list of field operators and $n$ be a natural number such that $n < \text{length}(\varphi_s)$. Let $a \in \mathcal{F}.\text{fieldOpToCrAnType}(\varphi_s[n])$ be a creation or annihilation label for the $n$-th field operator, and let $s \in \text{CrAnSection}(\varphi_s.\text{eraseIdx } n)$ be a section for the list of field operators where the $n$-th element has been removed. The inverse of the equivalence $\text{eraseIdxEquiv}$, which reconstructs a full section from a specific label and a truncated section, satisfies: $$(\text{eraseIdxEquiv}(n, \varphi_s, h_n))^{-1} \langle a, s \rangle = \text{congr}\left(h, \text{append}(\text{take}(n, s), \text{cons}(a, \text{drop}(n, s)))\right)$$ where: - $\text{take}(n, s)$ consists of the first $n$ creation/annihilation operators in $s$. - $\text{drop}(n, s)$ consists of the remaining operators in $s$ after the first $n$. - $\text{cons}(a, \dots)$ prepends the label $a$ to the dropped part of the section. - $\text{append}(\dots)$ concatenates the two sections. - $\text{congr}(h, \cdot)$ is the equivalence between the constructed section type and $\text{CrAnSection}(\varphi_s)$ induced by the equality of the underlying lists of field operators.