10 Haag Kastler Axioms Blueprint

With all the original Haag Kastler Axioms unpacked, we are now in a position to “sharpen” their formulation.

However, before even stating the “sharpened” axioms, the first thing we need to do is to define a number of terms to a level amenable to auto-formalization and also prove a number of theorems.

10.1 GNS Construction Details

Here we will state and prove the GNS Construction Theorem, which we make use of in the axioms we present later.

We generally follow the clear, straightforward presentation in Entanglement in Algebraic Quantum Field Theories.

10.1.1 GNS Construction Theorem

In this section we will state the GNS Construction Theorem, which we prove in subsequent sections.

Before stating the theorem we’ll need to introduce terminology that appears in the theorem’s statement. We begin with the definition of "state" and some closely associated terms.

Definition 13 State

✓

Let $\mathfrak {U}$ be an abstract C*-algebra. A state is an element $\omega $ of the dual space $\mathfrak {U}^*$ that is

Positive - for any $a \in \mathfrak {U}$ we have $0 \le \omega (a^*a)$ and
Normalized - the operator norm satisfies $\| \omega \| =1$.

Furthermore, a state $\omega $ is said to be faithful if for any non-zero $a$ in $\mathfrak {U}$, it follows that $0 {\lt} \omega (a^*a)$.

We will also have need of the term "cyclic vector".

Definition 14 Cyclic Vector

✓

Let $\mathcal{A}$ be an algebra represented by the bounded operators $\pi (\mathcal{A})$ on the Hilbert space $\mathcal{H}$. A vector $\Omega $ in $\mathcal{H}$ is said to be a cyclic vector if the set

\begin{align} \{ A\Omega : A \in \pi (\mathcal{A}) \} \end{align}

is dense in $\mathcal{H}$.

With this terminology we are then able to state the GNS Construction Theorem.

Theorem 15 GNS Construction Theorem

✓

Let $\omega $ be a state over a unital C*-algebra $\mathfrak {U}$. One can then construct a Hilbert space $\mathcal{H}_\omega $ and *-representation $\pi _\omega $ of $\mathfrak {U}$ by bounded operators on $\mathcal{H}_\omega $ such that

\begin{align} \pi _\omega (a^*) = \pi _\omega (a)^\dagger . \end{align}

As $\mathfrak {U}$ is unital, there exists a cyclic vector $\Omega $ in $\mathcal{H}_\omega $ for the representation $\pi _\omega $ such that

\begin{align} \omega (a) = \left\langle \Omega , \pi _\omega (a)\Omega \right\rangle _{\mathcal{H}_\omega }. \end{align}

The triple $(\mathcal{H}_\omega , \pi _\omega , \Omega )$ is called the GNS triple associated to $(\mathfrak {U}, \omega )$ or the cyclic representation of $(\mathfrak {U}, \omega )$. Furthermore, if $\omega $ is a faithful state, then the *-representation $\pi _\omega $ is faithful. In addition the GNS triple associated to $(\mathfrak {U}, \omega )$ is unique up to unitary equivalence.

With the GNS Construction Theorem stated, we can now commence with its proof.

This proof has five parts: (1) the construction of the GNS Hilbert space $\mathcal{H}_\omega $, (2) the construction of the *-representation $\pi _\omega $, (3) the construction of the cyclic vector $\Omega $ in $\mathcal{H}_\omega $, (4) the proof that the *-representation $\pi _\omega $ is faithful, and (5) the proof of uniqueness up to unitary equivalence. Each part corresponds to a subsequent subsection.

Construction of the GNS Hilbert Space

We’ll construct the GNS Hilbert space $\mathcal{H}_\omega $ from the C*-algebra $\mathfrak {U}$ itself, modifying $\mathfrak {U}$ as needed to obtain the desired $\mathcal{H}_\omega $.

Let’s start by attempting to place an inner product on $\mathfrak {U}$. Naively one might hope the following defines an inner product

\begin{align} \left\langle a, b \right\rangle \equiv \omega (a^*b) \end{align}

on $\mathfrak {U}$. Unfortunately it doesn’t. Let’s examine why this fails.

Consider the set

\begin{align} \mathcal{N} \equiv \{ n \in \mathfrak {U} : \omega (n^*n) = 0 \} . \end{align}

Generically $\omega $ isn’t faithful. Thus in $\mathcal{N}$ there exist non-zero $n$. For such $n$ one has

\begin{align} \left\langle n, n \right\rangle \equiv \omega (n^*n) = 0. \end{align}

Hence, there are non-zero $n$ in $\mathfrak {U}$ such that $\left\langle n, n \right\rangle = 0$. The existence of such $n$ proves that our naive inner product on $\mathfrak {U}$

\begin{align} \left\langle a, b \right\rangle \equiv \omega (a^*b) \end{align}

actually isn’t an inner product. However, the form $\mathcal{N}$ takes gives us a hint as to how to repair this naive inner product.

In particular, if we quotient $\mathfrak {U}$ by $\mathcal{N}$ we may rid ourselves of the problem we encountered above and hopefully be able to construct an inner product on $\mathfrak {U} / \mathcal{N}$ and its completion. We’ll see this plan actually works.

However, before being able to see this plan through we’ll need to take a quick detour and prove a few needed results.

The most famous of these results is the Cauchy-Schwarz Inequality

Lemma 16 Cauchy-Schwarz Inequality

Let $\mathcal{A}$ be a *-algebra and $\omega $ a positive element of the dual space $\mathcal{A}^*$, i.e. $\omega $ is an element of the dual space $\mathcal{A}^*$ such that for any $a \in \mathcal{A}$ one has $0 \le \omega (a^*a)$. Then

\begin{align} \omega (a^*b) & = \overline{\omega (b^*a)} \\ |\omega (a^*b)|^2 & \le \omega (a^*a) \omega (b^*b) \end{align}

for all $a$ and $b$ in $\mathcal{A}$.

Proof ▶

Positivity of $\omega $ implies that for any $a$ and $b$ in $\mathcal{A}$ and $\lambda \in \mathbb {C}$ one has

\begin{align} 0 \le \omega \left((\lambda a + b)^*(\lambda a + b)\right). \end{align}

As $\omega $ is an element of the dual space $\mathcal{A}^*$ and thus linear, this implies

\begin{align} 0 \le |\lambda |^2\omega (a^*a) + \overline{\lambda }\omega (a^*b) + \lambda \omega (b^*a) + \omega (b^*b). \end{align}

This inequality then implies both desired results,

\begin{align} \omega (a^*b) & = \overline{\omega (b^*a)} \\ |\omega (a^*b)|^2 & \le \omega (a^*a) \omega (b^*b). \end{align}

We will prove these one-by-one. Let us first prove this inequality implies $\omega (a^*b) = \overline{\omega (b^*a)}$.

Notice that the inequality is between two real numbers, $0$ and the right-hand side. As $\omega $ is positive, the first and last summands on the right-hand side are obviously real. This then implies

\begin{align} \overline{\lambda }\omega (a^*b) + \lambda \omega (b^*a) \in \mathbb {R}. \end{align}

As $\lambda $ is arbitrary, we are free to choose it to be real, which implies the imaginary parts of $\omega (a^*b)$ and $\omega (b^*a)$ are equal but have the opposite signs.

Similarly, we are free to choose $\lambda $ to be imaginary, which implies that the real parts of $\omega (a^*b)$ and $\omega (b^*a)$ are equal. Together these facts imply the first result

\begin{align} \omega (a^*b) = \overline{\omega (b^*a)}. \end{align}

Let us next prove that our inequality

\begin{align} 0 \le |\lambda |^2\omega (a^*a) + \overline{\lambda }\omega (a^*b) + \lambda \omega (b^*a) + \omega (b^*b) \end{align}

implies $\lvert \omega (a^*b) \rvert ^2 \le \omega (a^*a) \omega (b^*b)$.

Again, as $\lambda $ is arbitrary, we are free to choose it to extremize the right-hand side of the inequality. Extremizing the right-hand of this inequality with respect to $\overline{\lambda }$ and assuming $\omega (a^*a) \ne 0$ one finds at the extrema

\begin{align} \lambda = - \frac{\omega (a^*b)}{\omega (a^*a)}. \end{align}

Substituting this into the inequality, multiplying by $\omega (a^*a)$ while using the fact that $\omega $ is positive, and using $\omega (a^*b) = \overline{\omega (b^*a)}$, then one obtains

\begin{align} 0 \le \lvert \omega (a^*b) \rvert ^2 - \lvert \omega (a^*b) \rvert ^2 - \lvert \omega (a^*b) \rvert ^2 + \omega (a^*a) \omega (b^*b) \end{align}

which implies

\begin{align} \lvert \omega (a^*b) \rvert ^2 \le \omega (a^*a) \omega (b^*b), \end{align}

the second desired result under the assumption that $\omega (a^*a) \ne 0$.

If we now allow for the case $\omega (a^*a) = 0$, our inequality reduces to

\begin{align} 0 \le \overline{\lambda }\omega (a^*b) + \lambda \omega (b^*a) + \omega (b^*b). \end{align}

Our previous result implies $\omega (b^*a) = \overline{\omega (a^*b)}$. Hence, this inequality takes the form

\begin{align} 0 \le \overline{\lambda }\omega (a^*b) + \lambda \overline{\omega (a^*b)} + \omega (b^*b) = 2\text{Re}\left(\overline{\lambda } \omega (a^*b)\right) + \omega (b^*b). \end{align}

Now as $\lambda $ is arbitrary we are free to select it as follows

\begin{align} \overline{\lambda } = -r \overline{\omega (a^*b)} \end{align}

where $0 {\lt} r$ is an arbitrary positive real number. Then the previous inequality takes the form

\begin{align} 0 & \le 2\text{Re}\left(\overline{\lambda } \omega (a^*b)\right) + \omega (b^*b) \\ & = -2r \lvert \omega (a^*b) \rvert ^2 + \omega (b^*b). \end{align}

Now if we assume for the moment that $0 {\lt} \lvert \omega (a^*b) \rvert $, then we can always select $0 {\lt} r$ large enough such that this inequality is violated, the $-2r \lvert \omega (a^*b) \rvert ^2$ term dominating the $\omega (b^*b)$ term. Hence, it must be the case that $\lvert \omega (a^*b) \rvert = 0$.

Now we have $\omega (a^*a) = 0$ and $\lvert \omega (a^*b) \rvert = 0$. Hence, the desired inequality

\begin{align} \lvert \omega (a^*b) \rvert ^2 \le \omega (a^*a) \omega (b^*b), \end{align}

follows trivially, completing our proof.

The next result we need to prove is:

Lemma 17

Let $\omega $ be a state over a unital C*-algebra $\mathfrak {U}$. Then the set $\mathcal{N}_1$ defined by

\begin{align} \mathcal{N}_1 \equiv \{ n \in \mathfrak {U} : \omega (b^*n) = 0 \; \; \forall \, b \in \mathfrak {U} \} \end{align}

is equivalent to the set $\mathcal{N}$ defined by

\begin{align} \mathcal{N} \equiv \{ n \in \mathfrak {U} : \omega (n^*n) = 0 \} . \end{align}

Proof ▶

We will first prove that $\mathcal{N} \subseteq \mathcal{N}_1$. Then we will prove $\mathcal{N}_1 \subseteq \mathcal{N}$. Together these imply $\mathcal{N} = \mathcal{N}_1$, the final desired result.

Let us begin by proving $\mathcal{N} \subseteq \mathcal{N}_1$.

$\mathfrak {U}$ is a C*-algebra and thus a *-algebra. In addition $\omega $ is a state and thus a positive element of the dual space $\mathfrak {U}^*$. Thus, for arbitrary $b$ and $n$ in $\mathfrak {U}$ we can apply the Cauchy-Schwarz inequality to obtain

\begin{align} \lvert \omega (b^*n) \rvert ^2 \le \omega (b^*b) \omega (n^*n). \end{align}

Thus if $n$ is in $\mathcal{N}$, and thus satisfies $\omega (n^*n) = 0$, then this inequality implies $\omega (b^*n) = 0$ for all $b$ in $\mathfrak {U}$. This then implies $n$ is in $\mathcal{N}_1$. As $n$ was an arbitrary element of $\mathcal{N}$, this in turn implies that $\mathcal{N} \subseteq \mathcal{N}_1$, the first desired result.

Next let us prove that $\mathcal{N}_1 \subseteq \mathcal{N}$.

Consider an arbitrary $n_1$ in $\mathcal{N}_1$. By definition $\omega (b^*n_1) = 0$ for any $b$ in $\mathfrak {U}$. In particular we can select $b=n_1$. Doing so we have $\omega (n_1^*n_1) = 0$. This then implies $n_1$ is in $\mathcal{N}$. As $n_1$ was an arbitrary element of $\mathcal{N}_1$ this further implies $\mathcal{N}_1 \subseteq \mathcal{N}$, the second desired result.

We have thus proven $\mathcal{N} \subseteq \mathcal{N}_1$ and $\mathcal{N}_1 \subseteq \mathcal{N}$ which together imply $\mathcal{N} = \mathcal{N}_1$, the final desired result.

Next we will prove $\mathcal{N}$ is a closed, linear subspace of $\mathfrak {U}$. Establishing this will allow us to take the quotient of $\mathfrak {U}$ by $\mathcal{N}$.

Lemma 18

Let $\omega $ be a state over a unital C*-algebra $\mathfrak {U}$. Then the set $\mathcal{N}$ defined by

\begin{align} \mathcal{N} \equiv \{ n \in \mathfrak {U} : \omega (n^*n) = 0 \} . \end{align}

is a closed, linear subspace of $\mathfrak {U}$.

Proof ▶

First let us prove that $\mathcal{N}$ is a linear subspace of $\mathfrak {U}$.

Consider arbitrary $n,m \in \mathcal{N}$ and arbitrary $\lambda , \mu \in \mathbb {C}$. As proven above $\mathcal{N} = \mathcal{N}_1$, thus for arbitrary $b \in \mathfrak {U}$, one has

\begin{align} \omega (b^*n) & = 0 \\ \omega (b^*m) & = 0. \end{align}

Hence, the linearity of $\omega $ then implies

\begin{align} \omega (b^*(\lambda n + \mu m)) = \lambda \omega (b^*n) + \mu \omega (b^*m) = 0. \end{align}

As $b \in \mathfrak {U}$ was arbitrary, this implies that $(\lambda n + \mu m) \in \mathcal{N}_1$. As we previously proved $\mathcal{N} = \mathcal{N}_1$, this in turn implies $(\lambda n + \mu m) \in \mathcal{N}$. Hence $\mathcal{N}$ is a linear subspace of $\mathfrak {U}$, the first desired result.

Next let us prove that $\mathcal{N}$ is a closed subspace of $\mathfrak {U}$.

First, let us note that as $\omega $ is a state, it is by definition a linear, normalized operator on $\mathfrak {U}$. Hence, it is a linear, bounded operator on $\mathfrak {U}$, a normed space. Thus, as a result of the standard theorem (Theorem B.2.4 of Entanglement in Algebraic Quantum Field Theories)

Theorem. Let $X$ and $Y$ be normed spaces and $T: \mathcal{D}(T) \rightarrow Y$ be a linear operator where $\mathcal{D}(T) \subseteq X$. Then $T$ is continuous if and only if it is bounded.

along with the fact that $\mathbb {C}$ is a normed space, it follows that $\omega $ is continuous.

With the continuity of $\omega $ in hand, consider a sequence $(n_i)_{i \in \mathbb {N}}$ in $\mathcal{N}$ that converges to $n$ in $\mathfrak {U}$. As $\omega $ is continuous, for any $b$ in $\mathfrak {U}$ one has

\begin{align} \omega \left(b^*n\right) = \omega \left(b^*(\lim \limits _{i \rightarrow \infty } n_i)\right) = \lim \limits _{i \rightarrow \infty } \omega (b^*n_i) = 0, \end{align}

where the final equality follows from our previous result $\mathcal{N} = \mathcal{N}_1$. This proves that $n$ is an element of $\mathcal{N}_1$ and thus, as a consequence of our previous result $\mathcal{N}_1 = \mathcal{N}$, that $n$ is an element of $\mathcal{N}$. This establishes that $\mathcal{N}$ is closed, proving the second and final desired result, $\mathcal{N}$ is a closed subspace of $\mathfrak {U}$.

As we have established that $\mathcal{N}$ is a closed, linear subspace of $\mathfrak {U}$, we can now take the quotient of $\mathfrak {U}$ by $\mathcal{N}$. Elements of the quotient $\mathfrak {U} / \mathcal{N}$ are equivalence classes of the form

\begin{align} [a] \equiv \{ a + n : n \in \mathcal{N} \} \end{align}

with the zero vector in $\mathfrak {U} / \mathcal{N}$ given by

\begin{align} [0] \equiv \{ n : n \in \mathcal{N} \} . \end{align}

On $\mathfrak {U} / \mathcal{N}$ we can introduce an inner product

\begin{align} \left\langle [a], [b]\right\rangle \equiv \omega (a^*b) \end{align}

motivated by our naive attempt at placing an inner product on $\mathfrak {U}$. This inner product is well-defined on $\mathfrak {U} / \mathcal{N}$ as one can see from its invariance under $a \rightarrow a + n$ where $n$ is in $\mathcal{N}$,

\begin{align} \omega ((a + n)^*b) = \omega (a^*b) + \omega (n^*b) = \omega (a^*b) + \overline{\omega (b^*n)} = \omega (a^*b). \end{align}

In this the first equality follows from $\omega $ being linear, the second from our previous result $\omega (n^*b) = \overline{\omega (b^*n)}$, and the final from our previous result $\mathcal{N} = \mathcal{N}_1$. A similar argument using $\mathcal{N} = \mathcal{N}_1$ yields invariance under $b \rightarrow b + n$ too.

Furthermore, the inner product

\begin{align} \left\langle [a], [b]\right\rangle \equiv \omega (a^*b) \end{align}

on $\mathfrak {U} / \mathcal{N}$ doesn’t suffer from the same problem that our naive inner product on $\mathfrak {U}$ did. In particular, one can easily prove

\begin{align} \left\langle [a], [a]\right\rangle = 0 \end{align}

if and only if $[a] = [0]$. This is essentially by construction.

The final step in going from $\mathfrak {U} / \mathcal{N}$ to the Hilbert space $\mathcal{H}_\omega $ consists of completing $\mathfrak {U} / \mathcal{N}$ in the norm defined by the inner product above. As this is standard, we will not present the details here. The completion of $\mathfrak {U} / \mathcal{N}$ in this norm is the Hilbert space $\mathcal{H}_\omega $ of the GNS Construction Theorem.

Construction of the GNS Representation

Next we will construct $\pi _\omega $ the *-representation of $\mathfrak {U}$ by bounded operators on $\mathcal{H}_\omega $. This will be much easier than the construction of $\mathcal{H}_\omega $.

By construction we can consider $\mathfrak {U} / \mathcal{N}$ as dense in $\mathcal{H}_\omega $. On this dense subset we define the action of $\pi _\omega $ the *-representation of $\mathfrak {U}$ on $\mathfrak {U} / \mathcal{N}$ as follows

\begin{align} \pi _\omega (a)[z] \equiv [az] \end{align}

where $[z]$ is an arbitrary element of $\mathfrak {U} / \mathcal{N}$.

This definition of $\pi _\omega $ on $\mathfrak {U} / \mathcal{N}$ is well-defined as for any other member of the equivalence class $[z]$ of the form $[z + n]$ one has

\begin{align} \pi _\omega (a)[z + n] = [az + an] = [az], \end{align}

where the second equality follows from our previous result $\mathcal{N}_1 = \mathcal{N}$. In other words, $\pi _\omega $ is well-defined as $\mathcal{N}$ is a left-ideal in $\mathfrak {U}$.

Furthermore, it trivially follows from the definition of $\pi _\omega $ that it is linear and an algebraic morphism. So it remains to prove that $\pi _\omega $ is bounded and also a *-morphism.

Let us first prove that $\pi _\omega $ is bounded.

Consider a non-zero $[z]$ in $\mathfrak {U} / \mathcal{N}$. Simply applying definitions one has

\begin{align} \| \pi _\omega (a)[z]\| ^2 & = \| [az]\| ^2 \\ & = \left\langle [az], [az]\right\rangle \\ & = \omega ((az)^*(az)) \\ & = \omega (z^*(a^*a)z) \\ & = \frac{\omega (z^*(a^*a)z)}{\omega (z^*z)} \omega (z^*z) \\ & = \frac{\omega (z^*(a^*a)z)}{\omega (z^*z)} \| [z]\| ^2. \end{align}

With that last equation in mind let us define the map $\phi $ acting on $\mathfrak {U}$ by

\begin{align} \phi (a) \equiv \frac{\omega (z^*az)}{\omega (z^*z)}. \end{align}

One can easily check that $\phi $ when acting on $\mathfrak {U}$ is linear and positive as

\begin{align} \phi (c^*c) = \frac{\omega (z^*(c^*c)z)}{\omega (z^*z)} = \frac{\omega ((cz)^*(cz))}{\omega (z^*z)} \ge 0 \end{align}

as a result of $\omega $ being positive.

Now as $\phi $ is a positive, linear function on the unital C*-algebra $\mathfrak {U}$ we can invoke the theorem (Chapter III Theorem 2.2.9 of Haag)

Theorem. A positive, linear operator $\phi $ on a unital Banach *-algebra $\mathcal{A}$ is bounded and satisfies
\begin{align} \| \phi \| = \phi (\mathbf{1}) \end{align}
where $\phi (\mathbf{1})$ is $\phi $ acting on the unit $\mathbf{1}$ of $\mathcal{A}$.

