The time-t map of a C¹ vector field agrees with a complete integral curve through interior points

Let $M$ be a Hausdorff smooth 3-manifold with boundary (modelled on the closed half-space) and let $X$ be a C¹ vector field on $M$. Let $\gamma:\mathbb R\to M$ be a complete integral curve of $X$ (defined for all times) all of whose points $\gamma(s)$ are interior points of $M$. Then for every real $t$,

where $X^t$ is the time-$t$ map of the (partial) flow of $X$.

In words: the time-$t$ map is given by the complete integral curve whenever one exists through the interior. This is the uniqueness of integral curves of a C¹ vector field, applied to the mission's definition of the flow; it is a general fact, not stated in the paper. In the formal proof of the parent statement it gives the invariance $X^t(\Lambda_X)\subseteq\Lambda_X$ of the maximal invariant set under the time-$t$ maps.

Formalization Note The time-$t$ map $X^t$ is the mission's flowMap: when some integral curve of $X$ through $x$ is defined on the closed time interval between $0$ and $t$, $X^t(x)$ is the value at time $t$ of a chosen such curve; otherwise $X^t(x)=x$. Nothing in the definition asserts that this choice is unique. The statement says that this choice agrees with $\gamma$ when $\gamma$ is a complete integral curve through interior points. The interior hypothesis matches Mathlib's uniqueness theorem isMIntegralCurveOn_Ioo_eqOn_of_contMDiff, which is proved for curves through interior points; the statement is expected to hold without it, but that is not asserted. C¹ is the mission's IsC1VectorField (the section $x\mapsto(x,X(x))$ of the tangent bundle is C¹).