Physlib.QFT.PerturbationTheory.FieldSpecification.TimeOrder

For a given field specification $\mathcal{F}$, the relation $\text{timeOrderRel}(\phi_0, \phi_1)$ on field operators $\phi_0, \phi_1 \in \text{FieldOp}(\mathcal{F})$ is defined to hold if $\phi_0$ is chronologically "later" than or equal to $\phi_1$. Following the convention that outgoing asymptotic states exist at $t = +\infty$ and incoming asymptotic states exist at $t = -\infty$, the relation holds in the following cases: - $\phi_0$ is an outgoing asymptotic operator ($\text{outAsymp}$), regardless of $\phi_1$. - $\phi_0$ and $\phi_1$ are both position-space operators at spacetime points $x_0$ and $x_1$ respectively, and the time component $x_0^0 \ge x_1^0$. - $\phi_0$ is a position-space operator and $\phi_1$ is an incoming asymptotic operator ($\text{inAsymp}$). - $\phi_0$ and $\phi_1$ are both incoming asymptotic operators. In all other cases—such as when $\phi_0$ is a position-space operator and $\phi_1$ is an outgoing operator, or when $\phi_0$ is an incoming operator and $\phi_1$ is a position-space operator—the relation is false.

For any two field operators $\phi, \phi' \in \text{FieldOp}(\mathcal{F})$ in a given field specification $\mathcal{F}$, the time-ordering relation $\text{timeOrderRel}(\phi, \phi')$ is decidable. This means there is a formal procedure to determine whether $\phi$ is chronologically later than or equal to $\phi'$. The determination follows these rules: - If $\phi$ is an outgoing asymptotic operator ($\text{outAsymp}$), the relation is true regardless of $\phi'$. - If both $\phi$ and $\phi'$ are position-space operators at spacetime points $x$ and $x'$, the relation is true if the time components satisfy $x^0 \ge (x')^0$. - If $\phi$ is a position-space operator and $\phi'$ is an incoming asymptotic operator ($\text{inAsymp}$), the relation is true. - If both are incoming asymptotic operators, the relation is true. - In all other cases, the relation is false. Note that while this relation is logically decidable, it is non-computable because it depends on the decidability of the $\le$ relation on real numbers $\mathbb{R}$.

For a given field specification $\mathcal{F}$, the time ordering relation $\text{timeOrderRel}$ on the set of field operators $\text{FieldOp}(\mathcal{F})$ is total. That is, for any two field operators $\phi_0, \phi_1 \in \text{FieldOp}(\mathcal{F})$, either $\text{timeOrderRel}(\phi_0, \phi_1)$ holds (meaning $\phi_0$ is chronologically later than or equal to $\phi_1$) or $\text{timeOrderRel}(\phi_1, \phi_0)$ holds.

For a given field specification $\mathcal{F}$, the time-ordering relation $\text{timeOrderRel}$ on the set of field operators $\text{FieldOp}(\mathcal{F})$ is transitive. That is, for any field operators $\phi_1, \phi_2, \phi_3 \in \text{FieldOp}(\mathcal{F})$, if $\text{timeOrderRel}(\phi_1, \phi_2)$ holds (meaning $\phi_1$ is chronologically later than or equal to $\phi_2$) and $\text{timeOrderRel}(\phi_2, \phi_3)$ holds, then $\text{timeOrderRel}(\phi_1, \phi_3)$ holds.

Given a non-empty list of field operators $L = [\phi_0, \phi_1, \dots, \phi_n]$ (represented as a head $\phi$ and a tail $\phi_s$), this function returns the zero-based index $k \in \{0, \dots, n\}$ of the operator that is chronologically latest according to the relation $\text{timeOrderRel}$. If multiple operators share the same maximum time, the index of the first such operator is returned. For example, given a list of operators at times $[t=4, t=5, t=3, t=5]$, the function returns $1$, as the first occurrence of the maximum time ($t=5$) is at index $1$.

For a given field specification $\mathcal{F}$, let $\phi \in \text{FieldOp}(\mathcal{F})$ be a field operator and $\Phi_s$ be a list of field operators. Let $L = \phi :: \Phi_s$ be the list formed by prepending $\phi$ to $\Phi_s$. The index $k = \text{maxTimeFieldPos}(\phi, \Phi_s)$ of the chronologically latest operator in $L$ (relative to the time-ordering relation $\text{timeOrderRel}$) is strictly less than the length of the list $L$.

Given a field operator $\phi$ and a list of field operators $[\phi_1, \phi_2, \dots, \phi_n]$ belonging to a field specification $\mathcal{F}$, this function returns the chronologically latest operator in the combined sequence $[\phi, \phi_1, \dots, \phi_n]$. The "latest" property is determined by the relation $\text{timeOrderRel}$, where outgoing asymptotic operators are considered at $t = +\infty$, incoming operators at $t = -\infty$, and position-space operators by their time component $x^0$. If multiple operators share the same maximum time, the function returns the operator that appears leftmost in the sequence.

Given a field specification $\mathcal{F}$, a field operator $\phi \in \text{FieldOp}(\mathcal{F})$, and a list of field operators $\Phi_s$, the function `eraseMaxTimeField` identifies the chronologically latest operator in the list formed by prepending $\phi$ to $\Phi_s$. Specifically, it removes the first (left-most) occurrence of the operator that is maximal with respect to the time-ordering relation $\text{timeOrderRel}$. For example, if the operators in the list $[\phi, \phi_1, \dots, \phi_n]$ have associated times $[4, 5, 3, 5]$, the function returns a list with the times $[4, 3, 5]$ by removing the first operator with time $t=5$.

For a given field specification $\mathcal{F}$, let $\phi \in \text{FieldOp}(\mathcal{F})$ be a field operator and $\Phi_s$ be a list of field operators. The length of the list resulting from `eraseMaxTimeField` (which removes the chronologically latest operator from the sequence formed by prepending $\phi$ to $\Phi_s$) is equal to the length of the original list $\Phi_s$.

For a given field specification $\mathcal{F}$, let $\phi \in \text{FieldOp}(\mathcal{F})$ be a field operator and $\Phi_s$ be a list of field operators. The index of the chronologically latest operator in the list formed by $\phi$ and $\Phi_s$, denoted by $\text{maxTimeFieldPos}(\phi, \Phi_s)$, is strictly less than the successor of the length of the list produced by removing that same latest operator from the sequence. Mathematically, $\text{maxTimeFieldPos}(\phi, \Phi_s) < \text{length}(\text{eraseMaxTimeField}(\phi, \Phi_s)) + 1$.

For a given field specification $\mathcal{F}$, let $\Phi = [\phi, \phi_1, \dots, \phi_n]$ be a list of field operators in $\text{FieldOp}(\mathcal{F})$. This function returns the index $k \in \{0, \dots, n\}$, represented as an element of the finite type $\text{Fin}(n+1)$, of the first (left-most) operator that is maximal with respect to the time-ordering relation $\text{timeOrderRel}$. The relation $\text{timeOrderRel}(\phi_a, \phi_b)$ indicates that $\phi_a$ is chronologically later than or equal to $\phi_b$, considering outgoing asymptotic states at $t = +\infty$, incoming asymptotic states at $t = -\infty$, and position-space operators at their respective time coordinates $x^0$.

For any field specification $\mathcal{F}$, let $\Phi = [\phi, \phi_1, \dots, \phi_n]$ be a sequence of field operators. Let $\phi_{\text{max}}$ be the chronologically latest operator in $\Phi$ as determined by the relation $\text{timeOrderRel}$ (specifically, the leftmost operator among those with maximal time). For any operator $\phi_j$ that appears in the sequence at an index $j$ strictly less than the index of $\phi_{\text{max}}$, the relation $\text{timeOrderRel}(\phi_j, \phi_{\text{max}})$ does not hold.

For a given field specification $\mathcal{F}$, let $\phi$ be a field operator and $\Phi_s$ be a list of field operators. Let $\phi_{\text{max}} = \text{maxTimeField}(\phi, \Phi_s)$ be the chronologically latest operator in the sequence formed by prepending $\phi$ to $\Phi_s$, as determined by the relation $\text{timeOrderRel}$. Then, for any operator $\phi'$ at index $i$ in the list $\text{eraseMaxTimeField}(\phi, \Phi_s)$ (which is the sequence with the first occurrence of $\phi_{\text{max}}$ removed), the relation $\text{timeOrderRel}(\phi_{\text{max}}, \phi')$ holds.