to prove that $\| \phi \| = \phi (\mathbf{1})$. A short computation finds

\begin{align} \phi (\mathbf{1}) = \frac{\omega (z^*\mathbf{1}z)}{\omega (z^*z)} = 1 \end{align}

proving $\| \phi \| =1$, i.e. $\phi $ is normalized. As $\phi $ is a linear, positive, normalized operator on the unital C*-algebra $\mathfrak {U}$, it is indeed a state.

Now as $\phi $ is normalized and thus $\| \phi \| =1$, the definition of the norm $\| \phi \| $ implies

\begin{align} \| \phi (c)\| \le \| \phi \| \, \| c\| = \| c\| . \end{align}

This along with our previous derivation gives

\begin{align} \| \pi _\omega (a)[z]\| ^2 & = \phi (a^*a) \| [z]\| ^2 \\ & \le \| \phi \| \, \| a^*a\| \, \| [z]\| ^2 \\ & = \| a^*a\| \, \| [z]\| ^2 \\ & = \| a\| ^2 \, \| [z]\| ^2. \end{align}

Using the definition of the norm $\| \pi _\omega (a)\| $ this equation then implies

\begin{align} \| \pi _\omega (a)\| \le \| a\| \end{align}

which is the statement that $\pi _\omega (a)$ is a bounded operator on $\mathfrak {U} / \mathcal{N}$.

Thus using the following standard theorem (Theorem A.36 Hall)

Bounded Linear Transformation Theorem. Let $V_1$ be a normed space and $V_2$ a Banach space. Suppose $W$ is a dense subspace of $V_1$ and $T: W \rightarrow V_2$ is a bounded linear map. Then there exists a unique bounded linear map $\widetilde{T}: V_1 \rightarrow V_2$ such that $\widetilde{T}|_W = T$. Furthermore, the norm of $\widetilde{T}$ equals the norm of $T$.

one can extend $\pi _\omega $ from the dense subset $\mathfrak {U} / \mathcal{N}$ of $\mathcal{H}_\omega $ to all of $\mathcal{H}_\omega $. We do so and use the same notation $\pi _\omega $ for this extension.

Finally we need to prove that $\pi _\omega $ is not only an algebraic morphism but is a *-morphism. Thankfully this is relatively simple.

For $[x]$ and $[y]$ in $\mathfrak {U} / \mathcal{N}$ and $a$ in $\mathfrak {U}$, we have

\begin{align} \left\langle [x], \pi _\omega (a^*)[y]\right\rangle & = \left\langle [x], [a^*y]\right\rangle \\ & = \omega (x^*a^*y) \\ & = \omega ((ax)^*y) \\ & = \left\langle [ax], [y]\right\rangle \\ & = \left\langle \pi _\omega (a)[x], [y]\right\rangle \\ & = \left\langle [x], \pi _\omega (a)^\dagger [y]\right\rangle \end{align}

Hence, $\pi _\omega (a^*) = \pi _\omega (a)^\dagger $ and $\pi _\omega $ is a *-morphism.

Construction of the Cyclic Vector

Our next task is to construct the cyclic vector $\Omega $. This is relatively straightforward.

As $\mathfrak {U}$ is unital we can make the definition

\begin{align} \Omega \equiv [\mathbf{1}]. \end{align}

Tracing definitions we have

\begin{align} \{ \pi _\omega (a)\Omega : a \in \mathfrak {U}\} = \{ [a] : a \in \mathfrak {U}\} = \mathfrak {U} / \mathcal{N}. \end{align}

As $\mathfrak {U} / \mathcal{N}$ is dense in $\mathcal{H}_\omega $, this implies that $\Omega $ is a cyclic vector in $\mathcal{H}_\omega $ for the representation $\pi _\omega $, the property claimed of $\Omega $ in the GNS Construction Theorem.

In addition tracing definitions gives

\begin{align} \left\langle \Omega , \pi _\omega (a)\Omega \right\rangle = \left\langle [\mathbf{1}], \pi _\omega (a)[\mathbf{1}]\right\rangle = \left\langle [\mathbf{1}], [a]\right\rangle = \omega (\mathbf{1}a) = \omega (a) \end{align}

which proves another relation

\begin{align} \omega (a) = \left\langle \Omega , \pi _\omega (a)\Omega \right\rangle \end{align}

claimed in the GNS Construction Theorem.

Faithfulness of the GNS Representation

Now we are going to prove the *-representation $\pi _\omega $ is faithful if $\omega $ is a faithful state.

For this section of the proof, assume that $\omega $ is a faithful state.

To prove that $\pi _\omega $ is a faithful representation, we must prove that $\ker \pi _\omega = \{ 0\} $. In other words, we must prove that $\pi _\omega (a) = 0$ implies that $a=0$.

Assume that $\pi _\omega (a) = 0$. Thus we have

\begin{align} 0 = \left\langle \pi _\omega (a)\Omega , \pi _\omega (a)\Omega \right\rangle = \omega (a^*a). \end{align}

As $\omega $ is assumed faithful in this section of the proof, this implies that $a=0$. This in turn implies $\ker \pi _\omega = \{ 0\} $, which proves that if $\omega $ is faithful, then $\pi _\omega $ is faithful, the desired result.

Uniqueness up to Unitary Equivalence

Finally to complete the proof of the GNS Construction Theorem we now prove that the GNS triple associated to $(\mathfrak {U}, \omega )$ is unique up to unitary equivalence.

To that end let $(\mathcal{H}_\omega ', \pi _\omega ', \Omega ')$ be a second GNS triple associated to $(\mathfrak {U}, \omega )$. (This implies, in particular, that the inner product on $\mathcal{H}_\omega '$ is given by $\omega $.) Then define an operator $U$ by

\begin{align} U\pi _\omega (a)\Omega \equiv \pi _\omega (a)’\Omega ’. \end{align}

The operator $U$ is obviously linear. Furthermore, as $\Omega $ and $\Omega '$ are cyclic, the domain of $U$ is dense in $\mathcal{H}_\omega $ and its range is dense in $\mathcal{H}_\omega '$. Now, as a result of chasing definitions

\begin{align} \left\langle U\pi _\omega (a)\Omega , U\pi _\omega (b)\Omega \right\rangle ’ & = \left\langle \pi _\omega (a)’\Omega ’, \pi _\omega (b)’\Omega ’\right\rangle ’ \\ & = \omega (a^*b) \\ & = \left\langle \pi _\omega (a)\Omega , \pi _\omega (b)\Omega \right\rangle \end{align}

we find that $U$ preserves the inner product and is thus bounded. Furthermore, as $U$ preserves the inner product on its dense domain and dense range, it’s also unitary there.

As $U$ is bounded on its dense domain, the Bounded Linear Transformation Theorem (Theorem A.36 Hall)

Bounded Linear Transformation Theorem. Let $V_1$ be a normed space and $V_2$ a Banach space. Suppose $W$ is a dense subspace of $V_1$ and $T: W \rightarrow V_2$ is a bounded linear map. Then there exists a unique bounded linear map $\widetilde{T}: V_1 \rightarrow V_2$ such that $\widetilde{T}|_W = T$. Furthermore, the norm of $\widetilde{T}$ equals the norm of $T$.

can be used to extend the domain of $U$ to all of $\mathcal{H}_\omega $. This gives a well-defined, unitary map from $\mathcal{H}_\omega $ to $\mathcal{H}_\omega '$ that we also denote by $U : \mathcal{H}_\omega \rightarrow \mathcal{H}_\omega '$.

Now, the definition of $U$

\begin{align} U\pi _\omega (a)\Omega = \pi _\omega (a)’\Omega ’. \end{align}

gives for the case $a = \mathbf{1}$

\begin{align} U\Omega = \Omega ’. \end{align}

Hence, the fact that $U$ is unitary and thus $U^{-1}$ is well-defined gives

\begin{align} \left\langle U\pi _\omega (a)\Omega , U\pi _\omega (b)\Omega \right\rangle ’ & = \left\langle U\pi _\omega (a)U^{-1}U\Omega , U\pi _\omega (b)\Omega \right\rangle ’ \\ & = \left\langle U\pi _\omega (a)U^{-1}U\Omega , \pi _\omega (b)’\Omega ’ \right\rangle ’ \\ & = \left\langle U\pi _\omega (a)U^{-1}\Omega ’, \pi _\omega (b)’\Omega ’ \right\rangle ’. \end{align}

However, the definition of $U$ implies

\begin{align} \left\langle U\pi _\omega (a)\Omega , U\pi _\omega (b)\Omega \right\rangle ’ = \left\langle \pi _\omega (a)’\Omega ’, \pi _\omega (b)’\Omega ’\right\rangle ’. \end{align}

Thus the previous two equations imply

\begin{align} \left\langle U\pi _\omega (a)U^{-1}\Omega ’, \pi _\omega (b)’\Omega ’ \right\rangle ’ = \left\langle \pi _\omega (a)’\Omega ’, \pi _\omega (b)’\Omega ’\right\rangle ’. \end{align}

As a result of cyclicity of $\Omega '$ this implies that

\begin{align} U\pi _\omega (a)U^{-1}\Omega ’ = \pi _\omega (a)’\Omega ’. \end{align}

To complete the proof we must first show that $U\pi _\omega (a)U^{-1}$ and $\pi _\omega (a)'$ agree not only on $\Omega '$, but also on $\pi _\omega (c)'\Omega '$, which as $\Omega '$ is cyclic is dense in $\mathcal{H}_\omega '$. This can then be used along with the Bounded Linear Transformation Theorem to prove that $U\pi _\omega (a)U^{-1}$ and $\pi _\omega (a)'$ agree on $\mathcal{H}_\omega '$.

Let us first prove that $U\pi _\omega (a)U^{-1}$ and $\pi _\omega (a)'$ agree on $\pi _\omega (c)'\Omega '$. We have

\begin{align} U\pi _\omega (a)U^{-1} \pi _\omega (c)’\Omega ’ & = U\pi _\omega (a)U^{-1} U\pi _\omega (c)U^{-1} \Omega ’ \\ & = U\pi _\omega (a)\pi _\omega (c)U^{-1} \Omega ’ \\ & = U\pi _\omega (ac)U^{-1} \Omega ’ \\ & = \pi _\omega (ac)’ \Omega ’ \\ & = \pi _\omega (a)’\pi _\omega (c)’ \Omega ’ \end{align}

Thus $U\pi _\omega (a)U^{-1}$ and $\pi _\omega (a)'$ agree on $\pi _\omega (c)'\Omega '$.

As $\Omega '$ is cyclic, $\pi _\omega (c)'\Omega '$ is dense in $\mathcal{H}_\omega '$, and thus the Bounded Linear Transformation Theorem (Theorem A.36 Hall)

Bounded Linear Transformation Theorem. Let $V_1$ be a normed space and $V_2$ a Banach space. Suppose $W$ is a dense subspace of $V_1$ and $T: W \rightarrow V_2$ is a bounded linear map. Then there exists a unique bounded linear map $\widetilde{T}: V_1 \rightarrow V_2$ such that $\widetilde{T}|_W = T$. Furthermore, the norm of $\widetilde{T}$ equals the norm of $T$.

can be invoked to prove that $U\pi _\omega (a)U^{-1}$ and $\pi _\omega (a)'$ agree on $\mathcal{H}_\omega '$, proving that

\begin{align} \pi _\omega (a)’ = U\pi _\omega (a)U^{-1}, \end{align}

and two GNS triples associated to $(\mathfrak {U}, \omega )$ can differ at most by a unitary transformation, completing our proof of the GNS Construction Theorem.

10.1.2 Summary

This concludes the proof of the GNS Construction Theorem (see Theorem 15). To summarise: given a state $\omega $ over a unital C*-algebra $\mathfrak {U}$ one can construct a Hilbert space $\mathcal{H}_\omega $, a *-representation $\pi _\omega $ of $\mathfrak {U}$ by bounded operators on $\mathcal{H}_\omega $ satisfying $\pi _\omega (a^*) = \pi _\omega (a)^\dagger $, and a cyclic vector $\Omega $ in $\mathcal{H}_\omega $ such that

\begin{align} \omega (a) = \left\langle \Omega , \pi _\omega (a)\Omega \right\rangle _{\mathcal{H}_\omega }. \end{align}

The triple $(\mathcal{H}_\omega , \pi _\omega , \Omega )$ is called the GNS triple associated to $(\mathfrak {U}, \omega )$, or the cyclic representation of $(\mathfrak {U}, \omega )$. If $\omega $ is faithful then so is $\pi _\omega $, and the GNS triple is unique up to unitary equivalence.

The reason we provided such detail is that we will have need not only of the theorem, but also of the details of the theorem’s proof in subsequent blog posts.

10.2 Spacetime

Definition 19 Spacetime

✓

A spacetime is a real, four-dimensional, connected, smooth, Hausdorff manifold $M$ with a globally defined smooth tensor field $g$ of type $(0,2)$ which is non-degenerate and “Lorentzian”. By Lorentzian we mean that for any $p \in M$ there is a basis of the tangent space $TM|_p$ to $M$ at $p$ relative to which $g|_p$ is zero in its non-diagonal entries and on the diagonal takes the form $\text{diag}(-1,1,1,1)$.

Definition 20 Standard Minkowski Spacetime

✓

Standard Minkowski spacetime is a spacetime in which the underlying real, four-dimensional, connected, smooth, Hausdorff manifold is $\mathbb {R}^4$ with the Euclidean topology. In addition $g$ takes the form $g|_p=\text{diag}(-1,1,1,1)$ for all $p$ in $\mathbb {R}^4$ with respect to the standard coordinates on $\mathbb {R}^4$.

Definition 21 Timelike, Spacelike, or Null Vectors

✓

Let $M$ be a spacetime, $p$ a point in $M$, and $g$ the tensor field of type $(0,2)$ associated to $M$. Any tangent vector $v \in TM|_p$ is timelike, spacelike, or null if $g|_p(v,v)$ is negative, positive, or zero respectively.

Lemma 22 Causal Classification

✓

Every tangent vector $v \in TM|_p$ is exactly one of timelike, null, or spacelike. In particular the three classes are mutually exclusive, and the zero vector is null.

Proof ▶

Immediate from the trichotomy of ${\lt}$, $=$, ${\gt}$ applied to $g|_p(v,v)$, together with $g|_p(0,0) = 0$ since $g|_p$ is bilinear.

Lemma 23 Reverse Cauchy-Schwarz for Timelike Vectors

Let $g$ be a symmetric Lorentzian bilinear form on a real four-dimensional vector space and let $v, w$ be timelike, that is $g(v,v) {\lt} 0$ and $g(w,w) {\lt} 0$. Then the reverse Cauchy-Schwarz inequality holds:

\begin{align} g(v,v)\, g(w,w) \le g(v,w)^2. \end{align}

In particular this applies pointwise to the metric $g|_p$ of any spacetime $M$ and any two timelike tangent vectors at a point $p$.

Proof ▶

Choose a Lorentzian basis $b$, so that $g$ has Gram matrix $\mathrm{diag}(-1,1,1,1)$. Expanding $v$ and $w$ in this basis and using bilinearity, $g(v,v) = -(v^0)^2 + \lVert \mathbf{v}\rVert ^2$ and $g(v,w) = -v^0 w^0 + \langle \mathbf{v}, \mathbf{w}\rangle $, where $v^0, w^0$ are the time components, $\mathbf{v}, \mathbf{w}$ the spatial parts, and $\langle \cdot ,\cdot \rangle $, $\lVert \cdot \rVert $ the Euclidean inner product and norm on the three spatial coordinates. Timelikeness gives $(v^0)^2 {\gt} \lVert \mathbf{v}\rVert ^2$ and $(w^0)^2 {\gt} \lVert \mathbf{w}\rVert ^2$. The ordinary Cauchy-Schwarz inequality gives $\lvert \langle \mathbf{v},\mathbf{w}\rangle \rvert \le \lVert \mathbf{v}\rVert \, \lVert \mathbf{w}\rVert {\lt} \lvert v^0\rvert \, \lvert w^0\rvert $, so $\lvert g(v,w)\rvert \ge \lvert v^0 w^0\rvert - \lVert \mathbf{v}\rVert \, \lVert \mathbf{w}\rVert \ge 0$. Squaring and applying the algebraic identity

\begin{align} (pq - rs)^2 - (p^2 - r^2)(q^2 - s^2) = (ps - rq)^2 \ge 0 \end{align}

with $p = \lvert v^0\rvert $, $q = \lvert w^0\rvert $, $r = \lVert \mathbf{v}\rVert $, $s = \lVert \mathbf{w}\rVert $ yields $g(v,w)^2 \ge g(v,v)\, g(w,w)$.

Lemma 24 Timelike Cone Convexity and Reverse Triangle Inequality

Let $g$ be a symmetric Lorentzian bilinear form on a real four-dimensional vector space and let $v, w$ be timelike and aligned, that is $g(v,v) {\lt} 0$, $g(w,w) {\lt} 0$ and $g(v,w) \le 0$. Then $v + w$ is timelike, and the reverse (Lorentzian) triangle inequality holds:

\begin{align} \sqrt{-g(v,v)} + \sqrt{-g(w,w)} \le \sqrt{-g(v+w,\, v+w)}. \end{align}

In particular the timelike vectors sharing a time cone (so that $g(v,w) \le 0$) form a convex cone, and this applies pointwise to the metric $g|_p$ of any spacetime.

Proof ▶

Bilinearity and symmetry give $g(v+w,v+w) = g(v,v) + 2g(v,w) + g(w,w)$. Writing $a = -g(v,v) {\gt} 0$, $b = -g(w,w) {\gt} 0$ and $c = -g(v,w) \ge 0$, this equals $-(a + b + 2c) {\lt} 0$, so $v+w$ is timelike. The reverse Cauchy-Schwarz inequality (23) gives $g(v,w)^2 \ge g(v,v)\, g(w,w)$, that is $c^2 \ge ab$, hence $c \ge \sqrt{ab} = \sqrt a \, \sqrt b$. Therefore $-g(v+w,v+w) = a + b + 2c \ge a + b + 2\sqrt a\, \sqrt b = (\sqrt a + \sqrt b)^2$, and taking square roots yields the reverse triangle inequality.

Definition 25 Time Orientation

✓

A spacetime $M$ is time-orientable if it admits a smooth, non-vanishing vector field $t$ that is timelike. Such a smooth, non-vanishing vector field is called a time-orientation.

Definition 26 Future and Past Pointing Vectors

✓

For any $p$ in a spacetime $M$ a timelike tangent vector $v \in TM|_p$ is future-pointing if $g|_p(t,v)$ is negative and past-pointing if $g|_p(t,v)$ is positive. A null tangent vector $n \in TM|_p$ is future-pointing if it is the limit of future-pointing timelike tangent vectors and it is past-pointing if it is the limit of past-pointing timelike tangent vectors.

Lemma 27 Orientation of Pointing Vectors

✓

A future-pointing or past-pointing vector is timelike or null. Moreover a timelike vector cannot be both future-pointing and past-pointing with respect to a fixed time orientation.

Proof ▶

The first claim is immediate from the definition, which is a disjunction over the timelike and null cases. For the second, a timelike $v$ is not null, so both pointing conditions reduce to their timelike branches $g|_p(t,v) {\lt} 0$ and $g|_p(t,v) {\gt} 0$, which cannot hold simultaneously.

Lemma 28 Sign Lemma for the Future Cone

Let $g$ be a symmetric Lorentzian bilinear form, $t$ a timelike vector, and write $t^\perp = \{ u : g(t,u) = 0\} $ for the spacelike complement. Then $g$ is positive semidefinite on $t^\perp $ (so the ordinary Cauchy-Schwarz inequality holds there), and consequently for any timelike $v, w$ with $g(t,v) {\lt} 0$ and $g(t,w) {\lt} 0$ one has $g(v,w) {\lt} 0$. In particular two timelike tangent vectors that are future-pointing with respect to a common time orientation have negative inner product; by time reversal the same holds for two past-pointing timelike vectors (with $g(t,v) {\gt} 0$ and $g(t,w) {\gt} 0$).

Proof ▶

If $u \in t^\perp $ had $g(u,u) {\lt} 0$ then $u$ would be timelike, and reverse Cauchy-Schwarz (23) would give $g(t,t)\, g(u,u) \le g(t,u)^2 = 0$, contradicting $g(t,t)\, g(u,u) {\gt} 0$; hence $g$ is positive semidefinite on $t^\perp $, and Cauchy-Schwarz follows from nonnegativity of the quadratic $s \mapsto g(s u + u', s u + u')$. For the sign claim, decompose $v$ and $w$ along $t$: the vectors $v_\perp = g(t,t)\, v - g(t,v)\, t$ and $w_\perp = g(t,t)\, w - g(t,w)\, t$ lie in $t^\perp $, and $g(v,w) = g(t,t)^{-2}\big(g(t,t)\, g(v,w)\big)$ expands so that $g(t,t)\, g(v,w) = g(t,v)\, g(t,w) + g(v_\perp , w_\perp )/g(t,t)$. Applying Cauchy-Schwarz to $g(v_\perp ,w_\perp )$ together with the reverse Cauchy-Schwarz bounds $g(t,v)^2 \ge g(t,t)g(v,v)$ and $g(t,w)^2 \ge g(t,t)g(w,w)$ forces $g(t,t)\, g(v,w) {\gt} 0$, and since $g(t,t) {\lt} 0$ this gives $g(v,w) {\lt} 0$.

Lemma 29 Definiteness of the Spacelike Complement

