Physlib.QFT.PerturbationTheory.FieldStatistics.Basic

The type $\text{FieldStatistic}$ is an inductive type consisting of exactly two elements: $\text{bosonic}$ and $\text{fermionic}$. It is used to categorize whether a physical field or operator obeys Bose-Einstein statistics (bosonic) or Fermi-Dirac statistics (fermionic).

For any two field statistics $s_1, s_2 \in \text{FieldStatistic}$, it is decidable whether $s_1 = s_2$. This means there exists an algorithmic procedure to determine if two given statistics are both $\text{bosonic}$, both $\text{fermionic}$, or different.

The type $\text{FieldStatistic}$ forms a commutative group where the identity element is $\text{bosonic}$. The group operation $\cdot$ follows the rules of parity: - $\text{bosonic} \cdot \text{bosonic} = \text{bosonic}$ - $\text{bosonic} \cdot \text{fermionic} = \text{fermionic}$ - $\text{fermionic} \cdot \text{bosonic} = \text{fermionic}$ - $\text{fermionic} \cdot \text{fermionic} = \text{bosonic}$ In this structure, every element is its own inverse, and the group is isomorphic to $\mathbb{Z}_2$.

In the commutative group of quantum field statistics ($\text{FieldStatistic}$), where $\text{bosonic}$ is the identity element, the product of a bosonic statistic with itself is a bosonic statistic. That is: $$\text{bosonic} \cdot \text{bosonic} = \text{bosonic}$$

In the commutative group of quantum field statistics ($\text{FieldStatistic}$), where the identity element is $\text{bosonic}$ and the non-trivial element is $\text{fermionic}$, the product of a bosonic statistic and a fermionic statistic is a fermionic statistic. That is: $$\text{bosonic} \cdot \text{fermionic} = \text{fermionic}$$

In the commutative group of quantum field statistics ($\text{FieldStatistic}$), where the identity element is $\text{bosonic}$ and the non-trivial element is $\text{fermionic}$, the product of a fermionic statistic and a bosonic statistic is a fermionic statistic. That is: $$\text{fermionic} \cdot \text{bosonic} = \text{fermionic}$$

In the commutative group of field statistics ($\text{FieldStatistic}$), the product of two fermionic statistics is a bosonic statistic. This reflects the $\mathbb{Z}_2$ parity structure where the combination of two odd (fermionic) elements results in an even (bosonic) element: $$\text{fermionic} \cdot \text{fermionic} = \text{bosonic}$$

In the commutative group of quantum field statistics $\text{FieldStatistic}$, which classifies fields as either $\text{bosonic}$ or $\text{fermionic}$, the product of any statistic $a$ with the $\text{bosonic}$ statistic is equal to $a$: $$a \cdot \text{bosonic} = a$$ This confirms that the $\text{bosonic}$ statistic acts as the identity element within this group structure.

For any field statistic $a \in \text{FieldStatistic}$, the product of $a$ with itself is the identity element $1$ of the commutative group of field statistics, i.e., $a \cdot a = 1$. This identity element $1$ corresponds to the bosonic statistic.

The type $\text{FieldStatistic}$, which classifies quantum fields as either $\text{bosonic}$ or $\text{fermionic}$, is a finite type (an instance of `Fintype`). It consists of exactly two distinct elements: $\{\text{bosonic}, \text{fermionic}\}$.

The field statistics $\text{fermionic}$ and $\text{bosonic}$ are not equal, i.e., $\text{fermionic} \neq \text{bosonic}$.

The equality between the field statistics $\text{bosonic}$ and $\text{fermionic}$ is equivalent to $\text{False}$.

For any quantum field statistic $a \in \text{FieldStatistic}$, $a$ is not fermionic if and only if $a$ is bosonic. Here, $\text{FieldStatistic}$ is the type classifying fields as either $\text{bosonic}$ or $\text{fermionic}$.

For any field statistic $a \in \text{FieldStatistic}$, it holds that $a \neq \text{bosonic}$ if and only if $a = \text{fermionic}$.

For any field statistic $a \in \text{FieldStatistic}$, the condition that $a$ is not bosonic is equivalent to the condition that $a$ is fermionic. In mathematical notation, $\text{bosonic} \neq a \iff \text{fermionic} = a$.

