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 one of the parts below.

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

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

Consider the set

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

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}\)

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, which are stated and proved separately below.

The most famous of these results is the Cauchy-Schwarz Inequality (16).

The next result we need to prove is the equality \(\mathcal{N} = \mathcal{N}_1\) of the two null sets (17).

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

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

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

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

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}\),

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

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

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

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

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

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

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

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

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

This along with our previous derivation gives

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

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

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

Tracing definitions we have

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

which proves another relation

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

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

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

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\)

gives for the case \(a = \mathbf{1}\)

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

However, the definition of \(U\) implies

Thus the previous two equations imply

As a result of cyclicity of \(\Omega '\) this implies that

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

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

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.

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

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

This inequality then implies both desired results,

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

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

Let us next prove that our inequality

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

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

which implies

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

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

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

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

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

follows trivially, completing our 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

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.

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

Hence, the linearity of \(\omega \) then implies

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

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}\).

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.

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

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)\).

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.

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.

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\).

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\).

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.

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\).

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.

The projection is induced by the fact that an orientation-preserving reparametrisation is in particular a reparametrisation, so passing to the coarser quotient is well-defined, and it is surjective because every smooth path represents both an oriented and an unoriented smooth curve. The timelike and causal predicates factor through it by their reparametrisation-invariance (35), and a future- or past-oriented curve is causal because a future- or past-pointing tangent vector is timelike or null (27).

Take \(s \in \Sigma \) minimal. Since \(s \in \Sigma \), it suffices by mem_frontier_iff_notMem_interior to show \(s \notin \mathrm{int}\, \Sigma \). If it were, some ball \(B(s,\varepsilon ) = (s-\varepsilon , s+\varepsilon )\) (Real.ball_eq_Ioo) would lie in \(\Sigma \), and then \(s - \varepsilon /2 \in \Sigma \) contradicts minimality. The maximal case is symmetric. The consequence is immediate: a witness \(s\) for a past (resp. future) endpoint is minimal (resp. maximal) in \(\Sigma \), hence lies in \(\partial \Sigma \), so \(\mu (s) = p\) exhibits \(p\) as an endpoint.

The witness for the past endpoint is a minimum \(a\) of \(\Sigma \) and the witness for the future endpoint is a maximum \(b\), so \(\Sigma \) is bounded below and above, with \(\inf \Sigma = a\) and \(\sup \Sigma = b\). Being also connected, nonempty and closed (31), \(\Sigma = [a,b]\) by eq_Icc_csInf_csSup_of_connected_bdd_closed. Finally \(a {\lt} b\), since \(a \le b\) and \(a = b\) would make \(\Sigma \) a singleton, contradicting that \(\Sigma \) has more than one point.

Two trips joined at the common point \(q\) concatenate to a single piecewise trip; this is exactly the transitivity of the transitive closure.

For irreflexivity of chronological precedence, \(p \ll p\) would give \(p \prec p\) because chronological precedence implies causal precedence (49), which the causality condition forbids. For asymmetry and antisymmetry, \(p \prec q\) and \(q \prec p\) cannot both hold, since transitivity (44) would give the forbidden \(p \prec p\).

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.

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.

All three are immediate from transitivity of causal precedence (44). For (i), if \(x \in D(p,q)\) then \(p \prec x\) and \(x \prec q\); combining with \(p' \prec p\) and \(q \prec q'\) by transitivity gives \(p' \prec x\) and \(x \prec q'\), so \(x \in D(p',q')\). For (ii), from \(a \in D(p,q)\) we have \(p \prec a\), and \(a \prec z\) gives \(p \prec z\); from \(b \in D(p,q)\) we have \(b \prec q\), and \(z \prec b\) gives \(z \prec q\), so \(z \in D(p,q)\). For (iii), any \(x \in D(p,q)\) satisfies \(p \prec x\) and \(x \prec q\), whence \(p \prec q\) by transitivity.

Chronological precedence refines causal precedence (49), so \(I^+(p) \subseteq J^+(p)\) and \(I^-(p) \subseteq J^-(p)\); intersecting these inclusions gives \(I^+(p) \cap I^-(q) \subseteq J^+(p) \cap J^-(q)\). The characterisation of the Alexandrov basis is the definition of the Alexandrov topology (73), whose basis consists of exactly the sets \(I^+(p) \cap I^-(q)\). The final claim combines the two: an Alexandrov basis set equals some \(I^+(p) \cap I^-(q)\), which is contained in \(J^+(p) \cap J^-(q)\).

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.

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.

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.

All three are read off the order structure of the spacelike complement (59). Monotonicity is antitonicity applied twice: \(\mathbf{B}_1 \subseteq \mathbf{B}_2\) gives \(\mathbf{B}_2^{\perp } \subseteq \mathbf{B}_1^{\perp }\), and applying antitonicity again gives \(\mathbf{B}_1^{\perp \perp } \subseteq \mathbf{B}_2^{\perp \perp }\). Extensivity is the double-complement inclusion. For idempotence, the triple-complement collapse gives \(\mathbf{B}^{\perp \perp \perp } = \mathbf{B}^{\perp }\), and taking the spacelike complement of both sides yields \(\mathbf{B}^{\perp \perp \perp \perp } = \mathbf{B}^{\perp \perp }\).