A Lorentzian bilinear form is nondegenerate: if $g(v,w) = 0$ for every $w$, then $v = 0$ (this is read off the signature basis, on which the Gram matrix $\mathrm{diag}(-1,1,1,1)$ is invertible). Consequently $g$ is positive definite on the spacelike complement: if $t$ is timelike and $u \ne 0$ satisfies $g(t,u) = 0$, then $g(u,u) {\gt} 0$, i.e. $u$ is spacelike.

Proof ▶

Nondegeneracy follows because $g(v, b_j) = (b.\mathrm{repr}\, v)_j \cdot \mathrm{diag}(-1,1,1,1)_{jj}$ in the signature basis $b$, and the diagonal entries are nonzero; so $g(v, \cdot ) = 0$ forces every coordinate of $v$ to vanish. For definiteness, semidefiniteness (28) gives $g(u,u) \ge 0$; if $g(u,u) = 0$ then for any $u' \in t^\perp $ Cauchy-Schwarz gives $g(u,u')^2 \le g(u,u)\, g(u',u') = 0$, so $u$ is orthogonal to all of $t^\perp $, and since it is also orthogonal to $t$ it is orthogonal to everything, whence $u = 0$ by nondegeneracy, contradicting $u \ne 0$.

Lemma 30 Convexity of the Future Cone

The sum of two timelike future-pointing tangent vectors (with respect to a fixed time orientation) is again timelike and future-pointing. More generally, the sum of any two future-pointing tangent vectors – timelike or null – is future-pointing, so the full future cone, including its null boundary, is convex. Since a vector is past-pointing exactly when its negation is future-pointing, the past cone is convex as well. Downstream this packages as the statement that the future-pointing and past-pointing tangent vectors each form a convex cone: they are closed under positive scaling and, more generally, under positive linear combinations $a v + b w$ with $a, b {\gt} 0$.

Proof ▶

For two timelike future-pointing $v, w$ we have $g(t,v) {\lt} 0$ and $g(t,w) {\lt} 0$. By the sign lemma (28) $g(v,w) {\lt} 0$, so $v$ and $w$ are aligned and $v + w$ is timelike by cone convexity (24); moreover $g(t, v+w) = g(t,v) + g(t,w) {\lt} 0$, so $v + w$ is future-pointing. For the general case, every future-pointing vector is a limit of future-pointing timelike vectors (the constant sequence if timelike, the approximating sequence from the definition if null). Approximating $v$ and $w$ by such sequences $v_n, w_n$, each $v_n + w_n$ is timelike future-pointing by the timelike case. Passing to the limit gives $g(v,w) \le 0$ (continuity of the fixed maps $u \mapsto g(a,u)$ with symmetry), so $g(v+w,v+w) = g(v,v) + 2g(v,w) + g(w,w) \le 0$ and $v+w$ is causal, and $g(t,v+w) = g(t,v) + g(t,w) \le 0$. If $g(v+w,v+w) {\lt} 0$ the sum is timelike and reverse Cauchy-Schwarz makes $g(t,v+w) \ne 0$, hence negative, so the sum is future-pointing timelike; if $g(v+w,v+w) = 0$ the sum is null and is the limit of the future-pointing timelike sequence $v_n + w_n$, hence future-pointing null.

Definition 31 Paths

✓

A path is a continuous map $\mu :\Sigma \rightarrow M$ from the parameter space–a closed, connected subset $\Sigma $ of $\mathbb {R}$ that contains more than a single point–to a spacetime $M$. A smooth path is a path $\mu $ that is smooth and has a non-vanishing derivative.

Definition 32 Curves

✓

A curve is an equivalence class of paths equivalent under homeomorphisms of the parameter space. A smooth curve is an equivalence class of smooth paths equivalent under diffeomorphisms of the parameter space.

Definition 33 Timelike and Causal Smooth Curves

✓

A timelike smooth curve is a smooth curve with a tangent vector that is timelike at every point along the smooth curve. A causal smooth curve is a smooth curve with a tangent vector that is timelike or null at every point along the smooth curve.

Definition 34 Future and Past Oriented Smooth Curves

✓

A future-oriented smooth curve is a smooth curve with a tangent vector that is future-pointing at every point. A past-oriented smooth curve is a smooth curve with a tangent vector that is past-pointing at every point.

Theorem 35 Reparametrisation-Invariance of the Causal Type

✓

The timelike and causal predicates are well-defined on smooth curves, independently of the chosen path representative: a smooth path is timelike (resp. causal) if and only if its associated smooth curve is. The invariance rests on the chain rule for the tangent under a smooth reparametrisation $\varphi $, namely $\mathrm{tangent}(\mu \circ \varphi )(s) = \varphi '(s)\cdot \mathrm{tangent}(\mu )(\varphi (s))$, together with the scale-invariance of the causal classification: since $g(c\, v, c\, v) = c^2\, g(v,v)$, the vector $c\, v$ is timelike/null exactly when $v$ is, for $c \neq 0$.

Definition 36 Oriented Smooth Curve

✓

An orientation-reversing reparametrisation flips the time-orientation of the tangent, so future/past orientation is well-defined only on the finer quotient by orientation-preserving reparametrisations (those with positive within-derivative). An oriented smooth curve is an equivalence class of smooth paths under this finer relation.

Theorem 37 Reparametrisation-Invariance of Orientation

✓

Future- and past-orientation are well-defined on oriented smooth curves: a smooth path is future-oriented (resp. past-oriented) if and only if its oriented smooth curve is. The positive within-derivative of an orientation-preserving reparametrisation, together with the positive-scaling invariance of pointing vectors ($c\, v$ is future-pointing iff $v$ is, for $c {\gt} 0$), gives the invariance.

Theorem 38 The Forgetful Projection of Oriented Curves

✓

Every oriented smooth curve has an underlying smooth curve, via a canonical surjection $\mathrm{OrientedSmoothCurve} \to \mathrm{SmoothCurve}$ that forgets the orientation data. The timelike and causal predicates factor through it, and a future- or past-oriented curve projects to a causal smooth curve.

Definition 39 Endpoints

✓

A point $p$ in a spacetime $M$ is the endpoint of a path $\mu $ or its associated curve if it is a member of the image $\mu (\partial \Sigma )$ of the boundary $\partial \Sigma $ of the parameter space under $\mu $. If $\mu $ is a smooth path and its associated smooth curve is timelike and future-oriented, then an endpoint $p$ is a past endpoint if it is the image under $\mu $ of the lesser of the two boundary components of $\partial \Sigma $. It is a future endpoint if it is the image under $\mu $ of the greater of the two boundary components of $\partial \Sigma $.

Definition 40 Trip

✓

A trip segment is a curve which is a future-oriented, timelike geodesic. A trip is a curve which is piecewise a future-oriented, timelike geodesic: a finite chain of trip segments $p = x_0, x_1, \dots , x_n = q$ joined at matching endpoints. Formally this is the transitive closure of single-segment precedence, which is what makes the relation transitive by concatenation. A trip from $p$ to $q$ is a trip with past endpoint $p$ and future endpoint $q$. We write $p \ll q$ if and only if there exists a trip from $p$ to $q$.

Definition 41 Causal Trip

✓

A causal trip segment is a curve which is a future-oriented, causal geodesic. (Note a causal geodesic is possibly degenerate.) A causal trip is a curve which is piecewise a future-oriented, causal geodesic: a finite chain of causal trip segments joined at matching endpoints. A causal trip from $p$ to $q$ is a causal trip with past endpoint $p$ and future endpoint $q$. We write $p \prec q$ if and only if there exists a causal trip from $p$ to $q$.

Remark (geodesic placeholder in the formalization). In the Lean formalization the “geodesic” clause of a (causal) trip segment is currently a placeholder: the predicate Physicslib4.Spacetime.IsGeodesic is defined to be True, so it imposes no constraint. A faithful geodesic condition requires the Levi-Civita connection of the metric (auto-parallelism of the tangent vector along the curve), which the version of Mathlib pinned by this project does not provide. Consequently the formalized (causal) trip segments are future-oriented timelike (resp. causal) curves with the correct past and future endpoints, but their geodesic property is not yet enforced; the endpoint, timelike/causal, and future-orientation content is faithful. This is the one place where 40 and 41 diverge from their Lean implementations, and it should be replaced by the genuine geodesic condition once a Lorentzian Levi-Civita connection is available in Mathlib.

Theorem 42 Transitivity of chronological and causal precedence

✓

Chronological precedence $\ll $ and causal precedence $\prec $ are transitive: if $p \ll q$ and $q \ll r$ then $p \ll r$, and likewise for $\prec $. Two trips joined at the common point $q$ concatenate to a single piecewise trip; this is exactly the transitivity of the transitive closure.

Definition 43 No Closed Causal Curve (Causality Condition)

✓

A spacetime $M$ with time orientation $t$ satisfies the causality condition — equivalently, has no closed causal curve — when no point causally precedes itself: $\lnot (p \prec p)$ for every $p$. A closed causal curve through $p$ would be a causal trip from $p$ back to $p$, i.e. $p \prec p$, so its absence is exactly this condition. This is the standard causality condition, strictly weaker than strong causality and strictly stronger than the chronology condition ($\lnot (p \ll p)$ for all $p$).

Definition 45 Chronological Future and Chronological Past

✓

For a spacetime $M$ and $p$ in $M$ the set $I^+(p) = \{ q \in M : p \ll q\} $ is called the chronological future of $p$. $I^-(p) = \{ q \in M : q \ll p\} $ is called the chronological past of $p$. The chronological future of a set $S \subset M$ is the union of the chronological future of each element of the set

\begin{align} I^+(S) = \bigcup \limits _{p \in S} I^+(p). \end{align}

The chronological past of $S$ is defined similarly

\begin{align} I^-(S) = \bigcup \limits _{p \in S} I^-(p). \end{align}

Definition 46 Causal Future and Causal Past

✓

For a spacetime $M$ and $p$ in $M$ the set $J^+(p) = \{ q \in M : p \prec q\} $ is called the causal future of $p$. $J^-(p) = \{ q \in M : q \prec p\} $ is called the causal past of $p$. The causal future of a set $S \subset M$ is the union of the causal future of each element of the set

\begin{align} J^+(S) = \bigcup \limits _{p \in S} J^+(p). \end{align}

The causal past of $S$ is defined similarly

\begin{align} J^-(S) = \bigcup \limits _{p \in S} J^-(p). \end{align}

Lemma 47 Chronological Precedence Implies Causal Precedence

✓

Every trip is a causal trip, so $p \ll q$ implies $p \prec q$. Consequently $I^+(p) \subseteq J^+(p)$ and $I^-(p) \subseteq J^-(p)$.

Proof ▶

A timelike tangent vector is in particular causal (timelike or null), so a future-oriented timelike geodesic is a future-oriented causal geodesic. Hence any trip witnessing $p \ll q$ is also a causal trip witnessing $p \prec q$. The set inclusions follow by unfolding the definitions of the futures and pasts.

Lemma 48 Monotonicity of Futures and Pasts

✓

The set-valued chronological and causal futures and pasts are monotone: if $S \subseteq T$ then $I^\pm (S) \subseteq I^\pm (T)$ and $J^\pm (S) \subseteq J^\pm (T)$.

Proof ▶

Each operator is an indexed union over the points of its argument set, and a union over a larger index set contains the union over a smaller one.

Definition 50 Completely Spacelike

✓

Consider two sets $\mathbf{O}_1$ and $\mathbf{O}_2$ in a spacetime. $\mathbf{O}_1$ and $\mathbf{O}_2$ are completely spacelike with respect to each other if every $p_1$ in $\mathbf{O}_1$ is spacelike related to every $p_2$ in $\mathbf{O}_2$.

Lemma 51 Symmetry of Spacelike Separation

✓

Spacelike relatedness is symmetric, and consequently complete spacelike separation is symmetric in its two regions: $\mathbf{O}_1, \mathbf{O}_2$ are completely spacelike if and only if $\mathbf{O}_2, \mathbf{O}_1$ are.

Proof ▶

The relation $p_2 \notin J^+(p_1) \cup J^-(p_1)$ is symmetric in $p_1, p_2$ since $J^+(p_1)$ and $J^-(p_1)$ swap roles with $J^-(p_2)$ and $J^+(p_2)$ under the exchange. Symmetry of complete spacelike separation follows by applying this pointwise.

Lemma 52 Structural Properties of Complete Spacelike Separation

✓

Complete spacelike separation is monotone under shrinking either region; the empty region is completely spacelike to any region; and a union of regions is completely spacelike to $\mathbf{O}$ if and only if each part is. The same properties hold for the bundled Lorentzian spacetime.

Proof ▶

Each follows directly from the pointwise definition: monotonicity by restricting the universally-quantified points, the empty cases vacuously, and the union cases by splitting the membership disjunction.

Definition 53 Spacelike Complement of a Region

✓

The spacelike complement $\mathbf{B}^\perp $ of a region $\mathbf{B}$ is the set of points completely spacelike-separated from all of $\mathbf{B}$: $\mathbf{B}^\perp = \{ x \mid \{ x\} \text{ is completely spacelike to } \mathbf{B} \} $. It is the geometric substrate of locality and Haag duality.

Lemma 54 Order Structure of the Spacelike Complement

✓

The spacelike complement is antitone ($\mathbf{B}_1 \subseteq \mathbf{B}_2 \Rightarrow \mathbf{B}_2^\perp \subseteq \mathbf{B}_1^\perp $), a region is contained in its double complement ($\mathbf{B} \subseteq \mathbf{B}^{\perp \perp }$), and the triple complement collapses ($\mathbf{B}^{\perp \perp \perp } = \mathbf{B}^\perp $). Moreover $\mathbf{B}_1 \subseteq \mathbf{B}_2^\perp $ if and only if $\mathbf{B}_1$ and $\mathbf{B}_2$ are completely spacelike-separated, so complementation is the Galois connection attached to the spacelike-separation relation.

Proof ▶

Antitonicity and the Galois bridge are the pointwise monotonicity of complete spacelike separation; the double-complement inclusion follows by symmetry of the relation; and the triple-complement identity is the standard consequence of antitonicity together with the double-complement inclusion.

Definition 55 Causal closure operator

✓

The double spacelike complement $\mathbf{B} \mapsto \mathbf{B}^{\perp \perp }$ is a closure operator on the regions of a Lorentzian spacetime: it is monotone, extensive ($\mathbf{B} \subseteq \mathbf{B}^{\perp \perp }$), and idempotent ($\mathbf{B}^{\perp \perp \perp \perp } = \mathbf{B}^{\perp \perp }$). Its three defining properties are exactly the order structure of the spacelike complement.

Definition 56 Causally complete region

✓

A region is causally complete if it equals its own double complement, $\mathbf{B}^{\perp \perp } = \mathbf{B}$ (a fixed point of the causal closure operator). These are the regions on which algebraic QFT is naturally indexed.

Theorem 57 Lattice of causally complete regions

✓

The causally complete regions form a complete lattice (meets are intersections, joins are causal closures of unions), obtained from the causal closure operator via its Galois insertion. The spacelike complement of any region is causally complete, causally complete regions are closed under intersection, and the causal complement $\mathbf{B} \mapsto \mathbf{B}^\perp $ is an order-reversing involution on this lattice ($\mathbf{B}^{\perp \perp } = \mathbf{B}$). (The full orthocomplement law $\mathbf{B} \wedge \mathbf{B}^\perp = \bot $ does not hold at this generality, because the trip-based causal relation is irreflexive, so a point is spacelike-separated from itself; what holds is the complete lattice with an order-reversing De Morgan involution.)

Lemma 58 De Morgan Laws for the Spacelike Complement

✓

At the level of the underlying sets, the spacelike complement turns unions into intersections. In binary form, for regions $\mathbf{B}_1, \mathbf{B}_2$,

\begin{align} (\mathbf{B}_1 \cup \mathbf{B}_2)^\perp = \mathbf{B}_1^\perp \cap \mathbf{B}_2^\perp , \end{align}

and, for an arbitrary indexed family $(\mathbf{B}_i)_{i \in I}$,

\begin{align} \Bigl(\bigcup _{i \in I} \mathbf{B}_i\Bigr)^\perp = \bigcap _{i \in I} \mathbf{B}_i^\perp . \end{align}

Proof ▶

Unfold the spacelike complement pointwise: $x \in \mathbf{B}^\perp $ means the singleton $\{ x\} $ is completely spacelike to $\mathbf{B}$. By the structural properties of complete spacelike separation (52), $\{ x\} $ is completely spacelike to a union $\bigcup _i \mathbf{B}_i$ if and only if it is completely spacelike to each member $\mathbf{B}_i$. Hence membership in the complement of the union is the conjunction of membership in the individual complements, which is exactly membership in their intersection. The binary case is the special case of a two-element family.

Theorem 59 De Morgan Laws for the Causal Complement

✓

On the complete lattice of causally complete regions the causal complement $\mathbf{B} \mapsto \mathbf{B}^\perp $ is an order-reversing involution, and therefore satisfies the full De Morgan laws. Explicitly:

(order-reversing) $\mathbf{B}_1 \le \mathbf{B}_2 \Rightarrow \mathbf{B}_2^\perp \le \mathbf{B}_1^\perp $;
(bounds) $\bot ^\perp = \top $ and $\top ^\perp = \bot $;
(binary De Morgan) $(\mathbf{B}_1 \sqcup \mathbf{B}_2)^\perp = \mathbf{B}_1^\perp \sqcap \mathbf{B}_2^\perp $ and $(\mathbf{B}_1 \sqcap \mathbf{B}_2)^\perp = \mathbf{B}_1^\perp \sqcup \mathbf{B}_2^\perp $;
(infinitary De Morgan) $\bigl(\bigsqcup _i \mathbf{B}_i\bigr)^\perp = \bigsqcap _i \mathbf{B}_i^\perp $ and $\bigl(\bigsqcap _i \mathbf{B}_i\bigr)^\perp = \bigsqcup _i \mathbf{B}_i^\perp $.

Proof ▶

Recall from the lattice structure (57) that on causally complete regions meets are intersections of the underlying sets, joins are the causal closures of unions ($\mathbf{B}_1 \sqcup \mathbf{B}_2 = (\mathbf{B}_1 \cup \mathbf{B}_2)^{\perp \perp }$ and dually for arbitrary families), the complement of any region is causally complete, and every region in the lattice satisfies the involution $\mathbf{B}^{\perp \perp } = \mathbf{B}$; in particular the triple-complement identity $\mathbf{C}^{\perp \perp \perp } = \mathbf{C}^\perp $ holds for any underlying set $\mathbf{C}$, since $\mathbf{C}^\perp $ is causally complete. Each law is then a direct computation on the underlying sets driven by the set-level De Morgan lemma (58).

(order-reversing) This is the antitonicity half of the order-reversing involution supplied by 57: $\mathbf{B}_1 \le \mathbf{B}_2$ means $\mathbf{B}_1 \subseteq \mathbf{B}_2$, whence $\mathbf{B}_2^\perp \subseteq \mathbf{B}_1^\perp $, i.e. $\mathbf{B}_2^\perp \le \mathbf{B}_1^\perp $.
(join laws) Since the join is the causal closure of the union, the triple-complement identity collapses one level of complement:

\begin{align} (\mathbf{B}_1 \sqcup \mathbf{B}_2)^\perp = \bigl((\mathbf{B}_1 \cup \mathbf{B}_2)^{\perp \perp }\bigr)^\perp = (\mathbf{B}_1 \cup \mathbf{B}_2)^{\perp \perp \perp } = (\mathbf{B}_1 \cup \mathbf{B}_2)^\perp = \mathbf{B}_1^\perp \cap \mathbf{B}_2^\perp = \mathbf{B}_1^\perp \sqcap \mathbf{B}_2^\perp , \end{align}

the fourth equality being the binary set-level De Morgan lemma (58) and the last using that lattice meets are intersections. The indexed form is identical with the indexed De Morgan lemma in place of the binary one, giving $\bigl(\bigsqcup _i \mathbf{B}_i\bigr)^\perp = \bigsqcap _i \mathbf{B}_i^\perp $.
(meet laws) Apply the set-level De Morgan lemma to the complements $\mathbf{B}_1^\perp , \mathbf{B}_2^\perp $ and use $\mathbf{B}_i^{\perp \perp } = \mathbf{B}_i$ (each $\mathbf{B}_i$ is causally complete): $(\mathbf{B}_1^\perp \cup \mathbf{B}_2^\perp )^\perp = \mathbf{B}_1^{\perp \perp } \cap \mathbf{B}_2^{\perp \perp } = \mathbf{B}_1 \cap \mathbf{B}_2$. Taking the complement of both sides and recognising the meet as the intersection and the join as the double-complement of the union,

\begin{align} (\mathbf{B}_1 \sqcap \mathbf{B}_2)^\perp = (\mathbf{B}_1 \cap \mathbf{B}_2)^\perp = (\mathbf{B}_1^\perp \cup \mathbf{B}_2^\perp )^{\perp \perp } = \mathbf{B}_1^\perp \sqcup \mathbf{B}_2^\perp , \end{align}

and likewise $\bigl(\bigsqcap _i \mathbf{B}_i\bigr)^\perp = \bigsqcup _i \mathbf{B}_i^\perp $ from the indexed De Morgan lemma.
(bounds) The empty-family case of the indexed De Morgan lemma (58) reads $\varnothing ^\perp = \mathrm{univ}$, so $\top = \mathrm{univ} = \varnothing ^\perp $. Hence $\top ^\perp = \varnothing ^{\perp \perp } = \bot $, while $\bot = \varnothing ^{\perp \perp }$ and the triple-complement identity give $\bot ^\perp = \varnothing ^{\perp \perp \perp } = \varnothing ^\perp = \top $.

