Proper time along a $C^1$ future timelike curve: strictly increasing reparametrization with $\eta (U,U)=-c^2$

$J$ is order-convex with at least two elements, and every point of $J$ is a limit point of $J$ and lies in its interior: $J$ is a nonempty open interval and so has one of the forms $(a,b)$, $(a,\mathrm{\infty })$, $(-\mathrm{\infty },b)$, $\mathbb{R}$ with strict defining inequalities, so a sufficiently small neighbourhood of any $s\in J$ is contained in $J$, whence a punctured neighbourhood of $s$ meets $J$ again, and $J$ contains two distinct points.

$g$ is continuous on $J$: by [L3] each component $z^a$ of the $C^1$ curve has a continuous derivative $z^a{}^{\mathrm{\prime }}$. By [L1], $g(s)=-\eta (z^{\mathrm{\prime }}(s),z^{\mathrm{\prime }}(s))=(z^0{}^{\mathrm{\prime }}(s){)}^2-{\sum }_{i=1}^3(z^i{}^{\mathrm{\prime }}(s){)}^2={\sum }_{a=0}^3{ϵ}_a(z^a{}^{\mathrm{\prime }}(s){)}^2$ with $ϵ=(1,-1,-1,-1)$. This finite sum of squares and scalar multiples of continuous functions is continuous by [L7].

$s\mapsto \sqrt{g(s)}$ is continuous on $J$: on $[0,\mathrm{\infty })$ the map $x\mapsto x^2$ is continuous by [L7], strictly increasing by [L6], and its image is $[0,\mathrm{\infty })$ by [L5]; hence its inverse, which is $\sqrt{\cdot }$ by the uniqueness in [L5], is continuous on $[0,\mathrm{\infty })$ by [L8], and composing with the continuous $g$ gives a continuous function by [L9].

$h(s):=c^{-1}\sqrt{g(s)}$ is continuous on $J$: it is the scalar multiple of the continuous function $\sqrt{g}$ by the constant $c^{-1}$, which exists because $c>0$, and scalar multiples of continuous functions are continuous by [L7].

$\tau$ is a primitive of $h$ on $J$, so $\tau$ is differentiable on $J$ with ${\tau }^{\mathrm{\prime }}(s)=h(s)=c^{-1}\sqrt{g(s)}$ for every $s\in J$, and $\tau$ is continuous on $J$: $J$ is order-convex with at least two elements by step 1.1 and $h$ is continuous by step 4.1, so the primitive assertion of [L10] applies to $h$ on $J$ with base point $s_0$, giving the derivative everywhere on $J$, and differentiability at the limit point $s$ of $J$ gives continuity at $s$ by [L12].

${\tau }^{\mathrm{\prime }}(s)=c^{-1}\sqrt{g(s)}>0$ for every $s\in J$: by step 5.1, ${\tau }^{\mathrm{\prime }}(s)=c^{-1}\sqrt{g(s)}$; here $g(s)>0$ by hypothesis, so $\sqrt{g(s)}>0$ because $\sqrt{g(s)}$ is the nonnegative square root of $g(s)$ [L5], and $c^{-1}>0$ because $c>0$ [L1]; the product of two positive reals is positive.

Null case: if $\eta (z^{\mathrm{\prime }}(s),z^{\mathrm{\prime }}(s))=0$ for all $s\in J$, then $g=0$ by its definition and $h=0$; by step 5.1, $\tau$ is a primitive of the zero function on $J$, so ${\tau }^{\mathrm{\prime }}=0$ at every point of $J$ and $\tau$ is constant on $J$ by [L16]; moreover $\tau (s_0)={\int }_{s_0}^{s_0}\sqrt{g(u)}du=0$ by [L17], so the constant is $0$ and $\tau \equiv 0$ on $J$; a constant function on $J$ is not injective because $J$ has at least two elements, so a null curve carries no proper-time parametrization.

$\tau$ is strictly increasing on $J$, hence injective: $\tau$ is continuous on $J$ by step 5.1, $J$ is order-convex and every point of $J$ is interior to $J$ by step 1.1, and ${\tau }^{\mathrm{\prime }}(s)>0$ at every $s\in J$ by step 6.1, so [L11] applies; a strictly increasing function is injective.

$\tau [J]$ is an interval (order-convex), the map $\tau :J\to \tau [J]$ is a bijection with inverse ${\tau }^{-1}:\tau [J]\to J$, and ${\tau }^{-1}$ is continuous on $\tau [J]$: this is [L8] applied to the continuous injective map $\tau$ on the order-convex set $J$, whose image is $\tau [J]$ by definition; the order-convexity of $J$ and continuity of $\tau$ are steps 1.1 and 5.1, and injectivity is step 7.1.