The lattice is obtained from the causal closure operator (61) via its Galois insertion: the causally complete regions are exactly the fixed points of the closure operator, so meets are intersections and joins are the causal closures of unions. That the spacelike complement of any region is causally complete, and that complementation is an order-reversing involution on this lattice, are the antitonicity and the triple-complement identity of the spacelike complement (59).

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 (57), \(\{ 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.

Recall from the lattice structure (63) 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 (64).

• (order-reversing) This is the antitonicity half of the order-reversing involution supplied by 63: \(\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 (64) 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 (64) 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.

This is exactly the causal-convexity property of the causal diamond (part (ii) of the structural lemma, 52), repackaged as the region predicate: if \(a, b \in J^+(p) \cap J^-(q)\) with \(a \prec z\) and \(z \prec b\), then \(z \in J^+(p) \cap J^-(q)\), which is precisely the statement that \(J^+(p) \cap J^-(q)\) is causally convex.

For (i), suppose \(p, r \in \mathbf{B}^\perp \) and \(p \prec q \prec r\); we must show \(q \in \mathbf{B}^\perp \), i.e. that \(q\) is spacelike to every point of \(\mathbf{B}\). This is a consequence of transitivity of causal precedence (44): if \(q\) were causally related to some \(b \in \mathbf{B}\), then composing that relation with \(p \prec q\) or \(q \prec r\) would make \(p\) or \(r\) causally related to \(b\), contradicting \(p, r \in \mathbf{B}^\perp \). Hence \(q\) is spacelike to all of \(\mathbf{B}\), so \(q \in \mathbf{B}^\perp \).

For (ii), a causally complete region satisfies \(\mathbf{B} = \mathbf{B}^{\perp \perp } = (\mathbf{B}^\perp )^\perp \), so it is the spacelike complement of the region \(\mathbf{B}^\perp \); causal convexity then follows immediately from part (i) applied to \(\mathbf{B}^\perp \).

Each claim is immediate from the definition of causal convexity (66). For \(\mathrm{univ}\) the membership condition \(q \in M\) is vacuously satisfied, and for \(\varnothing \) the hypothesis \(p, r \in \varnothing \) never holds. For an intersection, suppose \(p, r\) lie in the intersection and \(p \prec q \prec r\); then \(p, r\) lie in every member of the family, so by that member’s causal convexity \(q\) lies in every member, hence in the intersection. The binary and indexed forms are the special cases of a two-element and an indexed family, and the set-indexed form (\(\bigcap _0 \mathcal{S}\)) unfolds membership through \(\mathtt{mem\_ sInter}\) to the same argument.

For (i), membership in the intersection \(\bigcap _0\) unfolds to membership in every member of the family, and every member contains \(\mathbf{B}\) by the defining condition of the family; so any \(x \in \mathbf{B}\) lies in each member and hence in \(\mathrm{ccHull}(\mathbf{B})\). For (ii), the intersected family consists of causally convex regions, and causal convexity is preserved under set-indexed intersections (69); note the family is nonempty, since the whole space \(M\) contains \(\mathbf{B}\) and is causally convex by the same lemma.

(i) If \(\mathbf{B} \subseteq \mathbf{C}\) and \(\mathbf{C}\) is causally convex, then \(\mathbf{C}\) is a member of the intersected family, so \(\mathrm{ccHull}(\mathbf{B}) \subseteq \mathbf{C}\) as an intersection is contained in each of its members.

(ii) If \(\mathbf{B}_1 \subseteq \mathbf{B}_2\), then \(\mathbf{B}_1 \subseteq \mathbf{B}_2 \subseteq \mathrm{ccHull}(\mathbf{B}_2)\) by extensivity, and \(\mathrm{ccHull}(\mathbf{B}_2)\) is causally convex (71); applying (i) with \(\mathbf{C} = \mathrm{ccHull}(\mathbf{B}_2)\) gives \(\mathrm{ccHull}(\mathbf{B}_1) \subseteq \mathrm{ccHull}(\mathbf{B}_2)\).

(iii) If \(\mathbf{C}\) is causally convex, then \(\mathbf{C} \subseteq \mathrm{ccHull}(\mathbf{C})\) by extensivity, while (i) with \(\mathbf{B} = \mathbf{C}\) (and \(\mathbf{C} \subseteq \mathbf{C}\)) gives \(\mathrm{ccHull}(\mathbf{C}) \subseteq \mathbf{C}\); hence \(\mathrm{ccHull}(\mathbf{C}) = \mathbf{C}\).

(iv) Idempotence is (iii) applied to \(\mathbf{C} = \mathrm{ccHull}(\mathbf{B})\), which is causally convex by 71.

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

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

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

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 (74), 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, 44.)

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 75: 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.

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.

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\).

Suppose a point \(x\) lay in no diamond \(I^+(p) \cap I^-(q)\). Then by 80 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.

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 81. 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 89.

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).

Dual to 83: 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.

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 (83) yields \(a\) with \(p_1 \ll a\), \(p_2 \ll a\), and \(a \ll x\); future interpolation (84) 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 \) (44) \(y \in I^+(p_i) \cap I^-(q_i)\); hence \(B_3 \subseteq B_1 \cap B_2\).

Take \(p\) on the time axis, \(p = (t, \mathbf{0})\), with \(t\) small enough. Then \(p_i - p\) has time component \(p_i^0 - t\) and spatial part that of \(p_i\), so \(p \ll p_i\) amounts to \(|\mathbf{p}_i|^2 {\lt} (p_i^0 - t)^2\) together with \(t {\lt} p_i^0\). Both spatial norms are fixed nonnegative reals, so choosing a single \(t\) below \(\min _i\bigl(p_i^0 - |\mathbf{p}_i|\bigr)\) makes each time gap exceed the corresponding spatial separation; the estimate is a direct coordinate computation (linarith after expanding the squares).

Dual to 86, but proved independently rather than by invoking it (the time-shift estimate is run in the other direction, so there is no dependency edge): take \(q = (t, \mathbf{0})\) with \(t\) above \(\max _i\bigl(q_i^0 + |\mathbf{q}_i|\bigr)\), so that for each \(i\) the vector \(q - q_i\) has positive time component exceeding the spatial separation and is therefore future-pointing timelike.

Write \(B_1 = I^+(p_1) \cap I^-(q_1)\) and \(B_2 = I^+(p_2) \cap I^-(q_2)\). Apply 86 to \(p_1, p_2\) to get \(p\) with \(p \ll p_1\) and \(p \ll p_2\), and 87 to \(q_1, q_2\) to get \(q\) with \(q_1 \ll q\) and \(q_2 \ll q\). Put \(B = I^+(p) \cap I^-(q)\), again a diamond. By monotonicity of the Minkowski forward and backward cones — i.e. transitivity of \(\ll \) (44) — \(p \ll p_i\) gives \(I^+(p_i) \subseteq I^+(p)\) and \(q_i \ll q\) gives \(I^-(q_i) \subseteq I^-(q)\); intersecting these, \(B_i \subseteq B\) for \(i = 1, 2\).

This lemma is already formalized, as Physicslib4.Spacetime.alexandrovBasis_directed, and so are the two point-existence helpers it consumes, exists_common_past and exists_common_future.

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

Scaling multiplies the defining quadratic form by \(\lambda ^2 {\gt} 0\) and the time-order difference by \(\lambda {\gt} 0\), so neither strict inequality changes.

Via the cone characterization of the chronological future and past on standard Minkowski (76) together with 90.

The scaling identity is bilinearity of the Minkowski form. For the timelike unit vector \(e_0\) one has \(g(\lambda e_0, \lambda e_0) = -\lambda ^2 \neq -1 = g(e_0, e_0)\) whenever \(\lambda ^2 \neq 1\), which exhibits a pair of vectors on which \(g\) is not preserved. Thus for \(\lambda {\gt} 0\) with \(\lambda \neq 1\) the dilation is a causal automorphism (91) that is not an isometry.

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.

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.

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.

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^-\).

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.

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

This is Mathlib’s Diffeomorph.mfderivToContinuousLinearEquiv, which packages the differential of a \(C^n\) diffeomorphism (\(n \neq 0\)) at a point as a ContinuousLinearEquiv between the tangent spaces; Diffeomorph.mfderivToContinuousLinearEquiv_coe identifies its underlying map with \(d\psi _x\).

Two implementation points. First, the statement deliberately claims only that \(d\psi _x\) is an isomorphism, and does not identify the inverse of that equivalence with \(d(\psi ^{-1})_{\psi (x)}\). Such an identification is not available definitionally: Diffeomorph.mfderivToContinuousLinearEquiv is built as \((\psi .\mathtt{isLocalDiffeomorph}\; x).\mathtt{mfderivToContinuousLinearEquiv}\), so its inverse function comes from IsLocalDiffeomorphAt.mfderivToContinuousLinearEquiv — the differential of a local inverse chosen by that construction, not of the global \(\psi ^{-1}\). Where the notation \((d\psi _x)^{-1}\) appears below it therefore means the symm of this equivalence, not a priori \(d(\psi ^{-1})_{\psi (x)}\), and the purely algebraic consumers — 103, 106, 112, 114 — need nothing more, since they use only the two cancellation identities \(\mathtt{symm\_ apply\_ apply}\) and \(\mathtt{apply\_ symm\_ apply}\) of the equivalence, which hold for whatever the symm happens to be.

It must not be inferred from this that the identification is never needed. A second group of nodes reasons about \(d(\psi ^{-1})\) as such, i.e. about \(\mathtt{mfderiv}\; \psi .\mathtt{symm}\), because the orientation hypothesis they invoke is applied to the inverse diffeomorphism. What those nodes require is the chain-rule cancellation

and Mathlib has no such lemma for a global Diffeomorph (there is no Diffeomorph analogue of the \(\mathtt{mfderiv}\)/symm identities; searching turns up only Diffeomorph.apply_symm_apply at the level of points). It has to be proved by hand; that obligation is no longer left implicit here but is discharged by the separate nodes 101 and 102. It is genuine work and is not supplied by the equivalence above.