The mathematical subtlety is that this lattice is not linearly ordered, so the binary equalities do not follow from antitonicity alone: a general antitone map only yields the inequality $f(\mathbf{B}_1 \sqcup \mathbf{B}_2) \le f\mathbf{B}_1 \sqcap f\mathbf{B}_2$. The equalities hold precisely because the causal complement is an order-reversing bijection (the involution $\mathbf{B}^{\perp \perp } = \mathbf{B}$), equivalently an order isomorphism onto the order-dual lattice; it is this bijectivity that both forces the finite equalities above and, through the same set-level De Morgan computation applied to arbitrary unions, upgrades them to the infinitary laws by carrying suprema to infima.

Definition 60 Alexandrov Topology

✓

Alexandrov topology on a spacetime $M$ is the topology generated by the basis consisting of all sets of the form $I^+(p) \cap I^-(q)$ for points $p$ and $q$ in $M$.

Lemma 61 Basis Sets Are Alexandrov-Open

✓

Every basis set $I^+(p) \cap I^-(q)$ is open in the Alexandrov topology.

Proof ▶

By construction the Alexandrov topology is generated by these basis sets, and any generating set is open in the generated topology.

Lemma 62 Openness of Chronological Futures and Pasts

✓

Let $M$ be a spacetime with time orientation $t$, equipped with the Alexandrov topology.

For all points $p, q \in M$ the set $I^+(p) \cap I^-(q)$ is open. This is just the basis lemma (61) restated on chronological futures and pasts.
If every point of $I^+(p)$ has a chronological-future point, i.e. for all $x \in I^+(p)$ there exists $b$ with $x \ll b$, then the chronological future $I^+(p)$ is open.
Dually, if every point of $I^-(p)$ has a chronological-past point, i.e. for all $x \in I^-(p)$ there exists $a$ with $a \ll x$, then the chronological past $I^-(p)$ is open.

The per-point hypotheses in the last two items are quantified over the members of the set in question, so they hold vacuously when that set is empty; this is consistent, since the empty set is open. The flat unconditional claim “$I^+(p)$ is always open” is false for a general spacetime: if $I^+(p)$ is nonempty and contains a future-endpoint point $x$ (a point with no $b$ satisfying $x \ll b$), then $x$ lies in no basis set $I^+(a) \cap I^-(b)$, since membership there forces $a \ll x \ll b$ and in particular $x \ll b$. Hence $x$ has no basic Alexandrov neighbourhood contained in $I^+(p)$ and $I^+(p)$ fails to be open. The hypothesis is exactly the “no future endpoints” condition that removes this obstruction, and dually for pasts.

Proof ▶

The first item is the basis lemma (61) directly: $I^+(p) \cap I^-(q)$ is a basis set, hence open.

For the second item, under the hypothesis we have the set identity

\begin{align} I^+(p) = \bigcup _{b \in M} \bigl(I^+(p) \cap I^-(b)\bigr). \end{align}

The right-hand side is contained in $I^+(p)$ since every term is. Conversely, if $x \in I^+(p)$ then by hypothesis there is $b$ with $x \ll b$, i.e. $x \in I^-(b)$, so $x$ lies in the $b$-th term. Each set $I^+(p) \cap I^-(b)$ is a basis set and hence open (61), and an arbitrary union of open sets is open; therefore $I^+(p)$ is open. The third item is dual, using $I^-(p) = \bigcup _{a \in M} \bigl(I^+(a) \cap I^-(p)\bigr)$. (Recall also that chronological precedence $\ll $ is transitive, 42.)

Lemma 63 Unconditional Openness of Chronological Futures and Pasts on Standard Minkowski

✓

Work on standard Minkowski spacetime, with underlying manifold $\mathbb {R}^4$, and let $e_0$ denote the unit time vector (the first standard coordinate vector).

Every point has a chronological future point and a chronological past point: for all $x \in \mathbb {R}^4$ there exist $b, a$ with $x \ll b$ and $a \ll x$. Concretely $b = x + e_0$ lies in the forward cone of $x$ and $a = x - e_0$ lies in the backward cone of $x$, since the connecting vector $\pm e_0$ is future-, respectively past-pointing timelike.
For every point $p$ the chronological future $I^+(p)$ and the chronological past $I^-(p)$ are open in the Euclidean (manifold) topology on $\mathbb {R}^4$. On standard Minkowski the coordinate cone characterisation identifies $I^+(p)$ with the forward Minkowski cone of $p$ and $I^-(p)$ with the backward Minkowski cone of $p$, and each such cone is an open subset of $\mathbb {R}^4$.
For every point $p$ the chronological future $I^+(p)$ and the chronological past $I^-(p)$ are open in the Alexandrov topology, unconditionally: the per-point hypothesis of 62 is discharged on standard Minkowski by part (i).

Proof ▶

Part (i) is read off the coordinate cone description of standard Minkowski: for any $x$ the difference $(x + e_0) - x = e_0$ has metric square $g(e_0, e_0) = -1 {\lt} 0$ and positive time component, so it is future-pointing timelike; hence $x \ll x + e_0$ and the forward cone of $x$ is nonempty. Dually $(x - e_0) - x = -e_0$ is past-pointing timelike, so $x - e_0 \ll x$ and the backward cone of $x$ is nonempty.

Part (ii) combines the coordinate characterisation of $I^\pm $ on standard Minkowski with the openness of the explicit cones. Under the identification of $I^+(p)$ with the forward Minkowski cone $\{ y \in \mathbb {R}^4 : g(y - p, y - p) {\lt} 0,\ (y - p)^0 {\gt} 0\} $, this set is the intersection of the preimages of the open sets $(-\infty , 0)$ and $(0, \infty )$ under the continuous maps $y \mapsto g(y - p, y - p)$ (a quadratic form) and $y \mapsto (y - p)^0$ (a coordinate projection); hence it is open in the Euclidean topology on $\mathbb {R}^4$. The backward cone description of $I^-(p)$ is dual and open by the same argument.

Part (iii) applies the general lemma 62: its last two items give the openness of $I^+(p)$ and $I^-(p)$ in the Alexandrov topology provided every point of the set in question has, respectively, a chronological-future point and a chronological-past point. On standard Minkowski these hypotheses hold at every point by part (i), so both conclusions are unconditional.

Definition 64 Minkowski Spacetime

✓

Minkowski spacetime is standard Minkowski spacetime equipped with Alexandrov topology.

Definition 65 Lorentzian Spacetime

✓

Lorentzian spacetime is a spacetime equipped with a Hausdorff Alexandrov topology.

Lemma 66 Bundled Spacelike Separation and Basis Openness

✓

On a Lorentzian spacetime, complete spacelike separation of two regions is symmetric, and every basis set $I^+(p) \cap I^-(q)$ is open in the Alexandrov topology.

Proof ▶

These are restatements of the symmetry of complete spacelike separation and the openness of basis sets for the underlying spacetime, transported through the bundling of a Lorentzian spacetime over its underlying spacetime and time orientation.

Lemma 67 No-Diamond Points Have Only the Whole Space as Neighbourhood

✓

On a spacetime equipped with the Alexandrov topology, suppose a point $x$ lies in no diamond $I^+(p) \cap I^-(q)$. Then every Alexandrov-open set containing $x$ is the whole space $M$: the only open neighbourhood of $x$ is $M$ itself.

Proof ▶

The Alexandrov topology is generated by the diamond subbasis, so its open sets are exactly those built by the inductive generating construction, and we induct over that construction to show any generated-open set $U$ with $x \in U$ equals $M$. A basic generating set is a diamond, which cannot contain $x$ by hypothesis, so that case is vacuous. The whole-space generator is $M$. A binary intersection $s \cap t$ containing $x$ has $x \in s$ and $x \in t$, so $s = t = M$ by the induction hypothesis and $s \cap t = M$. A union $\bigcup _i s_i$ containing $x$ contains $x$ in some member $s_i$, which equals $M$ by the induction hypothesis, so the union contains $M$ and hence equals $M$. Thus no generated-open set other than $M$ contains $x$.

Lemma 68 Covering from the Hausdorff Assumption

✓

On a Lorentzian spacetime with at least two points, the Alexandrov diamonds cover the whole space: every point lies in some diamond $I^+(p) \cap I^-(q)$. Equivalently, every point has both a chronological past point and a chronological future point (a “no endpoints” condition). This is a genuine consequence of the Hausdorff assumption on the Alexandrov topology, not an extra hypothesis.

Proof ▶

Suppose a point $x$ lay in no diamond $I^+(p) \cap I^-(q)$. Then by 67 the only Alexandrov-open set containing $x$ is the whole space $M$. Since the space has a second point $y \ne x$, the Hausdorff assumption on the Alexandrov topology provides disjoint open sets separating $x$ and $y$; but the one containing $x$ must be all of $M$, which also contains $y$, contradicting disjointness. Hence every point lies in some diamond, which is exactly the covering half of the Alexandrov-basis property; unfolding membership in a diamond gives the equivalent “no endpoints” statement.

Theorem 69 The Alexandrov Diamonds Form a Topological Basis

✓

On a Lorentzian spacetime with at least two points, suppose the diamonds are downward-directed: for any two diamonds $B_1, B_2$ and any point $x \in B_1 \cap B_2$ there is a diamond $B_3$ with $x \in B_3 \subseteq B_1 \cap B_2$ (the intersection property). Then the diamonds form a genuine topological basis for the Alexandrov topology.

Proof ▶

The three conditions of a topological basis all hold. The intersection (downward-directedness) property is the standing hypothesis. The covering condition — that the diamonds’ union is the whole space — is 68. The topology-generation condition holds by definition, since the Alexandrov topology is defined as the topology generated by the diamond subbasis. The directedness hypothesis is the genuinely geometric content: it is exactly the assertion that the Alexandrov topology has the diamonds as a base, and it is not implied by Hausdorffness alone; it is discharged for standard Minkowski in 73.

Lemma 70 Past Interpolation on Standard Minkowski

✓

On standard Minkowski spacetime, if $p_1 \ll x$ and $p_2 \ll x$ then there is a point $a$ with $p_1 \ll a$, $p_2 \ll a$, and $a \ll x$.

Proof ▶

Take $a$ with the same spatial coordinates as $x$ and time coordinate $a^0 = x^0 - \varepsilon $ for a small $\varepsilon {\gt} 0$. Then $x - a = (\varepsilon , \mathbf{0})$ is future-pointing timelike, so $a \ll x$. For each $i$ the connecting vector $a - p_i$ has the same spatial part as $x - p_i$ while its time component is $(x^0 - p_i^0) - \varepsilon $; since $p_i \ll x$ makes the spatial separation strictly smaller than $x^0 - p_i^0$, for $\varepsilon $ small enough the reduced time gap still dominates the spatial separation and remains positive, so $a - p_i$ is future-pointing timelike and $p_i \ll a$. Both strict inequalities hold for a common small $\varepsilon $; the estimate is a direct coordinate computation (nlinarith).

Lemma 71 Future Interpolation on Standard Minkowski

✓

On standard Minkowski spacetime, if $x \ll q_1$ and $x \ll q_2$ then there is a point $b$ with $x \ll b$, $b \ll q_1$, and $b \ll q_2$.

Proof ▶

Dual to 70: take $b$ with the same spatial coordinates as $x$ and time coordinate $b^0 = x^0 + \varepsilon $ for a small $\varepsilon {\gt} 0$. Then $b - x = (\varepsilon , \mathbf{0})$ is future-pointing timelike, so $x \ll b$, and for each $i$ the vector $q_i - b$ keeps the spatial part of $q_i - x$ with time component $(q_i^0 - x^0) - \varepsilon $; for $\varepsilon $ small enough it stays future-pointing timelike, giving $b \ll q_i$ for both $i$ by the same coordinate estimate.

Lemma 72 Standard Minkowski Diamonds Are Downward-Directed

✓

On standard Minkowski spacetime the Alexandrov diamonds have the downward intersection property: for any two diamonds $B_1 = I^+(p_1) \cap I^-(q_1)$ and $B_2 = I^+(p_2) \cap I^-(q_2)$ and any $x \in B_1 \cap B_2$, there is a diamond $B_3$ with $x \in B_3 \subseteq B_1 \cap B_2$.

Proof ▶

From $x \in B_1 \cap B_2$ we have $p_1 \ll x$, $p_2 \ll x$, $x \ll q_1$, and $x \ll q_2$. Past interpolation (70) yields $a$ with $p_1 \ll a$, $p_2 \ll a$, and $a \ll x$; future interpolation (71) yields $b$ with $x \ll b$, $b \ll q_1$, and $b \ll q_2$. Set $B_3 = I^+(a) \cap I^-(b)$; then $a \ll x \ll b$ gives $x \in B_3$. For containment, any $y$ with $a \ll y \ll b$ satisfies $p_i \ll a \ll y$ and $y \ll b \ll q_i$ for each $i$, so by transitivity of $\ll $ (42) $y \in I^+(p_i) \cap I^-(q_i)$; hence $B_3 \subseteq B_1 \cap B_2$.

Theorem 73 The Alexandrov Diamonds are a Basis on Standard Minkowski

✓

On standard Minkowski spacetime the Alexandrov diamonds form a genuine topological basis for the Alexandrov topology, unconditionally.

Proof ▶

Apply 69. Its downward intersection hypothesis is discharged by 72, and its covering condition holds because on standard Minkowski every point has a chronological past point and a chronological future point (63). The topology-generation condition holds by definition of the Alexandrov topology.

10.2.1 Isometries and basis-set preservation

Lemma 74 Isometries Preserve the Causal Classification

✓

An isometry $\varphi $ of a spacetime preserves the metric square of a tangent vector, $g_{\varphi (x)}(d\varphi _x v, d\varphi _x v) = g_x(v,v)$, and therefore $d\varphi _x v$ is timelike, null, or spacelike if and only if $v$ is.

Proof ▶

Specialising the metric-preservation property of an isometry to $w = v$ gives the square identity; the three classification equivalences then follow from the sign of $g(v,v)$ being unchanged.

Lemma 75 Unique Differentials Along a Path

✓

The parameter space of a path has unique differentials: being a closed, connected subset of $\mathbb {R}$ with more than one point, it is a non-degenerate interval, hence convex with non-empty interior.

Proof ▶

A connected subset of $\mathbb {R}$ is convex, and a closed convex set with at least two points contains a non-degenerate open interval, so has non-empty interior; convex sets with non-empty interior have unique differentials.

Lemma 76 Pushforward of a Path Under an Isometry

✓

An isometry $\varphi $ pushes a smooth path $\mu $ forward to the smooth path $\varphi \circ \mu $ on the same parameter space, with tangent vector $d\varphi (\dot\mu )$. The pushforward preserves the timelike and causal conditions and carries the past and future endpoints of $\mu $ to those of $\varphi \circ \mu $.

Proof ▶

Smoothness and non-vanishing of the derivative of $\varphi \circ \mu $ follow from the chain rule (using unique differentials on the parameter space) together with the fact that an isometry’s differential is a linear isomorphism. The tangent identity then transports the classification and endpoint conditions.

Lemma 77 Isometries Preserve Chronology

✓

Say an isometry $\varphi $ preserves the future orientation if its differential sends future-pointing vectors to future-pointing vectors; this property holds for the identity and is closed under composition. Under it, $\varphi $ carries trips to trips, so $p \ll q$ implies $\varphi (p) \ll \varphi (q)$, and the chronological futures and pasts satisfy $\varphi (I^\pm (p)) = I^\pm (\varphi (p))$.

Proof ▶

Future-orientation preservation makes the pushforward of a future-oriented trip a future-oriented trip, giving $p \ll q \Rightarrow \varphi (p) \ll \varphi (q)$. Applying this to $\varphi $ and to $\varphi ^{-1}$ yields the image equalities for $I^+$ and $I^-$.

Lemma 78 Isometries Preserve Basis Sets

✓

The future-orientation-preserving isometries (those $\varphi $ with both $\varphi $ and $\varphi ^{-1}$ preserving the orientation) form a subgroup, and intersecting it with the identity component gives the oriented identity component. Every such isometry maps Alexandrov-basis diamonds to diamonds, $\varphi (I^+(p) \cap I^-(q)) = I^+(\varphi (p)) \cap I^-(\varphi (q))$, both as an image and in pointwise-action form $\varphi \cdot \mathbf{B}$, and this lifts to the bundled Lorentzian spacetime.

Proof ▶

Bundling the inverse into the predicate makes the subgroup axioms follow from the identity and composition cases with no appeal to the group topology. Basis-set preservation is then the image of an intersection of a chronological future and past, computed via the previous lemma using injectivity of the isometry.

Lemma 79 Axiom 5 Basis-Set Preservation

✓

Instantiating the abstract curved-spacetime interface with the oriented identity component, every isometry $\varphi $ of the abstract spacetime carries Alexandrov-basis sets to basis sets, $\varphi \cdot \mathbf{B}$ is again a basis set. This is exactly the well-definedness condition for the Axiom 5 action $\mathfrak {U}(\mathbf{B}) \to \mathfrak {U}(\varphi (\mathbf{B}))$.

Proof ▶

The abstract isometry group of the bridge is, by definition, the oriented identity component, so basis-set preservation transfers verbatim from the concrete statement.

10.3 Haag Kastler Axioms

With that out of the way we can state the axioms. Each axiom below is presented as a definition so that it is captured as a node in the blueprint declaration graph. In the Lean formalization each axiom corresponds to a Prop-valued predicate (or, in the case of Local Algebras, a data field), and the bundling structure HaagKastlerNet packages them together (see 87). Downstream theorems take an instance of HaagKastlerNet as a hypothesis and invoke each axiom as a projection.

Definition 80 Axiom 1: Local Algebras

✓

For any basis element $\mathbf{B}$ of the Alexandrov topology on Minkowski spacetime, i.e. any set of the form $I^+(p) \cap I^-(q)$, there is a corresponding abstract C*-algebra $\mathfrak {U}(\mathbf{B})$

\begin{align} \mathbf{B} \longmapsto \mathfrak {U}(\mathbf{B}), \end{align}

and when $\mathbf{B}$ is the empty set, we have the distinguished correspondence

\begin{align} \emptyset \longmapsto \mathbb {C} \mathbf{1}, \end{align}

where $\mathbf{1}$ is the multiplicative identity in the abstract C*-algebra $\mathbb {C} \mathbf{1}$.

Definition 81 Axiom 2: Isotony

✓

Let $\mathbf{B}_1$ and $\mathbf{B}_2$ be any two basis elements of the Alexandrov topology on Minkowski spacetime, i.e. any two sets of the form $I^+(p_1) \cap I^-(q_1)$ and $I^+(p_2) \cap I^-(q_2)$.

If $\mathbf{B}_1 \subset \mathbf{B}_2$ then $\mathfrak {U}(\mathbf{B}_1) \subset \mathfrak {U}(\mathbf{B}_2)$, where inclusion is implemented by

\begin{align} i : \mathfrak {U}(\mathbf{B}_1) \hookrightarrow \mathfrak {U}(\mathbf{B}_2), \end{align}

a unital *-monomorphism.

Before introducing the next axiom, we must introduce the definition:

Definition 82 Quasilocal Algebra

✓

Consider the set-theoretic union of all $\mathfrak {U}(\mathbf{B})$. As previously proven, this set-theoretic union is a normed *-algebra. Also, as previously proven, taking its completion one obtains a C*-algebra denoted as $\mathfrak {U}$. This C*-algebra $\mathfrak {U}$ is called the quasilocal algebra.

Definition 83 Axiom 3: Local Commutativity

✓

If $\mathbf{B_1}$ and $\mathbf{B_2}$ are completely spacelike, then $\mathfrak {U}(\mathbf{B_1})$ and $\mathfrak {U}(\mathbf{B_2})$ commute in the quasilocal algebra $\mathfrak {U}$, i.e. for any $a_1$ in $\mathfrak {U}(\mathbf{B_1})$ and $a_2$ in $\mathfrak {U}(\mathbf{B_2})$ it follows that

\begin{align} i(a_1) i(a_2) - i(a_2) i(a_1) = 0 \end{align}

in the quasilocal algebra $\mathfrak {U}$.

The next axiom makes use of the following new definition:

Definition 84 Quasilocal Observable

✓

The image $\pi _\omega (a)$ of a self-adjoint member $a$ of the quasilocal algebra $\mathfrak {U}$ under a GNS *-homomorphism $\pi _\omega $ is self-adjoint and thus corresponds to an “observable”. Any “observable” corresponding to such a self-adjoint $\pi _\omega (a)$ is called a quasilocal observable.

Definition 85 Axiom 4: Quasilocal Completeness

✓

All “observables” are quasilocal observables.

Definition 86 Axiom 5: Lorentz Covariance

✓

Let $\mathbf{B}$ be any basis element of the Alexandrov topology on Minkowski spacetime, i.e. any set of the form $I^+(p) \cap I^-(q)$.

A member $L$ of the inhomogeneous Lorentz group connected to the identity acts on $\mathfrak {U}(\mathbf{B})$ as follows

\begin{align} \alpha _L : \mathfrak {U}(\mathbf{B}) & \longrightarrow \mathfrak {U}(L\mathbf{B}) \\ a & \longmapsto \alpha _L(a) \end{align}

where $L\mathbf{B}$ is the image of the region $\mathbf{B}$ under the transformation $L$ and $\alpha _L$ is a unital *-isomorphism generated by $L$. The map $\alpha _L$ is such that (1) for the identity element $\mathbf{1}$ of the Lorentz group it satisfies

\begin{align} \alpha _{\mathbf{1}}(a) = a, \end{align}

(2) for all appropriate $a$, $L$, and $L'$ it satisfies