For any field statistic $a$, it holds that $a$ is not equal to $\text{fermionic}$ if and only if $a$ is equal to $\text{bosonic}$. In mathematical terms, for $a \in \text{FieldStatistic}$, $\text{fermionic} \neq a \iff \text{bosonic} = a$.

For any quantum field statistics $a, b \in \text{FieldStatistic}$, the product $a \cdot b$ is equal to the identity element $1$ (the $\text{bosonic}$ statistic) if and only if $a = b$. The type $\text{FieldStatistic}$ classifies fields as either $\text{bosonic}$ or $\text{fermionic}$ and forms a commutative group where every element is its own inverse.

In the commutative group of quantum field statistics $\text{FieldStatistic}$ (where elements are either $\text{bosonic}$ or $\text{fermionic}$), the product of two statistics $a$ and $b$ is the identity element $1$ (the $\text{bosonic}$ statistic) if and only if $a$ and $b$ are equal.

For any quantum field statistics $a, b, c \in \text{FieldStatistic}$, the product $a \cdot b = c$ if and only if $a = b \cdot c$. Here, $\text{FieldStatistic}$ is the type classifying fields as either $\text{bosonic}$ or $\text{fermionic}$, forming a commutative group where the identity element is $\text{bosonic}$ and every element is its own inverse ($b \cdot b = \text{bosonic}$).

For any quantum field statistics $a, b, c \in \text{FieldStatistic}$, the product $a \cdot b = c$ holds if and only if $b = a \cdot c$. Here, $\text{FieldStatistic}$ is the type classifying fields as either bosonic or fermionic, forming a commutative group where the identity element is bosonic and every element is its own inverse (i.e., $x \cdot x = \text{bosonic}$ for any statistic $x$).

Given a mapping $s: \mathcal{F} \to \text{FieldStatistic}$ that assigns a statistic (either $\text{bosonic}$ or $\text{fermionic}$) to each field in a collection $\mathcal{F}$, the function determines the collective statistic of a finite list of fields $[\phi_1, \phi_2, \dots, \phi_n]$. The resulting statistic is $\text{fermionic}$ if there is an odd number of fields in the list for which $s(\phi_i) = \text{fermionic}$; otherwise, the result is $\text{bosonic}$. Mathematically, this corresponds to the product $\prod_{i=1}^n s(\phi_i)$ where the statistics follow the group rules of $\mathbb{Z}_2$.

Let $s: \mathcal{F} \to \text{FieldStatistic}$ be a mapping that assigns a statistic (either $\text{bosonic}$ or $\text{fermionic}$) to each field in a collection $\mathcal{F}$. For any field $\phi \in \mathcal{F}$ and any finite list of fields $\phi s$, the collective statistic of the list formed by prepending $\phi$ to $\phi s$ (denoted $\phi :: \phi s$) is equal to the product of the statistic of $\phi$ and the collective statistic of the original list $\phi s$: $$\text{ofList}(s, \phi :: \phi s) = s(\phi) \cdot \text{ofList}(s, \phi s)$$ where the multiplication $\cdot$ follows the $\mathbb{Z}_2$ group structure of $\text{FieldStatistic}$ (where $\text{bosonic}$ is the identity and $\text{fermionic} \cdot \text{fermionic} = \text{bosonic}$).

Let $\mathcal{F}$ be a collection of fields and $s: \mathcal{F} \to \text{FieldStatistic}$ be a mapping that assigns a statistic (bosonic or fermionic) to each field. For any list of fields $\phi s = [\phi_1, \phi_2, \dots, \phi_n]$, the collective statistic $\text{ofList}(s, \phi s)$ is equal to the product of the statistics of the individual fields in the list: $$\text{ofList}(s, \phi s) = \prod_{i=1}^n s(\phi_i)$$ where the product is taken in the commutative group structure of $\text{FieldStatistic}$ (with $\text{bosonic}$ as the identity).