${\tau }^{-1}$ is differentiable at every point $\tau (s)$ of $\tau [J]$, with $({\tau }^{-1}{)}^{\mathrm{\prime }}(\tau (s))=1\mathrm{/}{\tau }^{\mathrm{\prime }}(s)=c\mathrm{/}\sqrt{g(s)}$: the inverse ${\tau }^{-1}:\tau [J]\to J$ is the one supplied by step 8.1 from [L8], and [L14] applies to $\tau$ with $c$ there equal to $s$ and $b=\tau (s)$; its hypotheses are the order-convexity of $J$ with at least two elements (step 1.1), continuity (step 5.1) and injectivity (step 7.1), and ${\tau }^{\mathrm{\prime }}(s)\mathrm{\ne }0$ by step 6.1, so the derivative is $1\mathrm{/}{\tau }^{\mathrm{\prime }}(s)=c\mathrm{/}\sqrt{g(s)}$ by step 5.1.

For each $a\in \{0,1,2,3\}$ the composite $z^a\circ {\tau }^{-1}:\tau [J]\to \mathbb{R}$ is differentiable at $\tau (s)$ with derivative $z^a{}^{\mathrm{\prime }}(s)\cdot c\mathrm{/}\sqrt{g(s)}$: $z^a$ is differentiable at the limit point $s$ of $J$ by [L3] and step 1.1, ${\tau }^{-1}$ is differentiable at $\tau (s)$ by step 9.1, and $\tau (s)$ is a limit point of $\tau [J]$ by [L14] as used in step 9.1, so the chain rule [L15] applies and gives the displayed derivative by [L4].

The reparametrized curve $z\circ {\tau }^{-1}:\tau [J]\to {\mathbb{R}}^4$ is differentiable at every $\tau (s)$, with tangent $U(\tau (s))=c{z}^{\mathrm{\prime }}(s)\mathrm{/}\sqrt{g(s)}$: by [L4] applied to the components of step 10.1, the curve is differentiable exactly when its components are and its derivative has those components, so $U(\tau (s))$ is the vector with components $z^a{}^{\mathrm{\prime }}(s)c\mathrm{/}\sqrt{g(s)}$, which is $c{z}^{\mathrm{\prime }}(s)\mathrm{/}\sqrt{g(s)}$.

$\eta (U(\tau (s)),U(\tau (s)))=-c^2$: by step 11.1, $U(\tau (s))=c{z}^{\mathrm{\prime }}(s)\mathrm{/}\sqrt{g(s)}$, and bilinearity and symmetry of $\eta$ [L1] give $\eta (U,U)=(c^2\mathrm{/}g(s))\eta (z^{\mathrm{\prime }}(s),z^{\mathrm{\prime }}(s))=-(c^2\mathrm{/}g(s))g(s)=-c^2$, since $g(s)=-\eta (z^{\mathrm{\prime }}(s),z^{\mathrm{\prime }}(s))>0$.

Straight-line case: assume $z(s)=p+sv$ with $\eta (v,v)<0$ and $v^0>0$, so $z^{\mathrm{\prime }}$ is the constant $v$ and $g$ is the constant $k:=-\eta (v,v)>0$, and $h$ is the constant $c^{-1}\sqrt{k}$ by step 5.1; the function $G(s):=c^{-1}\sqrt{k}(s-s_0)$ is a primitive of $h$ on $J$, its difference quotient at any $c\in J$ being the constant $c^{-1}\sqrt{k}$ by [L13], so for $s>s_0$ the evaluation formula of [L10] gives $\tau (s)=G(s)-G(s_0)=G(s)$, for $s=s_0$ one has $\tau (s_0)={\int }_{s_0}^{s_0}h=0=G(s_0)$ by [L17], and for $s<s_0$ antisymmetry [L17] gives $\tau (s)=-{\int }_s^{s_0}h=-(G(s_0)-G(s))=G(s)$; hence $\tau (s)=c^{-1}\sqrt{-\eta (v,v)}(s-s_0)$, and the tangent of step 11.1 is the constant $U(\tau (s))=cv\mathrm{/}\sqrt{k}=cv\mathrm{/}\sqrt{-\eta (v,v)}$.

All six claims are established: claim (1) by steps 2.1 and 3.1; claim (2) by steps 5.1 (differentiability and derivative), 6.1 (strict positivity), 7.1 (strict increase and injectivity) and 5.1 (continuity); claim (3) by steps 8.1 and 9.1; claim (4) by steps 10.1, 11.1 and 12.1; claim (5) by step 6.2; and claim (6) by step 12.2; the identification of straight lines with inertial motion is not asserted.