\begin{align} \alpha _{L' \cdot L}(a) = \alpha _{L'}(\alpha _{L}(a)), \end{align}

and (3) for basis elements $\mathbf{B}_\iota \subset \mathbf{B}_\kappa $ and the unital *-monomorphism $i$ of Axiom 2 (Isotony) $\alpha _L$ commutes with $i$. In other words the following diagram

$\begin{tikzcd} \mathfrak{U}(\mathbf{B}_\kappa) \arrow[r, "\alpha_L"] & \mathfrak{U}(L\mathbf{B}_\kappa) \\ \mathfrak{U}(\mathbf{B}_\iota) \arrow[r, "\alpha_L"] \arrow[u, "i"] & \mathfrak{U}(L\mathbf{B}_\iota) \arrow[u, "i"] \end{tikzcd}$

commutes.

Definition 87 Haag-Kastler Net

✓

A Haag-Kastler net on Minkowski spacetime is the bundling of the data of 80 together with the properties of 81, 83, 85, and 86. In the Lean formalization this is a single structure whose fields are the assignment $\mathbf{B} \mapsto \mathfrak {U}(\mathbf{B})$ and proofs that this assignment satisfies the four remaining axioms. Theorems about AQFT take an instance of this structure as a hypothesis and invoke each axiom as a projection.

This concludes the presentation of the “sharpened” axioms. As proven in this blog post, these “sharpened” axioms entail the original axioms save Axiom 6 (Primitivity), which is an axiom that we abandon.

These “sharpened” axioms also allow for a straightforward generalization to a set of axioms describing AQFT in curved spacetime, i.e. a set of axioms describing AQFT in a curved spacetime background that is fixed and treated classically. In a subsequent blog post we will detail these axioms.

10.3.1 Einstein Causality

Local commutativity (83) is an algebraic statement about the quasilocal algebra. Its physical content - that spacelike-separated measurements do not interfere - is its operator form: in any representation of the quasilocal algebra, spacelike-separated local observables commute as bounded operators on the Hilbert space.

Theorem 88 Einstein Causality in a Representation

✓

Let $\pi $ be any $*$-representation of the quasilocal algebra on a Hilbert space $H$. If $\mathbf{B}_1, \mathbf{B}_2$ are completely spacelike-separated basis regions, then for all $a \in \mathfrak {U}(\mathbf{B}_1)$ and $b \in \mathfrak {U}(\mathbf{B}_2)$ the operators $\pi (\iota _{\mathbf{B}_1} a)$ and $\pi (\iota _{\mathbf{B}_2} b)$ commute. This is the image under $\pi $ of the local commutativity relation (83); since the GNS representation of any state is such a $\pi $, spacelike-separated local observables commute on every GNS Hilbert space.

10.3.2 Local von Neumann Algebras

The abstract C*-algebras $\mathfrak {U}(\mathbf{B})$ are a stepping stone; the genuine object of algebraic quantum field theory is the net of von Neumann algebras they generate in a representation. Given a $*$-representation $\pi $ of the quasilocal algebra on a Hilbert space $H$, the local von Neumann algebra of a region $\mathbf{B}$ is the bicommutant $R(\mathbf{B}) = \pi (\mathfrak {U}(\mathbf{B}))''$ of the local observable operators. We model the commutant by the centralizer in $\mathcal{B}(H)$.

Definition 89 Local von Neumann Algebra

✓

Let $\pi $ be a $*$-representation of the quasilocal algebra on $H$. The local observable operators of a region $\mathbf{B}$ are the image $\pi (\mathfrak {U}(\mathbf{B})) = \{ \pi (\iota _{\mathbf{B}} a) : a \in \mathfrak {U}(\mathbf{B})\} $. The local von Neumann algebra $R(\mathbf{B})$ is the bicommutant $\pi (\mathfrak {U}(\mathbf{B}))''$.

Definition 90 $R(\mathbf{B})$ as a von Neumann Algebra

✓

The local algebra $R(\mathbf{B})$ is registered as a genuine VonNeumannAlgebra (Mathlib’s bundled structure), not merely a set of operators. The general fact is that the bicommutant $S''$ of any self-adjoint set $S$ of bounded operators is a von Neumann algebra: $S'$ is a $*$-subalgebra (the centralizer of a self-adjoint set is $*$-closed), and $S'' = S''''$ since the triple commutant collapses. The local observable operators $\pi (\mathfrak {U}(\mathbf{B}))$ are self-adjoint ($\pi $ and $\iota $ are $*$-homomorphisms), so $R(\mathbf{B}) = \pi (\mathfrak {U}(\mathbf{B}))''$ is a von Neumann algebra whose underlying set is the bicommutant of 89.

Theorem 91 Microcausality at the von Neumann Level

✓

For completely spacelike-separated basis regions $\mathbf{B}_1, \mathbf{B}_2$, the local von Neumann algebras commute: $R(\mathbf{B}_1) \subseteq R(\mathbf{B}_2)'$. This is the von Neumann form of Einstein causality (88): elementwise commutation $\pi (\mathfrak {U}(\mathbf{B}_2)) \subseteq \pi (\mathfrak {U}(\mathbf{B}_1))'$, with the antitonicity of the commutant and the identity $S''' = S'$ collapsing the iterated commutants. A Haag-Kastler net is thus a net of mutually commuting von Neumann algebras for spacelike regions.

Theorem 92 Isotony of the von Neumann Net

✓

For basis regions $\mathbf{B}_1 \subseteq \mathbf{B}_2$, the local von Neumann algebras are nested: $R(\mathbf{B}_1) \subseteq R(\mathbf{B}_2)$. The local observables of $\mathbf{B}_1$ embed into those of $\mathbf{B}_2$ via the quasilocal isotony coherence, and the double commutant is monotone.

Theorem 93 Bundled von Neumann Microcausality and Isotony

✓

Phrased on the bundled VonNeumannAlgebra $R(\mathbf{B})$ with its order $\le $ and Mathlib’s commutant: for completely spacelike-separated regions $R(\mathbf{B}_1) \le R(\mathbf{B}_2)'$, and for $\mathbf{B}_1 \subseteq \mathbf{B}_2$, $R(\mathbf{B}_1) \le R(\mathbf{B}_2)$. Both reduce to the set-level statements through the coercion $\uparrow R(\mathbf{B}) = \pi (\mathfrak {U}(\mathbf{B}))''$.

Definition 94 The Net of von Neumann Algebras

✓

Packaging isotony, the assignment $\mathbf{B} \mapsto R(\mathbf{B})$ is an order-preserving map from the poset of basis regions (ordered by inclusion) to the von Neumann algebras of $\mathcal{B}(H)$. This realizes the net as a functor on the inclusion poset: containment of regions is sent to containment of algebras. It is the central object of the algebraic approach.

Theorem 95 Statistical Independence (Schlieder Property)

✓

If $\Omega $ is cyclic for the local observables of $\mathbf{B}_1$, then for a spacelike-separated region $\mathbf{B}_2$ every $R \in R(\mathbf{B}_2)$ with $R\Omega = 0$ is zero, so $\Omega $ is separating for $R(\mathbf{B}_2)$. The implication is elementary ($R$ vanishes on the dense set of vectors $A\Omega $ for $A$ a local observable of $\mathbf{B}_1$, since $R(\mathbf{B}_2)$ commutes with those observables by microcausality, 91). In Minkowski spacetime the cyclicity hypothesis is exactly the content of the Reeh-Schlieder theorem, which rests on the spectrum condition; here it is taken as an explicit hypothesis, mirroring the curved-spacetime version where no spectrum condition is available.

Theorem 96 Statistical Independence, bundled

✓

The separating property phrased on the bundled VonNeumannAlgebra $R(\mathbf{B}_2)$: with $\Omega $ cyclic for the local observables of $\mathbf{B}_1$, every $R$ in the bundled algebra $R(\mathbf{B}_2)$ of a spacelike-separated region with $R\Omega = 0$ is zero. It reduces to 95 through the coercion $\uparrow R(\mathbf{B}_2) = \pi (\mathfrak {U}(\mathbf{B}_2))''$.

Theorem 97 Additive-Free Locality via the Spacelike Complement

✓

Locality expressed through the spacelike complement, without attaching any algebra to the unbounded complement: for basis sets $\mathbf{B}' \subseteq \mathbf{B}^\perp $, the local von Neumann algebra $R(\mathbf{B}')$ lies in the commutant $R(\mathbf{B})'$. It is a direct repackaging of bundled microcausality (93) through the Galois bridge $\mathbf{B}' \subseteq \mathbf{B}^\perp \iff \mathbf{B}', \mathbf{B}$ completely spacelike, staying strictly within the physically local (bounded, diamond) regions. No local algebra is ever attached to the unbounded complement.

Theorem 98 Geometric Covariance of the von Neumann Net

✓

In a covariant representation $\pi $ of the quasilocal algebra with the operator covariance $U(L)\, \pi (a)\, U(L)^{-1} = \pi (\beta _L a)$, conjugation by the implementing unitary $U(L)$ carries the local von Neumann algebra of a region $\mathbf{B}$ onto that of the Lorentz-transformed region $L \cdot \mathbf{B}$:

\[ U(L)\, R(\mathbf{B})\, U(L)^{-1} = R(L \cdot \mathbf{B}). \]

This is the statement that the symmetry group acts geometrically on the net of von Neumann algebras. The proof rests on three ingredients, all already available: operator covariance (the last clause of 146); the fact that $\beta _L = $ the covariance action sends $\iota _{\mathbf{B}}(\mathfrak {U}(\mathbf{B}))$ onto $\iota _{L\cdot \mathbf{B}}(\mathfrak {U}(L\cdot \mathbf{B}))$ (from the action-on-generators identity and surjectivity of the covariance equivalence $\alpha _L$); and the algebraic fact that conjugation by a unit is a multiplicative automorphism, which therefore commutes with the bicommutant. The reusable core is that a multiplicative automorphism maps the centralizer of a set onto the centralizer of its image, hence maps bicommutants to bicommutants. In particular $R(\mathbf{B})$ and $R(L \cdot \mathbf{B})$ are unitarily equivalent (conjugate by $U(L)$), so any unitary-conjugation-invariant property of a local von Neumann algebra — such as being a factor — is constant along the Lorentz orbit of a region.

Theorem 99 Orbit-Invariance of Factoriality

✓

If the local von Neumann algebra $R(\mathbf{B})$ is a factor (its center $R(\mathbf{B}) \cap R(\mathbf{B})'$ is exactly the scalars), then so is $R(L \cdot \mathbf{B})$ for every Lorentz transformation $L$. Geometric covariance (98) exhibits $R(L \cdot \mathbf{B}) = U(L) R(\mathbf{B}) U(L)^{-1}$; conjugation by a unitary is a multiplicative automorphism that carries the center onto the center and fixes the scalars, so it preserves the factor property. Thus being a factor is constant along the Lorentz orbit of a region.

Theorem 100 Geometric Covariance as a von Neumann Algebra Isomorphism

✓

The geometric-covariance set equality is upgraded to a first-class $*$-algebra isomorphism of the bundled local von Neumann algebras, $R(\mathbf{B}) \cong R(L \cdot \mathbf{B})$. It is the restriction of the conjugation $*$-automorphism $T \mapsto U(L) T U(L)^{-1}$ of $\mathcal{B}(H)$ (Mathlib’s conjStarAlgEquiv, whose adjoint-is-inverse property makes conjugation by a unitary star-preserving) to $R(\mathbf{B})$, whose image is exactly $R(L \cdot \mathbf{B})$. The reusable ingredient is that a $*$-automorphism carrying the underlying set of one star-subalgebra onto another restricts to a star-algebra equivalence between them. This makes the unitary equivalence of orbit-related local algebras an explicit transportable object.

10.3.3 Irreducibility and Schur’s Lemma

A representation is irreducible when its commutant is trivial: the only operators commuting with every $\pi (a)$ are scalars. This is the von Neumann (commutant) form of irreducibility. The cornerstone, connecting the commutant to the GNS state, is the topological Schur lemma for a cyclic representation.

Definition 101 Irreducible Representation

✓

A $*$-representation $\pi : A \to \mathcal{B}(H)$ is irreducible if every bounded operator $T$ commuting with all $\pi (a)$ is a scalar multiple of the identity, $T = c \cdot 1$.

Theorem 102 Topological Schur Lemma

✓

Let $\Omega $ be a cyclic vector for $\pi $. If $T$ commutes with every $\pi (a)$ and the diagonal coefficient $a \mapsto \langle \Omega , T\, \pi (a)\Omega \rangle $ equals $c$ times $a \mapsto \langle \Omega , \pi (a)\Omega \rangle $, then $T = c \cdot 1$. The proof is pure Hilbert-space analysis: using the $*$-representation property and the commutation relation, every off-diagonal coefficient $\langle \pi (b)\Omega , (T - c)\, \pi (a)\Omega \rangle $ vanishes, so $(T - c)$ annihilates the dense cyclic orbit and is therefore zero.

Theorem 103 Commutant Scalar iff Proportional Coefficient

✓

In a cyclic representation reproducing a state $\omega $, an operator $T$ commuting with all $\pi (a)$ is a scalar multiple of the identity if and only if its diagonal coefficient $a \mapsto \langle \Omega , T\, \pi (a)\Omega \rangle $ is a scalar multiple of $\omega $. This is the precise operator-theoretic bridge to purity: irreducibility (every commutant element is scalar) is exactly the statement that every commutant coefficient is proportional to $\omega $.

Definition 104 Pure State

✓

A state $\omega $ is pure if every positive linear functional $\psi $ dominated by $\omega $ (that is, $0 \le \psi (a^*a) \le \omega (a^*a)$ for all $a$) is a scalar multiple of $\omega $. This order-theoretic characterization is the extreme-point notion of purity, phrased to avoid convex-combination and normalization bookkeeping.

One direction of the classical equivalence “$\omega $ pure $\iff $ GNS representation irreducible” is established below.

Theorem 105 Pure Implies Irreducible

✓

If $\omega $ is pure, then any cyclic representation reproducing $\omega $ (in particular its GNS representation) is irreducible. Since the commutant is $*$-closed, a commuting operator decomposes into self-adjoint real and imaginary parts; for a self-adjoint commuting $S$, the affine rescaling $T = (2(\Vert S\Vert +1))^{-1} S + \tfrac 12$ satisfies $0 \le T \le 1$, so its coefficient functional $a \mapsto \langle \Omega , T\, \pi (a)\Omega \rangle $ is positive and dominated by $\omega $. Purity forces it proportional to $\omega $, whence $T$ (and so $S$, and so the original operator) is a scalar by 103.

The converse, irreducible $\Rightarrow $ pure, requires the other half of the GNS Radon-Nikodym correspondence: that every dominated positive functional $\psi \le \omega $ is represented by an operator $T$ in the commutant, via the bounded sesquilinear form $(\pi (a)\Omega , \pi (b)\Omega ) \mapsto \psi (a^* b)$. The analytic crux is that this form is well-defined and bounded.

Theorem 106 The GNS Radon-Nikodym Form is Bounded

✓

For a positive functional $\psi $ dominated by the state $\omega $ in its cyclic GNS representation, the form values obey $\Vert \psi (a^* b)\Vert \le \Vert \pi (a)\Omega \Vert \, \Vert \pi (b)\Omega \Vert $. This follows from the Cauchy-Schwarz inequality for $\psi $, the domination $\psi \le \omega $, and the reproducing identity $\omega (x^* x) = \Vert \pi (x)\Omega \Vert ^2$. In particular the form depends only on the GNS vectors $\pi (a)\Omega , \pi (b)\Omega $, not on the representatives $a, b$, so it is well-defined on the cyclic subspace.

Theorem 107 The GNS Radon-Nikodym Operator

✓

The bounded form of 106 is the inner product of an operator $T$ on the GNS space: extending the densely-defined bounded form by the Fréchet-Riesz representation and a norm-controlled dense extension yields $T$ with $\langle \pi (a)\Omega , T\, \pi (b)\Omega \rangle = \psi (a^* b)$. From this reproducing identity, $T$ commutes with every $\pi (c)$ (an adjoint computation on the dense cyclic vectors), and $\psi (a) = \langle \Omega , T\, \pi (a)\Omega \rangle $ (taking $a = 1$ in the first slot).

Theorem 108 Pure $\iff $ Irreducible

✓

A state $\omega $ is pure if and only if its cyclic GNS representation is irreducible. For the converse direction, given a dominated $\psi $, its Radon-Nikodym operator $T$ commutes with $\pi $, so by irreducibility $T = c \cdot 1$; the reproducing identity then gives $\psi (a) = c\, \omega (a)$, so $\psi $ is a scalar multiple of $\omega $ and $\omega $ is pure.

Irreducibility has a von Neumann algebraic reading: the representation generates a factor.

Theorem 109 An Irreducible Representation Generates a Factor

✓

The von Neumann algebra $\pi (A)''$ generated by an irreducible representation has trivial center: an operator lies in the center $\pi (A)'' \cap (\pi (A)'')'$ if and only if it is a scalar multiple of the identity. Indeed the center is contained in $(\pi (A)'')' = \pi (A)'$ (the triple commutant collapses to the single one), which irreducibility makes the scalars; conversely scalars are central.

Theorem 110 Irreducibility $\iff $ Generating $\mathcal{B}(H)$

✓

A representation is irreducible if and only if the von Neumann algebra $\pi (A)''$ it generates is all of $\mathcal{B}(H)$: $\pi (A)'' = \mathcal{B}(H)$. For the forward direction, irreducibility makes the commutant $\pi (A)'$ exactly the scalars, and the centralizer of the scalars is everything (every bounded operator commutes with $c \cdot 1$), so $\pi (A)'' = (\text{scalars})' = \mathcal{B}(H)$. The converse uses that $\mathcal{B}(H)$ is a central $\mathbb {C}$-algebra (its center is the scalars): if the bicommutant is everything, every operator commutes with the commutant, so any operator commuting with $\pi (A)$ is central, hence scalar. This is the density (bicommutant-theorem) form of irreducibility, sharpening the factor statement 109.

Theorem 111 Bundled Density Form of Irreducibility

✓

The von Neumann algebra $\pi (A)''$ generated by a representation is bundled as a first-class VonNeumannAlgebra (gnsVonNeumannAlgebra), the image $\pi (A)$ being self-adjoint. For an irreducible representation, this bundled algebra is all of $\mathcal{B}(H)$: its underlying set is everything, and equivalently it is the greatest von Neumann algebra on $H$ (every $S$ satisfies $S \le \pi (A)''$). This is the bundled counterpart of 110. Mathlib’s VonNeumannAlgebra carries no lattice $\top $, so the literal $\pi (A)'' = \top $ is phrased at the level of the underlying set together with the greatest-element statement under the existing $\le $.

Theorem 112 The GNS Representation of a Pure State is a Factor

✓

For a pure state $\omega $ there is a cyclic GNS triple $(H, \pi , \Omega )$ reproducing $\omega $ whose generated von Neumann algebra $\pi (A)''$ has trivial center, i.e. is a factor. This combines the GNS construction, purity $\Rightarrow $ irreducibility (108), and 109. It applies verbatim to the quasilocal algebra $\mathfrak {U}$ and to each local algebra $\mathfrak {U}(\mathbf{B})$, since both are C*-algebras.

Theorem 113 The GNS Representation of a Pure State Generates $\mathcal{B}(H)$

✓

The density (bicommutant-theorem) sharpening of 112: for a pure state $\omega $ there is a cyclic GNS triple $(H, \pi , \Omega )$ reproducing $\omega $ whose generated von Neumann algebra is all of $\mathcal{B}(H)$, $\pi (A)'' = \mathcal{B}(H)$. It combines the GNS construction, purity $\Rightarrow $ irreducibility (108), and the density form 110. As with the factor statement, it applies verbatim to the quasilocal algebra $\mathfrak {U}$ and to each local algebra $\mathfrak {U}(\mathbf{B})$.

The order-theoretic definition of purity (104) coincides with the convex-geometric one: $\omega $ is an extreme point of the state space. The analytic key is the normalization identity for positive functionals.

Theorem 114 Norm of a Positive Functional

✓

For a positive linear functional $\varphi $ on a unital C*-algebra, $\Vert \varphi \Vert = \mathrm{Re}\, \varphi (1)$. The bound $\mathrm{Re}\, \varphi (1) \le \Vert \varphi \Vert $ is immediate from $\Vert 1\Vert = 1$; conversely Cauchy-Schwarz with the first slot equal to $1$ gives $\Vert \varphi (b)\Vert ^2 \le \mathrm{Re}\, \varphi (1)\cdot \mathrm{Re}\, \varphi (b^* b) \le \mathrm{Re}\, \varphi (1)\cdot \Vert \varphi \Vert \, \Vert b\Vert ^2$, whence $\Vert \varphi \Vert ^2 \le \mathrm{Re}\, \varphi (1)\cdot \Vert \varphi \Vert $. In particular every state satisfies $\omega (1) = 1$.

Definition 115 Extreme Point of the State Space

✓

A state $\omega $ is an extreme point of the (convex) state space if it is not a nontrivial convex combination of two distinct states: whenever $\omega = t\, \omega _1 + (1-t)\, \omega _2$ with $0 {\lt} t {\lt} 1$ and $\omega _1, \omega _2$ states, then $\omega _1 = \omega _2$.

Theorem 116 Pure $\iff $ Extreme Point

✓

A state $\omega $ is pure if and only if it is an extreme point of the state space. If $\omega $ is pure and $\omega = t\, \omega _1 + (1-t)\, \omega _2$, then $t\, \omega _1$ is a positive functional dominated by $\omega $, hence (by purity) a scalar multiple of $\omega $; evaluating at $1$, where every state gives $1$, pins the scalar to $t$ and forces $\omega _1 = \omega = \omega _2$. Conversely, if $\omega $ is extreme and $\psi \le \omega $ is dominated, set $\lambda = \mathrm{Re}\, \psi (1) \in [0,1]$; for $\lambda \in (0,1)$ the rescaled functionals $\lambda ^{-1}\psi $ and $(1-\lambda )^{-1}(\omega - \psi )$ are states (normalized via 114) whose convex combination is $\omega $, so extremality identifies them and forces $\psi = \lambda \, \omega $; the boundary cases $\lambda = 0$ and $\lambda = 1$ give $\psi = 0$ and $\psi = \omega $ respectively.

Theorem 117 State-Space Convexity and the Extreme-Point Bridge

✓

Realizing the state space as the subset $\mathrm{stateSpace}(A) \subseteq A \to _L \mathbb {C}$ (the latter a real topological vector space via $\texttt{NormedSpace.complexToReal}$), it is convex: a real convex combination $a\, \omega _1 + b\, \omega _2$ of states is again a state, via $\texttt{State.convexCombo}$. Moreover a state $\omega $ lies in Mathlib’s $\mathrm{extremePoints}_{\mathbb {R}}$ of the state space exactly when it is extreme in the sense of 115, connecting the purity characterizations to the Krein-Milman/Choquet API.

Theorem 118 Weak-* Compactness of the State Space

✓

The state space, realized inside the weak-* dual $\mathrm{WeakDual}\, \mathbb {C}\, A$ as the positive functionals with $\varphi (1) = 1$, is weak-* compact. By Banach-Alaoglu it suffices that it is a weak-* closed subset of the closed unit ball: the positivity conditions $0 \le \varphi (a^* a)$ and the normalization $\varphi (1) = 1$ are each weak-* closed (evaluation at a fixed element is weak-* continuous), and a positive functional with $\varphi (1)=1$ has $\| \varphi \| = 1$. This is the analytic input for the existence of pure states via Krein-Milman.

These equivalences specialize to the quasilocal algebra $\mathfrak {U}$ of a Minkowski net, where they characterize purity of a global state - the natural setting for the vacuum and other distinguished states.

Theorem 119 Pure $\iff $ Extreme Point on the Quasilocal Algebra

✓

A state $\omega $ on the canonical quasilocal algebra $\mathfrak {U}$ of a Haag-Kastler net is pure if and only if it is an extreme point of the state space of $\mathfrak {U}$. This is the abstract equivalence 116 applied to the C*-algebra $\mathfrak {U}$.

Theorem 120 Pure $\iff $ Irreducible GNS on the Quasilocal Algebra

✓

For a state $\omega $ on the quasilocal algebra $\mathfrak {U}$ there is a GNS triple $(H, \pi , \Omega )$ reproducing $\omega $ in which $\omega $ is pure if and only if the representation $\pi $ is irreducible. This combines the GNS construction with the abstract 108.

10.3.4 Unitary Equivalence and Superselection

The comparison of representations is the entry point to superselection theory. For $*$-representations $\pi : A \to \mathcal{B}(H)$ of a C*-algebra — in particular of the quasilocal algebra $\mathfrak {U}$ or a local algebra $\mathfrak {U}(\mathbf{B})$ — we record three successively coarser notions of sameness (unitary equivalence, quasi-equivalence, and the negation of the finest, disjointness) and the representation-theoretic invariants they preserve.

Definition 121 Unitary Equivalence of Representations

✓

Two $*$-representations $\pi _1 : A \to \mathcal{B}(H_1)$ and $\pi _2 : A \to \mathcal{B}(H_2)$ are unitarily equivalent when there is an isometric isomorphism $U : H_1 \simeq H_2$ of the underlying Hilbert spaces intertwining them: $U(\pi _1(a)\, x) = \pi _2(a)(U x)$. This is an equivalence relation — reflexive, symmetric, and transitive.

Theorem 122 Irreducibility and Factoriality are Unitary Invariants

✓

Unitarily equivalent representations share their representation-theoretic type: $\pi _1$ is irreducible if and only if $\pi _2$ is, and the generated von Neumann algebra $\pi _1(A)''$ is a factor if and only if $\pi _2(A)''$ is. The transport is packaged through the cross-space conjugation $T \mapsto U T U^{-1}$, a multiplicative isomorphism $\mathcal{B}(H_1) \simeq \mathcal{B}(H_2)$ that carries $\pi _1(A)$ onto $\pi _2(A)$, centralizers onto centralizers, and scalars onto scalars; irreducibility (commutant equal to the scalars) and factoriality (trivial center of $\pi (A)''$) are then preserved.

Definition 123 Disjoint Representations

✓

An intertwiner $T : H_1 \to H_2$ between $\pi _1$ and $\pi _2$ satisfies $T(\pi _1(a)\, x) = \pi _2(a)(T x)$; intertwiners are closed under sums, scalars, composition, and the adjoint (the adjoint of a $\pi _1 \to \pi _2$ intertwiner is a $\pi _2 \to \pi _1$ intertwiner). Two representations are disjoint when the only intertwiner between them is $0$. Disjointness is symmetric (take adjoints), and a representation on a nonzero Hilbert space is never disjoint from itself; more generally, unitarily equivalent representations on nonzero spaces are never disjoint, since the implementing unitary is a nonzero intertwiner.

Definition 124 Quasi-Equivalence of Representations

✓

Two representations are quasi-equivalent when there is a $*$-isomorphism of their generated von Neumann algebras $\pi _1(A)'' \simeq \pi _2(A)''$ carrying $\pi _1(a)$ to $\pi _2(a)$. This is an equivalence relation, and it is coarser than unitary equivalence: unitary equivalence implies quasi-equivalence, because the conjugation $*$-isomorphism $T \mapsto U T U^{-1}$ restricts to a $*$-isomorphism of the generated von Neumann algebras.

Theorem 125 Schur’s Lemma and the Irreducible Dichotomy

✓

A nonzero intertwiner $T$ between two irreducible representations rescales to a unitary equivalence: $T^\ast T$ commutes with $\pi _1$, hence is a positive scalar $r \cdot 1$ with $r {\gt} 0$, so $(\sqrt r)^{-1}\, T$ is a linear isometry; and $T T^\ast $ is a nonzero scalar (irreducibility of $\pi _2$), which makes $T$ surjective, so the isometry is a unitary. Consequently two irreducible representations are either disjoint or unitarily equivalent — the foundational trichotomy of superselection theory, identifying sectors with unitary-equivalence classes of irreducible representations.

Lemma 126 Schur Multiplicity

✓

The space of intertwiners between two irreducible representations is at most one-dimensional: any two intertwiners $S, T$ with $S \neq 0$ are proportional, $T = \lambda \cdot S$. Indeed $S^\ast S = a\cdot 1$ and $S^\ast T = b \cdot 1$ (commuting with $\pi _1$, hence scalar), and $S S^\ast = c \cdot 1$ with $c \neq 0$ (irreducibility of $\pi _2$) makes $S^\ast $ injective; since $S^\ast \big(T - (b/a)\, S\big) = 0$, injectivity gives $T = (b/a)\, S$. So irreducible representations intertwine multiplicity-free.

Lemma 127 Endomorphism Algebra of an Irreducible Representation

✓

The endomorphism algebra of an irreducible representation is $\mathbb {C}\cdot 1$: every self-intertwiner of an irreducible representation is a scalar multiple of the identity. This is the commutant form of irreducibility read through the intertwiner language, and it identifies each irreducible sector with a simple (one-dimensional-centred) object.

Theorem 128 The commutant (self-intertwiner) von Neumann algebra

✓

The commutant $\pi (A)'$ of a representation is packaged as a von Neumann algebra — the algebra of self-intertwiners, i.e. the intertwiner/gauge algebra of $\pi $. Its underlying set is the centralizer of $\pi (A)$ (self-adjoint, and a commutant is always a von Neumann algebra since $S''' = S'$), an operator lies in it exactly when it is a self-intertwiner of $\pi $, and $\pi $ is irreducible if and only if this algebra is trivial ($\pi (A)' = \mathbb {C}\cdot 1$) — the von Neumann form of Schur’s lemma.

