If a vector field with unique integral curves has C¹ short-time flow maps near every point of an orbit segment, its time-t map is C¹ near the starting point

Let $N$ be a smooth 3-manifold with boundary (modelled on the closed half-space) and let $Z$ be a vector field on $N$; no regularity of $Z$ is assumed. An integral curve of a vector field $Z$ on a manifold $N$ on a set of times $S\subseteq\mathbb R$ is a curve $\gamma:\mathbb R\to N$ whose derivative within $S$ at every $u\in S$ is $Z(\gamma(u))$ (Mathlib's IsMIntegralCurveOn; at the endpoints of an interval the derivative is one-sided). We write $[0,t]$ for the closed interval between $0$ and $t$, in either order (Mathlib's uIcc 0 t). A vector field $Z$ on a 3-manifold $N$ has local C¹ step maps at a point $p$ if there are $\varepsilon>0$ and an open neighbourhood $O$ of $p$ such that for every $h$ with $|h|\le\varepsilon$ there is a map $f_h:N\to N$ of class C¹ on $O$ with this property: every $y\in O$ is the starting point of an integral curve $\eta$ of $Z$ on $[0,h]$ with $\eta(h)=f_h(y)$. We write $\phi^Z_t$ for the time-$t$ map of $Z$, the mission's flowMap Z t: it sends $y$ to $\gamma(t)$ for a chosen integral curve $\gamma$ of $Z$ on $[0,t]$ with $\gamma(0)=y$ when one exists (the mission's FlowDefined Z y t), and to $y$ otherwise. Assume:

1. (uniqueness) for every $t$, two integral curves of $Z$ on $[0,t]$ with the same starting point are equal on $[0,t]$;
2. $\gamma$ is an integral curve of $Z$ on $[0,t]$, and $Z$ has local C¹ step maps at $\gamma(s)$ for every $s\in[0,t]$. Then there is an open neighbourhood $O$ of $\gamma(0)$ such that the orbit of every $y\in O$ is defined on $[0,t]$ and

In words: if short-time flow maps are C¹ near every point of a compact orbit segment, then the time-$t$ map is C¹ near the starting point. The proof covers the segment by finitely many step neighbourhoods (Lebesgue number), composes the step maps, and uses uniqueness to identify the composition with the time-$t$ map. It is a step of the mission's proof of the C¹ regularity that the proof of Proposition 1.1 (Section 3.1 of arXiv v1, p. 14) takes for granted. There $Z$ is the glued field, which is not known to be C¹ across the seam; the step maps come from localSteps_of_embedding and plugGluing_localSteps_seam.

Formalization Note The step maps are phrased with integral curves and not with flowMap, because flowMap is junk-valued where no integral curve exists. The interval $[0,t]$ is uIcc 0 t, so both time directions are covered. No Hausdorff and no compactness hypothesis is assumed. C¹ on $O$ is ContMDiffOn I3 I3 1 f O.