Physlib.QFT.PerturbationTheory.CreateAnnihilate

The type $\text{CreateAnnihilate}$ is a set consisting of exactly two elements: $\text{create}$ and $\text{annihilate}$. This type is used to classify whether a quantum field operator is a creation operator or an annihilation operator (or a combination such as a sum or integral thereof).

The default element of the type $\text{CreateAnnihilate}$, which is defined as the set $\{\text{create}, \text{annihilate}\}$ used to classify quantum field operators.

The type $\text{CreateAnnihilate}$, defined as the set $\{\text{create}, \text{annihilate}\}$, is inhabited, meaning it contains at least one element that can serve as a default value.

Given two elements $x, y$ of the set $\text{CreateAnnihilate} = \{\text{create}, \text{annihilate}\}$, this function returns a boolean value indicating whether $x$ and $y$ are identical.

The instance `instBEqCreateAnnihilate` provides a boolean equality operator for the set $\text{CreateAnnihilate} = \{\text{create}, \text{annihilate}\}$. For any two labels $x, y \in \text{CreateAnnihilate}$, it evaluates whether $x$ and $y$ are the same element and returns a boolean value.

The equality relation on the set $\text{CreateAnnihilate} = \{\text{create}, \text{annihilate}\}$ is decidable. Specifically, for any two labels $x, y \in \text{CreateAnnihilate}$, it can be computationally determined whether $x = y$ or $x \neq y$.

The set of creation and annihilation labels, $\text{CreateAnnihilate} = \{ \text{create}, \text{annihilate} \}$, is a finite set. This finiteness is established by the exhaustive enumeration of its two elements.

The relation $\text{normalOrder}$ is defined on the set of labels $\text{CreateAnnihilate} = \{\text{create}, \text{annihilate}\}$. For any two labels $a, b \in \text{CreateAnnihilate}$, the statement $\text{normalOrder}(a, b)$ is true for the pairs $(\text{create}, \text{create})$, $(\text{create}, \text{annihilate})$, and $(\text{annihilate}, \text{annihilate})$, and it is false if and only if $a = \text{annihilate}$ and $b = \text{create}$. This relation defines the standard normal ordering convention where annihilation operators are not permitted to the left of creation operators.

The normal ordering relation $\text{normalOrder}$ on the set of labels $\text{CreateAnnihilate} = \{\text{create}, \text{annihilate}\}$ is decidable. For any two labels $\phi, \phi' \in \text{CreateAnnihilate}$, there is a deterministic procedure to verify whether $\text{normalOrder}(\phi, \phi')$ holds, based on the definition that the relation is false if and only if $\phi = \text{annihilate}$ and $\phi' = \text{create}$.

The normal ordering relation $\preceq$ on the set of labels $\text{CreateAnnihilate} = \{\text{create}, \text{annihilate}\}$ is total. That is, for any two labels $\phi, \psi \in \text{CreateAnnihilate}$, it holds that $\phi \preceq \psi$ or $\psi \preceq \phi$. Here, the relation $\phi \preceq \psi$ is defined to be true for all pairs except when $\phi = \text{annihilate}$ and $\psi = \text{create}$.

The normal ordering relation $\text{normalOrder}$ on the set of creation and annihilation labels $\text{CreateAnnihilate} = \{\text{create}, \text{annihilate}\}$ is transitive. That is, for any labels $a, b, c \in \text{CreateAnnihilate}$, if the pair $(a, b)$ is in normal order and the pair $(b, c)$ is in normal order, then the pair $(a, c)$ is also in normal order.

Let $\text{CreateAnnihilate} = \{\text{create}, \text{annihilate}\}$ be the set of labels used to classify quantum field operators. Let $\text{normalOrder}(a, b)$ be the relation representing the standard normal ordering convention, which is defined to be false if and only if $a = \text{annihilate}$ and $b = \text{create}$. For any label $a \in \text{CreateAnnihilate}$, the statement $\neg \text{normalOrder}(a, \text{annihilate})$ is equivalent to False.

Let $M$ be an additive commutative monoid and let $f: \text{CreateAnnihilate} \to M$ be a function. Given that the set of creation and annihilation labels is defined as $\text{CreateAnnihilate} = \{\text{create}, \text{annihilate}\}$, the sum of $f$ over all elements in $\text{CreateAnnihilate}$ is equal to the sum of the values of $f$ at $\text{create}$ and $\text{annihilate}$: $$\sum_{i \in \text{CreateAnnihilate}} f(i) = f(\text{create}) + f(\text{annihilate})$$

Let $\text{CreateAnnihilate} = \{\text{create}, \text{annihilate}\}$ be the set of labels for creation and annihilation operators. The cardinality of this set is equal to 2, denoted as $|\text{CreateAnnihilate}| = 2$.