Theorem 129 Double-Commutant Duality

✓

The generated von Neumann algebra $\pi (A)''$ and the commutant von Neumann algebra $\pi (A)'$ (128) are each other’s commutants. On one side, the commutant of $\pi (A)''$ is $\pi (A)'$: this is an instance of the triple-commutant collapse $S''' = S'$ applied to the self-adjoint image $\pi (A)$. On the other side, the commutant of $\pi (A)'$ is $\pi (A)''$, which is exactly the definition of the bicommutant. Together these are von Neumann’s double-commutant relation for this pair, and they exhibit the bicommutant as idempotent: taking the commutant twice returns $(\pi (A)'')'' = \pi (A)''$, so $\pi (A)''$ and $\pi (A)'$ form a mutually dual pair under $S \mapsto S'$.

Theorem 130 A Factor and its Commutant; Triviality Duality

✓

A von Neumann algebra and its commutant share the same center: the intersection $\pi (A)'' \cap (\pi (A)'')' = \pi (A)'' \cap \pi (A)'$ is symmetric under the duality of 129, being simultaneously the center of $\pi (A)''$ and the center of $\pi (A)'$. Consequently $\pi (A)''$ is a factor (trivial center) if and only if its commutant $\pi (A)'$ is a factor. Dually, at the extreme of triviality, the commutant collapses to the scalars $\pi (A)' = \mathbb {C}\cdot 1$ if and only if the generated algebra is everything $\pi (A)'' = \mathcal{B}(H)$; this is the commutant form of the equivalence “irreducible $\iff $ generates $\mathcal{B}(H)$” (128), passing between the two sides through the bicommutant $(\mathbb {C}\cdot 1)' = \mathcal{B}(H)$.

Theorem 131 The Pure-State Dichotomy

✓

The GNS representations of two pure states are either disjoint or unitarily equivalent. Indeed the GNS representation of a pure state is irreducible (108), so the irreducible dichotomy (125) applies. Pure states thus fall into superselection sectors: the sector of a pure state is the unitary-equivalence class of its irreducible GNS representation.

10.3.5 Direct Sums, Amplification, and Reducibility

Given a family of $*$-representations $\pi _i : A \to \mathcal{B}(H_i)$, their direct sum acts on the $\ell ^2$-direct sum $\bigoplus _i H_i$. This is the construction underlying amplifications and the reducibility of non-primary representations.

Definition 132 Direct-Sum Representation

✓

The direct sum $\bigoplus _i \pi _i : A \to \mathcal{B}(\ell ^2(\iota , H))$ of a family of $*$-representations acts coordinatewise: $(\bigoplus _i \pi _i)(a)$ is the diagonal operator $x \mapsto (\pi _i(a)\, x_i)_i$ on the $\ell ^2$-direct sum. It is a $*$-representation, the diagonal being uniformly bounded by $\Vert a\Vert $ since each $\pi _i$ is contractive.

Theorem 133 Subrepresentations and Commutant of a Direct Sum

✓

Each summand embeds as a subrepresentation: the isometric inclusion $H_j \hookrightarrow \ell ^2(\iota , H)$ intertwines $\pi _j$ with $\bigoplus _i \pi _i$. Moreover the orthogonal projection onto the $j$-th summand lies in the commutant of the direct sum, so each summand is a reducing subspace.

Definition 134 Amplification

✓

The $\iota $-fold amplification $\iota \cdot \pi := \bigoplus _{i : \iota } \pi $ of a single representation is the direct sum of $\iota $ copies of $\pi $; $\pi $ embeds as each summand.

Theorem 135 Reducibility of a Direct Sum

✓

A direct sum with two summands carrying nonzero vectors is reducible. Were $\bigoplus _i \pi _i$ irreducible, every summand projection would be a scalar (its commutant being trivial); but the projection onto one of two nonzero summands is a nontrivial projection, hence not scalar. In particular an amplification $\iota \cdot \pi $ with at least two copies (and $\pi $ acting on a nonzero space) is reducible — the multiplicity is visible in the commutant.

10.3.6 Covariant States and the Covariance Action

The Lorentz covariance of a Haag-Kastler net (86) acts on the net fiberwise, through the $*$-isomorphisms $\alpha _L : \mathfrak {U}(\mathbf{B}) \to \mathfrak {U}(L\cdot \mathbf{B})$. We record two consequences: the notion of a Lorentz-covariant family of local states, and the lift of the fiberwise action to a single dynamical $*$-automorphism of the quasilocal algebra.

Definition 136 Covariant Family of Local States

✓

Given a Haag-Kastler net (87), a covariant family of local states assigns to every region $\mathbf{B}$ a state $\omega _{\mathbf{B}}$ on the local algebra $\mathfrak {U}(\mathbf{B})$ such that, for every Lorentz transformation $L$ and every $a \in \mathfrak {U}(\mathbf{B})$, one has $\omega _{\mathbf{B}}(a) = \omega _{L\cdot \mathbf{B}}(\alpha _L a)$, where $\alpha _L$ is the covariance isomorphism of 86. The local states are thus intertwined by the Lorentz action.

Lemma 137 Composition of Covariance

✓

For a covariant family of local states, the covariance relation composes along the group: $\omega _{\mathbf{B}}(a) = \omega _{L'\cdot (L\cdot \mathbf{B})}\big(\alpha _{L'}(\alpha _L a)\big)$, reflecting the multiplicativity of the Lorentz action.

Definition 138 Quasilocal Covariance Automorphism

✓

A lift of the fiberwise Lorentz action of $L$ to a quasilocal algebra $\mathfrak {U}$ (82) is a $*$-automorphism $\beta _L$ of $\mathfrak {U}$ intertwining the local embeddings $\iota _{\mathbf{B}}$ with the covariance isomorphisms: $\beta _L(\iota _{\mathbf{B}} a) = \iota _{L\cdot \mathbf{B}}(\alpha _L a)$ for every Alexandrov-basis set $\mathbf{B}$.

Lemma 139 Uniqueness of the Quasilocal Lift

✓

Any two lifts of the same $L$ have the same underlying automorphism: they agree on the union of the local images, which is dense in $\mathfrak {U}$, and $*$-automorphisms of a C*-algebra are continuous.

Theorem 140 Existence of the Quasilocal Lift

✓

For a covariance-compatible quasilocal algebra, the fiberwise Lorentz action extends to a $*$-automorphism of $\mathfrak {U}$, so the lift of 138 exists. The intertwiner is defined on the directed union of local images (a dense $*$-subalgebra) and extended by uniform continuity; the inverse is supplied by $L^{-1}$, and the group laws $\beta _{L'L} = \beta _{L'}\circ \beta _L$ and $\beta _{1} = \mathrm{id}$ furnish the two-sided inverse.

Theorem 141 Existence for the Trivial Net

✓

The covariance-compatibility hypothesis is satisfiable: the trivial net’s quasilocal algebra is covariance-compatible (every $*$-automorphism of $\mathbb {C}$ is the identity), so the quasilocal lift exists unconditionally for the trivial net.

Definition 142 Covariant Quasilocal Algebra

✓

A covariant quasilocal algebra bundles a Haag-Kastler net (87), a quasilocal algebra of that net (82), and a proof that the embeddings are covariance-compatible for every Lorentz transformation. On such data the quasilocal lift (138) exists for every $L$ by 140, yielding the covariance action $L \mapsto \beta _L$ on the quasilocal algebra; the trivial net provides an instance. This is the natural home for the covariance dynamics: the compatibility hypothesis of 140 becomes structural data rather than a side condition.

Lemma 143 Group-Action Coherence of the Covariance Automorphism

✓

The covariance action $L \mapsto \beta _L$ of a covariant quasilocal algebra is a genuine action of the Lorentz group by $*$-automorphisms of the quasilocal algebra: $\beta _{\mathbf{1}} = \mathrm{id}$ and $\beta _{L'L} = \beta _{L'} \circ \beta _L$.

Definition 144 Invariant State

✓

A state $\omega $ on the quasilocal algebra of a covariant quasilocal algebra (142) is (Poincaré-)invariant if it is a fixed point of the dual covariance action: $\omega (\beta _L a) = \omega (a)$ for every Lorentz transformation $L$ and observable $a$. This is the invariance condition of a vacuum state; further conditions (e.g. the spectrum condition) are imposed separately.

Theorem 145 GNS Unitary Implementation of an Invariant State

✓

For an invariant state $\omega $, the covariance action is implemented on the GNS Hilbert space by a family of unitaries $U(L)$ satisfying $U(L)\, \pi (a)\Omega = \pi (\beta _L a)\, \Omega $ and $U(L)\Omega = \Omega $. The unitaries are obtained by extending the densely-defined isometry $\pi (a)\Omega \mapsto \pi (\beta _L a)\Omega $ - isometric because $\omega $ preserves the GNS inner product $\langle \pi (a)\Omega , \pi (b)\Omega \rangle = \omega (a^* b)$ - to the whole GNS space.

Combining invariance with purity makes the GNS representation both covariant and irreducible. We emphasise that this is a precursor to a vacuum representation, not a vacuum itself: a genuine vacuum additionally requires the spectrum condition (positivity of the energy-momentum spectrum), which is not imposed - and indeed not expressible - here.

Theorem 146 Irreducible Covariant Representation of a Pure Invariant State

✓

A state $\omega $ on the quasilocal algebra that is both invariant under the covariance action and pure yields a GNS representation that is simultaneously covariant - implemented by a unitary representation $U(L)$ of the inhomogeneous Lorentz group fixing the cyclic vector $\Omega $, with operator covariance $U(L)\, \pi (a)\, U(L)^{-1} = \pi (\beta _L a)$ - and irreducible; in particular it generates all of $\mathcal{B}(H)$ ($\pi (\mathfrak {U})'' = \mathcal{B}(H)$, by 110). This combines the covariant GNS triple of 145 with purity $\Rightarrow $ irreducibility (108). It is a necessary precursor to a vacuum representation; the spectrum condition would be the remaining ingredient.

Definition 147 Positive Energy (bounded-generator scaffold)

✓

A strongly continuous one-parameter unitary group $V : \mathbb {R} \to \mathcal{U}(H)$ has positive energy when its generator is a positive operator: there exists a positive bounded operator $P$ (hence self-adjoint, with non-negative spectrum) such that $V(t) = e^{i t P}$ for all $t$. The positivity of $P$ is the energy-positivity asserted by the spectrum condition. The generator of a physical translation is unbounded, so requiring $P$ bounded is a genuine restriction; the faithful unbounded form requires Stone’s theorem and the theory of unbounded self-adjoint operators, which Mathlib does not yet provide. This is the bounded-generator scaffold.

Theorem 148 Positive-Energy API

✓

Structural properties of the positive-energy condition, all Stone-free. (i) Trivial subgroup: the constant group $t \mapsto \mathrm{id}$ has positive energy, with zero generator. (ii) Uniqueness of the generator: if two bounded generators induce the same one-parameter group, $e^{i t P} = e^{i t Q}$ for all $t$, then $P = Q$ — differentiating at $t = 0$ gives $i P = i Q$; positivity is not needed. Hence the generator witnessing positive energy is unique. (iii) Unitary invariance: if $V$ has positive energy, so does its conjugate $t \mapsto W \circ V(t) \circ W^{-1}$ by a unitary $W$, with generator $W P W^{-1}$ (positive, being the unitary conjugate of $P$); the energy exponential transports via $e^{W A W^{-1}} = W e^{A} W^{-1}$. Physically, the spectrum condition does not depend on the choice of unitary frame. (iv) Strong continuity: a positive-energy group is strongly continuous — $t \mapsto V(t) x$ is continuous for every $x$, since $t \mapsto (i t) P$ is continuous and the operator exponential is continuous. This justifies calling it a strongly continuous one-parameter unitary group.

Definition 149 Vacuum State (generator-parameterized scaffold)

✓

A state $\omega $ on the quasilocal algebra is a vacuum state (relative to a future-timelike-translation predicate) when it is invariant under the covariance action (144) and, in a GNS representation reproducing $\omega $ and implementing the action by unitaries $U(L)$, every future-timelike translation one-parameter subgroup $\gamma $ has positive energy: $t \mapsto U(\gamma (t))$ satisfies 147. This packages the two necessary vacuum conditions — invariance and the spectrum condition — with the spectrum condition entering as the positive-energy hypothesis on the implementing unitaries. The future-timelike-translation predicate is a parameter, to be instantiated once the translation subgroup of the Lorentz group and its causal structure are wired in; the positive-energy condition is the bounded-generator scaffold. Constructing/discharging the spectrum condition for a concrete net is the Stone-gated next layer.

Theorem 150 No-Stone Consequences of a Vacuum State

✓

The conditions a vacuum state satisfies that need neither the spectrum condition nor Stone’s theorem. First, a vacuum state is invariant (the first conjunct of the definition). Second, a pure vacuum state yields the irreducible covariant GNS representation of 146: a covariant GNS triple with implementing unitaries $U(L)$ fixing $\Omega $ and operator covariance $U(L)\pi (a)U(L)^{-1} = \pi (\beta _L a)$, whose representation is irreducible and generates all of $\mathcal{B}(H)$. Both follow by projecting to invariance and chaining with purity $\Rightarrow $ irreducibility; the spectrum-condition content of the vacuum is not used.

Definition 151 Future-Timelike Translation Subgroup

✓

The pure translations of the inhomogeneous Lorentz group: an element is a pair $(\text{linear}, \text{translation})$, and a pure translation $\mathrm{translationSub}(n) = (\mathrm{id}, n)$ has trivial linear part, so $n \mapsto (\mathrm{id}, n)$ embeds the additive group of the spacetime carrier ($\mathrm{translationSub}(0) = 1$, $\mathrm{translationSub}(n+m) = \mathrm{translationSub}(n)\, \mathrm{translationSub}(m)$). The one-parameter translation flow in a direction $n$ is $\mathrm{translationFlow}(n)(t) = (\mathrm{id}, t \cdot n)$, which is a one-parameter subgroup. A one-parameter subgroup $\gamma $ is a future-timelike translation when $\gamma = \mathrm{translationFlow}(n)$ for some future-pointing timelike $n$ — i.e. $n$ lies in the forward Minkowski cone at the origin. This wires in the translation subgroup and its causal structure, giving the concrete predicate with which the abstract future-timelike-translation parameter of 149 is discharged.

Definition 152 Vacuum State with the Concrete Spectrum Condition

✓

The vacuum-state condition of 149 with its future-timelike-translation parameter fixed to the concrete predicate 151: the spectrum condition is imposed on exactly the one-parameter translation subgroups $t \mapsto (\mathrm{id}, t \cdot n)$ with $n$ future-pointing timelike. The vacuum definition then depends on no free predicate. Invariance and (for a pure state) the irreducible covariant representation follow as in 150, since the concrete form unfolds to the parameterized one.

Theorem 153 Purity is Covariance-Invariant

✓

Purity is preserved by any $*$-automorphism: for $\Phi : \mathfrak {U} \xrightarrow {\sim } \mathfrak {U}$, the pullback state $\omega \circ \Phi $ is pure if and only if $\omega $ is. A dominated positive functional $\psi \le \omega \circ \Phi $ transports to $\psi \circ \Phi ^{-1} \le \omega $, which purity sends to a scalar multiple of $\omega $; transporting back gives $\psi $ proportional to $\omega \circ \Phi $. Applied to the covariance automorphism $\Phi = \beta _L$, this says purity of a state is a Lorentz-covariance-invariant property.

10.3.7 The Separating Vector of a Faithful State

A faithful state has a sharper consequence at the level of the GNS construction than the faithfulness of its representation: its cyclic vector is also separating. This is the basic datum of the modular (Tomita-Takesaki) theory of the associated von Neumann algebra.

Theorem 154 Separating Vector of a Faithful State

✓

Let $\omega $ be a faithful state and $(\mathcal{H}_\omega , \pi _\omega , \Omega )$ its GNS triple. Then the cyclic vector $\Omega $ is separating for $\pi _\omega (\mathfrak {U})$: if $\pi _\omega (a)\Omega = 0$ then $a = 0$. Indeed $\pi _\omega (a)\Omega = 0$ gives $\omega (a^* a) = \langle \Omega , \pi _\omega (a^* a)\Omega \rangle = \langle \pi _\omega (a)\Omega , \pi _\omega (a)\Omega \rangle = 0$, and faithfulness forces $a = 0$. This holds in any representation reproducing a faithful state, not only the GNS one.

10.3.8 The KMS Condition and Thermal Equilibrium

Poincaré (or Killing-flow) invariance is only part of what singles out a physical equilibrium state. The Kubo-Martin-Schwinger (KMS) condition is the algebraic characterization of thermal equilibrium at inverse temperature $\beta $. It is phrased purely as an analyticity statement about correlation functions, so - unlike the spectrum condition - it needs no unbounded-operator theory (no Stone theorem, no spectral measures). It is exactly the condition satisfied by the curved-spacetime examples of 198: the Hartle-Hawking state on a black-hole exterior and the Gibbons-Hawking state in the de Sitter static patch are KMS for the relevant Killing flow.

Definition 155 One-Parameter Automorphism Group

✓

A family $\alpha : \mathbb {R} \to (A \simeq _{\star \mathrm{a}} A)$ of $*$-automorphisms of a C$^*$-algebra $A$ is a one-parameter group if $\alpha _0 = \mathrm{id}$ and $\alpha _{s+t} = \alpha _s \circ \alpha _t$. This is the algebraic time evolution; in the curved-spacetime setting it is the automorphism group induced by a Killing flow.

Definition 156 KMS State

✓

A state $\omega $ on $A$ is $(\alpha , \beta )$-KMS for a one-parameter automorphism group $\alpha $ (155) at inverse temperature $\beta $ if for every $a, b \in A$ the correlation function $t \mapsto \omega (a\, \alpha _t b)$ extends to a function $F$ on the closed strip $0 \le \operatorname {Im} z \le \beta $ that is continuous there, holomorphic on the open strip, bounded, and whose boundary value on $\operatorname {Im} z = \beta $ is $t \mapsto \omega (\alpha _t b\, \cdot a)$.

Theorem 157 The KMS State Set is Convex

✓

A convex combination $s\, \omega _1 + (1-s)\, \omega _2$ ($0 \le s \le 1$) of two $(\alpha , \beta )$-KMS states is again $(\alpha , \beta )$-KMS: for each pair $(a, b)$ the analytic interpolant is the convex combination $s\, F_1 + (1-s)\, F_2$ of the two interpolants, which is continuous, bounded, and holomorphic on the strip, with boundary values that add. Thus the equilibrium states at a fixed temperature form a convex set.

Lemma 158 Boundary Coincidence for $a = 1$

✓

For a KMS state $\omega $ and any observable $a$, the correlation function $F$ of the pair $(1, a)$ has its two boundary values equal - both are $t \mapsto \omega (\alpha _t a)$. This is the algebraic heart of the invariance argument: it follows directly from the KMS condition with $a := 1$, since $\omega (1\cdot \alpha _t a) = \omega (\alpha _t a \cdot 1) = \omega (\alpha _t a)$.

Definition 159 Strip-Liouville Principle

✓

The strip-Liouville principle at width $\beta $ is the statement that any function $F$ continuous and bounded on the closed strip $0 \le \operatorname {Im} z \le \beta $, holomorphic on the open strip, and with equal boundary values $F(t) = F(t + i\beta )$ for all real $t$, is constant along the real axis: $F(t) = F(0)$. It is the analytic input that turns boundary coincidence into invariance.

Theorem 160 $i\beta $-Periodic Entire Extension (Strip Schwarz Reflection)

✓

A function $F$ continuous on the closed strip $0 \le \operatorname {Im} z \le \beta $, holomorphic on the open strip, bounded, and with equal boundary values $F(t) = F(t + i\beta )$ on the real axis, admits a bounded entire extension $H$ agreeing with $F$ on $\mathbb {R}$. The extension is the $i\beta $-periodic continuation $H(z) = F\! \left(z - \lfloor \operatorname {Im} z / \beta \rfloor \, i\beta \right)$, which folds every point into the fundamental strip: it is continuous across each gluing line $\operatorname {Im} z = k\beta $ because the boundary values match by periodicity, holomorphic off the lines as $F$ composed with a holomorphic shift, and holomorphic on the lines by the horizontal-line removable-singularity theorem (Morera). This is the analytic engine behind the strip-Liouville principle.

Theorem 161 Strip-Liouville Holds for $\beta {\gt} 0$

✓

At positive width $\beta {\gt} 0$ the strip-Liouville principle (159) is a theorem. The equal boundary values let $F$ extend to a bounded $i\beta $-periodic entire function by the strip Schwarz reflection (160), which is then constant on $\mathbb {R}$ by Liouville’s theorem. The hypothesis $\beta {\gt} 0$ is necessary: at $\beta = 0$ the open strip is empty and at $\beta {\lt} 0$ the strip itself is empty, and in both cases the principle is false.

Theorem 162 KMS States are Invariant

✓

At positive inverse temperature $\beta {\gt} 0$, every $(\alpha , \beta )$-KMS state $\omega $ is $\alpha $-invariant: $\omega (\alpha _t a) = \omega (a)$ for all $t$ and $a$. By boundary coincidence (158) the KMS correlation function of $(1, a)$ has equal boundary values $F(t) = F(t + i\beta ) = \omega (\alpha _t a)$; the strip-Liouville principle for $\beta {\gt} 0$ (161) forces $F(t) = F(0)$, so $\omega (\alpha _t a) = F(t) = F(0) = \omega (\alpha _0 a) = \omega (a)$.

Theorem 163 Uniqueness on the Strip from Boundary Values

✓

Two functions continuous and bounded on the closed strip $0 \le \operatorname {Im} z \le \beta $ (with $\beta {\gt} 0$), holomorphic on the open strip, that agree on both boundary lines $\operatorname {Im} z = 0$ and $\operatorname {Im} z = \beta $, agree on the whole strip. Indeed their difference has vanishing boundary values, so its $i\beta $-periodic extension (160) is a bounded entire function, constant by Liouville, equal to its value $0$ at the origin.

Theorem 164 Uniqueness of the KMS Correlation Function

✓

For $\beta {\gt} 0$, the analytic completion of a KMS correlation function is unique: any two functions satisfying the KMS analytic data for the same pair $(a, b)$ - continuous and bounded on the strip, holomorphic on the interior, with the prescribed boundary values $t \mapsto \omega (a\, \alpha _t b)$ and $t \mapsto \omega (\alpha _t b\, \cdot a)$ - agree on the whole strip. This is the strip uniqueness (163) applied to the two analytic completions, which share both boundary values.

10.3.9 KMS States for the Covariance Flow

A one-parameter subgroup $t \mapsto L_t$ of the inhomogeneous Lorentz group - for instance the time-translation subgroup - induces, via the quasilocal lift $\beta _L$ (143), a one-parameter group of $*$-automorphisms of the global quasilocal algebra $\mathfrak {U}$. Unlike the curved case, where the absence of a global algebra forces a restriction to the stabilizer $\mathrm{Stab}(\mathbf{B})$, here $\beta _L$ is a genuine automorphism of the single algebra $\mathfrak {U}$ for every $L$, so no restriction is needed.

Definition 165 Covariance-Flow Automorphism Family

✓

Given a one-parameter subgroup $t \mapsto L_t$ of the inhomogeneous Lorentz group, the covariance-flow automorphism family of $\mathfrak {U}$ is $t \mapsto \beta _{L_t}$, the covariance action evaluated along the flow.

Lemma 166 A Lorentz One-Parameter Subgroup Induces a One-Parameter Group

✓

If $t \mapsto L_t$ is a one-parameter subgroup ($L_0 = 1$, $L_{s+t} = L_s L_t$), then the induced automorphisms $t \mapsto \beta _{L_t}$ of $\mathfrak {U}$ form a one-parameter automorphism group (155), by the coherence of the covariance action (143).

Definition 167 KMS State for the Covariance Flow

✓

A state $\omega $ on the quasilocal algebra $\mathfrak {U}$ is a KMS state for the covariance flow $L$ at inverse temperature $\beta $ if it satisfies the KMS condition (156) for the induced one-parameter automorphism group (166).

Theorem 168 Convexity of the Covariance-Flow KMS States

✓

A convex combination $s\, \omega _1 + (1-s)\, \omega _2$ ($0 \le s \le 1$) of two KMS states on $\mathfrak {U}$ for the same covariance flow $L$ at the same inverse temperature $\beta $ is again a KMS state for that flow. This specializes the abstract KMS convexity (157) to the induced one-parameter group $\mathrm{flowAut}$. Physically, the equilibrium states for a one-parameter symmetry flow form a convex set.

Definition 169 Ground State for a Covariance Flow

✓

A state $\omega $ on the quasilocal algebra $\mathfrak {U}$ is a ground state for a one-parameter subgroup $t \mapsto L_t$ of the inhomogeneous Lorentz group (e.g. a translation or boost flow) when it is invariant under the flow and, in a GNS representation reproducing $\omega $ and implementing the flow by unitaries $U(t)$ fixing $\Omega $, the one-parameter unitary group $t \mapsto U(t)$ has positive energy (147). This is the ground-state ($\beta \to \infty $, spectrum-condition) counterpart of the covariance-flow KMS state 167: the stationary state whose flow generator, the Hamiltonian for a timelike flow, is positive. Two Stone-free consequences: a ground state is flow-invariant, and its implementing unitary group is strongly continuous. It is the Minkowski analogue of the curved Killing-flow ground state 207.

10.4 Haag Kastler Axioms in Curved Spacetime

Here we recount the axioms we’ve established for AQFT in Lorentzian spacetime.

The first axiom states:

Definition 170 Axiom 1: Local Algebras

✓

For any basis element $\mathbf{B}$ of the Alexandrov topology on a Lorentzian spacetime, i.e. any set of the form $I^+(p) \cap I^-(q)$, there is a corresponding abstract C*-algebra $\mathfrak {U}(\mathbf{B})$

\begin{align} \mathbf{B} \longmapsto \mathfrak {U}(\mathbf{B}), \end{align}

and when $\mathbf{B}$ is the empty set, we have the distinguished correspondence

\begin{align} \emptyset \longmapsto \mathbb {C} \mathbf{1}, \end{align}

where $\mathbf{1}$ is the multiplicative identity in the abstract C*-algebra $\mathbb {C} \mathbf{1}$.

The second axiom can be immediately stated too.

Definition 171 Axiom 2: Isotony

✓

Let $\mathbf{B}_1$ and $\mathbf{B}_2$ be any two basis elements of the Alexandrov topology on a Lorentzian spacetime, i.e. any two sets of the form $I^+(p_1) \cap I^-(q_1)$ and $I^+(p_2) \cap I^-(q_2)$.

If $\mathbf{B}_1 \subset \mathbf{B}_2$ then $\mathfrak {U}(\mathbf{B}_1) \subset \mathfrak {U}(\mathbf{B}_2)$, where inclusion is implemented by

\begin{align} i : \mathfrak {U}(\mathbf{B}_1) \hookrightarrow \mathfrak {U}(\mathbf{B}_2), \end{align}

a unital *-monomorphism.

The next axiom can be stated as follows:

Definition 172 Axiom 3: Local Commutativity

✓

If $\mathbf{B_1}$ and $\mathbf{B_2}$ are completely spacelike, for any Alexandrov topology basis element $\mathbf{B}$ such that $\mathbf{B_1}, \mathbf{B_2} \subseteq \mathbf{B}$ the algebras $\mathfrak {U}(\mathbf{B_1})$ and $\mathfrak {U}(\mathbf{B_2})$ commute in the C*-algebra $\mathfrak {U}(\mathbf{B})$, i.e. for any $a_1$ in $\mathfrak {U}(\mathbf{B_1})$ and $a_2$ in $\mathfrak {U}(\mathbf{B_2})$ we have

\begin{align} i(a_1) i(a_2) - i(a_2) i(a_1) = 0 \end{align}

in the C*-algebra $\mathfrak {U}(\mathbf{B})$, where $i$ is the unital *-monomorphism Axiom 2 (Isotony).

If no such $\mathbf{B}$ exists, then it simply doesn’t make sense to consider if $\mathfrak {U}(\mathbf{B_1})$ and $\mathfrak {U}(\mathbf{B_2})$ commute as they are not in the same algebra.

The next axiom has need of the following definition

Definition 173 Local Observable

✓

For Lorentzian spacetime $M$ the image $\pi _\omega (a)$ of a self-adjoint member $a$ of the local algebra $\mathfrak {U}(\mathbf{B})$ under the GNS *-homomorphism $\pi _\omega $ of a state $\omega $ on $\mathfrak {U}(\mathbf{B})$ is self-adjoint and thus corresponds to an “observable”. Any “observable” corresponding to such a self-adjoint $\pi _\omega (a)$ is called a local observable.

and can be stated as follows:

Definition 174 Axiom 4: Local Completeness

✓

All “observables” are local observables.

The final axiom states:

Definition 175 Axiom 5: Isometric Covariance

✓

Let $\mathbf{B}$ be any basis element of the Alexandrov topology on a Lorentzian spacetime $M$, i.e. any set of the form $I^+(p) \cap I^-(q)$.

A member $\varphi $ of the group of isometries of $M$ connected to the identity acts on $\mathfrak {U}(\mathbf{B})$ as follows

\begin{align} \alpha _\varphi : \mathfrak {U}(\mathbf{B}) & \longrightarrow \mathfrak {U}(\varphi (\mathbf{B})) \\ a & \longmapsto \alpha _\varphi (a) \end{align}

where $\varphi (\mathbf{B})$ is the image of the basis element $\mathbf{B}$ under the isometry $\varphi $ and $\alpha _\varphi $ is a unital *-isomorphism generated by $\varphi $. The map $\alpha _\varphi $ is such that (1) for the identity isometry $\mathbf{1}$ it satisfies

\begin{align} \alpha _{\mathbf{1}}(a) = a, \end{align}

(2) for all appropriate $a$, $\varphi $, and $\varphi '$ it satisfies

\begin{align} \alpha _{\varphi ' \circ \varphi }(a) = \alpha _{\varphi '}(\alpha _{\varphi }(a)), \end{align}

and (3) for Alexandrov topology basis elements $\mathbf{B}_\iota \subset \mathbf{B}_\kappa $ and the unital *-monomorphism $i$ of Axiom 2 (Isotony) $\alpha _\varphi $ commutes with $i$. In other words the following diagram

$\begin{tikzcd} \mathfrak{U}(\mathbf{B}_\kappa) \arrow[r, "\alpha_\varphi"] & \mathfrak{U}(\varphi(\mathbf{B}_\kappa)) \\ \mathfrak{U}(\mathbf{B}_\iota) \arrow[r, "\alpha_\varphi"] \arrow[u, "i"] & \mathfrak{U}(\varphi(\mathbf{B}_\iota)) \arrow[u, "i"] \end{tikzcd}$

commutes.

Definition 176 Haag-Kastler Net in Curved Spacetime

✓

A Haag-Kastler net in curved spacetime on a Lorentzian spacetime is the bundling of the data of 170 together with the properties of 171, 172, 174, and 175. In the Lean formalization this is a single structure whose fields are the assignment $\mathbf{B} \mapsto \mathfrak {U}(\mathbf{B})$ and proofs that this assignment satisfies the four remaining axioms. Theorems about AQFT in curved spacetime take an instance of this structure as a hypothesis and invoke each axiom as a projection.

Generally these axioms follow in a straightforward manner from those of AQFT in Minkowski spacetime. The only “surprise” in this presentation is the absence of a quasilocal algebra. However, as we found, its absence is simply a reflection of the observational constraints of Lorentzian spacetime which don’t exist in Minkowski spacetime.

10.4.1 Einstein Causality in Curved Spacetime

The operator form of local commutativity (172) carries over to curved spacetime. The only adaptation is dictated by the absence of a quasilocal algebra: causality is expressed in a representation of a common containing local algebra $\mathfrak {U}(\mathbf{B})$, rather than of a global quasilocal algebra.

Theorem 177 Einstein Causality in a Representation (Curved Spacetime)

✓

Let $\pi $ be any $*$-representation of a containing basis algebra $\mathfrak {U}(\mathbf{B})$ on a Hilbert space $H$. If $\mathbf{B}_1, \mathbf{B}_2 \subseteq \mathbf{B}$ are completely spacelike-separated basis regions, then the images of the local observables of $\mathbf{B}_1$ and $\mathbf{B}_2$ in $\mathfrak {U}(\mathbf{B})$ commute under $\pi $ as bounded operators on $H$. This is the image under $\pi $ of the curved local commutativity (172); it holds in particular on the GNS Hilbert space of any state on $\mathfrak {U}(\mathbf{B})$. It is the curved-spacetime counterpart of 88, with the containing local algebra playing the role of the quasilocal algebra.

10.4.2 Local von Neumann Algebras in Curved Spacetime

The von Neumann net carries over to curved spacetime, again relative to a containing basis algebra $\mathfrak {U}(\mathbf{B})$. Given a $*$-representation $\pi $ of $\mathfrak {U}(\mathbf{B})$ on a Hilbert space $H$, the local von Neumann algebra of a subregion $\mathbf{B}' \subseteq \mathbf{B}$ is the bicommutant $R(\mathbf{B}') = \pi (\mathfrak {U}(\mathbf{B}'))''$, where $\mathfrak {U}(\mathbf{B}')$ is embedded into $\mathfrak {U}(\mathbf{B})$ by the isotony witness of Axiom 2.

Definition 178 Local von Neumann Algebra in Curved Spacetime

✓

Let $\pi $ be a $*$-representation of a containing basis algebra $\mathfrak {U}(\mathbf{B})$ on $H$. For a subregion $\mathbf{B}' \subseteq \mathbf{B}$, the local observable operators are the image $\pi (\mathfrak {U}(\mathbf{B}'))$ under the isotony embedding, and the local von Neumann algebra $R(\mathbf{B}')$ is the bicommutant $\pi (\mathfrak {U}(\mathbf{B}'))''$.

Definition 179 $R(\mathbf{B}')$ as a von Neumann Algebra (Curved Spacetime)

✓

As in the Minkowski case, $R(\mathbf{B}')$ is registered as a genuine VonNeumannAlgebra: the local observable operators $\pi (\mathfrak {U}(\mathbf{B}'))$ are self-adjoint (the isotony embedding and $\pi $ are $*$-homomorphisms), so their bicommutant is a von Neumann algebra whose underlying set is the bicommutant of 178. The construction is the same general bicommutant-of-a-self-adjoint-set lemma.

Theorem 180 Microcausality at the von Neumann Level (Curved Spacetime)

✓

For completely spacelike-separated basis subregions $\mathbf{B}_1, \mathbf{B}_2 \subseteq \mathbf{B}$, the local von Neumann algebras commute: $R(\mathbf{B}_1) \subseteq R(\mathbf{B}_2)'$. This is the von Neumann form of curved Einstein causality (177), via the antitonicity of the commutant and $S''' = S'$. It is the curved counterpart of 91.

