Global existence, uniqueness and differentiability of the retarded root

For all $s_1,s_2\in \mathbb{R}$ the restriction of $z$ to the interval with endpoints $s_1,s_2$ is continuous with derivative bounded by $v_{\ast }$ at interior points, so [L1] gives $\mathrm{\mid }z(s_2)-z(s_1)\mathrm{\mid }\le v_{\ast }\mathrm{\mid }{s}_2-s_1\mathrm{\mid }$; consequently $z$, and by [L3] each map $s\mapsto g_x(s)=s+\mathrm{\mid }x-z(s)\mathrm{\mid }\mathrm{/}c$, is continuous.

For $s_2>s_1$ the reverse triangle inequality [L2] gives $\mathrm{\mid }x-z(s_2)\mathrm{\mid }\ge \mathrm{\mid }x-z(s_1)\mathrm{\mid }-\mathrm{\mid }z(s_2)-z(s_1)\mathrm{\mid }$, so by step 1.1 $g_x(s_2)-g_x(s_1)\ge (s_2-s_1)-\frac{v_{\ast }}{c}(s_2-s_1)=(s_2-s_1)(1-\frac{v_{\ast }}{c})>0$: the map $g_x$ is strictly increasing and $g_x(s)\ge s$ for every $s$. Moreover $\mathrm{\mid }x-z(s)\mathrm{\mid }\le \mathrm{\mid }x-z(0)\mathrm{\mid }+\mathrm{\mid }z(s)-z(0)\mathrm{\mid }\le \mathrm{\mid }x-z(0)\mathrm{\mid }+v_{\ast }\mathrm{\mid }s\mathrm{\mid }$, so for $s<0$ one has $g_x(s)\le s+\frac{\mathrm{\mid }x-z(0)\mathrm{\mid }-v_{\ast }s}{c}=s(1-\frac{v_{\ast }}{c})+\frac{\mathrm{\mid }x-z(0)\mathrm{\mid }}{c}$.

Given $t$, put $C=\mathrm{\mid }x-z(0)\mathrm{\mid }\mathrm{/}c$ and choose $s_{+}=\max (t,0)+1$ and $s_{-}=\min (0,t,\frac{t-C}{1-v_{\ast }\mathrm{/}c})-1$, so that $s_{-}<t<s_{+}$; step 2.1 gives $g_x(s_{+})\ge s_{+}>t$ and $g_x(s_{-})<t$. Since $g_x$ is continuous by step 1.1, Intermediate value theorem, by bisection with a canonical left-half rule: a continuous function on $[a,b]$ takes every value between $f(a)$ and $f(b)$ on the nondegenerate interval $[s_{-},s_{+}]$ supplies a root $s$ of $g_x(s)=t$, i.e. of $t-s=\mathrm{\mid }x-z(s)\mathrm{\mid }\mathrm{/}c$. If $s_1<s_2$ were two roots then $g_x(s_1)=g_x(s_2)$ would contradict the strict increase of step 2.1, so this root is unique; it satisfies $s\le t$ because $g_x(s)\ge s$, with $s=t$ if and only if $\mathrm{\mid }x-z(t)\mathrm{\mid }=0$, that is if and only if $x=z(t)$. Hence off the instantaneous trajectory, where $x\mathrm{\ne }z(t)$, one has $s<t$ and $r=\mathrm{\mid }x-z(s)\mathrm{\mid }=c(t-s)>0$, and the set $D=\{(x,t):x\mathrm{\ne }z(t)\}$ is open because $z$ is continuous.

Fix $(x_0,t_0)\in D$, let $s_0=s(x_0,t_0)$, $r_0=\mathrm{\mid }{x}_0-z(s_0)\mathrm{\mid }=c(t_0-s_0)>0$, $n_0=(x_0-z(s_0))\mathrm{/}{r}_0$, ${\beta }_0=z^{\mathrm{\prime }}(s_0)\mathrm{/}c$ and ${\kappa }_0=1-n_0\cdot {\beta }_0$. Since $\mathrm{\mid }{n}_0\mathrm{\mid }=1$ and $\mathrm{\mid }{\beta }_0\mathrm{\mid }\le v_{\ast }\mathrm{/}c<1$, one has $1-v_{\ast }\mathrm{/}c\le {\kappa }_0\le 1+v_{\ast }\mathrm{/}c$ and ${\kappa }_0>0$.