For a list of field operators $[\phi_1, \phi_2, \dots, \phi_n]$ associated with a field specification $\mathcal{F}$, this function computes the sign $\epsilon \in \{1, -1\} \subset \mathbb{C}$ required to arrange the operators into chronological order (where the operator with the latest time is on the left). The sign is determined by the Koszul convention: a factor of $-1$ is picked up for every swap of two fermionic operators (where the statistics are defined by `fieldOpStatistic`), while swaps involving bosonic operators do not change the sign. The ordering is determined by the relation $\text{timeOrderRel}$.

For any field specification $\mathcal{F}$, the time-ordering sign of an empty list of field operators is equal to 1.

Let $\mathcal{F}$ be a field specification and $\phi, \psi \in \text{FieldOp}(\mathcal{F})$ be field operators. If $\phi$ is chronologically later than or equal to $\psi$ (i.e., the relation $\text{timeOrderRel}(\phi, \psi)$ holds), then the time-ordering sign of the list $[\phi, \psi]$ is $1$.

For a field specification $\mathcal{F}$ and two field operators $\phi, \psi \in \text{FieldOp}(\mathcal{F})$, if $\phi$ is not chronologically later than or equal to $\psi$ (i.e., $\neg \text{timeOrderRel}(\phi, \psi)$ holds), then the time-ordering sign of the list $[\phi, \psi]$ is given by the swap sign $\mathcal{S}(\mathcal{F} \triangleright_s \phi, \mathcal{F} \triangleright_s \psi)$, where $\mathcal{F} \triangleright_s \phi$ and $\mathcal{F} \triangleright_s \psi$ denote the field statistics (bosonic or fermionic) of $\phi$ and $\psi$ respectively.

