Hyperbolicity of the maximal invariant set of a transverse plug gluing, given one metric, uniqueness of integral curves and C¹ time-t maps

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¹. Assume in addition that $(U,X)$ and $(V,Y)$ are hyperbolic plugs (their maximal invariant sets $\Lambda_X$, $\Lambda_Y$ are hyperbolic sets), and that the gluing is transverse: at every point $p\in\varphi(L^u_X\cap T^{out})\cap L^s_Y$ the pushed exit leaf $\varphi_*(\text{leaf of } L^u_X)$ and the entrance leaf of $L^s_Y$ through $p$ are transverse curves in $\partial V$ (the mission's CurvesTransverseAt), where $L^u_X$ and $L^s_Y$ are the exit and entrance laminations. A set $\Lambda\subseteq M$ is a hyperbolic set of a vector field $X$ (the mission's IsHyperbolicSet X Λ) if there are a continuous Riemannian metric $g$, line fields $E^s$, $E^u$ on $\Lambda$ and constants $C>0$, $\lambda>0$ such that at every $x\in\Lambda$: $E^s_x\oplus\mathbb R X(x)\oplus E^u_x=T_xM$, the two line fields are invariant under the derivatives of the time-$t$ maps $\phi_t$ of the flow of $X$ for all $t\in\mathbb R$, and $\|D\phi_t(v)\|_g\le C e^{-\lambda t}\|v\|_g$ for $v\in E^s_x$, $t\ge0$, and $\|D\phi_{-t}(v)\|_g\le C e^{-\lambda t}\|v\|_g$ for $v\in E^u_x$, $t\ge0$. The time-$t$ map is the mission's flowMap X t, which sends $x$ to $\gamma(t)$ for a chosen integral curve $\gamma$ of $X$ on $[0,t]$ with $\gamma(0)=x$ when one exists, and to $x$ otherwise. Assume the maximal invariant set of $Z$ is described (the hypothesis hΛ, proved in the mission as plugGluing_maxInvSet_subset and plugGluing_maxInvSet_superset):

Assume further the following. Each is the conclusion of another mission theorem, applied to the data above:

1. (one metric for both pieces) a continuous Riemannian metric $g$ on $W$ together with line fields and constants, separately for each piece, that make $i_U(\Lambda_X)$ and $i_V(\Lambda_Y)$ hyperbolic sets of $Z$ with respect to this same $g$ (isHyperbolicSet_of_metric applied to plugGluing_pieces_hyperbolic);
2. (uniqueness) integral curves of $Z$ on $[0,t]$ are determined by their starting point, for every $t$ (plugGluing_integralCurveOn_unique);
3. (C¹ time-$t$ maps) for every point $w$ of the maximal invariant set $\Lambda_Z$ (the points that lie on an integral curve of $Z$ defined for all times), $w$ is an interior point of $W$, and for every $t\in\mathbb R$ there is an open neighbourhood $O$ of $w$ such that the orbit of every $y\in O$ is defined on $[0,t]$ and the time-$t$ map of $Z$ is of class C¹ on $O$ (plugGluing_flowMap_contMDiffOn). Then the whole maximal invariant set is hyperbolic:

In words: this is the fifth sentence of the paper's proof of Proposition 1.1, which says that, by a classical consequence of the hyperbolic theory, the orbit of $\varphi_*(L^u_X)\cap L^s_Y$ inherits a hyperbolic structure, with the paper's description of the bundles at a connecting point $y\in T^{in}$: the stable bundle is $\mathbb R\,Y(y)\oplus T_yL^s_Y$ and the unstable bundle is $\mathbb R\,\varphi_*X(y)\oplus T_y\varphi_*(L^u_X)$, pushed into $W$ by $Di_V$. The expected proof: by hypotheses 2 and 3 the time-$t$ maps of $Z$ near a connecting orbit are C¹ maps given by the orbits, and the two pieces are flow invariant; the hyperbolic structures of the two pieces extend to cone fields on neighbourhoods; an unstable cone transported from $i_U(\Lambda_X)$ along a connecting orbit crosses the seam and, by the transversality hypothesis, lands inside the unstable cone of $i_V(\Lambda_Y)$ after a bounded transit time; the cone-field criterion with uniform constants gives the invariant splitting on all of $\Lambda_Z$; the unstable estimate is the same argument for $-Z$.

Formalization Note This theorem is plugGluing_hyperbolic_of_pieces_of_flows with its two hypotheses on C¹ local flows of $X$ and $Y$ at interior points replaced by hypothesis 3, the verbatim conclusion of plugGluing_flowMap_contMDiffOn. This theorem is now reduced to three companion theorems: flowMap_flowProperty_of_regularity and plugGluing_pieces_flowMap_invariant (the flow properties of flowMap Z on the maximal invariant set and the invariance of the two pieces, both proved), and plugGluing_hyperbolic_of_pieces_of_flowProperty (open), which contains the hyperbolic theory of transverse heteroclinic connections: the stable manifold theorem for the two hyperbolic sets, cone fields, their transport across the seam, and uniform constants. Mathlib (at the pinned version) has none of it. The paper's description of the bundles at connecting points is not asserted, because IsHyperbolicSet is existential in the bundles. The field $Z$ is not assumed C¹; the time-$t$ map flowMap Z t is junk-valued where no integral curve exists.