Define $F(x,\tau ,y)=c^2(\tau -y{)}^2-\mathrm{\mid }x-z(y){\mathrm{\mid }}^2$ on ${\mathbb{R}}^5$. Each component of $z$ is $C^k$ and the expression is a finite sum of products of $C^k$ functions composed with $z$, so $F$ is $C^k$ by [L5]. At the base point of step 4.1, $F(x_0,t_0,s_0)=c^2(t_0-s_0{)}^2-r_0^2=0$, and computing the partial $y$-derivative along the differentiable curve $y\mapsto z(y)$ gives ${\mathrm{\partial }}_{y}F(x_0,t_0,s_0)=-2c^2(t_0-s_0)+2(x_0-z(s_0))\cdot z^{\mathrm{\prime }}(s_0)=-2c{r}_0+2r_{0}c{\beta }_0\cdot n_0=-2c{r}_0{\kappa }_0\mathrm{\ne }0$. The parametrized implicit function theorem [L5] (with $y=s$, parameters $(x,\tau )$) therefore gives open neighbourhoods $P\ni (x_0,t_0)$, $Q\ni s_0$ and a unique $C^k$ map $\phi :P\to Q$ with $F(x,\tau ,\phi (x,\tau ))=0$ on $P$ and $D\phi =-D_y{F}^{-1}{D}_{(x,\tau )}F$.

By [L3] the map $(x,\tau )\mapsto \phi (x,\tau )-\tau$ is continuous and negative at $(x_0,t_0)$ because $\phi$ is continuous with $\phi (x_0,t_0)=s_0<t_0$; shrinking $P$ if necessary, $\phi (x,\tau )<\tau$ there. On that neighbourhood $F=0$ reads $c^2(\tau -\phi {)}^2=\mathrm{\mid }x-z(\phi ){\mathrm{\mid }}^2$ with $\tau -\phi >0$, hence $\tau -\phi =\mathrm{\mid }x-z(\phi )\mathrm{\mid }\mathrm{/}c$, that is $g_x(\phi )=\tau$; by uniqueness of the root (step 3.1) $\phi =s$. Thus $s$ is $C^k$ on a neighbourhood of $(x_0,t_0)$; since $(x_0,t_0)\in D$ and $k\ge 1$ were arbitrary (and a smooth $z$ is $C^k$ for every $k$), $s$ is $C^k$ on $D$, and smooth when $z$ is smooth.

Reading off the displayed derivative formula at the base point of step 5.1, ${\mathrm{\partial }}_{\tau }F(x_0,t_0,s_0)=2c^2(t_0-s_0)=2c{r}_0$ and ${\mathrm{\partial }}_{x_i}F(x_0,t_0,s_0)=-2(x_0-z(s_0){)}_i=-2r_0{n}_{0,i}$, so ${\mathrm{\partial }}_{t}s={\mathrm{\partial }}_{\tau }\phi =-{\mathrm{\partial }}_{\tau }F\mathrm{/}{\mathrm{\partial }}_{y}F=1\mathrm{/}{\kappa }_0$ and ${\mathrm{\partial }}_{x_i}s=-{\mathrm{\partial }}_{x_i}F\mathrm{/}{\mathrm{\partial }}_{y}F=-n_{0,i}\mathrm{/}(c{\kappa }_0)$; since the point was arbitrary in $D$, the same formulas hold on all of $D$, with $1-v_{\ast }\mathrm{/}c\le \kappa \le 1+v_{\ast }\mathrm{/}c$ by step 4.1.