For a field specification $\mathcal{F}$ and a list of field operators $L = [\phi, \phi_1, \dots, \phi_n]$, let $\phi_{\text{max}}$ be the chronologically latest operator in $L$ (as determined by `maxTimeField`) and let $L_{<k}$ be the sublist of operators appearing before the first occurrence of $\phi_{\text{max}}$ in $L$. The time-ordering sign of the list obtained by removing the first occurrence of $\phi_{\text{max}}$ from $L$ is given by: $$\text{timeOrderSign}(L \setminus \{\phi_{\text{max}}\}) = \text{timeOrderSign}(L) \cdot \mathcal{S}(\mathcal{F} \triangleright_s \phi_{\text{max}}, \mathcal{F} \triangleright_s L_{<k})$$ where $\mathcal{S}$ is the swap sign and $\mathcal{F} \triangleright_s \cdot$ denotes the field statistic (bosonic or fermionic) of an operator or a sequence of operators.

Given a list of field operators $[\phi_1, \phi_2, \dots, \phi_n]$ within a field specification $\mathcal{F}$, the function `timeOrderList` returns a new list containing the same operators sorted according to the time-ordering relation $\text{timeOrderRel}$. This results in a sequence where operators corresponding to later times (or outgoing asymptotic states) precede those corresponding to earlier times (or incoming asymptotic states). For example, a list containing operators at times $t=3, t=5, t=4$ would be reordered to $[t=5, t=4, t=3]$.

For any field operators $\phi, \psi \in \text{FieldOp}(\mathcal{F})$ in a field specification $\mathcal{F}$, if $\phi$ is chronologically later than or equal to $\psi$ (i.e., $\text{timeOrderRel}(\phi, \psi)$ holds), then the time-ordered list of the pair $[\phi, \psi]$ is equal to $[\phi, \psi]$.

For any two field operators $\phi, \psi \in \text{FieldOp}(\mathcal{F})$, if the time-ordering relation $\text{timeOrderRel}(\phi, \psi)$ does not hold (meaning $\phi$ is not chronologically later than or equal to $\psi$), then the time-ordered list of these operators, $\text{timeOrderList}([\phi, \psi])$, is equal to the swapped list $[\psi, \phi]$.

For any field specification $\mathcal{F}$, the time-ordered version of an empty list of field operators is itself an empty list. Mathematically, this is expressed as: $$\text{timeOrderList}([\,]) = [\,]$$

For a given field specification $\mathcal{F}$, let $\phi \in \text{FieldOp}(\mathcal{F})$ be a field operator and $\Phi_s$ be a list of field operators. The time-ordered version of the list $[\phi, \phi_1, \dots, \phi_n]$ is equal to the chronologically latest operator (as determined by $\text{maxTimeField}$) followed by the time-ordered list of the operators remaining after the first occurrence of that latest operator is removed (via $\text{eraseMaxTimeField}$). Mathematically, this is expressed as: $$\text{timeOrderList}(\phi :: \Phi_s) = \text{maxTimeField}(\phi, \Phi_s) :: \text{timeOrderList}(\text{eraseMaxTimeField}(\phi, \Phi_s))$$ where the chronological order is defined by the relation $\text{timeOrderRel}$, which treats outgoing asymptotic operators as $t = +\infty$, incoming asymptotic operators as $t = -\infty$, and position-space operators according to their time coordinate $x^0$.

