Theorem 1.8 (Béguin–Bonatti–Yu): every transitive Anosov flow is a factor of a richer one

Open

AnosovPlugs.thm_1_8_richer_transitive_anosov

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

3-manifoldsanosov-flowsdynamical-systemshyperbolic-dynamics

Given any transitive Anosov vector field $X$ on a closed (orientable) three-manifold $M$ , there exists a transitive Anosov vector field $Z$ on a closed (orientable) three-manifold $N$ such that the dynamics of $Z$ is richer than the dynamics of $X$ : there exist a compact set $\Lambda\subset N$ invariant under the flow of $Z$ and a continuous onto map $\pi:\Lambda\to M$ with

\pi\circ Z^t = X^t\circ\pi\qquad\text{for every } t\in\mathbb R.

Formalization Note The paper prints $\pi\circ X^t=Z^t\circ\pi$ , which does not type-check since $\pi:\Lambda\to M$ ; the semiconjugacy $\pi\circ Z^t=X^t\circ\pi$ is formalized. The parenthetical "(orientable)" is formalized as: if $M$ is orientable then $N$ can be taken orientable.

Preamble

import Mathlib
import Definitions.Def_AnosovPlugs_Hyperbolic

open scoped Manifold ContDiff Topology
open Set

Formal statement

namespace AnosovPlugs

theorem thm_1_8_richer_transitive_anosov
    {M : Type} [TopologicalSpace M] [ChartedSpace (EuclideanHalfSpace 3) M]
    [IsManifold I3 ∞ M] [T2Space M] [CompactSpace M] [BoundarylessManifold I3 M]
    (X : (x : M) → TangentSpace I3 x) (hX : IsAnosov X) (hXtr : IsTransitiveFlow X) :
    ∃ (N : Type) (_ : TopologicalSpace N) (_ : ChartedSpace (EuclideanHalfSpace 3) N)
      (_ : IsManifold I3 ∞ N) (_ : T2Space N) (_ : CompactSpace N)
      (_ : BoundarylessManifold I3 N),
      (IsOrientable M → IsOrientable N) ∧
      ∃ Z : (y : N) → TangentSpace I3 y, IsAnosov Z ∧ IsTransitiveFlow Z ∧
        ∃ (Λ : Set N) (π : N → M), IsCompact Λ ∧ (∀ y ∈ Λ, ∀ t : ℝ, flowMap Z t y ∈ Λ) ∧
          ContinuousOn π Λ ∧ π '' Λ = univ ∧
          ∀ y ∈ Λ, ∀ t : ℝ, π (flowMap Z t y) = flowMap X t (π 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. 1843, Theorem 1.8 (proof in §8)

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: $M$ a Hausdorff, compact, boundaryless $C^\infty$ manifold over the half-space in $\mathbb R^3$ (connectedness and orientability not assumed); $X$ a vector field on $M$ with IsAnosov $X$ ( $C^1$ , whole $M$ hyperbolic) and IsTransitiveFlow $X$ (a dense orbit).

Conclusion: there is a Hausdorff, compact, boundaryless $C^\infty$ 3-manifold $N$ (over the half-space model) such that (IsOrientable $M$ implies IsOrientable $N$ ), and a vector field $Z$ on $N$ with IsAnosov $Z$ and IsTransitiveFlow $Z$ , and a set $\Lambda\subseteq N$ and a map $\pi:N\to M$ with: $\Lambda$ compact; flowMap $Z\,t$ maps $\Lambda$ into $\Lambda$ for all real $t$ ; $\pi$ continuous on $\Lambda$ ; $\pi(\Lambda)=M$ ; and $\pi(\mathrm{flowMap}\,Z\,t\,y)=\mathrm{flowMap}\,X\,t\,(\pi y)$ for all $y\in\Lambda$ , $t\in\mathbb R$ . ( $\Lambda$ may equal $N$ ; nothing forbids $\pi$ to be a homeomorphism.)

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