Theorem 181 Isotony of the von Neumann Net (Curved Spacetime)

✓

For nested basis subregions $\mathbf{B}_1 \subseteq \mathbf{B}_2 \subseteq \mathbf{B}$, the local von Neumann algebras are nested: $R(\mathbf{B}_1) \subseteq R(\mathbf{B}_2)$. Unlike Minkowski, the curved Axiom 3 isotony embeddings are chosen witnesses with no built-in composition law, so the coherence of the embeddings (that the $\mathbf{B}_1 \hookrightarrow \mathbf{B}$ embedding factors through $\mathbf{B}_2$) is taken as an explicit hypothesis; it holds automatically whenever the Axiom 3 witnesses form a genuine inclusion family. Given it, the local observables of $\mathbf{B}_1$ embed into those of $\mathbf{B}_2$ and the double commutant is monotone.

Theorem 182 Bundled von Neumann Microcausality and Isotony (Curved Spacetime)

✓

Phrased on the bundled VonNeumannAlgebra $R(\mathbf{B}')$ with its order $\le $ and Mathlib’s commutant: for completely spacelike-separated subregions $R(\mathbf{B}_1) \le R(\mathbf{B}_2)'$, and for $\mathbf{B}_1 \subseteq \mathbf{B}_2$ (with the isotony coherence) $R(\mathbf{B}_1) \le R(\mathbf{B}_2)$. Both reduce to the set-level statements through the coercion $\uparrow R(\mathbf{B}') = \pi (\mathfrak {U}(\mathbf{B}'))''$.

