A causal curve in a convex normal ball whose position vector is null at one time has null velocity almost everywhere up to that time

Given: A convex normal ball $C$ as in Local causality in a convex normal ball: causal reachability is the exponential cone, the Lorentzian length is bounded by the displacement radius, and null endpoints force the null geodesic, a future causal curve $\sigma :[0,1]\to C$ from $p$, and $t_0\in (0,1]$ with $D_p^2(\sigma (t_0))=0$.

$D_p^2\circ \sigma \le 0$ and $v(t):={\exp }_p^{-1}(\sigma (t))$ is future causal or zero for every $t$ by Local causality in a convex normal ball: causal reachability is the exponential cone, the Lorentzian length is bounded by the displacement radius, and null endpoints force the null geodesic clause (a). The coordinate choice in the Statement gives $u^0(\sigma (t))=-g_p(v(t),n_p)\ge 0$, since a future causal vector pairs nonpositively with the future timelike vector $n_p$ (Pairing of an observer with future causal vectors).

The function $t\mapsto D_p^2(\sigma (t))$ is AC with derivative $2g_{\sigma (t)}(P(p,\sigma (t)),{\sigma }^{\mathrm{\prime }}(t))$ at almost every $t$ (The differential of the squared-displacement function and the position vector of the reversed geodesic clause (a), Chart independence, concatenation, reparametrization and transitivity for causal curves clause (b), The chain rule for total derivatives: $D(g\circ f)(a)=Dg(f(a))\circ Df(a)$).

Null pairing rigidity, derived locally. Relative to the specified future unit observer $e$, decompose nonzero future causal vectors as $T=ae+u$, $z=be+w$, with $u,w\perp e$, $a,b>0$, $\mathrm{\mid }u\mathrm{\mid }\le a$, $\mathrm{\mid }w\mathrm{\mid }\le b$ in the positive rest-space norm. Then $g(T,z)=-ab+⟨u,w⟩\le -ab+\mathrm{\mid }u\mathrm{\mid }\mathrm{\mid }w\mathrm{\mid }\le 0$. Equality forces $\mathrm{\mid }u\mathrm{\mid }=a$, $\mathrm{\mid }w\mathrm{\mid }=b$ and positive collinearity in Cauchy-Schwarz, so both vectors are null and positive multiples (The observer rest-space decomposition and the spatial projection, Pairing of an observer with future causal vectors, Cauchy–Schwarz: $\mathrm{\mid }⟨u,v⟩\mathrm{\mid }\le \parallel u\parallel \parallel v\parallel$, with equality exactly for linearly dependent vectors).

If an AC function is identically zero on an interval, then its derivative vanishes almost everywhere on that interval (Fundamental theorem of calculus for absolutely continuous functions).

The length of the restriction is $L_g(\sigma {\mathrm{\mid }}_{[0,t_0]})={\int }_0^{t_0}\sqrt{-g({\sigma }^{\mathrm{\prime }},{\sigma }^{\mathrm{\prime }})}$, the Lebesgue length for locally absolutely continuous future causal curves defined in Length monotonicity of the squared displacement: once a future causal curve in a normal neighborhood has a future timelike position vector, the displacement radius grows at least as fast as the accumulated Lorentzian length.

If $f$ is absolutely continuous on an interval and $c\in \mathbb{R}$, then $f^{\mathrm{\prime }}=0$ almost everywhere on $f^{-1}(c)$. At a differentiability point $s$ of that level set with $f^{\mathrm{\prime }}(s)\mathrm{\ne }0$, the definition of derivative implies that $f(u)\mathrm{\ne }c$ for every sufficiently close $u\mathrm{\ne }s$, so $s$ is isolated in the level set. The isolated points are countable: assign to each one the first rational-endpoint open interval in a fixed enumeration that contains it and no other level-set point; distinct isolated points receive distinct intervals. The nondifferentiability set of an absolutely continuous function and this countable set are null, proving the claim. Applying this coordinatewise on a countable cover of the preimage of a point gives ${\sigma }^{\mathrm{\prime }}=0$ almost everywhere on $\{s:\sigma (s)=p\}$ (Absolute continuity on a compact interval, Absolutely continuous functions have integrable derivatives, Both $\mathbb{Q}$ and $\mathbb{R}\setminus \mathbb{Q}$ are dense in $\mathbb{R}$, and every nonempty open subset of $\mathbb{R}$ is uncountable, $\mathbb{Q}$ is countably infinite).