Proposition 1.1 (Béguin–Bonatti–Yu): gluing two hyperbolic plugs gives a hyperbolic plug

Open

AnosovPlugs.prop_1_1_gluing_hyperbolic_plugs

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

3-manifoldsanosov-flowsdynamical-systemshyperbolic-dynamics

Let $(U,X)$ and $(V,Y)$ be hyperbolic plugs. Let $T^{out}$ be a union of connected components of $\partial^{out}U$ and $T^{in}$ a union of connected components of $\partial^{in}V$ , and let $\varphi:T^{out}\to T^{in}$ be a diffeomorphism such that $\varphi_*(L^u_X)$ is transverse to the lamination $L^s_Y$ . Let $Z$ be the vector field induced by $X$ and $Y$ on $W:=(U\sqcup V)/\varphi$ . Then

(W,Z) \text{ is a hyperbolic plug.}

This is the elementary gluing operation of the "construction game" of the paper.

Formalization Note $W$ is any compact smooth 3-manifold with C¹ embeddings $i_U,i_V$ realising the gluing and pushing $X,Y$ to $Z$ . The conclusion is that $Z$ is nonsingular, transverse to $\partial W$ , and has hyperbolic maximal invariant set; C¹ regularity of $Z$ is not asserted.

Preamble

import Mathlib
import Definitions.Def_AnosovPlugs_Gluing

open scoped Manifold ContDiff Topology
open Set

Formal statement

namespace AnosovPlugs

theorem prop_1_1_gluing_hyperbolic_plugs
    {U : Type} [TopologicalSpace U] [ChartedSpace (EuclideanHalfSpace 3) U]
    [IsManifold I3 ∞ U] [T2Space U] [CompactSpace U]
    {V : Type} [TopologicalSpace V] [ChartedSpace (EuclideanHalfSpace 3) V]
    [IsManifold I3 ∞ V] [T2Space V] [CompactSpace V]
    {W : Type} [TopologicalSpace W] [ChartedSpace (EuclideanHalfSpace 3) W]
    [IsManifold I3 ∞ W] [T2Space W] [CompactSpace W]
    (X : (x : U) → TangentSpace I3 x) (Y : (y : V) → TangentSpace I3 y)
    (hX : IsHyperbolicPlug X) (hY : IsHyperbolicPlug Y)
    (Tout : Set U) (Tin : Set V) (hTout : IsUnionOfComponents Tout (outBoundary X))
    (hTin : IsUnionOfComponents Tin (inBoundary Y)) (φ : U → V)
    (hφ : IsBoundaryDiffeo φ Tout Tin)
    (htransv : ∀ p ∈ φ '' (exitLamination X ∩ Tout) ∩ entranceLamination Y,
      CurvesTransverseAt (pushLeaf φ Tout (exitLeaf X) p) (entranceLeaf Y p) p)
    (Z : (w : W) → TangentSpace I3 w) (iU : U → W) (iV : V → W)
    (hglue : IsPlugGluing X Y Tout φ Z iU iV) :
    IsNonsingularTransverse Z ∧ IsHyperbolicSet Z (maxInvSet Z) := 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. 1839, Proposition 1.1 (proof in §4.1)

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,V,W$ are Hausdorff compact $C^\infty$ manifolds modelled on the half-space in $\mathbb R^3$ ; $X$ , $Y$ , $Z$ are vector fields on $U,V,W$ ; $T^{out}\subseteq U$ , $T^{in}\subseteq V$ ; $\varphi:U\to V$ , $i_U:U\to W$ , $i_V:V\to W$ maps.

Hypotheses: IsHyperbolicPlug $X$ and IsHyperbolicPlug $Y$ ; $T^{out}$ is a union of connected components of outBoundary $X$ ; $T^{in}$ is a union of connected components of inBoundary $Y$ ; $\varphi$ is a $C^1$ bijection $T^{out}\to T^{in}$ with $C^1$ inverse along $T^{in}$ ; for every $p\in\varphi(\text{exitLamination }X\cap T^{out})\cap\text{entranceLamination }Y$ , the pushed exit leaf through $p$ and the entrance leaf of $Y$ through $p$ contain $C^1$ curves through $p$ with linearly independent velocities; IsPlugGluing $X\,Y\,T^{out}\,\varphi\,Z\,i_U\,i_V$ ( $i_U,i_V$ $C^1$ topological embeddings with injective derivatives, jointly onto $W$ , $i_U(x)=i_V(y)\iff x\in T^{out}\wedge y=\varphi(x)$ , pushing $X$ , $Y$ to $Z$ ).

Conclusion: $Z$ is nonzero everywhere, $Z(w)_0\neq0$ at every boundary point $w$ of $W$ , and the maximal invariant set of $Z$ is a hyperbolic set of $Z$ . ( $C^1$ -regularity of $Z$ is neither assumed nor concluded.)

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