Definition 183 The Net of von Neumann Algebras in Curved Spacetime

✓

The curved counterpart of the von Neumann net (94). Fixing a containing basis region $\mathbf{B}$ and a $*$-representation $\pi $ of $\mathfrak {U}(\mathbf{B})$, the assignment $\mathbf{B}' \mapsto R(\mathbf{B}')$ is an order-preserving map from the poset of basis subregions of $\mathbf{B}$ (ordered by inclusion) to the von Neumann algebras of $\mathcal{B}(H)$ — the local net, restricted to a containing region, as a functor on the inclusion poset.

Unlike the Minkowski case, the coherence of the isotony embeddings (coherent below $\mathbf{B}$: the $\mathbf{B}_1 \hookrightarrow \mathbf{B}$ embedding factors through $\mathbf{B}_2$ for all nested $\mathbf{B}_1 \subseteq \mathbf{B}_2 \subseteq \mathbf{B}$) is supplied as a single hypothesis rather than discharged geometrically. This is intrinsic, not a gap: the coherence is a property of the net’s chosen Axiom 3 isotony witnesses, not of the spacetime, so — unlike spacelike-monotonicity — it cannot be discharged over a concrete spacetime. The curved Axiom 3 selects those witnesses by choice (with no built-in composition law), so the coherence is unavailable for free even for the trivial net; it holds for any net whose witnesses form a genuine inclusion family. Given it once, the map’s monotonicity carries no per-edge side condition.

Theorem 184 Statistical Independence (Schlieder Property)

✓

The abstract mechanism is: if $\Omega $ is cyclic for a set $S$ of operators, then any $R$ commuting with all of $S$ with $R\Omega = 0$ is zero (it vanishes on the dense set $S\Omega $). Applied to the net: if $\Omega $ is cyclic for the local observables of $\mathbf{B}_1$ - the role supplied in Minkowski spacetime by Reeh-Schlieder - then for a spacelike-separated subregion $\mathbf{B}_2$, every $R \in R(\mathbf{B}_2)$ with $R\Omega = 0$ is zero, since $R(\mathbf{B}_2)$ commutes with the observables of $\mathbf{B}_1$ by curved microcausality (180). Thus $\Omega $ is separating for $R(\mathbf{B}_2)$: a nonzero observable of one region cannot be annihilated by the cyclic vector of a spacelike-separated region, the operator-algebraic form of statistical independence.

Theorem 185 Statistical Independence, bundled (curved spacetime)

✓

The separating property phrased on the bundled VonNeumannAlgebra $R(\mathbf{B}_2)$: with $\Omega $ cyclic for the local observables of $\mathbf{B}_1$, every $R$ in the bundled algebra $R(\mathbf{B}_2)$ of a spacelike-separated subregion with $R\Omega = 0$ is zero. It reduces to 184 through the coercion $\uparrow R(\mathbf{B}_2) = \pi (\mathfrak {U}(\mathbf{B}_2))''$.

Theorem 186 Additive-Free Locality via the Spacelike Complement (Curved Spacetime)

✓

The geometric specialisation of additive-free locality to a curved local net over a concrete Lorentzian spacetime $L$: for basis sets $\mathbf{B}_1 \subseteq \mathbf{B}_2^\perp $ inside a common containing region $\mathbf{B}$, the local von Neumann algebra $R(\mathbf{B}_1)$ lies in the commutant $R(\mathbf{B}_2)'$. As in Minkowski, the spacelike complement $\mathbf{B}_2^\perp $ only selects the bounded regions spacelike to $\mathbf{B}_2$; no algebra is attached to the unbounded complement. The Galois bridge discharges the spacelike hypothesis, and $L.\mathtt{toAbstract}$ identifies the concrete and abstract spacelike relations.

Theorem 187 Geometric Covariance of the von Neumann Net (Curved Spacetime)

✓

The curved, stabilizer-subgroup analogue of geometric covariance. There is no quasilocal algebra in curved spacetime, so the only symmetries acting on the containing algebra $\mathfrak {U}(\mathbf{B})$ are the stabilizer $\mathrm{Stab}(\mathbf{B}) = \{ g : g \cdot \mathbf{B} = \mathbf{B}\} $. For $g \in \mathrm{Stab}(\mathbf{B})$, the implementing unitary $U(g)$ of the stabilizer GNS representation (198) conjugates the local von Neumann algebra of a subregion $\mathbf{B}_1 \subseteq \mathbf{B}$ onto that of $g \cdot \mathbf{B}_1$:

\[ U(g)\, R(\mathbf{B}_1)\, U(g)^{-1} = R(g \cdot \mathbf{B}_1). \]

Hence $R(\mathbf{B}_1)$ and $R(g \cdot \mathbf{B}_1)$ are unitarily equivalent. Unlike Minkowski, the abstract LorentzianSpacetime interface supplies neither basis-set preservation $M.\mathrm{IsBasisSet}(g \cdot \mathbf{B}_1)$ nor the coherence relating the stabilizer action $\hat\alpha _g$ to the chosen isotony embeddings (171); both enter as explicit hypotheses, discharged for a net from a concrete geometric spacetime. The proof reuses the shared conjugation core: conjugation by a unit is a multiplicative automorphism, which maps centralizers — hence bicommutants — to those of the image.

Theorem 188 Orbit-Invariance of Factoriality (Curved Spacetime)

✓

If the local von Neumann algebra $R(\mathbf{B}_1)$ of a subregion is a factor, then so is $R(g \cdot \mathbf{B}_1)$ for every $g \in \mathrm{Stab}(\mathbf{B})$. Geometric covariance exhibits $R(g \cdot \mathbf{B}_1) = U(g) R(\mathbf{B}_1) U(g)^{-1}$, and conjugation by a unitary preserves the factor property; so being a factor is constant along the stabilizer orbit of a subregion.

Theorem 189 Geometric Covariance as a von Neumann Algebra Isomorphism (Curved Spacetime)

✓

For $g \in \mathrm{Stab}(\mathbf{B})$, the geometric-covariance set equality is upgraded to a first-class $*$-algebra isomorphism of the bundled local von Neumann algebras, $R(\mathbf{B}_1) \cong R(g \cdot \mathbf{B}_1)$, given by restricting the conjugation $*$-automorphism $T \mapsto U(g) T U(g)^{-1}$ of $\mathcal{B}(H)$ to $R(\mathbf{B}_1)$. It reuses the same restriction construction as the Minkowski case (100).

10.4.3 Purity of States on Local Algebras in Curved Spacetime

Each local algebra $\mathfrak {U}(\mathbf{B})$ of a Haag-Kastler net in curved spacetime is itself a unital C*-algebra with its own state space and GNS representations. The abstract characterizations of purity therefore apply per region, registered here for $\mathfrak {U}(\mathbf{B})$. There is no quasilocal algebra in curved spacetime, so - unlike the Minkowski covariant-vacuum picture - these are genuinely local statements, one for each region.

Theorem 190 Pure $\iff $ Extreme Point on a Local Algebra

✓

A state $\omega $ on the local algebra $\mathfrak {U}(\mathbf{B})$ is pure if and only if it is an extreme point of the state space of $\mathfrak {U}(\mathbf{B})$. This is the abstract equivalence 116 applied to the C*-algebra $\mathfrak {U}(\mathbf{B})$.

Theorem 191 Pure $\iff $ Irreducible GNS on a Local Algebra

✓

For a state $\omega $ on the local algebra $\mathfrak {U}(\mathbf{B})$ there is a GNS triple $(H, \pi , \Omega )$ reproducing $\omega $ in which $\omega $ is pure if and only if the representation $\pi $ is irreducible (its commutant is trivial). This combines the GNS construction with the abstract 108.

Theorem 192 Pure GNS on a Local Algebra is a Factor Generating $\mathcal{B}(H)$

✓

For a pure state $\omega $ on the local algebra $\mathfrak {U}(\mathbf{B})$ there is a cyclic GNS triple reproducing $\omega $ whose generated von Neumann algebra $\pi (\mathfrak {U}(\mathbf{B}))''$ has trivial center (it is a factor) and is in fact all of $\mathcal{B}(H)$. These are the abstract factor (112) and density (113) statements registered per region on the curved local algebra $\mathfrak {U}(\mathbf{B})$, the right generality in curved spacetime where there is no quasilocal algebra.

Theorem 193 The Irreducible Dichotomy for a Curved Local Algebra

✓

Two irreducible representations of a curved local algebra $\mathfrak {U}(\mathbf{B})$ are either disjoint or unitarily equivalent. This is the abstract irreducible dichotomy (125) registered per region on the C*-algebra $\mathfrak {U}(\mathbf{B})$ — the right generality in curved spacetime, where sectors are attached to the local algebras.

10.4.4 Covariant States in Curved Spacetime

As in the Minkowski case, the isometric covariance (175) acts fiberwise through the $*$-isomorphisms $\alpha _\varphi : \mathfrak {U}(\mathbf{B}) \to \mathfrak {U}(\varphi (\mathbf{B}))$. Since there is no quasilocal algebra, only the local notion of a covariant family of states is available.

Definition 194 Covariant Family of Local States in Curved Spacetime

✓

Given a Haag-Kastler net on a Lorentzian spacetime (176), a covariant family of local states assigns to every region $\mathbf{B}$ a state $\omega _{\mathbf{B}}$ on $\mathfrak {U}(\mathbf{B})$ such that, for every identity-component isometry $\varphi $ and every $a \in \mathfrak {U}(\mathbf{B})$, $\omega _{\mathbf{B}}(a) = \omega _{\varphi (\mathbf{B})}(\alpha _\varphi a)$, where $\alpha _\varphi $ is the covariance isomorphism of 175.

Lemma 195 Composition of Covariance in Curved Spacetime

✓

For a covariant family of local states, the covariance relation composes along the isometry group: $\omega _{\mathbf{B}}(a) = \omega _{\varphi '(\varphi (\mathbf{B}))}\big(\alpha _{\varphi '}(\alpha _\varphi a)\big)$.

10.4.5 The Stabilizer GNS Unitary in Curved Spacetime

In the Minkowski case the fiberwise covariance action lifts to a $*$-automorphism of the quasilocal algebra $\mathfrak {U}$, on whose GNS space an invariant state induces a unitary representation of the full Poincaré group (145). In curved spacetime there is no quasilocal algebra, so the covariance isomorphisms $\alpha _\varphi : \mathfrak {U}(\mathbf{B}) \to \mathfrak {U}(\varphi (\mathbf{B}))$ map between different local algebras and do not assemble into a single unitary representation.

They do, however, restrict to a genuine action by automorphisms of one fixed local algebra $\mathfrak {U}(\mathbf{B})$ on the stabilizer subgroup $\mathrm{Stab}(\mathbf{B}) = \{ \varphi : \varphi (\mathbf{B}) = \mathbf{B}\} $ of the region: when $\varphi (\mathbf{B}) = \mathbf{B}$, the isomorphism $\alpha _\varphi : \mathfrak {U}(\mathbf{B}) \to \mathfrak {U}(\varphi (\mathbf{B})) = \mathfrak {U}(\mathbf{B})$ is an automorphism of $\mathfrak {U}(\mathbf{B})$. Physically $\mathrm{Stab}(\mathbf{B})$ is the curved-spacetime stand-in for the global symmetry group, typically a Killing flow (the stationary flow of a black-hole exterior, giving a Hartle-Hawking/KMS state; the de Sitter static-patch boost, giving the Gibbons-Hawking temperature) or a spatial-symmetry subgroup (the rotations fixing a comoving ball in an FLRW cosmology).

Definition 196 Stabilizer Action on a Local Algebra

✓

For an identity-component isometry $\varphi $ fixing the region $\mathbf{B}$ (so $\varphi (\mathbf{B}) = \mathbf{B}$), the covariance isomorphism $\alpha _\varphi $ of 175 lands back in $\mathfrak {U}(\mathbf{B})$ and so defines an automorphism $\hat\alpha _\varphi $ of the single algebra $\mathfrak {U}(\mathbf{B})$.

Lemma 197 The Stabilizer Action is a Group Action

✓

The assignment $\varphi \mapsto \hat\alpha _\varphi $ is a monoid action of $\mathrm{Stab}(\mathbf{B})$ by automorphisms of $\mathfrak {U}(\mathbf{B})$: $\hat\alpha _1 = \mathrm{id}$ and $\hat\alpha _{\varphi '\varphi } = \hat\alpha _{\varphi '}\circ \hat\alpha _\varphi $. These follow from the identity and composition laws of the covariance action (175); the canonical region-casts collapse because all the regions involved equal $\mathbf{B}$.

Theorem 198 GNS Unitary Representation of the Stabilizer

✓

Let $\omega $ be a state on $\mathfrak {U}(\mathbf{B})$ invariant under the stabilizer action, $\omega (\hat\alpha _\varphi a) = \omega (a)$ for all $\varphi \in \mathrm{Stab}(\mathbf{B})$. Then the action is implemented on the GNS Hilbert space of $\omega $ by a unitary representation $U$ of $\mathrm{Stab}(\mathbf{B})$: there is a GNS triple $(H, \pi , \Omega )$ and unitaries $U(\varphi )$ with $U(\varphi )\, \pi (a)\Omega = \pi (\hat\alpha _\varphi a)\, \Omega $, $U(\varphi )\Omega = \Omega $, the group laws, and $U(1) = \mathrm{id}$. This is the curved-spacetime counterpart of 145: in the absence of a quasilocal algebra, the unitary representation is of the stabilizer subgroup acting on the single algebra $\mathfrak {U}(\mathbf{B})$, rather than of the full isometry group.

Theorem 199 Strongly Continuous Stabilizer GNS Unitary

✓

If moreover the isometry group carries a topology (the abstract interface supplies none, so it is an added hypothesis) and the matrix coefficients $\varphi \mapsto \omega \big(a^*\, \hat\alpha _\varphi b\big)$ are continuous on $\mathrm{Stab}(\mathbf{B})$, then the representation $U$ is strongly continuous: $\varphi \mapsto U(\varphi )\psi $ is continuous for every GNS vector $\psi $. The stabilizer subgroup inherits its topology as a subspace of the isometry group.

Theorem 200 Irreducible Covariant Representation of a Pure Invariant State (Curved Spacetime)

✓

A state $\omega $ on a local algebra $\mathfrak {U}(\mathbf{B})$ that is invariant under the stabilizer action and pure yields a GNS representation that is simultaneously covariant - implemented by a unitary representation $U$ of $\mathrm{Stab}(\mathbf{B})$ fixing the cyclic vector $\Omega $, with operator covariance $U(\varphi )\, \pi (a)\, U(\varphi )^{-1} = \pi (\hat\alpha _\varphi a)$ - and irreducible; in particular it generates all of $\mathcal{B}(H)$ ($\pi (\mathfrak {U}(\mathbf{B}))'' = \mathcal{B}(H)$, by 110). This is the curved, per-region analogue of 146 (there is no quasilocal algebra), combining 198 with purity $\Rightarrow $ irreducibility. It is not a vacuum: curved spacetime admits no global vacuum, and the analogue of the spectrum condition (the Hadamard / microlocal spectrum condition) is a separate requirement not imposed here.

Theorem 201 Purity is Invariant under the Stabilizer Action

✓

A state $\omega $ on a local algebra $\mathfrak {U}(\mathbf{B})$ is pure if and only if its pullback $\omega \circ \hat\alpha _\varphi $ along the stabilizer automorphism is pure, for every $\varphi \in \mathrm{Stab}(\mathbf{B})$. This is the curved specialization of 153: purity is invariant under the isometric symmetry that fixes the region.

10.4.6 KMS States for a Killing Flow

The stabilizer subgroup of a region is, in the genuinely curved examples, a one-parameter Killing flow rather than the full isometry group. Such a flow makes the local algebra $\mathfrak {U}(\mathbf{B})$ into a dynamical system, and the natural equilibrium states are the KMS states (156) for that flow. This is the precise sense in which the curved-spacetime thermal states are thermal: the Hartle-Hawking state on a Schwarzschild exterior is KMS for the stationary Killing flow at the Hawking temperature, and the Bunch-Davies state restricted to a de Sitter static patch is KMS for the boost Killing flow at the Gibbons-Hawking temperature.

Definition 202 Killing-Flow Automorphism Family

✓

A Killing flow fixing a region $\mathbf{B}$ is a map $t \mapsto \varphi _t$ from $\mathbb {R}$ into the stabilizer $\mathrm{Stab}(\mathbf{B})$. Through the stabilizer automorphism (196) it induces, for each $t$, an automorphism $\hat\alpha _{\varphi _t}$ of the single local algebra $\mathfrak {U}(\mathbf{B})$ - the time evolution of $\mathfrak {U}(\mathbf{B})$ along the flow.

Lemma 203 A Killing Flow Induces a One-Parameter Group

✓

If the flow is a one-parameter subgroup of $\mathrm{Stab}(\mathbf{B})$ ($\varphi _0 = 1$ and $\varphi _{s+t} = \varphi _s\, \varphi _t$), then the induced family $t \mapsto \hat\alpha _{\varphi _t}$ is a one-parameter automorphism group of $\mathfrak {U}(\mathbf{B})$ (155). This is immediate from the group-action laws of the stabilizer action (197).

Definition 204 KMS State for a Killing Flow

✓

A state $\omega $ on $\mathfrak {U}(\mathbf{B})$ is a KMS state for the Killing flow $\varphi $ at inverse temperature $\beta $ if it satisfies the KMS condition (156) for the induced one-parameter automorphism group (203). When $\beta {\gt} 0$ such a state is automatically invariant under the flow (162), so it induces, by the stabilizer GNS unitary (198), a unitary representation of the flow on its GNS space - the modular/thermal time evolution.

Theorem 205 The Killing-Flow KMS Thermal Representation

✓

Let $\omega $ be a KMS state on $\mathfrak {U}(\mathbf{B})$ for a one-parameter Killing flow $t \mapsto \varphi _t$ into $\mathrm{Stab}(\mathbf{B})$, at inverse temperature $\beta {\gt} 0$, whose matrix coefficients $t \mapsto \omega (a^* \hat\alpha _{\varphi _t} b)$ are continuous. Then its GNS triple $(H, \pi , \Omega )$ carries a strongly continuous one-parameter unitary group $U : \mathbb {R} \to \mathcal{U}(H)$ implementing the flow: $U_t\, \pi (a)\Omega = \pi (\hat\alpha _{\varphi _t} a)\Omega $, $U_t\Omega = \Omega $, $U_0 = \mathrm{id}$, $U_{s+t} = U_s U_t$, and $t \mapsto U_t\psi $ is continuous for every $\psi $. This is the curved-spacetime equilibrium (thermal) representation - the analogue of the Minkowski vacuum representation - realized for the Hartle-Hawking and Gibbons-Hawking states. KMS at $\beta {\gt} 0$ supplies the flow-invariance, which feeds the strongly continuous GNS unitary construction.

Theorem 206 Convexity of the Killing-Flow KMS States

✓

A convex combination $s\, \omega _1 + (1-s)\, \omega _2$ ($0 \le s \le 1$) of two KMS states on $\mathfrak {U}(\mathbf{B})$ for the same Killing flow $\varphi $ at the same inverse temperature $\beta $ is again a KMS state for that flow. This specializes the abstract KMS convexity (157) to the induced one-parameter group $\mathrm{flowAut}$. Physically, the curved-spacetime thermal equilibrium states for a stationary Killing flow form a convex set.

Definition 207 Ground State for a Killing Flow

✓

A state $\omega $ on $\mathfrak {U}(\mathbf{B})$ is a ground state for a one-parameter Killing flow $t \mapsto \varphi _t$ into $\mathrm{Stab}(\mathbf{B})$ when it is invariant under the flow and, in a GNS representation reproducing $\omega $ and implementing the flow by unitaries $U(t)$ fixing $\Omega $, the one-parameter unitary group $t \mapsto U(t)$ has positive energy (147). This is the ground-state ($\beta \to \infty $, spectrum-condition) counterpart of the Killing-flow KMS state 204: it selects the stationary state whose Killing-flow generator, the local Hamiltonian, is positive. Two Stone-free consequences: a ground state is flow-invariant, and its implementing unitary group is strongly continuous. The positive-energy condition is the bounded-generator scaffold; the faithful unbounded form is Stone-gated.