Theorem 1.13 (Béguin–Bonatti–Yu): 3-manifolds with arbitrarily many transitive Anosov flows

Open

AnosovPlugs.thm_1_13_many_anosov_flows

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

3-manifoldsanosov-flowsdynamical-systemshyperbolic-dynamics

For any $n\ge1$ there is a closed orientable three-manifold $M$ supporting at least $n$ transitive Anosov vector fields $Z_1,\dots,Z_n$ which are pairwise topologically nonequivalent:

i\neq j\ \Longrightarrow\ Z_i \not\simeq Z_j .

Formalization Note $M$ is connected, compact, Hausdorff, boundaryless and orientable; the vector fields are indexed by $\mathrm{Fin}\,n$ .

Preamble

import Mathlib
import Definitions.Def_AnosovPlugs_Hyperbolic

open scoped Manifold ContDiff Topology
open Set

Formal statement

namespace AnosovPlugs

theorem thm_1_13_many_anosov_flows (n : ℕ) (hn : 1 ≤ n) :
    ∃ (M : Type) (_ : TopologicalSpace M) (_ : ChartedSpace (EuclideanHalfSpace 3) M)
      (_ : IsManifold I3 ∞ M) (_ : T2Space M) (_ : CompactSpace M) (_ : ConnectedSpace M)
      (_ : BoundarylessManifold I3 M), IsOrientable M ∧
      ∃ Z : Fin n → (x : M) → TangentSpace I3 x,
        (∀ i, IsAnosov (Z i) ∧ IsTransitiveFlow (Z i)) ∧
        ∀ i j, i ≠ j → ¬ TopologicallyEquivalent (Z i) (Z j) := 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. 1846, Theorem 1.13 (proof in §10)

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: a natural number $n$ with $1\le n$ . Conclusion: there exist a type $M$ with a topology, a charted-space structure over the half-space $\{x_0\ge0\}\subset\mathbb R^3$ , a $C^\infty$ manifold structure, Hausdorff, compact, connected, and boundaryless (every point is an interior point), which is orientable (IsOrientable), and a family $Z_0,\dots,Z_{n-1}$ of vector fields on $M$ with IsAnosov $Z_i$ and IsTransitiveFlow $Z_i$ for every $i$ , such that for $i\neq j$ there is no homeomorphism $h:M\to M$ that is an orbit equivalence from $Z_i$ to $Z_j$ (not TopologicallyEquivalent $Z_i\,Z_j$ ).

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