Theorem 1.12 (Béguin–Bonatti–Yu): hyperbolic plugs with filling MS laminations embed in Anosov flows

Open

AnosovPlugs.thm_1_12_embedding_plugs_in_anosov

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

3-manifoldsanosov-flowsdynamical-systemshyperbolic-dynamics

Consider a hyperbolic plug with filling MS laminations $(U_0,X_0)$ .

Up to changing $(U_0,X_0)$ by a topological equivalence, one can find an Anosov vector field $X$ on a closed orientable three-manifold $M$ and an embedding $\theta:U_0\hookrightarrow M$ with $\theta_*X_0=X$ (on $\theta(U_0)$ ).
Moreover, if the maximal invariant set of $(U_0,X_0)$ contains neither attractors nor repellers, the construction can be done so that $X$ is transitive.

Formalization Note Item 1 is formalized as: there are a closed orientable $M$ , an Anosov $X$ on $M$ , a C¹ embedding $\iota:U_0\to M$ and the pulled-back field $Y=\iota^*X$ on $U_0$ ( $D\iota(Y)=X\circ\iota$ ), transverse to $\partial U_0$ , with $Y$ topologically equivalent to $X_0$ . Connectedness of $M$ is not claimed in the conclusion.

Preamble

import Mathlib
import Definitions.Def_AnosovPlugs_Laminations

open scoped Manifold ContDiff Topology
open Set

Formal statement

namespace AnosovPlugs

theorem thm_1_12_embedding_plugs_in_anosov {U : Type} [TopologicalSpace U] [ChartedSpace (EuclideanHalfSpace 3) U]
    [IsManifold I3 ∞ U] [T2Space U] [CompactSpace U]
    (X₀ : (x : U) → TangentSpace I3 x) (hX₀ : IsFillingHyperbolicPlug X₀) :
    (∃ (M : Type) (_ : TopologicalSpace M) (_ : ChartedSpace (EuclideanHalfSpace 3) M)
        (_ : IsManifold I3 ∞ M) (_ : T2Space M) (_ : CompactSpace M)
        (_ : BoundarylessManifold I3 M), IsOrientable M ∧
      ∃ X : (x : M) → TangentSpace I3 x, IsAnosov X ∧
        ∃ (ι : U → M) (Y : (x : U) → TangentSpace I3 x),
          ContMDiff I3 I3 1 ι ∧ Topology.IsEmbedding ι ∧
          (∀ x, Function.Injective (mfderiv I3 I3 ι x)) ∧
          (∀ x, mfderiv I3 I3 ι x (Y x) = X (ι x)) ∧ IsNonsingularTransverse Y ∧
          TopologicallyEquivalent X₀ Y) ∧
    (NoAttractorNorRepeller X₀ →
      ∃ (M : Type) (_ : TopologicalSpace M) (_ : ChartedSpace (EuclideanHalfSpace 3) M)
        (_ : IsManifold I3 ∞ M) (_ : T2Space M) (_ : CompactSpace M)
        (_ : BoundarylessManifold I3 M), IsOrientable M ∧
      ∃ X : (x : M) → TangentSpace I3 x, IsAnosov X ∧ IsTransitiveFlow X ∧
        ∃ (ι : U → M) (Y : (x : U) → TangentSpace I3 x),
          ContMDiff I3 I3 1 ι ∧ Topology.IsEmbedding ι ∧
          (∀ x, Function.Injective (mfderiv I3 I3 ι x)) ∧
          (∀ x, mfderiv I3 I3 ι x (Y x) = X (ι x)) ∧ IsNonsingularTransverse Y ∧
          TopologicallyEquivalent X₀ Y) := 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. 1845, Theorem 1.12 (proof in §9)

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$ a Hausdorff compact $C^\infty$ 3-manifold over the half-space model; $X_0$ a vector field on $U$ with IsFillingHyperbolicPlug $X_0$ .

Conclusion: a conjunction. (a) There exist a Hausdorff compact boundaryless $C^\infty$ 3-manifold $M$ (half-space model) with IsOrientable $M$ , a vector field $X$ on $M$ with IsAnosov $X$ , a map $\iota:U\to M$ and a vector field $Y$ on $U$ such that $\iota$ is $C^1$ , a topological embedding, with injective derivative at every point, $D\iota_x(Y x)=X(\iota x)$ for all $x$ , $Y$ is nonzero everywhere with $Y(x)_0\neq0$ at boundary points, and TopologicallyEquivalent $X_0\,Y$ (a self-homeomorphism of $U$ mapping $X_0$ -orbit segments to $Y$ -orbit segments, as in the Flows file). (b) If NoAttractorNorRepeller $X_0$ , then the same holds with additionally IsTransitiveFlow $X$ . $M$ is not required to be connected.

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