Counterexample: attainment of the endpoint bound does not force the future time orientation

Given: An inertial frame with chart $\xi$ and ${\eta }_0=\mathrm{diag}(-1,1,1,1)$; the coordinate vector $d=(5,3,0,0)$; the events $p={\xi }^{-1}(0,0,0,0)$, $q={\xi }^{-1}(-5,-3,0,0)$; and the curve $x(s)=p-sd$ on $[0,1]$ (Inertial frames and inertial charts of the affine Minkowski model).

Pairing in the frame: $\eta (r,r^{\mathrm{\prime }})=-r^0{r}^{\mathrm{\prime }0}+r^1{r}^{\mathrm{\prime }1}+r^2{r}^{\mathrm{\prime }2}+r^3{r}^{\mathrm{\prime }3}$ for coordinate vectors, by the diagonal form and bilinearity (Inertial frames and inertial charts of the affine Minkowski model, Lorentz forms of inertia (3,1,0) on a 4-dimensional real vector space).

Causal classification and cone coordinates: $r$ is timelike when $\eta (r,r)<0$, spacelike when $\eta (r,r)>0$; in a frame with future first vector, $r$ is future timelike exactly when $r^0>\mathrm{\mid }{r}_s\mathrm{\mid }$ and past timelike exactly when $r^0<-\mathrm{\mid }{r}_s\mathrm{\mid }$ (Timelike, null, spacelike and causal vectors of a Lorentz vector space, Time orientation, future and past timelike/null/causal vectors, and the closed cones, The timelike set has exactly two convex components, described in orthonormal coordinates).

Worldlines (Curves, regular causal curves and future timelike worldlines in affine Minkowski space): a future timelike worldline is a $C^1$ curve all of whose tangents are future timelike; the parametrization is part of the curve, and the image of a future timelike worldline is also the image of the past-directed curve $s\mapsto x(-s)$, which is not a worldline of the model.

Constant-integrand evaluation (If $m\le f\le M$ on $[a,b]$ then $m(b-a)\le L(f,P)\le \underset{‾}{{\int }_a^b}f\le \overline{{\int }_a^b}f\le U(f,P)\le M(b-a)$ for every partition $P$; in particular every constant function is integrable, with ${\int }_a^{b}c=c(b-a)$, The integral with oriented limits: ${\int }_a^{a}f:=0$ and ${\int }_b^{a}f:=-{\int }_a^{b}f$): for a real constant $K$ and $a<b$, the Riemann integral is ${\int }_a^{b}K=K(b-a)$. For any timelike $w$ the number $K=\sqrt{-\eta (w,w)}$ is real; this computation uses no future-orientation or clock-reading premise.

Square roots (Square roots exist: a unique $\sqrt{a}\ge 0$ with $(\sqrt{a}{)}^2=a$; the positives are $\{x^2:x\mathrm{\ne }0\}$, Ordered field): $\sqrt{16}=4$, and $4>0$.

The endpoint bound and its equality case (The endpoint bound for proper time and the maximality of the straight worldline in affine Minkowski space): for a weak piecewise $C^1$ future timelike worldline from $p$ to $q$, $c\mathrm{\Delta }\tau \le \sqrt{-\eta (q-p,q-p)}$ with equality exactly for the strictly increasing reparametrizations of the straight segment; the theorem is stated for future timelike worldlines and attaches no reading to past-directed curves.