Stationary product time is a Cauchy temporal coordinate

Smoothness of $s$ follows from the supplied inverse diffeomorphism. The flow laws give ${\varphi }_t^{-1}={\varphi }_{-t}$ and $s\circ {\varphi }_t=s+t$. The flow definition of the Lie derivative and the group law give $\frac{d}{dt}{\varphi }_t^{\ast }g={\varphi }_t^{\ast }({\mathcal{L}}_{T}g)=0$, so each ${\varphi }_t$ is an isometry. It preserves time orientation: the image of a future timelike vector varies continuously with $t$, stays timelike, and starts in the future cone, so it cannot change to the past cone. The isometry therefore preserves future causal cones as well. Thus the levels $s^{-1}(t)={\varphi }_t(C)$ are spacelike.

Fix $t\in \mathbb{R}$ and an inextendible future causal curve $\gamma :I\to E$. By [F3], $\eta ={\varphi }_{-t}\circ \gamma$ is locally absolutely continuous with $\eta \mathrm{\prime }=d{\varphi }_{-t}(\gamma \mathrm{\prime })$ almost everywhere. The isometry has invertible differential and preserves future causal cones, so this velocity is nonzero future causal almost everywhere. If $\eta$ converged to $q\in E$ at either parameter end, continuity of ${\varphi }_t$ would force $\gamma ={\varphi }_t\circ \eta$ to converge to ${\varphi }_t(q)$ there, contrary to [F2]. Thus $\eta$ is inextendible. Since $C$ is Cauchy, $\eta$ meets $C$ at exactly one parameter value; equivalently $\gamma$ meets ${\varphi }_t(C)$ exactly once. For a past causal curve the same argument preserves its past causal velocity and gives exactly one crossing as well. Hence every level of $s$ is Cauchy.

The covector $ds$ annihilates the spacelike tangent hyperplane of its level and satisfies $ds(T)=1$. At ${\varphi }_t(p)$ let $n_t=d{\varphi }_t(n_p)$ and $N=-g(T,n_t)$. Invariance of $T$ under its own isometric flow gives $N=-g(T,n_p)>0$. Write $T=N{n}_t+X$ with $X$ tangent to the level. Then $1=ds(T)=Nds(n_t)$, so $ds(n_t)=1\mathrm{/}N$ and the metric dual is $\mathrm{\nabla }s=-n_t\mathrm{/}N$. It is therefore past timelike. In a Lorentz orthonormal frame with future unit vector $n_t$, any nonzero future causal $v$ has positive time component, whence $ds(v)=-g(n_t,v)\mathrm{/}N>0$.

For any future causal $\gamma :I\to E$, [F3] makes $h=s\circ \gamma$ locally absolutely continuous with $h\mathrm{\prime }(r)=ds(\gamma \mathrm{\prime }(r))>0$ almost everywhere by [F2] and step 2.2. On each compact $[a,b]\subseteq I$, finite subdivision from [F3] gives absolute continuity of $h$ on the whole interval: for a test family of disjoint intervals, split at the finitely many subdivision points and use each piece's absolute-continuity bound with tolerance divided by the number of pieces. For $a<b$, [F4] gives $h(b)-h(a)={\int }_a^{b}h\mathrm{\prime }(r)dr$. Choose the nonnegative measurable representative of $h\mathrm{\prime }$ obtained by setting it to zero on its null exceptional set. It is positive almost everywhere on the positive-measure interval $[a,b]$, so [F5] makes its integral strictly positive. Consequently $h(b)>h(a)$ and $s$ increases strictly along every future causal curve.

For an inextendible future causal curve, step 2.1 gives exactly one meeting with each level $s^{-1}(R)$, for every $R\in \mathbb{R}$, so $s\circ \gamma$ has range $\mathbb{R}$. By strict increase from step 3.1, after the parameter where $s=R$ all values exceed $R$, and before it all values are below $R$. Since $R$ is arbitrary, the future and past endpoint limits are $+\mathrm{\infty }$ and $-\mathrm{\infty }$, respectively. Together with smoothness, the past timelike gradient and the spacelike Cauchy levels already proved, these are all the asserted conclusions.