Their direct consumers are exactly two: 116, which needs the cancellation to instantiate the \(\psi ^{-1}\) half of the two-sided orientation hypothesis, and 118, which needs it to turn the isometry equation for \(\psi \) into the isometry equation for \(\psi ^{-1}\). The nodes further downstream — 125, 126, 127 and 129 — do reason about \(\psi ^{-1}\), but they reach the cancellation only through those two, and so cite them rather than these nodes.

Second, Diffeomorph.mfderivToContinuousLinearEquiv_coe is not tagged @[simp], and its point argument \(x\) is implicit while the diffeomorphism and the hypothesis \(n \neq 0\) are explicit. It must therefore be rewritten by hand (typically as \(\leftarrow \) Diffeomorph.mfderivToContinuousLinearEquiv_coe with the \(n \neq 0\) side goal discharged inline), rather than being picked up by simp.

Differentiate the composite \(\psi \circ \psi ^{-1}\) at the point \(\psi (x)\), and apply the result to \(u\).

The chain rule to cite is mfderiv_comp_apply_of_eq, not mfderiv_comp (nor its _apply form). Its exact shape is

and the base-point argument \(hy\) is exactly what is needed here: instantiated at \(g := \psi \), \(f := \psi .\mathtt{symm}\), base point \(\psi (x)\) and \(y := x\), it requires \(hy : \psi .\mathtt{symm}(\psi \, x) = x\), which is Diffeomorph.symm_apply_apply. Without that transport the plain mfderiv_comp produces the outer factor as \(\mathtt{mfderiv}\; \psi \; \big(\psi .\mathtt{symm}(\psi \, x)\big)\), whose value lives in the tangent space at \(\psi (\psi .\mathtt{symm}(\psi \, x))\) rather than at \(\psi (x)\); those two tangent spaces are propositionally but not definitionally identified, so the composition does not typecheck until the base point has been transported. The _of_eq variant is the lemma that takes the transport as an argument and states its conclusion at \(y\).

The two differentiability hypotheses are Diffeomorph.mdifferentiable (side condition \(n \neq 0\)) applied to \(\psi \) and to \(\psi .\mathtt{symm}\). Finally \(\psi \circ \psi .\mathtt{symm}\) is the identity function by Diffeomorph.apply_symm_apply (and funext), so the left-hand side is \(\mathtt{mfderiv}\; \mathrm{id}\; (\psi \, x)\, u = u\) by mfderiv_id and ContinuousLinearMap.id_apply.

Since it is an mfderiv identity that is wanted and not a statement about the equivalence, 100 is deliberately not used: as recorded there, the symm of that equivalence is not definitionally \(d(\psi ^{-1})_{\psi (x)}\), so it cannot supply this.

The mirror of 101, run on \(\psi ^{-1} \circ \psi \) at \(x\): mfderiv_comp_apply_of_eq with \(g := \psi .\mathtt{symm}\), \(f := \psi \), base point \(x\) and \(y := \psi (x)\), so that the base-point argument \(hy : \psi \, x = \psi \, x\) is rfl in this order — the transport is trivial here, which is precisely why the two directions are separate nodes rather than one, the \(hy\) bookkeeping being asymmetric between them. The composite is the identity by Diffeomorph.symm_apply_apply, and mfderiv_id finishes as before.

Its consumer is 118, where it is paired with 101 to record that \(d(\psi ^{-1})_{\psi (x)}\) and \(d\psi _x\) are mutually inverse; 101 alone is what the orientation-transport nodes need.

Mathlib’s ContinuousLinearMap.inverse is defined by cases on invertibility and returns the junk value \(0\) when its argument is not invertible, so nothing can be cancelled against it until invertibility is exhibited. Here Diffeomorph.mfderivToContinuousLinearEquiv_coe identifies \(d\psi _x\) with the coercion of an equivalence, and ContinuousLinearMap.inverse_equiv rewrites the formal inverse of such a coercion as the symm of that equivalence. The two cancellation identities are then symm_apply_apply and apply_symm_apply.

Unfold 99 on both sides and apply the symmetry of \(g_{\psi (x)}\) to the pair \((d\psi _x v, d\psi _x w)\).

Since \(d\psi _x\) is surjective (100), every \(u \in TM|_{\psi (x)}\) is \(d\psi _x w\) for some \(w\), so the hypothesis says \(g_{\psi (x)}(d\psi _x v, \cdot )\) vanishes identically. Non-degeneracy of \(g\) gives \(d\psi _x v = 0\), and injectivity of \(d\psi _x\) gives \(v = 0\).

Let \(\{ e_i\} \) be a signature basis of \(TM|_{\psi (x)}\) for \(g_{\psi (x)}\), supplied by the Lorentzian condition of 19. Transport it along the inverse of the linear equivalence of 100 using Module.Basis.map, giving a basis \(\{ (d\psi _x)^{-1}e_i\} \) of \(TM|_x\). Its Gram matrix is computed by unfolding 99 and cancelling \(d\psi _x\) against \((d\psi _x)^{-1}\):

which is \(\mathrm{diag}(-1,1,1,1)\) by choice of \(\{ e_i\} \).

By the bundled form recorded in 99, the section in question is

so the goal is smoothness in \(x\) of a bilinear form obtained by precomposing a smooth family of bilinear forms with a family of continuous linear maps in both slots. Three ingredients feed it, all in the bundle-section idiom:

• smoothness of \(g\) as a section of the bilinear-form bundle over the base map \(\psi \) — the contMDiff field of the source spacetime 19, composed with \(\psi \);

• regularity of \(\psi \) itself, supplied by Diffeomorph.contMDiff, read at the same index \(\infty \) as the goal; it supplies the base map along which the previous item is read;

• smoothness of \(x \mapsto d\psi _x\) as a section of the hom bundle \(\mathrm{Hom}\big(TM|_x,\, TM|_{\psi (x)}\big)\) over the base map \(\psi \), together with invertibility of each \(d\psi _x\) (100) where the bundled form has to be recognised as a continuous linear map.

The assembly is not an instance of ContMDiff.clm_bundle_apply\(_2\): that lemma applies a bilinear-form section to two vector-field sections and returns a scalar section, so it evaluates rather than precomposes, and Mathlib has no bundle-level precomposition lemma at all — the only precomposition statement, ContMDiff.clm_comp, is for trivial bundles. The route to use instead is to unfold the goal through contMDiffAt_hom_bundle, as described next.

The route, now pinned down. This was previously recorded as an open API question. It is no longer open: every smoothness step is supplied by Mathlib, and what remains is two mechanical local identities. The chain is:

• smoothness of \(x \mapsto d\psi _x\) is ContMDiffAt.mfderiv_const (Mathlib/Geometry/Manifold/ContMDiffMFDeriv.lean:241), whose conclusion is \(\mathtt{ContMDiffAt}\) of \(\mathtt{inTangentCoordinates}\; I\; I\; \mathrm{id}\; \psi \; (\mathtt{mfderiv}\; \psi )\; x_0\). Its regularity gap \(m + 1 \le n\) holds at \(m = n = \infty \) because \(\infty + 1 = \infty \) (ENat.coe_top_add_one, which is rfl and @[simp]), so it is le_rfl, not le_top. Only \(\mathtt{At}\) and \(\mathtt{WithinAt}\) forms exist, so the global goal is opened with a single intro;

