Theorem 1.10 (Béguin–Bonatti–Yu): every MS foliation is the entrance foliation of a transitive hyperbolic attractor

Open

AnosovPlugs.thm_1_10_realizing_MS_foliations

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

3-manifoldsanosov-flowsdynamical-systemshyperbolic-dynamics

For every MS foliation $\mathcal F$ on a closed orientable surface $S$ , there exist an orientable transitive attracting hyperbolic plug $(U,X)$ and a homeomorphism $h:\partial^{in}U\to S$ such that

h_*\big(L^s(U,X)\big)=\mathcal F.

Formalization Note The foliation is given by a topological foliated atlas; $h_*(L^s)=\mathcal F$ is expressed leafwise: $h$ maps each leaf of the entrance lamination onto the leaf of $\mathcal F$ through the image point. "Transitive" means that the maximal invariant set has a dense orbit.

Preamble

import Mathlib
import Definitions.Def_AnosovPlugs_Surfaces

open scoped Manifold ContDiff Topology
open Set

Formal statement

namespace AnosovPlugs

theorem thm_1_10_realizing_MS_foliations
    {S : Type} [TopologicalSpace S] [ChartedSpace (EuclideanSpace ℝ (Fin 2)) S]
    [IsManifold (𝓡 2) ∞ S] [T2Space S] [CompactSpace S] (hS : IsOrientableSurface S)
    (A : Set (OpenPartialHomeomorph S (ℝ × ℝ))) (hA : IsMSFoliation A) :
    ∃ (U : Type) (_ : TopologicalSpace U) (_ : ChartedSpace (EuclideanHalfSpace 3) U)
      (_ : IsManifold I3 ∞ U) (_ : T2Space U) (_ : CompactSpace U), IsOrientable U ∧
      ∃ X : (x : U) → TangentSpace I3 x, IsAttractingPlug X ∧ IsHyperbolicPlug X ∧
        (∃ x ∈ maxInvSet X, maxInvSet X ⊆ closure (range fun t : ℝ => flowMap X t x)) ∧
        ∃ h : inBoundary X ≃ₜ S, ∀ p : inBoundary X,
          (fun q : inBoundary X => h q) '' {q | (q : U) ∈ entranceLeaf X p} =
            foliationLeaf A (h p) := 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.10 (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: $S$ a Hausdorff compact $C^\infty$ surface (charted over $\mathbb R^2$ , hence boundaryless), with IsOrientableSurface $S$ ; $A$ a set of partial homeomorphisms $S\rightharpoonup\mathbb R^2$ with IsMSFoliation $A$ .

Conclusion: there is a Hausdorff compact $C^\infty$ 3-manifold $U$ (half-space model, boundary allowed) with IsOrientable $U$ , and a vector field $X$ on $U$ with IsAttractingPlug $X$ ( $C^1$ , nonsingular, transverse to $\partial U$ , empty outBoundary), IsHyperbolicPlug $X$ , some $x$ in the maximal invariant set $\Lambda$ with $\Lambda\subseteq\overline{\text{orbit of }x}$ , and a homeomorphism $h$ from the subspace inBoundary $X$ onto $S$ such that for every $p\in$ inBoundary $X$ , the image under $h$ of $\{q\in\text{inBoundary }X : q\in\text{entranceLeaf }X\,p\}$ equals foliationLeaf $A\,(h\,p)$ .

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