Integral curves of the glued vector field of a plug gluing are unique, also through the seam

Let $(U,X)$ and $(V,Y)$ be plugs: compact Hausdorff smooth 3-manifolds with boundary carrying nonsingular C¹ vector fields transverse to the boundary. Let $T^{out}\subseteq\partial^{out}U$ and $T^{in}\subseteq\partial^{in}V$ be unions of connected components of the exit and entrance boundaries, and let $\varphi:T^{out}\to T^{in}$ be a C¹ diffeomorphism (the mission's IsBoundaryDiffeo). Let $(W,Z,i_U,i_V)$ be a plug gluing (the mission's IsPlugGluing): $W$ is a compact Hausdorff smooth 3-manifold with boundary, $i_U:U\to W$ and $i_V:V\to W$ are C¹ embeddings with injective derivatives whose images cover $W$ and meet exactly along the seam $i_U(x)=i_V(\varphi(x))$, $x\in T^{out}$, and $Z$ is the vector field on $W$ with $Z\circ i_U=Di_U\circ X$ and $Z\circ i_V=Di_V\circ Y$. The field $Z$ is not assumed to be C¹. An integral curve of a vector field $F$ 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 $F(\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 integral curves of the glued field $Z$ are determined by their starting point: for every $t\in\mathbb R$ and all integral curves $\gamma,\gamma'$ of $Z$ on $[0,t]$ with $\gamma'(0)=\gamma(0)$,

In words: although $Z$ is not known to be C¹ on $W$, its integral curves are unique, also through the seam. The proof shows first that $i_V(V)$ is forward invariant and $i_U(U)$ is backward invariant for every integral curve of $Z$. Suppose that an integral curve leaves $i_V(V)$. Its lift to $U$ then starts at a point of $T^{out}\subseteq\partial^{out}U$, where $X$ points outward. The one-sided derivative at a boundary point forbids this. The mirror argument uses $T^{in}\subseteq\partial^{in}V$. So from any time of agreement, both curves stay for a while in one piece, where they lift to integral curves of $X$ or $Y$ (integralCurve_lift_of_embedding) with the same starting point, and uniqueness on a manifold with boundary (integralCurveOn_uIcc_unique) applies; the set of agreement times is then closed and open in $[0,t]$. It is used in the proof of Proposition 1.1 (Section 3.1 of arXiv v1, p. 14; GT 2017 Section 4.1). There it makes the time-$t$ maps of $Z$ along the connecting orbits the maps given by those orbits, and it makes the two pieces of the maximal invariant set invariant under the flow of $Z$.

Formalization Note The hypotheses are those of the mission's gluing statements. Of the plug hypotheses only the C¹ regularity of $X$ and $Y$ is used (through integralCurveOn_uIcc_unique); Compactness of $U$ and $V$ and the Hausdorff property of $W$ make the images $i_U(U)$ and $i_V(V)$ closed. The Hausdorff property of $U$ and $V$ is used by integralCurveOn_uIcc_unique; it also follows from the embeddings into $W$. Of hTout and hTin only $T^{out}\subseteq\partial^{out}U$ (forward direction) and $T^{in}\subseteq\partial^{in}V$ (backward direction) are used. $\varphi$ enters only through $\varphi(T^{out})\subseteq T^{in}$. Compactness of $W$ and the hyperbolicity of the plugs are not used.