Theorem 1.5 (Béguin–Bonatti–Yu): gluing a hyperbolic plug to itself yields an Anosov flow

Open

AnosovPlugs.gluing_theorem

by Lucas · Oct 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

3-manifoldsanosov-flowsdynamical-systemshyperbolic-dynamics

Let $(U,X)$ be a hyperbolic plug with filling MS laminations (a compact 3-manifold $U$ with boundary, a nonsingular C¹ vector field $X$ transverse to $\partial U$ whose maximal invariant set $\Lambda$ is hyperbolic, and whose entrance and exit laminations $L^s_X\subset\partial^{in}U$ , $L^u_X\subset\partial^{out}U$ are filling). Assume that $\Lambda$ contains neither attractors nor repellers, and let $\varphi:\partial^{out}U\to\partial^{in}U$ be a strongly transverse gluing diffeomorphism.

Then there exist a hyperbolic plug $(U,Y)$ with filling MS laminations and a strongly transverse gluing diffeomorphism $\psi:\partial^{out}U\to\partial^{in}U$ such that

$(U,X,\varphi)$ and $(U,Y,\psi)$ are strongly isotopic, and
the vector field $Z$ induced by $Y$ on the closed manifold $U/\psi$ is Anosov:

Z \text{ on } U/\psi \ \text{ is Anosov}.

This is the paper's main gluing theorem: it allows one to build Anosov flows on closed 3-manifolds by gluing the exit boundary of a hyperbolic plug to its entrance boundary, after a strong isotopy.

Formalization Note The closed manifold $U/\psi$ is not built as a quotient type: the conclusion is stated for every closed smooth 3-manifold $N$ with a surjective C¹ immersion $q:U\to N$ realising the identification $x\sim\psi(x)$ and pushing $Y$ to $Z$ (such $N$ exist by Lemma 3.27, a separate milestone). "Anosov" is stated as hyperbolicity of the whole manifold for the flow of $Z$ (the induced field need not be C¹ for every compatible smooth structure).

Preamble

import Mathlib
import Definitions.Def_AnosovPlugs_Gluing

open scoped Manifold ContDiff Topology
open Set

Formal statement

namespace AnosovPlugs

theorem gluing_theorem {U : Type} [TopologicalSpace U] [ChartedSpace (EuclideanHalfSpace 3) U]
    [IsManifold I3 ∞ U] [T2Space U] [CompactSpace U]
    (X : (x : U) → TangentSpace I3 x) (φ : U → U)
    (hX : IsFillingHyperbolicPlug X) (hXnoAR : NoAttractorNorRepeller X)
    (hφ : IsStronglyTransverseGluing X φ) :
    ∃ (Y : (x : U) → TangentSpace I3 x) (ψ : U → U),
      IsFillingHyperbolicPlug Y ∧ IsStronglyTransverseGluing Y ψ ∧ StronglyIsotopic X φ Y ψ ∧
      ∀ (N : Type) [TopologicalSpace N] [ChartedSpace (EuclideanHalfSpace 3) N]
        [IsManifold I3 ∞ N] [T2Space N] [CompactSpace N] [BoundarylessManifold I3 N]
        (Z : (y : N) → TangentSpace I3 y) (q : U → N),
        IsSelfGluing Y ψ Z q → IsHyperbolicSet Z univ := by sorry

end AnosovPlugs

Source

F. Béguin, C. Bonatti, B. Yu, *Building Anosov flows on 3-manifolds*, Geom. Topol. 21 (2017) 1837–1930, https://doi.org/10.2140/gt.2017.21.1837, p. 1842, Theorem 1.5

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic) — same agent as the drafter; non-blind

Non-blind read-back — not independent testimony. This read-back was written by the same agent (Aristotle, by Harmonic) that drafted the Lean statements, with full knowledge of the source paper and of the intended meaning. It was NOT produced by an independent, blind auditor, and no reviewer should treat it as independent confirmation that the code says what the paper says. Compare it against the Lean code yourself.

Variables: $U$ is a type with a topology, a charted-space structure over the half-space $\{x_0\ge0\}\subset\mathbb R^3$ , a $C^\infty$ manifold structure, Hausdorff and compact (boundary allowed). $X$ is a vector field on $U$ and $\varphi:U\to U$ is any map.

Hypotheses:

IsFillingHyperbolicPlug $X$ : $X$ is $C^1$ , nonsingular, $X(x)_0\neq0$ on $\partial U$ ; the maximal invariant set is a hyperbolic set (continuous metric, lines $E^s,E^u$ , constants $C,\lambda>0$ , invariance and exponential estimates); every component of inBoundary $\setminus$ entranceLamination and of outBoundary $\setminus$ exitLamination is a strip.
NoAttractorNorRepeller $X$ : no subset of the maximal invariant set is an attractor of $X$ or of $-X$ .
IsStronglyTransverseGluing $X\,\varphi$ : $\varphi$ is a $C^1$ diffeomorphism from outBoundary $X$ onto inBoundary $X$ (with $C^1$ inverse along inBoundary), and $\varphi$ (exitLamination) and entranceLamination are strongly transverse on inBoundary $X$ .

Conclusion: there exist a vector field $Y$ on $U$ and a map $\psi:U\to U$ such that IsFillingHyperbolicPlug $Y$ , IsStronglyTransverseGluing $Y\,\psi$ , StronglyIsotopic $X\,\varphi\,Y\,\psi$ , and for every type $N$ with a topology, charted-space structure over the half-space, $C^\infty$ manifold structure, Hausdorff, compact and boundaryless, every vector field $Z$ on $N$ (no regularity assumed) and every map $q:U\to N$ satisfying IsSelfGluing $Y\,\psi\,Z\,q$ (i.e. $q$ is a surjective $C^1$ map with injective derivative everywhere, $q(x)=q(y)$ iff $x=y$ or one of them lies in outBoundary $Y$ and $\psi$ sends it to the other, and $Dq_x(Y(x))=Z(q(x))$ for all $x$ ), the whole of $N$ is a hyperbolic set of $Z$ : IsHyperbolicSet $Z$ (univ). Note that the conclusion about $N$ is universally quantified; it is vacuous if no such $N,q,Z$ exist. Anosov-ness is expressed only as hyperbolicity (IsHyperbolicSet), not IsAnosov, so $Z$ is not asserted to be $C^1$ .

Human review

Endorsed by Shuze Chen · Oct 1, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 1, 2026
Confirmed by the mission captain (proposal self-audit).

View graph