• the match between that \(\mathtt{inTangentCoordinates}\) conclusion and the \(\mathtt{inCoordinates}\) shape the goal wants is definitional: \(\mathtt{inTangentCoordinates}\) is defined as the two-base-point \(\mathtt{inCoordinates}\) (Mathlib/Geometry/Manifold/VectorBundle/Tangent.lean:518). Mathlib itself relies on this defeq, assigning the output of mfderivWithin_const directly to a goal spelled with raw inCoordinates (Mathlib/Geometry/Manifold/VectorField/Pullback.lean:423). That file’s ContMDiffWithinAt.mpullbackWithin_vectorField_inter is the canonical template for this whole node;

• the two-slot precomposition is Mathlib’s, via the identity \(\beta .\mathtt{bilinearComp}\, A\, A = (A.\mathtt{precomp}\, \mathbb {R}) \circ (\beta \circ A)\) and then ContMDiffAt.clm_precomp (Mathlib/Geometry/Manifold/ContMDiff/NormedSpace.lean:122) with ContMDiffAt.clm_comp (:170).

Two local algebraic helpers were indeed needed and had to be written by hand, but neither is a smoothness statement, and both were written as haves inside the single proof rather than as top-level lemmas. The first is the \(\mathtt{precomp}\) identity just displayed, \((\Gamma \, x).\mathtt{bilinearComp}\, (\Delta \, x)\, (\Delta \, x) = ((\Delta \, x).\mathtt{precomp}\; \mathbb {R}) \circ \big((\Gamma \, x) \circ (\Delta \, x)\big)\); it holds identically, with no side conditions, and was proved by filter_upwards, then ext v w, then simp [ContinuousLinearMap.bilinearComp_apply]. The second — that the \(\mathtt{inCoordinates}\) reading of a \(\mathtt{bilinearComp}\) is the \(\mathtt{bilinearComp}\) of the \(\mathtt{inCoordinates}\) readings — is not an identity: it holds only on the intersection of the two relevant trivialisation base sets, because continuousLinearMapAt and symmL are mutually inverse only there. It was therefore established as an eventual equality at \(x_0\), via filter_upwards on two neighbourhood facts: that \(x\) lies in the base set of the trivialisation at \(x_0\), and that \(\psi (x)\) lies in the base set of the trivialisation at \(\psi (x_0)\), the latter obtained from continuity of \(\psi \) by ContinuousAt.preimage_mem_nhds; both memberships come from FiberBundle.mem_baseSet_trivializationAt’ together with Trivialization.open_baseSet.mem_nhds. The computation then goes through hom_trivializationAt_apply, Bundle.ContinuousLinearMap.inCoordinates_apply_eq\(_2\) (twice), ContinuousLinearMap.inCoordinates_eq, and a small telescoping step cancelling a trivialisation against its inverse via Bundle.Trivialization.coe_linearMapAt_of_mem and Bundle.Trivialization.symm_linearMapAt, finishing with congr_of_eventuallyEq. One practical warning, recorded because it cost a formalization attempt: those last two lemmas live in the Bundle.Trivialization namespace, not Trivialization. In Mathlib/Topology/VectorBundle/Basic.lean the end Pretrivialization closes only the inner namespace, leaving Bundle open, so the block at line 169 nests as Bundle.Trivialization. Both helpers are of the same kind as the filter_upwards/ext/simp steps that already close the constant-metric case in Physicslib4/Spacetime/Minkowski.lean.

Two corrections to what was written here before. First, ContMDiff.clm_comp is not the only precomposition statement in Mathlib — the clm_precomp and clm_postcomp families live in the same file and are the ones actually needed. Second, the candidate list below was retained as a record of how the question was framed, but the second and third bullets are now settled by the two items above rather than open:

• on the goal side, contMDiffAt_hom_bundle in Mathlib/Geometry/Manifold/VectorBundle/Hom.lean does apply: the fibre here is \(TM|_x \to _L[\mathbb {R}] TM|_x \to _L[\mathbb {R}] \mathbb {R}\), whose source and target both sit over the single base point \(x\), and that lemma’s statement reads the fibre element through \(\mathtt{inCoordinates}\; F_1\; E_1\; F_2\; E_2\; (f\, x_0).1\; (f\, x).1\; (f\, x_0).1\; (f\, x).1\), i.e. with one and the same base point in the source and the target slots. Applying it reduces this node to smoothness of the \(\mathtt{inCoordinates}\) reading of \((\psi ^*g)_x\);

• that reduced goal is exactly the shape ContMDiffAt.mfderiv in Mathlib/Geometry/Manifold/MFDeriv/ produces for \(d\psi \), namely smoothness of the differential in the \(\mathtt{inTangentCoordinates}\) normalisation rather than as a bundle section — which is why the reduction is made in this direction and not the other;

• the surrounding inTangentCoordinates API of the same directory (inTangentCoordinates, inTangentCoordinates_eq), for matching the two readings up.

One thing to record so that it is not attempted: contMDiffAt_hom_bundle is not a possible target shape for \(x \mapsto d\psi _x\) itself. Its single-base-point form is precisely what rules that out, since \(d\psi _x : TM|_x \to _L[\mathbb {R}] TM|_{\psi (x)}\) has two base maps, the identity and \(\psi \). The two-base-map API is ContMDiffAt.clm_apply_of_inCoordinates and ContMDiffWithinAt.clm_apply_of_inCoordinates, whose hypothesis is stated as smoothness of \(\mathtt{inCoordinates}\; F_1\; E_1\; F_2\; E_2\; (b_1\, m_0)\; (b_1\, m)\; (b_2\, m_0)\; (b_2\, m)\; (\varphi \, m)\), with independent \(b_1\) and \(b_2\); Mathlib gives these only in the \(\mathtt{At}\) and \(\mathtt{WithinAt}\) forms, because the \(\mathtt{inCoordinates}\) hypothesis only makes sense around a point.

These do compose into the ingredient as stated. No intermediate top-level lemma was needed: the two local identities above are discharged inline, inside the single proof. All three ingredients are Mathlib-backed as they stand.

The manifold data are carried over verbatim from \((M,g)\), so only the metric obligations of 19 need discharging: symmetry is 104, non-degeneracy is 105, the Lorentzian condition is 106, and the contMDiff field — smoothness of the metric as a section of the bilinear-form bundle — is 107.

This is ContMDiff.mpullback_vectorField, whose four hypotheses must all be supplied — they are more than invertibility of the differential:

• \(hV\): \(\mathtt{CMDiff}\; m\; (\mathtt{T\% }\; V)\), the hypothesis of this node, which for \(V = t\) is the smooth field of 25 verbatim.

• \(hf\): \(\mathtt{CMDiff}\; n\; \psi \), from \(\psi \) being a smooth diffeomorphism (Diffeomorph.contMDiff); as everywhere in this section the index is \(n = \infty \), matching 19.

