A C¹ vector field has a local flow at every interior point, continuous in the initial point and unique among integral curves that stay in the neighbourhood

Let $M$ be a smooth 3-manifold with boundary (modelled on the closed half-space), let $X$ be a C¹ vector field on $M$, and let $x_0$ be an interior point of $M$. An integral curve of $X$ on a set of times $S\subseteq\mathbb R$ is a curve $\gamma:\mathbb R\to M$ whose derivative within $S$ at every $u\in S$ is $X(\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). Then there are $\varepsilon>0$, an open neighbourhood $O$ of $x_0$ and a map $\alpha:M\to\mathbb R\to M$ (a local flow) such that:

1. for every $y\in O$, $\alpha(y,0)=y$, the curve $\alpha(y,\cdot)$ is an integral curve of $X$ on $[-\varepsilon,\varepsilon]$, and $\alpha(y,\tau)$ is an interior point of $M$ for every $\tau\in[-\varepsilon,\varepsilon]$;
2. for every $\tau\in[-\varepsilon,\varepsilon]$, the map $y\mapsto\alpha(y,\tau)$ is continuous on $O$;
3. (uniqueness inside $O$) for every $y\in O$, every $h$ with $|h|\le\varepsilon$ and every integral curve $\eta$ of $X$ on $[0,h]$ with $\eta(0)=y$ and $\eta([0,h])\subseteq O$, one has

In words: near an interior point, a C¹ vector field has a local flow defined for a uniform short time, continuous in the initial point, and unique among integral curves that stay in the neighbourhood. This is the Picard–Lindelöf theorem with parameters, read in a chart at $x_0$. A general fact of ordinary differential equations, not stated in the paper; it is used tacitly in the proof of Proposition 1.1 (Section 3.1 of arXiv v1, p. 14), whose fourth and fifth sentences use, without comment, that the flow of the glued vector field Z near the maximal invariant set Λ_X of the plug (U, X) is the flow of X. In the proof of the companion statement exists_integralCurveOn_nhds it is the local building block that is iterated along a compact orbit segment.

Formalization Note No Hausdorff hypothesis is assumed: the uniqueness clause is restricted to curves that stay in $O$; the statement does not say that $O$ lies in one chart, but a proof may choose $O$ inside one chart, and then the clause follows from uniqueness for Lipschitz ordinary differential equations in $\mathbb R^3$; this is why the clause carries the hypothesis $\eta([0,h])\subseteq O$. Continuity in the initial point is stated for each fixed time $\tau$ separately, which is all the companion statement needs. Mathlib (at the pinned version) has the chart-level local flow (IsPicardLindelof.exists_forall_mem_closedBall_eq_hasDerivWithinAt_continuousOn) and short-time existence on manifolds (exists_isMIntegralCurveAt_of_contMDiffAt), but no local flow on manifolds. C¹ is the mission's IsC1VectorField.