Given a collection of fields $\mathcal{F}$ and a mapping $s: \mathcal{F} \to \text{FieldStatistic}$ that assigns a statistic (bosonic or fermionic) to each field, the collective statistic of a singleton list containing exactly one field $\phi \in \mathcal{F}$ is equal to the statistic of that field, $s(\phi)$.

Let $\mathcal{F}$ be a collection of fields and $s: \mathcal{F} \to \text{FieldStatistic}$ be a mapping that assigns a statistic (either $\text{bosonic}$ or $\text{fermionic}$) to each field. For any field $\phi \in \mathcal{F}$, the collective field statistic of the field when represented as a single-element word in the free monoid, denoted by $\text{FreeMonoid.of}(\phi)$, is equal to the statistic of the individual field $s(\phi)$.

Given a mapping $s : \mathcal{F} \to \text{FieldStatistic}$ that assigns a statistic (either $\text{bosonic}$ or $\text{fermionic}$) to each field in a collection $\mathcal{F}$, the collective field statistic of an empty list of fields is $\text{bosonic}$.

Given a mapping $s: \mathcal{F} \to \text{FieldStatistic}$ that assigns a statistic (either $\text{bosonic}$ or $\text{fermionic}$) to each field, the collective statistic of the concatenation of two lists of fields $\phi s$ and $\phi s'$ is $\text{bosonic}$ if the collective statistics of the individual lists $\phi s$ and $\phi s'$ are equal, and $\text{fermionic}$ otherwise.

Let $s: \mathcal{F} \to \text{FieldStatistic}$ be a mapping that assigns a statistic (either $\text{bosonic}$ or $\text{fermionic}$) to each field in a collection $\mathcal{F}$. For any two finite lists of fields $\varphi s$ and $\varphi s'$, the collective field statistic of their concatenation $\varphi s \mathbin{+\!+} \varphi s'$ is equal to the product of the collective statistics of the individual lists: $$\text{ofList}(s, \varphi s \mathbin{+\!+} \varphi s') = \text{ofList}(s, \varphi s) \cdot \text{ofList}(s, \varphi s')$$ where the multiplication $\cdot$ follows the rules of the $\text{FieldStatistic}$ commutative group (isomorphic to $\mathbb{Z}_2$), where $\text{bosonic}$ is the identity element.