• \(hf'\): \(\forall x,\ (\mathtt{mfderiv\% }\; \psi \; x).\mathtt{IsInvertible}\). This is \(\mathtt{ContinuousLinearMap.IsInvertible}\) — a predicate on a continuous linear map — and not a ContinuousLinearEquiv, so 100 does not supply it directly. The bridge is: rewrite \(d\psi _x\) as the coercion of the equivalence using Diffeomorph.mfderivToContinuousLinearEquiv_coe (backwards, by hand, since it is not a simp lemma; see 100), then close the goal with ContinuousLinearMap.isInvertible_equiv, which states that the coercion of any ContinuousLinearEquiv is invertible.

• \(hmn\): the exponent gap \(m + 1 \leq n\). Here \(m = n = \infty \), and the gap holds because \(\infty + 1 = \infty \) (ENat.coe_top_add_one, which is rfl and @[simp]), so it is le_rfl, not le_top.

It further requires the instances \([\mathtt{CompleteSpace}\; E]\) and \([\mathtt{IsManifold}\; I\; 1\; M]\) (both source and target instances, which coincide here since \(\psi \) maps \(M\) to itself); \(E = \mathbb {R}^4\) is complete and the \(\infty \)-smooth structure of 19 gives the manifold instance at order \(1\).

By 103 the formal inverse \((d\psi _x)^{-1}\) occurring in VectorField.mpullback is the symm of a continuous linear equivalence, hence injective (ContinuousLinearEquiv.injective), and it sends \(0\) to \(0\). Since \(t_{\psi (x)} \neq 0\) by the non-vanishing field of 25, the image is nonzero. Without 103 this fails: \(\mathtt{ContinuousLinearMap.inverse}\) returns the junk value \(0\) off the invertible case and is then not injective.

Unfold 99 (whose defining equation is recovered from the bundled form by \(\mathtt{bilinearComp\_ apply}\)), so that the left-hand side reads \(g_{\psi (x)}\big(d\psi _x\, (d\psi _x)^{-1} t_{\psi (x)},\, d\psi _x\, (d\psi _x)^{-1} t_{\psi (x)}\big)\). Cancel each occurrence by 103 alone. That suffices, and 101 is deliberately not needed here: the inverse appearing in this expression is the one written into \(\mathtt{VectorField.mpullback}\), namely \(\mathtt{ContinuousLinearMap.inverse}\, (d\psi _x)\), and not \(\mathtt{mfderiv}\; \psi .\mathtt{symm}\; (\psi \, x)\). So the cancellation required is the apply_symm_apply of the equivalence, exactly as recorded in the first implementation point of 100; the global-inverse round trip is a different identity and would be an unnecessary detour. The resulting quantity is negative by the timelike field of 25 for \(t\) at \(\psi (x)\).

Assemble the three fields of a \(\mathtt{TimeOrientation}\) for \(\psi ^*(M,g)\). Smoothness is one step: apply 110 at \(V = t\), whose hypothesis is the smooth field of 25 for \(t\) as it stands and whose conclusion is the smooth field required of \(\psi ^*t\); both sides are bundle-section statements, so no conversion is performed in either direction. Non-vanishing is 111 and timelikeness is 112.

Unfold 99 in the left-hand side and cancel \(d\psi _x\big((d\psi _x)^{-1} t_{\psi (x)}\big) = t_{\psi (x)}\) by 103. Timelikeness transports immediately, since \((\psi ^*g)_x(v,v) = g_{\psi (x)}(d\psi _x v, d\psi _x v)\) is the defining equation of 99 at \(w = v\). Both sides of the claimed equivalence therefore sit in the timelike branch of 26, where future-pointing is exactly negativity of the displayed quantity.

Future-pointing for a null vector is not a sign condition: by 26 it is the existence of a sequence \(v_n\) of future-pointing timelike vectors with \(v_n \to v\). So the sign argument of 114 does not apply directly and the witnessing sequence must be transported.

Given such a sequence for \(v\), put \(w_n := d\psi _x v_n\). Each \(w_n\) is timelike and future-pointing for \((g,t)\) by 114, and \(w_n \to d\psi _x v\) because \(d\psi _x\) is a continuous linear map (100), so \(\mathtt{Filter.Tendsto}\) composes with its continuity at \(v\). As \(d\psi _x v\) is null for \(g\), the sequence \((w_n)\) witnesses the null branch for \(d\psi _x v\). The converse runs the same argument with \((d\psi _x)^{-1}\), itself continuous and linear.

A future-pointing vector is either timelike or null (26). The timelike case is 114 and the null case is 115; each is an equivalence, so it yields both the forward direction for \(\psi \) and the forward direction for \(\psi ^{-1}\).

The \(\psi ^{-1}\) half is where 101 is spent, and it is worth naming the point exactly, since the edge is otherwise unlocatable in the argument. That half asks: for \(y \in M\) and \(u \in TM|_y\) future-pointing for \((g,t)\), show \(d(\psi ^{-1})_y u\) is future-pointing for \((\psi ^*g, \psi ^*t)\). Put \(x := \psi ^{-1}(y)\), so \(y = \psi (x)\), and apply the equivalence at \(x\) to the vector \(v := d(\psi ^{-1})_{\psi (x)}u\): it says \(v\) is future-pointing for \((\psi ^*g,\psi ^*t)\) iff \(d\psi _x v\) is future-pointing for \((g,t)\). But \(d\psi _x v = d\psi _x\big(d(\psi ^{-1})_{\psi (x)}u\big) = u\) by 101, so the right-hand side is the hypothesis. The same rewriting is also what supplies the causal-type side condition of the equivalence, \((\psi ^*g)_x(v,v) = g_{\psi (x)}(d\psi _x v, d\psi _x v) = g_y(u,u)\), so \(v\) sits in the same timelike-or-null branch as \(u\). Without the cancellation the two sides of the equivalence simply do not meet the hypothesis, since \(d\psi _x\, d(\psi ^{-1})_{\psi (x)}u\) is not syntactically \(u\).

Given \(y\), put \(x := \psi ^{-1}(y)\), so that \(y = \psi (x)\) by Diffeomorph.apply_symm_apply; every point of \(M\) is of this form, so it is enough to prove the equation at \(y = \psi (x)\). Instantiate the defining equation of 117 at \(x\) with \(v := d(\psi ^{-1})_{\psi (x)}u\) and \(w := d(\psi ^{-1})_{\psi (x)}u'\):

and rewrite the two arguments on the left with 101, which turns them into \(u\) and \(u'\). The two mutual-inverse identities are 101 and 102 as they stand.

This node exists to replace a hand-wave. The reverse inclusions in 125 and 126 apply 124 to \(\psi ^{-1}\), which requires \(\psi ^{-1}\) to be a cross-metric isometry in the opposite direction; that is not the defining equation of 117 “read backwards”, since reading it backwards gives an equation about \(d\psi \), not about \(d(\psi ^{-1})\), and passing between the two is exactly the cancellation above.

Specialise the defining equation of 117 to \(w = v\); the three equivalences follow because the sign of the metric square is unchanged. The single-metric 93 does not apply: source and target metrics differ here, so the statement is not an instance of it.

This is mfderivWithin_comp for the composite of \(\mu \) with \(\psi \). Write \(P\) for the parameter space of \(\mu \) (the inner set), \(u\) for the outer set, and keep \(s \in P\) for the parameter of the statement; the set and the point must be kept notationally apart, since mfderivWithin_comp takes both. With that convention its exact hypotheses are

of which two are easy to overlook. The uniqueness hypothesis is pointwise — a \(\mathtt{UniqueMDiffWithinAt}\) at the single parameter \(s\), not a \(\mathtt{UniqueMDiffOn}\) on the whole of \(P\) — so what 94 supplies must be specialised to \(s\) and converted, as \((\dots \, s\, hs).\mathtt{uniqueMDiffWithinAt}\). And there is a set side condition \(P \subseteq \mu ^{-1}(u)\) relating the inner set to the outer one; here \(u = \mathtt{univ}\), so it is immediate, and correspondingly the outer derivative is an unrestricted mfderiv obtained by mfderivWithin_univ. Differentiability of \(\mu \) within \(P\) comes from its smoothness, and differentiability of \(\psi \) from Diffeomorph.mdifferentiable (with side condition \(n \neq 0\)), which is what the repository template cited below actually uses — not from 100, which delivers a ContinuousLinearEquiv rather than an \(\mathtt{MDifferentiableWithinAt}\) hypothesis.

Do not re-derive this: the repository already contains the single-metric form of exactly this statement, Physicslib4.Spacetime.Isometry.mfderivWithin_comp_diffeo in Physicslib4/Spacetime/IsometryCausality.lean:43, whose proof carries out precisely the four steps above (including the uniqueMDiffWithinAt specialisation and the mfderivWithin_univ rewrite). The cross-metric statement is obtained by copying it with the target metric changed, since the identity is about the differential of \(\psi \) alone and mentions no metric. Similarly, the unique-differentials input 94 is already proved as Physicslib4.Spacetime.Path.uniqueDiffOn_parameterSpace in Physicslib4/Spacetime/Curves.lean:119 and should be cited rather than reproved.

The parameter space and its properties are copied. Continuity and smoothness of \(\psi \circ \mu \) follow by composing the smooth \(\psi \) with the smooth \(\mu \). Non-vanishing of the tangent vector is the only real obligation: rewrite it with 120 and use that \(d\psi _{\mu (s)}\) is injective (100) together with non-vanishing of \(\dot\mu (s)\).

Again this should be assembled from the existing template rather than rederived: Physicslib4.Spacetime.Isometry.pushforwardPath in Physicslib4/Spacetime/IsometryCausality.lean:70 is the single-metric version of this very construction, and its nonvanishing field is the template for the obligation above — it rewrites with mfderivWithin_comp_diffeo, then with \(\leftarrow \) Diffeomorph.mfderivToContinuousLinearEquiv_coe and ContinuousLinearEquiv.coe_coe to expose the equivalence, and finishes with its injective. The remaining fields (parameterSpace, isClosed, isConnected, nontrivial, continuousOn, smoothOn) are copied verbatim from that template, none of them mentioning a metric.

Fix \(s\) and rewrite the tangent vector of \(\psi \circ \mu \) using 120. The classification of \(d\psi _{\mu (s)}\dot\mu (s)\) for \(g_2\) agrees with that of \(\dot\mu (s)\) for \(g_1\) by 119; for the causal case split on the timelike and null disjuncts. This mirrors \(\mathtt{pushforwardPath\_ isTimelike}\) and \(\mathtt{pushforwardPath\_ isCausal}\).

Being an endpoint (39) asserts the existence of a parameter \(s\) that is minimal (respectively maximal) in the parameter space with \(\mu (s) = p\). The pushforward has the same parameter space and \((\psi \circ \mu )(s) = \psi (p)\), so the same \(s\) witnesses the condition; no metric or causal input is used. This mirrors \(\mathtt{pushforwardPath\_ isPastEndpoint}\) and \(\mathtt{pushforwardPath\_ isFutureEndpoint}\).

A witness for \(p \ll _1 q\) is a future-oriented trip (42) from \(p\) to \(q\) for \(g_1\). Push it forward by 121: it is timelike for \(g_2\) by 122, has endpoints \(\psi (p)\) and \(\psi (q)\) by 123, and is future-oriented because \(d\psi \) carries future-pointing tangent vectors to future-pointing tangent vectors (109). So it witnesses \(\psi (p) \ll _2 \psi (q)\).

The inclusion \(\subseteq \) is 124 applied to \(p \ll _1 q\). For \(\supseteq \), note that \(\psi ^{-1}\) is an isometry from \((M,g_2)\) to \((M,g_1)\) by 118, and preserves the future orientation by the second half of the two-sided hypothesis. Applying 124 to \(\psi ^{-1}\) at the point \(\psi (p)\) gives \(\psi ^{-1}\big(I^+_2(\psi (p))\big) \subseteq I^+_1(p)\), which is the reverse inclusion after applying the bijection \(\psi \).

Take the skeleton from the repository rather than inventing one: the single-metric forms Physicslib4.Spacetime.Isometry.chronologicalFuture_image_subset and ...chronologicalFuture_image in Physicslib4/Spacetime/IsometryCausality.lean:270,294 are exactly this argument, and the cross-metric version differs only in carrying two metrics. In particular their proofs use neither Set.image_subset_iff nor any Equiv.image_eq_preimage-style rewriting, which is the tempting but wrong route: the \(\subseteq \) half destructures the image membership directly (rintro _ \(\langle \)q, hq, rfl\(\rangle \)) and the \(\supseteq \) half exhibits the witness \(\psi ^{-1}(r)\) together with the point-level cancellation toDiffeo_inv_apply. The chronology step itself is lifted along the transitive closure by Relation.TransGen.lift.

Identical to 125 with the roles of the two endpoints of the trip exchanged: \(q \in I^-_1(p)\) means \(q \ll _1 p\), so the same two applications of 124, to \(\psi \) and to \(\psi ^{-1}\) — the latter being a cross-metric isometry from \((M,g_2)\) to \((M,g_1)\) by 118 — give the two inclusions.

The image of an intersection under an injective map is the intersection of the images, and the two factors are computed by 125 and 126. In the case of interest, \(g_1 = \psi ^*g_2\) with the pulled-back time orientation of 113, the orientation hypothesis holds by construction (116); in general it is carried as a hypothesis.

Purely topological, with no geometry involved. By continuous_generateFrom_iff continuity of \(f\) reduces to \(f^{-1}(T)\) being open for each \(T \in \mathcal{T}\), and \(f^{-1}(T) \in \mathcal{S}\) is open by TopologicalSpace.isOpen_generateFrom_of_mem. The same argument applied to \(f^{-1}\), using that \((f^{-1})^{-1}(S) = f(S) \in \mathcal{T}\) since \(f\) is a bijection, gives continuity of the inverse. Bundle the two with the bijection as a Homeomorph.

Two naming and notation points. The openness lemma lives in the TopologicalSpace namespace and must be cited by its fully qualified name: the unqualified isOpen_generateFrom_of_mem does not resolve. By contrast continuous_generateFrom_iff genuinely is in the root namespace and is cited as written. Its exact form is

so only the source topology is written explicitly, as the bracket argument \(t\), while the right-hand side carries a plain IsOpen — resolved against whatever instance is in scope on the source — and the target is forced to be a generateFrom. The point to record is that \(t\) is an implicit variable, not an instance argument: at the application site below the source is the carrier \(M\), which already carries its manifold topology as a registered instance, and that instance is what unification will pick unless \(t\) is instantiated by hand with the Alexandrov generateFrom term. So the lemma must be applied with \(t\) given explicitly (and the resulting plain IsOpen goals read against that same term), since the two Alexandrov topologies are TopologicalSpace terms, not instances on the carrier. Silently letting the manifold topology be inferred yields a well-typed but wrong statement, which is the failure mode to guard against here.

Apply 128 with \(f := \psi \), a bijection of the common carrier, and with \(\mathcal{S}\), \(\mathcal{T}\) the families of Alexandrov diamonds of \(\psi ^*g\) and of \(g\) (73), whose generated topologies are the two Alexandrov topologies by definition. The hypothesis that \(\psi \) carries \(\mathcal{S}\) onto \(\mathcal{T}\) is 127 applied to \(\psi \) and to \(\psi ^{-1}\), whose two-sided orientation hypothesis holds by 116.

The underlying spacetime is 108 and the time orientation is 113, so only the Hausdorff condition on the Alexandrov topology remains. It transports along the homeomorphism of 129 by Homeomorph.t2Space.

Unfolding DirectedOn turns the goal into the statement of 88, which is therefore applied directly. The passage from the set-level DirectedOn to the subtype-level IsDirectedOrder that the colimit construction wants as an instance is Mathlib’s DirectedOn.isDirectedOrder. There is no mathematical content here beyond 88; the node exists so that the colimit nodes can cite an instance rather than restate a \(\forall \exists \) statement.

Mathlib’s DirectedSystem f is a two-field class: map_self, saying \(f_{\le \mathrm{rfl}} = \mathrm{id}\), and map_map, saying \(f_{jk} \circ f_{ij} = f_{ik}\). These are literally Axiom 2(b) and Axiom 2(c) (132), so the instance is constructed by supplying those two projections. This is the node that cashes in the remark in 132 that (b) and (c) make the assignment a functor.

Two representatives of the same class become equal after transport into a common containing diamond, which exists by 133. That transport is by isotony embeddings, and those are isometric — NonUnitalStarAlgHom.norm_map applied with Axiom 2(a) (132) in the complex C*-algebras of Axiom 1 (131) — so each representative has the same norm as their common image and hence the same norm as the other.

This is Mathlib’s DirectLimit.exists_eq_mk\(_2\), theorem exists_eq_mk\(_2\) (z w : DirectLimit F f) : \(\exists \) i x y, z = [\(\langle \)i, x\(\rangle \)] \(\wedge \) w = [\(\langle \)i, y\(\rangle \)], applied to the directed system 134; its directedness hypothesis is 133 through DirectedOn.isDirectedOrder. When the goal is a proposition rather than data, the same fact is packaged as the induction principle DirectLimit.induction\(_2\), which is the form actually used in tactic proofs.

The node exists because every two-element claim about the colimit norm below opens with this move — subadditivity and submultiplicativity in 137 — and in Lean it is a two-line obtain that would otherwise be repeated verbatim.

Every clause is transport along a representative, which is why they share a node. For the two binary clauses take a common diamond \(\mathbf{B}\) and representatives \(a, b \in \mathfrak {U}(\mathbf{B})\) with \(x = \iota _{\mathbf{B}}(a)\), \(y = \iota _{\mathbf{B}}(b)\) by 136; for the unary clauses one representative suffices. Since \(\iota _{\mathbf{B}}\) is a unital \(\mathbb {C}\)-algebra homomorphism (the Algebra instance recorded at the start of this subsection), \(0\), \(-x\), \(c \cdot x\), \(x + y\) and \(xy\) are \(\iota _{\mathbf{B}}(0)\), \(\iota _{\mathbf{B}}(-a)\), \(\iota _{\mathbf{B}}(c \cdot a)\), \(\iota _{\mathbf{B}}(a+b)\) and \(\iota _{\mathbf{B}}(ab)\).

Rewriting every colimit norm as a \(\mathfrak {U}(\mathbf{B})\)-norm with 135 then reduces the clauses to norm_zero, norm_neg, norm_add_le, norm_mul_le and norm_smul in the C*-algebra \(\mathfrak {U}(\mathbf{B})\) (131).

Positive definiteness is the one clause with content beyond transport, and it is where Axiom 2(a) is spent. From \(\| x\| = 0\) and 135 we get \(\| a\| = 0\), hence \(a = 0\) by norm_eq_zero in \(\mathfrak {U}(\mathbf{B})\); the step from \(a = 0\) to \(x = 0\) is injectivity of \(\iota _{\mathbf{B}}\), which is DirectLimit.mk_injective applied with Axiom 2(a) (132).

Assembling the RingNorm and feeding it to RingNorm.toNormedRing, then adding homogeneity as norm_smul_le, is one term each.

Assemble. The \(*\)-algebra structure over \(\mathbb {C}\) is supplied by Mathlib’s DirectLimit instances, recorded at the start of this subsection and found by typeclass inference once 134 is in place; 135 supplies the norm function; 137 supplies the axioms that norm satisfies, in the assembled form NormedRing plus NormedSpace \(\mathbb {C}\). The NormedAlgebra \(\mathbb {C}\) structure asserted above is exactly that NormedSpace \(\mathbb {C}\) together with the Algebra \(\mathbb {C}\) instance from DirectLimit: NormedAlgebra has no field beyond Algebra other than norm_smul_le, which is the NormedSpace field. It is stated in the NormedAlgebra form here because that is what 140 consumes downstream. Bundling them is the normed \(*\)-algebra structure.

The StarModule \(\mathbb {C}\) field, \((c \cdot x)^{*} = \bar{c} \cdot x^{*}\), is explicitly part of what this node supplies, and it costs nothing: it is the StarModule \(\mathbb {C}\) (DirectLimit G f) instance (autogenerated name DirectLimit.instStarModule), found by typeclass inference from the corresponding StarModule \(\mathbb {C}\) structure on each local algebra. It is listed because downstream it is a required field of CStarAlgebra, and on the completion side (142) the analogous field is not free.

Nothing is claimed here about the involution being isometric, and nothing needs to be: \(\| x^{*}\| = \| x\| \) comes free from the C*-inequality (139) through CStarRing.to_normedStarGroup.

A single element is involved, so no directedness is needed here. Pick a representative \(a \in \mathfrak {U}(\mathbf{B})\) of \(x\). Then \(x^{*}x\) has the representative \(a^{*}a\) in the same \(\mathfrak {U}(\mathbf{B})\), since the involution acts on representatives by DirectLimit.star_def, and by 135 the colimit norms of \(x\) and \(x^{*}x\) are the norms of \(a\) and \(a^{*}a\) there. So the claim reduces to \(\| a\| \, \| a\| \le \| a^{*}a\| \) in \(\mathfrak {U}(\mathbf{B})\), which is the CStarRing instance carried by the local algebras (131), available as CStarRing.norm_mul_self_le.

Four component laws are asserted, and they are proved as four standalone named lemmas, not as inline field bodies: call them Completion.star_star’, Completion.star_add’, Completion.star_mul’ and Completion.star_smul’. Each is about four lines by one shared skeleton. Both sides of the law are continuous in their arguments, by continuity of \(\star _{\widehat{A}}\) (141) together with continuity of the relevant operation on the normed ring \(\widehat{A}\); so the locus where they agree is closed by isClosed_eq — whose continuity side goals are the fun_prop one-liners recorded in 141 — and UniformSpace.Completion.induction_on (in its \({}_2\) form for the two-variable laws) reduces the claim to the canonical image. There the characterisation \(\eta (a)^{*} = \eta (a^{*})\) of 141 (UniformSpace.Completion.map_coe) applies, and the four differ only in which coercion lemma and which component law of \(A\) are cited afterwards:

• star_star’: star_star in \(A\);

• star_add’: UniformSpace.Completion.coe_add then star_add in \(A\);

• star_mul’: UniformSpace.Completion.coe_mul then star_mul in \(A\);

• star_smul’: UniformSpace.Completion.coe_smul, giving \(c \cdot \eta (a) = \eta (c \cdot a)\), then star_smul in \(A\) — which is exactly the StarModule \(\mathbb {C}\) A hypothesis of 140, and the reason that hypothesis is on the list.

The two instances are then assembled from those named lemmas by two one-line wheres: StarRing \(\widehat{A}\) from the first three, StarModule \(\mathbb {C}\) \(\widehat{A}\) from the fourth. Writing the four out as lemmas rather than inlining them as field bodies is what keeps each piece at the four-line size; the assembly itself carries no content. Note that multiplication on \(\widehat{A}\) is continuous but not uniformly continuous, so the anti-multiplicativity step is genuinely a continuity-plus-density argument and not a uniform-extension one; the skeleton above is chosen for that reason. Mathlib’s own norm_mul_le field for UniformSpace.Completion.instNormedRing is written in precisely this style — induction_on\({}_2\), then isClosed_le discharged by fun_prop, then simpa only [\(\leftarrow \) coe_mul, norm_coe] — and is four lines long, so it is the in-tree template for every obligation in this block. The ring and norm structure on \(\widehat{A}\) is that same instNormedRing (141), found by typeclass inference; that \(\eta \) commutes with \(\star \) and has dense range, and that the extension is the unique continuous one, are recorded in 141.

Isometry of \(\star _{\widehat{A}}\) is deliberately not part of the statement and needs no density argument of its own: once \(\widehat{A}\) carries the C*-inequality (144) the NormedStarGroup \(\widehat{A}\) instance, and with it \(\| x^{*}\| = \| x\| \), is produced by CStarRing.to_normedStarGroup.

Every law needed is already available unbundled; the content of this node is that the bundling has to be done by hand, and it is worth a node precisely so that the fact is not mistaken for a citation. Mathlib supplies the coercion only as a ring homomorphism, UniformSpace.Completion.coeRingHom; there is no coeStarAlgHom, and no algebra-homomorphism counterpart either, anywhere in the completion files audited in 140. So map_one, map_mul, map_add come from coeRingHom, and the two remaining fields are supplied individually. The first is the AlgHom field, and its name matters: StarAlgHom \(\mathbb {C}\) extends AlgHom, whose scalar field is commutes’ — agreement of the map with the two algebraMaps — and not map_smul. It discharges essentially by rfl from the definition of UniformSpace.Completion.algebra, whose smul_def’ field already characterises the scalar action through \(\eta \circ \texttt{algebraMap}\); the unbundled coercion law \(c \cdot \eta (a) = \eta (c \cdot a)\), UniformSpace.Completion.coe_smul, is what backs it if the rfl does not fire. The second is map_star, which is the characterisation \(\eta (a)^{*} = \eta (a^{*})\) of 141, which 142 records as part of making \(\eta \) a \(*\)-homomorphism. Assembling those five fields into a StarAlgHom is a single anonymous-constructor term.

This node is stated for a general \(A\) rather than only for the colimit because that is the generality at which it is true and at which the rest of this block is written; its consumer is 153, which needs a bundled morphism and would otherwise have to inline this assembly.

Routine, not hard, and worth saying why. CStarRing is a Prop-valued class with exactly one field, norm_mul_self_le : \(\forall \, x,\ \| x\| * \| x\| \le \| x^{\star } * x\| \) (Analysis/CStarAlgebra/Basic.lean:89). That field is a non-strict inequality between two continuous real-valued functions of the single variable \(x\), so it transports to the completion in about four lines: the locus where it holds is closed by isClosed_le, and UniformSpace.Completion.induction_on reduces the goal to the canonical image.

On the canonical image it is the C*-inequality of \(A\): \(\eta \) is a ring and \(*\)-homomorphism (142) and is norm preserving by UniformSpace.Completion.norm_coe, so \(\| \eta (a)^{*}\eta (a)\| = \| \eta (a^{*}a)\| = \| a^{*}a\| \ge \| a\| \, \| a\| = \| \eta (a)\| \, \| \eta (a)\| \). Continuity of the two sides is the same package as elsewhere: the involution is continuous by 142, and multiplication and the norm are continuous on a normed ring.

Two consequences worth recording. First, isometry of the involution on \(\widehat{A}\) is not a separate obligation anywhere in this block: it follows from this inequality through CStarRing.to_normedStarGroup (Basic.lean:114). Second, CStarRing does not itself require completeness — its hypotheses are only NonUnitalNormedRing and StarRing — which is why the same inequality is available on the colimit before completing, as 139 asserts.

This node exists to work around one specific trap, and the trap is the whole of its content. Mathlib does have a NormedAlgebra instance on a completion (Analysis/Normed/Module/Completion.lean:87), but it is gated on SeminormedCommRing A — commutative — so it does not fire here: \(A\) is noncommutative in every case of interest. Without noticing this one would expect the instance for free and discover at formalization time that typeclass inference simply fails to find it.

Supplying it by hand is short. NormedAlgebra has exactly one field beyond Algebra, namely norm_smul_le, \(\| c \cdot x\| \le |c|\, \| x\| \); and that field is already available from the NormedSpace instance on the completion of a normed space (line 36 of the same file), which carries no commutativity hypothesis. So the instance is UniformSpace.Completion.algebra together with norm_smul_le borrowed from that NormedSpace instance — a where with a single field.

This is also where scalar-action compatibility would live, if it is needed at all, and the evidence is that it is not. There are two a priori different SMul \(\mathbb {C}\) \(\widehat{A}\) structures in play: the one underlying UniformSpace.Completion.algebra, characterised by its smul_def’ field as \(c \cdot x = \eta (\texttt{algebraMap } c)\, x\), and the one underlying the NormedSpace instance, which extends the scalar action on \(A\). Mathlib’s own commutative NormedAlgebra instance has the body norm_smul_le := norm_smul_le and nothing else: it borrows the NormedSpace field directly, with no agreement argument, and — decisively — never uses the commutativity hypothesis in that body. So the identical body compiles in the noncommutative setting, and this node is three lines. Nothing below is needed; it is recorded only against the remote possibility that the two actions fail to be definitionally equal, in which case the fix is the usual induction_on plus isClosed_eq step: on the canonical image each action sends \(\eta (a)\) to \(\eta (c \cdot a)\), the first by UniformSpace.Completion.coe_mul with Algebra.smul_def in \(A\), the second by UniformSpace.Completion.coe_smul.

For the record, so that none of it is re-proved: what is free on the completion, without commutativity, is UniformSpace.Completion.ring and UniformSpace.Completion.algebra — both named declarations, in Topology/Algebra/UniformRing.lean — together with UniformSpace.Completion.instNormedRing, the NormedSpace and NormedAddCommGroup instances of Analysis/Normed/Module/Completion.lean, and the norm-preservation lemma UniformSpace.Completion.norm_coe. Those three instances are declared anonymously in the source but carry the usual auto-generated names and can be cited by them; and none is commutativity-gated — instNormedRing asks only for SeminormedRing A, and the NormedSpace instance only for a seminormed additive group with a scalar action. It is precisely and only the NormedAlgebra instance twelve lines further down the same file that adds SeminormedCommRing, which is what makes this node necessary.

Pure bundling, and the audit confirms it is literally that: CStarAlgebra is declared as class CStarAlgebra (A : Type*) extends NormedRing A, StarRing A, CompleteSpace A, CStarRing A, NormedAlgebra \(\mathbb {C}\) A, StarModule \(\mathbb {C}\) A with an empty body (Analysis/CStarAlgebra/Classes.lean:30-42). It adds no field of its own beyond its parents, so once the parents below are in place this node is a where with an essentially empty body. Exactly those six parents are supplied for \(\widehat{A}\):

• NormedRing \(\widehat{A}\): found by typeclass inference, and citable by name as UniformSpace.Completion.instNormedRing (Analysis/Normed/Module/Completion.lean:75), whose only hypothesis is SeminormedRing A — no commutativity, unlike the NormedAlgebra instance in the same file that forces 145 to exist. Note that multiplication on \(A\) is not uniformly continuous — only uniformly continuous on bounded sets — so it is extended as a bounded bilinear map rather than by uniform continuity, which is exactly what that instance arranges.

• StarRing \(\widehat{A}\): 142.

• CompleteSpace \(\widehat{A}\): nothing to prove — this is the ambient CompleteSpace instance that comes with the completion, UniformSpace.Completion.completeSpace, not an obligation of this node.

• CStarRing \(\widehat{A}\): 144.

• NormedAlgebra \(\mathbb {C}\) \(\widehat{A}\): 145.

• StarModule \(\mathbb {C}\) \(\widehat{A}\): 142, which supplies this instance alongside the StarRing one above — the conjugate-linearity law is one of the four it establishes.