For a given field specification $\mathcal{F}$, the relation $\text{crAnTimeOrderRel}(\varphi_0, \varphi_1)$ on creation and annihilation field operators $\varphi_0, \varphi_1 \in \mathcal{F}.\text{CrAnFieldOp}$ holds if $\varphi_0$ is chronologically "later" than or equal to $\varphi_1$. This is defined by applying the time-ordering relation $\mathcal{F}.\text{timeOrderRel}$ to the underlying field operators $\phi_0$ and $\phi_1$ of $\varphi_0$ and $\varphi_1$, respectively. Specifically, the relation is true if: - $\phi_0$ is an outgoing asymptotic field operator (representing $t \to \infty$). - $\phi_1$ is an incoming asymptotic field operator (representing $t \to -\infty$). - Both $\phi_0$ and $\phi_1$ are position-space field operators at spacetime points $x_0$ and $x_1$ such that the time components satisfy $x_0^0 \geq x_1^0$.

For a given field specification $\mathcal{F}$, the time-ordering relation $\text{crAnTimeOrderRel}(\varphi, \varphi')$ between two creation and annihilation operators $\varphi, \varphi' \in \mathcal{F}.\text{CrAnFieldOp}$ is decidable. This decidability is inherited from the decidability of the time-ordering relation on the underlying field operators, which ultimately relies on the decidability of the $\leq$ relation between the time coordinates in $\mathbb{R}$. Note that while formally decidable, this is not strictly computable due to the non-computable nature of the $\leq$ relation on real numbers.

For a given field specification $\mathcal{F}$, the time-ordering relation $\text{crAnTimeOrderRel}$ on the set of creation and annihilation field operators $\mathcal{F}.\text{CrAnFieldOp}$ is total. That is, for any two operators $\varphi_0, \varphi_1 \in \mathcal{F}.\text{CrAnFieldOp}$, either $\varphi_0$ is chronologically later than or equal to $\varphi_1$ (such that $\text{crAnTimeOrderRel}(\varphi_0, \varphi_1)$ holds) or $\varphi_1$ is chronologically later than or equal to $\varphi_0$ (such that $\text{crAnTimeOrderRel}(\varphi_1, \varphi_0)$ holds).

For a given field specification $\mathcal{F}$, the time-ordering relation $\text{crAnTimeOrderRel}$ on the set of creation and annihilation field operators $\mathcal{F}.\text{CrAnFieldOp}$ is transitive. That is, for any $\varphi_1, \varphi_2, \varphi_3 \in \mathcal{F}.\text{CrAnFieldOp}$, if $\text{crAnTimeOrderRel}(\varphi_1, \varphi_2)$ and $\text{crAnTimeOrderRel}(\varphi_2, \varphi_3)$ hold, then $\text{crAnTimeOrderRel}(\varphi_1, \varphi_3)$ also holds.

For a given field specification $\mathcal{F}$, the time-ordering relation $\text{crAnTimeOrderRel}$ on the set of creation and annihilation field operators $\mathcal{F}.\text{CrAnFieldOp}$ is reflexive. That is, for any operator $\varphi \in \mathcal{F}.\text{CrAnFieldOp}$, the relation $\text{crAnTimeOrderRel}(\varphi, \varphi)$ holds.

For a given field specification $\mathcal{F}$ and a list of creation and annihilation field operators $\varphi_s = [\varphi_1, \varphi_2, \dots, \varphi_n]$ where each $\varphi_i \in \mathcal{F}.\text{CrAnFieldOp}$, the function returns the sign (as a complex number) associated with the permutation required to arrange the operators in chronological order. Specifically, the sign is calculated as $(-1)^N$, where $N$ is the number of exchanges between two fermionic operators performed by an insertion sort algorithm to satisfy the time-ordering relation $\mathcal{F}.\text{crAnTimeOrderRel}$. The statistics (bosonic or fermionic) of each operator are determined by $\mathcal{F}.\text{crAnStatistics}$.

For any field specification $\mathcal{F}$, the time-ordering sign of an empty list of creation and annihilation field operators is $1$.

For any field specification $\mathcal{F}$ and any creation or annihilation operators $\varphi, \psi \in \mathcal{F}.\text{CrAnFieldOp}$, if $\varphi$ and $\psi$ satisfy the time-ordering relation $\text{crAnTimeOrderRel}(\varphi, \psi)$ (meaning $\varphi$ is chronologically later than or equal to $\psi$), then the time-ordering sign of the sequence $[\varphi, \psi]$ is $1$.

For a given field specification $\mathcal{F}$ and two creation or annihilation field operators $\varphi, \psi \in \mathcal{F}.\text{CrAnFieldOp}$, if $\varphi$ is not chronologically later than or equal to $\psi$ (i.e., $\neg \text{crAnTimeOrderRel}(\varphi, \psi)$), then the time-ordering sign of the sequence $[\varphi, \psi]$ is equal to the statistical exchange factor $\mathcal{S}(\text{stat}(\varphi), \text{stat}(\psi))$, where $\text{stat}(\cdot)$ denotes the field statistic (bosonic or fermionic) of the operator.

Let $\mathcal{F}$ be a field specification. For any two creation or annihilation operators $\varphi, \psi \in \mathcal{F}.\text{CrAnFieldOp}$ that are chronologically simultaneous—meaning they satisfy the time-ordering relation in both directions, $\text{crAnTimeOrderRel}(\varphi, \psi)$ and $\text{crAnTimeOrderRel}(\psi, \varphi)$—the time-ordering sign of a list of operators is invariant under the swapping of $\varphi$ and $\psi$. Specifically, for any lists of operators $\varphi_s$ and $\varphi_s'$, it holds that: $$\text{crAnTimeOrderSign}(\varphi_s \mathbin{+\!+} [\varphi, \psi] \mathbin{+\!+} \varphi_s') = \text{crAnTimeOrderSign}(\varphi_s \mathbin{+\!+} [\psi, \varphi] \mathbin{+\!+} \varphi_s')$$ where $\mathbin{+\!+}$ denotes the concatenation of lists.

Given a field specification $\mathcal{F}$ and a list of creation and annihilation field operators $\varphi_s$, the function $\mathcal{F}.\text{crAnTimeOrderList}(\varphi_s)$ returns a permutation of $\varphi_s$ that is chronologically ordered. The sorting is performed using the insertion sort algorithm based on the relation $\text{crAnTimeOrderRel}$. The resulting list is arranged such that for any elements in the list, operators with later time coordinates (or outgoing asymptotic fields) appear before operators with earlier time coordinates (or incoming asymptotic fields).

For a given field specification $\mathcal{F}$, the time-ordering of an empty list of creation and annihilation field operators is an empty list. That is, $\text{crAnTimeOrderList}([]) = []$.

For any creation and annihilation field operators $\varphi, \psi \in \mathcal{F}.\text{CrAnFieldOp}$, if $\varphi$ is chronologically later than or equal to $\psi$ (meaning the relation $\text{crAnTimeOrderRel}(\varphi, \psi)$ holds), then the time-ordered list of these two operators is $\text{crAnTimeOrderList}([\varphi, \psi]) = [\varphi, \psi]$.

For a given field specification $\mathcal{F}$, let $\varphi$ and $\psi$ be creation and annihilation field operators in $\mathcal{F}.\text{CrAnFieldOp}$. If $\varphi$ is not chronologically later than or equal to $\psi$ according to the relation $\text{crAnTimeOrderRel}(\varphi, \psi)$, then the time-ordered list of these two operators, $\text{crAnTimeOrderList}([\varphi, \psi])$, is equal to the list $[\psi, \varphi]$.

For a given field specification $\mathcal{F}$, let $\phi, \psi \in \mathcal{F}.\text{CrAnFieldOp}$ be creation and annihilation field operators such that $\text{crAnTimeOrderRel}(\phi, \psi)$ and $\text{crAnTimeOrderRel}(\psi, \phi)$ both hold (meaning $\phi$ and $\psi$ are chronologically simultaneous). For any list of operators $\varphi_s$, the result of sequentially inserting $\psi$ then $\phi$ into $\varphi_s$ using the time-ordering relation $\text{crAnTimeOrderRel}$ is: $\text{orderedInsert}(\phi, \text{orderedInsert}(\psi, \varphi_s)) = L_{<} ++ [\phi, \psi] ++ L_{\geq}$ where $L_{<}$ is the prefix of $\varphi_s$ containing elements $b$ for which $\text{crAnTimeOrderRel}(\psi, b)$ is false, $L_{\geq}$ is the remaining suffix of $\varphi_s$, and $++$ denotes list concatenation.

Let $\mathcal{F}$ be a field specification. Let $\varphi, \psi, \varphi' \in \mathcal{F}.\text{CrAnFieldOp}$ be creation or annihilation field operators such that $\varphi$ and $\psi$ are simultaneous under the time-ordering relation, i.e., both $\text{crAnTimeOrderRel}(\varphi, \psi)$ and $\text{crAnTimeOrderRel}(\psi, \varphi)$ hold. For any lists of operators $\Phi_s$ and $\Phi_s'$, there exist lists $l_1$ and $l_2$ such that: 1. The result of performing an ordered insertion of $\varphi'$ into the concatenated list $\Phi_s \mathbin{+\!+} [\varphi, \psi] \mathbin{+\!+} \Phi_s'$ according to $\text{crAnTimeOrderRel}$ is $l_1 \mathbin{+\!+} [\varphi, \psi] \mathbin{+\!+} l_2$. 2. The result of performing an ordered insertion of $\varphi'$ into the concatenated list $\Phi_s \mathbin{+\!+} [\psi, \varphi] \mathbin{+\!+} \Phi_s'$ according to $\text{crAnTimeOrderRel}$ is $l_1 \mathbin{+\!+} [\psi, \varphi] \mathbin{+\!+} l_2$.

Let $\mathcal{F}$ be a field specification. Suppose $\varphi, \psi \in \mathcal{F}.\text{CrAnFieldOp}$ are creation or annihilation field operators that are simultaneous according to the time-ordering relation, meaning both $\text{crAnTimeOrderRel}(\varphi, \psi)$ and $\text{crAnTimeOrderRel}(\psi, \varphi)$ hold. For any lists of operators $\Phi_s$ and $\Phi_s'$, there exist lists $l_1$ and $l_2$ such that: 1. The time-ordered version of the list $\Phi_s \mathbin{+\!+} [\varphi, \psi] \mathbin{+\!+} \Phi_s'$, denoted as $\text{crAnTimeOrderList}(\Phi_s \mathbin{+\!+} [\varphi, \psi] \mathbin{+\!+} \Phi_s')$, is equal to $l_1 \mathbin{+\!+} [\varphi, \psi] \mathbin{+\!+} l_2$. 2. The time-ordered version of the list $\Phi_s \mathbin{+\!+} [\psi, \varphi] \mathbin{+\!+} \Phi_s'$, denoted as $\text{crAnTimeOrderList}(\Phi_s \mathbin{+\!+} [\psi, \varphi] \mathbin{+\!+} \Phi_s')$, is equal to $l_1 \mathbin{+\!+} [\psi, \varphi] \mathbin{+\!+} l_2$. This indicates that while the time-ordering function moves simultaneous operators to their correct collective position in the list, it preserves the relative order they had in the original input list.

Let $\mathcal{F}$ be a field specification. Suppose $\phi \in \mathcal{F}.\text{FieldOp}$ is a field operator and $\psi \in \mathcal{F}.\text{CrAnFieldOp}$ is a creation or annihilation operator such that its underlying field operator is $\phi$ (i.e., $\text{crAnFieldOpToFieldOp}(\psi) = \phi$). For any list of field operators $\varphi_s$ and any section of creation and annihilation operators $\psi_s \in \text{CrAnSection}(\varphi_s)$, the Koszul sign incurred by inserting $\psi$ into the list $\psi_s$ according to the time-ordering relation $\text{crAnTimeOrderRel}$ and field statistics $\text{crAnStatistics}$ is equal to the Koszul sign incurred by inserting $\phi$ into the list $\varphi_s$ according to $\text{timeOrderRel}$ and $\text{fieldOpStatistic}$.

For a given field specification $\mathcal{F}$, let $\varphi_s = [\phi_1, \phi_2, \dots, \phi_n]$ be a list of field operators in $\mathcal{F}.\text{FieldOp}$. Let $\psi_s$ be a creation and annihilation section for $\varphi_s$, which is a list of operators $[\psi_1, \psi_2, \dots, \psi_n]$ where each $\psi_i \in \mathcal{F}.\text{CrAnFieldOp}$ is a creation or annihilation component of the corresponding field operator $\phi_i$. The time-ordering sign associated with the list of creation and annihilation operators $\psi_s$ is equal to the time-ordering sign of the underlying list of field operators $\varphi_s$: $$\text{crAnTimeOrderSign}(\psi_s) = \text{timeOrderSign}(\varphi_s)$$ where the signs are determined by the Koszul convention for permutations required to achieve chronological order.

Let $\mathcal{F}$ be a field specification. Let $\phi \in \mathcal{F}.\text{FieldOp}$ be a field operator and $\psi \in \mathcal{F}.\text{CrAnFieldOp}$ be a creation or annihilation operator component such that the underlying field operator of $\psi$ is $\phi$. For any list of field operators $\varphi_s$ and any creation and annihilation section $\psi_s$ corresponding to $\varphi_s$ (meaning $\psi_s$ is a list of creation/annihilation components whose underlying operators are $\varphi_s$), the following identity holds: $$\text{map}(\text{proj}, \text{orderedInsert}(\leq_{\text{crAn}}, \psi, \text{list}(\psi_s))) = \text{orderedInsert}(\leq_{\text{field}}, \phi, \varphi_s)$$ where $\text{proj}$ is the projection function $\mathcal{F}.\text{crAnFieldOpToFieldOp}$, $\text{orderedInsert}$ is the function that inserts an element into a list at the first position that satisfies the given ordering relation, $\leq_{\text{crAn}}$ is the time-ordering relation $\mathcal{F}.\text{crAnTimeOrderRel}$, and $\leq_{\text{field}}$ is the time-ordering relation $\mathcal{F}.\text{timeOrderRel}$.

Let $\mathcal{F}$ be a field specification. For any list of field operators $\varphi_s$ and any creation and annihilation section $\psi_s$ corresponding to $\varphi_s$ (meaning $\psi_s$ is a list of creation/annihilation components such that projecting each component yields the operators in $\varphi_s$), the following identity holds: $$\text{map}(\text{proj}, \text{crAnTimeOrderList}(\psi_s)) = \text{timeOrderList}(\varphi_s)$$ where $\text{proj}$ is the projection function $\mathcal{F}.\text{crAnFieldOpToFieldOp}$ that maps a creation or annihilation operator component to its underlying field operator, $\text{crAnTimeOrderList}$ is the chronological ordering of those components, and $\text{timeOrderList}$ is the chronological ordering of field operators.

Given a field specification $\mathcal{F}$ and a list of field operators $\varphi_s = [\phi_1, \dots, \phi_n]$, let $\psi_s \in \text{CrAnSection}(\varphi_s)$ be a list of creation and annihilation operator components such that each component projects to the corresponding operator in $\varphi_s$. The function `crAnSectionTimeOrder` maps $\psi_s$ to a new section in $\text{CrAnSection}(\text{timeOrderList}(\varphi_s))$. This is achieved by chronologically reordering the operators in $\psi_s$ according to the relation `crAnTimeOrderRel`, such that the resulting list of components corresponds to the time-ordered list of the original field operators.

Let $\mathcal{F}$ be a field specification. Let $\psi, \psi' \in \mathcal{F}.\text{CrAnFieldOp}$ be two creation or annihilation field operators that share the same underlying field operator, such that $\text{crAnFieldOpToFieldOp}(\psi) = \text{crAnFieldOpToFieldOp}(\psi')$. For any list of field operators $\varphi_s$ and any sections $\psi_s, \psi'_s$ belonging to $\text{CrAnSection}(\varphi_s)$, if the time-ordered insertion of $\psi$ into the list $\psi_s$ is equal to the time-ordered insertion of $\psi'$ into the list $\psi'_s$, i.e., $$\text{orderedInsert}(\text{crAnTimeOrderRel}, \psi, \psi_s) = \text{orderedInsert}(\text{crAnTimeOrderRel}, \psi', \psi'_s)$$ then it must be that $\psi = \psi'$ and $\psi_s = \psi'_s$.

Let $\mathcal{F}$ be a field specification. For any list of field operators $\varphi_s$, the function $\text{crAnSectionTimeOrder}$, which maps a section of creation and annihilation operators $\psi_s \in \text{CrAnSection}(\varphi_s)$ to its chronologically reordered counterpart in $\text{CrAnSection}(\text{timeOrderList}(\varphi_s))$, is injective.

Let $\mathcal{F}$ be a field specification and $\varphi_s$ be a list of field operators. The function $\text{crAnSectionTimeOrder}$, which maps a section of creation and annihilation operators $\psi_s \in \text{CrAnSection}(\varphi_s)$ to its chronologically reordered counterpart in $\text{CrAnSection}(\text{timeOrderList}(\varphi_s))$, is bijective.

Let $\mathcal{F}$ be a field specification and $\varphi_s$ be a list of field operators. Let $M$ be an additive commutative monoid and $f : \text{CrAnSection}(\text{timeOrderList}(\varphi_s)) \to M$ be a function. Then the sum over all creation and annihilation sections of the time-ordered list $\text{timeOrderList}(\varphi_s)$ is equal to the sum over all sections of the original list $\varphi_s$ when composed with the time-ordering map $\text{crAnSectionTimeOrder}$: \[ \sum_{s \in \text{CrAnSection}(\text{timeOrderList}(\varphi_s))} f(s) = \sum_{s \in \text{CrAnSection}(\varphi_s)} f(\text{crAnSectionTimeOrder}(\varphi_s, s)) \] Here, $\text{CrAnSection}(\varphi_s)$ denotes the finite set of possible creation and annihilation operator assignments for the list $\varphi_s$, and $\text{crAnSectionTimeOrder}$ is the bijection that reorders these assignments according to the chronological order of the field operators.

For a given field specification $\mathcal{F}$, the relation $\text{normTimeOrderRel}(a, b)$ is defined on creation and annihilation field operators $a, b \in \mathcal{F}.\text{CrAnFieldOp}$. The relation holds if $a$ is chronologically later than or equal to $b$ according to the time-ordering relation $\text{crAnTimeOrderRel}$ (denoted here as $\succeq_T$), with the additional condition that if $a$ and $b$ occur at the same time, $a$ must precede $b$ according to the normal ordering relation $\text{normalOrderRel}$ (denoted here as $\le_{NO}$). Formally, the relation is: \[ a \succeq_T b \land (b \succeq_T a \implies a \le_{NO} b) \] This ensures that the time-ordering of operators is uniquely determined even for operators sharing the same time coordinate by falling back to their normal-ordered configuration.

For a given field specification $\mathcal{F}$, the relation $\text{normTimeOrderRel}(\varphi, \varphi')$ between two creation and annihilation operators $\varphi, \varphi' \in \mathcal{F}.\text{CrAnFieldOp}$ is decidable. This relation combines chronological ordering and normal ordering, defined such that $\text{normTimeOrderRel}(a, b)$ holds if $a$ is chronologically later than or equal to $b$ ($a \succeq_T b$), and if they occur at the same time ($b \succeq_T a$), then $a$ must precede $b$ in normal order ($a \le_{NO} b$). The decidability of this relation is inherited from the decidability of the underlying time-ordering and normal-ordering relations. Consistent with the treatment of real numbers in Lean, this property is formally decidable but non-computable due to the dependence on the decidability of the $\leq$ relation on $\mathbb{R}$.

For a given field specification $\mathcal{F}$, the norm-time ordering relation $\text{normTimeOrderRel}$ on the set of creation and annihilation field operators $\mathcal{F}.\text{CrAnFieldOp}$ is total. That is, for any two operators $a, b \in \mathcal{F}.\text{CrAnFieldOp}$, it holds that $\text{normTimeOrderRel}(a, b)$ or $\text{normTimeOrderRel}(b, a)$. The relation $\text{normTimeOrderRel}(a, b)$ is defined as $a \succeq_T b \land (b \succeq_T a \implies a \le_{NO} b)$, where $\succeq_T$ denotes the chronological time-ordering relation and $\le_{NO}$ denotes the normal ordering relation.

For a given field specification $\mathcal{F}$, the norm-time ordering relation $\text{normTimeOrderRel}$ on the set of creation and annihilation field operators $\mathcal{F}.\text{CrAnFieldOp}$ is transitive. Specifically, for any operators $a, b, c \in \mathcal{F}.\text{CrAnFieldOp}$, if $\text{normTimeOrderRel}(a, b)$ and $\text{normTimeOrderRel}(b, c)$ both hold, then $\text{normTimeOrderRel}(a, c)$ also holds. The relation $\text{normTimeOrderRel}(x, y)$ is defined such that $x$ is chronologically later than or equal to $y$, and if they occur at the same time, $x$ precedes $y$ according to the normal-ordering relation.

For a given field specification $\mathcal{F}$, let $\varphi_s = [\varphi_1, \varphi_2, \dots, \varphi_n]$ be a list of creation and annihilation operators in $\mathcal{F}.\text{CrAnFieldOp}$. The function returns the sign in $\mathbb{C}$ associated with permuting this list into its "normal-time ordered" configuration. This configuration is determined by the relation $\text{normTimeOrderRel}$, which sorts operators such that those at later times appear to the left, using a predefined normal-ordering convention to resolve ties for operators at the same time. The resulting sign is determined by the Koszul sign convention: a factor of $-1$ is introduced for every swap involving two fermionic operators (as defined by $\mathcal{F}.\text{crAnStatistics}$), while bosonic operators commute without a sign change.