Let $s: \mathcal{F} \to \text{FieldStatistic}$ be a mapping that assigns a field statistic (either $\text{bosonic}$ or $\text{fermionic}$) to each field in a collection $\mathcal{F}$. For any two lists of fields $l$ and $l'$, if $l$ is a permutation of $l'$, then their collective field statistics are equal: $$\text{ofList}(s, l) = \text{ofList}(s, l')$$ This property arises because the collective statistic is calculated as the product of individual statistics within a commutative group.

Let $s: \mathcal{F} \to \text{FieldStatistic}$ be a mapping that assigns a statistic (either $\text{bosonic}$ or $\text{fermionic}$) to each field in a collection $\mathcal{F}$. For any list of fields $\varphi s$, field $\varphi \in \mathcal{F}$, and decidable ordering relation $\le$ on $\mathcal{F}$, the collective field statistic of the list obtained by performing an ordered insertion of $\varphi$ into $\varphi s$ is equal to the collective statistic of the list formed by prepending $\varphi$ to the front of $\varphi s$: $$\text{ofList}(s, \text{orderedInsert}(\le, \varphi, \varphi s)) = \text{ofList}(s, \varphi :: \varphi s)$$

Let $s: \mathcal{F} \to \text{FieldStatistic}$ be a mapping that assigns a statistic (either $\text{bosonic}$ or $\text{fermionic}$) to each field in a collection $\mathcal{F}$. For any list of fields $\phi_s$ and any decidable binary relation $\le$ on $\mathcal{F}$, the collective field statistic of the list sorted via the insertion sort algorithm is equal to the collective field statistic of the original list: $$\text{ofList}(s, \text{insertionSort}(\le, \phi_s)) = \text{ofList}(s, \phi_s)$$ This result follows from the fact that insertion sort is a permutation of the original list, and the collective statistic (defined as the product of individual statistics in a commutative $\mathbb{Z}_2$ group) is invariant under permutations.

Let $s: \mathcal{F} \to \text{FieldStatistic}$ be a mapping that assigns a statistic to each field. For any list of fields $\phi_s$ and any list of indices $l$ into $\phi_s$ such that $l$ contains no duplicate indices, the collective statistic of the list of fields selected by $l$ is equal to the product over all indices $i \in \{0, \dots, \text{length}(\phi_s) - 1\}$ of $s(\phi_s[i])$ if $i \in l$, and the bosonic statistic (the identity $1$) otherwise. Mathematically: $$\text{ofList } s (\text{map } \phi_s \text{ } l) = \prod_{i=0}^{\text{length}(\phi_s)-1} \begin{cases} s(\phi_s[i]) & \text{if } i \in l \\ \text{bosonic} & \text{otherwise} \end{cases}$$ where the map operation constructs a new list of fields by selecting elements from $\phi_s$ at the indices specified in $l$.

Let $s: \mathcal{F} \to \text{FieldStatistic}$ be a mapping that assigns a statistic (either $\text{bosonic}$ or $\text{fermionic}$) to each field in a collection $\mathcal{F}$. For any two fields $\phi_1, \phi_2 \in \mathcal{F}$, the collective field statistic of the list containing these two fields is equal to the product of their individual statistics: $$\text{ofList}(s, [\phi_1, \phi_2]) = s(\phi_1) \cdot s(\phi_2)$$ where the multiplication $\cdot$ follows the $\mathbb{Z}_2$ commutative group structure of $\text{FieldStatistic}$ (with $\text{bosonic}$ as the identity element).

Given a mapping $q: \mathcal{F} \to \text{FieldStatistic}$ that assigns a statistic (either $\text{bosonic}$ or $\text{fermionic}$) to each field, let $\phi_s$ be a list of fields and $n$ be a natural number. The collective field statistic of the first $n$ elements of $\phi_s$ is equal to the collective field statistic of the first $n$ elements of the list obtained by inserting a field $\phi$ into $\phi_s$ at index $n$. Mathematically, this is expressed as: $$\text{ofList } q (\text{take } n \text{ } \phi_s) = \text{ofList } q (\text{take } n \text{ } (\text{insertIdx } \phi_s \text{ } n \text{ } \phi))$$ where $\text{take } n$ denotes the sublist of the first $n$ elements and $\text{insertIdx}$ denotes the insertion of an element at a specific position.

Let $\mathcal{F}$ be a collection of fields and $q: \mathcal{F} \to \text{FieldStatistic}$ be a mapping that assigns a statistic (either $\text{bosonic}$ or $\text{fermionic}$) to each field. For any list of fields $\varphi_s$ and any natural number $n$, the collective field statistic of the first $n$ elements of the list remains unchanged if the element at index $n$ is removed from $\varphi_s$. That is, $$\text{ofList}(q, \text{take}(n, \text{eraseIdx}(n, \varphi_s))) = \text{ofList}(q, \text{take}(n, \varphi_s))$$ where $\text{take}(n, L)$ returns the first $n$ elements of a list $L$, and $\text{eraseIdx}(n, L)$ removes the element at the $n$-th position.

For any list of fields $\varphi_s$ and any mapping $q: \mathcal{F} \to \text{FieldStatistic}$ that assigns a statistic to each field, the collective field statistic of the first $0$ elements of $\varphi_s$ is the identity element $1$ (which represents the bosonic statistic). Mathematically, this is expressed as: $$\text{ofList } q (\text{take } 0 \text{ } \varphi_s) = 1$$ where $\text{take } 0$ denotes the sublist containing the first zero elements (the empty list).

Let $q : \mathcal{F} \to \text{FieldStatistic}$ be a mapping that assigns a statistic (either bosonic or fermionic) to each field in a collection $\mathcal{F}$. For any natural number $n$, field $\phi_1 \in \mathcal{F}$, and list of fields $\phi s$, the collective field statistic of the first $n+1$ elements of the list formed by prepending $\phi_1$ to $\phi s$ is equal to the product of the statistic of $\phi_1$ and the collective field statistic of the first $n$ elements of $\phi s$. Mathematically: $$\text{ofList}(q, \text{take}(n + 1, \phi_1 :: \phi s)) = q(\phi_1) \cdot \text{ofList}(q, \text{take}(n, \phi s))$$ where $\text{take}(k, L)$ denotes the sublist of the first $k$ elements of $L$, and the multiplication $\cdot$ follows the $\mathbb{Z}_2$ group structure of field statistics.

Let $q : \mathcal{F} \to \text{FieldStatistic}$ be a mapping that assigns a statistic (either bosonic or fermionic) to each field in a collection $\mathcal{F}$. For any list of fields $\phi_s$, any field $\phi_1 \in \mathcal{F}$, and any natural numbers $n$ and $m$ such that $n < m$, the collective field statistic of the first $n$ elements of the list obtained by inserting $\phi_1$ into $\phi_s$ at index $m$ is equal to the collective field statistic of the first $n$ elements of the original list $\phi_s$.

Let $q : \mathcal{F} \to \text{FieldStatistic}$ be a mapping that assigns a statistic (either $\text{bosonic}$ or $\text{fermionic}$) to each field in a collection $\mathcal{F}$. For any list of fields $\phi_s$, a field $\phi_1 \in \mathcal{F}$, and natural numbers $n$ and $m$ such that $m \leq n$ and $m$ is within the bounds of the list ($m \leq \text{length}(\phi_s)$), the collective field statistic of the first $n + 1$ elements of the list obtained by inserting $\phi_1$ into $\phi_s$ at index $m$ is equal to the collective field statistic of the first $n + 1$ elements of the list obtained by prepending $\phi_1$ to the front of $\phi_s$. Mathematically: $$\text{ofList}(q, \text{take}(n + 1, \text{insertIdx}(\phi_s, m, \phi_1))) = \text{ofList}(q, \text{take}(n + 1, \phi_1 :: \phi_s))$$ where $\text{insertIdx}(L, i, x)$ denotes the insertion of element $x$ into list $L$ at position $i$, and $\text{take}(k, L)$ denotes the sublist consisting of the first $k$ elements of $L$.

Let $q : \mathcal{F} \to \text{FieldStatistic}$ be a mapping that assigns a statistic (either $\text{bosonic}$ or $\text{fermionic}$) to each field in a collection $\mathcal{F}$. For any list of fields $\phi_s$, a field $\phi_1 \in \mathcal{F}$, and natural numbers $n$ and $m$ such that $m \leq n$ and $m$ is within the bounds of the list ($m \leq \text{length}(\phi_s)$), the collective field statistic of the first $n + 1$ elements of the list obtained by inserting $\phi_1$ into $\phi_s$ at index $m$ is equal to the product of the statistic of $\phi_1$ and the collective field statistic of the first $n$ elements of the original list $\phi_s$. Mathematically: $$\text{ofList}(q, \text{take}(n + 1, \text{insertIdx}(\phi_s, m, \phi_1))) = q(\phi_1) \cdot \text{ofList}(q, \text{take}(n, \phi_s))$$ where $\text{insertIdx}(L, i, x)$ denotes the insertion of element $x$ into list $L$ at position $i$, $\text{take}(k, L)$ denotes the sublist consisting of the first $k$ elements of $L$, and the multiplication $\cdot$ follows the $\mathbb{Z}_2$ group structure of field statistics.

The type $\text{FieldStatistic}$ is endowed with an additive monoid structure. In this structure, the additive identity element (zero) is $\text{bosonic}$. The addition of two statistics $a + b$ is defined to be equal to their multiplication $a \cdot b$ in the underlying commutative group. Specifically, the addition follows parity rules: - $\text{bosonic} + \text{bosonic} = \text{bosonic}$ - $\text{bosonic} + \text{fermionic} = \text{fermionic}$ - $\text{fermionic} + \text{fermionic} = \text{bosonic}$ For any natural number $n \in \mathbb{N}$ and statistic $a$, the natural scalar multiplication $n \cdot a$ is defined as the $n$-fold sum of $a$, which corresponds to the product $\prod_{i=1}^n a$.

For any two field statistics $a, b \in \text{FieldStatistic}$ (which can be either bosonic or fermionic), the sum $a + b$ in the additive monoid is equal to the product $a \cdot b$ in the commutative group.