For the sharpness clause use [L7] with $K=[-1,1]\subset (-2,2)$ to choose $\chi \in C^{\mathrm{\infty }}(\mathbb{R})$ with $0\le \chi \le 1$, $\chi =1$ on $(-1,1)$ and $\chi =0$ outside $(-2,2)$, and put $f(s)=\chi (s)\mathrm{\mid }s{\mathrm{\mid }}^{3\mathrm{/}2}$. Then $f$ is $C^1$: on $(0,1)$ it equals $s^{3\mathrm{/}2}$ with derivative $(3\mathrm{/}2)s^{1\mathrm{/}2}$, on $(-1,0)$ it equals $(-s{)}^{3\mathrm{/}2}$ with derivative $-\frac{3}{2}(-s{)}^{1\mathrm{/}2}$ by [L6]; away from $0$ it is the smooth product of $\chi$ and $\mathrm{\mid }s{\mathrm{\mid }}^{3\mathrm{/}2}$, and its derivative vanishes outside the compact cutoff support, and at $0$ the difference quotient is $\mathrm{\mid }h{\mathrm{\mid }}^{3\mathrm{/}2}\mathrm{/}h=\mathrm{sgn}(h)\mathrm{\mid }h{\mathrm{\mid }}^{1\mathrm{/}2}\to 0$, so $f^{\mathrm{\prime }}(0)=0$; $f^{\mathrm{\prime }}$ is continuous on the compact interval $[-2,2]$ and zero outside it, so [L7] gives a finite bound $C_f:={\max }_{[-2,2]}\mathrm{\mid }{f}^{\mathrm{\prime }}\mathrm{\mid }$; the same supplier bounds $f$ globally. Choose $\epsilon >0$ with $\epsilon C_f<c\mathrm{/}2$ and set $z(s)=(\epsilon f(s),0,0)$, a $C^1$ trajectory with $\mathrm{\mid }{z}^{\mathrm{\prime }}\mathrm{\mid }\le v_{\ast }:=\epsilon C_f<c$; fix $L>2\epsilon {\sup }_{s}f(s)$ and $x=(L,0,0)$, so $\mathrm{\mid }x-z(s)\mathrm{\mid }=L-\epsilon f(s)$ and the equation $g_x(s)=t$ reads $s+(L-\epsilon f(s))\mathrm{/}c=:g(s)=t$. One has $g^{\mathrm{\prime }}(s)=1-\epsilon f^{\mathrm{\prime }}(s)\mathrm{/}c\ge 1-\epsilon C_f\mathrm{/}c>1\mathrm{/}2>0$, so $g$ is strictly increasing, and the root map $s$ is the inverse of $g$. At $0$ one has $g(0)=L\mathrm{/}c=:t_0$ and $g^{\mathrm{\prime }}(0)=1-\epsilon f^{\mathrm{\prime }}(0)\mathrm{/}c=1$, hence $s^{\mathrm{\prime }}(t_0)=1\mathrm{/}{g}^{\mathrm{\prime }}(0)=1\mathrm{\ne }0$; if $s$ were $C^2$ near $t_0$, then by [L6] (applied to the $C^2$ map $s$ with invertible derivative $1$ at $t_0$) its local inverse, namely $g$, would be $C^2$ near $0$. But $f^{\mathrm{\prime }}(h)=(3\mathrm{/}2)h^{1\mathrm{/}2}$ for small $h>0$, so $(g^{\mathrm{\prime }}(h)-g^{\mathrm{\prime }}(0))\mathrm{/}h=-\frac{\epsilon }{c}\cdot \frac{(3\mathrm{/}2)h^{1\mathrm{/}2}}{h}=-\frac{3\epsilon }{2c}{h}^{-1\mathrm{/}2}\to -\mathrm{\infty }$ as $h\downarrow 0$: $g$ is not twice differentiable at $0$, a contradiction. Hence a merely $C^1$ trajectory need not give a $C^2$ root.

Collecting: existence, uniqueness, $s\le t$ with equality exactly on $x=z(t)$, and the open domain $D$ with $s<t$, $r>0$ are step 3.1; $C^k$ (hence $C^1$, and smooth for smooth $z$) regularity on $D$ is step 6.1; the derivative formulas and the bound $1-v_{\ast }\mathrm{/}c\le \kappa \le 1+v_{\ast }\mathrm{/}c$ are steps 4.1 and 6.2; the non-improvement witness for a merely $C^1$ trajectory is step 7.1. No Choice principle is used anywhere.