Hyperbolicity of the maximal invariant set of a transverse plug gluing, given one metric, uniqueness of integral curves and C¹ local flows

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¹ local flows) at every interior point of $U$ the field $X$ has a local flow that is jointly C¹ in the initial point and the time, with the uniqueness clause of exists_localFlow_contMDiff_of_isInteriorPoint, and likewise for $Y$ on $V$. 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 hypothesis 2 the time-$t$ maps of $Z$ along a connecting orbit are given by that orbit, and the two pieces are flow invariant; the time-$t$ maps are C¹ along the connecting orbits: hypothesis 3 covers the interior of each piece, and near the seam a C¹ flow up to the boundary and the transversality of $X$ to $\partial U$ give a C¹ hitting time; 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 (compactness of $\Lambda_Z$ and of the set of connecting points) gives the invariant splitting on all of $\Lambda_Z$; the unstable estimate is the same argument for $-Z$.

Formalization Note This theorem is the target plugGluing_hyperbolic_of_pieces with three added hypotheses, each the verbatim conclusion of a mission theorem: hypothesis 1 is the conclusion of isHyperbolicSet_of_metric (the body of IsHyperbolicSet with the metric fixed to $g$), hypothesis 2 is the conclusion of plugGluing_integralCurveOn_unique, and hypothesis 3 is the conclusion of exists_localFlow_contMDiff_of_isInteriorPoint, quantified over interior points of $U$ and of $V$. This theorem is now reduced to two companion theorems: plugGluing_flowMap_contMDiffOn (the C¹ regularity of the time-$t$ maps of $Z$ near its maximal invariant set, also across the seam, which is proved) and plugGluing_hyperbolic_of_pieces_of_regularity (the hyperbolic theory of transverse heteroclinic connections: cone fields, their transport across the seam, and uniform constants, which is open). Hypothesis 3 gives only local flows at interior points; the regularity across the seam is proved separately in plugGluing_localSteps_seam. Mathlib (at the pinned version) has no hyperbolic theory. 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.