Proposition 1.6 (Béguin–Bonatti–Yu): combinatorial transitivity implies transitivity of the glued Anosov flow

Open

AnosovPlugs.prop_1_6_combinatorial_transitivity

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

3-manifoldsanosov-flowsdynamical-systemshyperbolic-dynamics

Under the hypotheses of Theorem 1.5, if $(U,X,\varphi)$ is combinatorially transitive (the oriented graph on the basic pieces of $X$ , with edges given by intersections $W^u(\Lambda_i)\cap W^s(\Lambda_j)$ inside $U$ or across the gluing $\varphi$ , is strongly connected), then the Anosov vector field $Z$ produced by Theorem 1.5 is transitive:

Z \text{ is Anosov and transitive on } U/\psi.

Formalization Note Stated as a strengthening of the conclusion of Theorem 1.5: the plug $(U,Y)$ and gluing map $\psi$ can be chosen so that, in addition, every induced field $Z$ on any realisation of $U/\psi$ is hyperbolic on the whole manifold and has a dense orbit.

Preamble

import Mathlib
import Definitions.Def_AnosovPlugs_Gluing

open scoped Manifold ContDiff Topology
open Set

Formal statement

namespace AnosovPlugs

theorem prop_1_6_combinatorial_transitivity {U : Type} [TopologicalSpace U] [ChartedSpace (EuclideanHalfSpace 3) U]
    [IsManifold I3 ∞ U] [T2Space U] [CompactSpace U]
    (X : (x : U) → TangentSpace I3 x) (φ : U → U)
    (hX : IsFillingHyperbolicPlug X) (hXnoAR : NoAttractorNorRepeller X)
    (hφ : IsStronglyTransverseGluing X φ) (hcomb : IsCombinatoriallyTransitive X φ) :
    ∃ (Y : (x : U) → TangentSpace I3 x) (ψ : U → U),
      IsFillingHyperbolicPlug Y ∧ IsStronglyTransverseGluing Y ψ ∧ StronglyIsotopic X φ Y ψ ∧
      ∀ (N : Type) [TopologicalSpace N] [ChartedSpace (EuclideanHalfSpace 3) N]
        [IsManifold I3 ∞ N] [T2Space N] [CompactSpace N] [BoundarylessManifold I3 N]
        (Z : (y : N) → TangentSpace I3 y) (q : U → N),
        IsSelfGluing Y ψ Z q → IsHyperbolicSet Z univ ∧ IsTransitiveFlow 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. 1843, Proposition 1.6 (proof in §6.3)

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.

Same variables and hypotheses 1–3 as Theorem 1.5, plus IsCombinatoriallyTransitive $X\,\varphi$ : for any two basic pieces $B,B'$ of $X$ (nonempty closed invariant subsets of the nonwandering set, relatively open in it, with a dense orbit), $B'$ is reachable from $B$ by finitely many PieceEdge steps (unstable set of one meets stable set of the next, or $\varphi$ maps a point of unstableSetOf $\cap$ outBoundary to a point of stableSetOf $\cap$ inBoundary).

Conclusion: there exist $Y$ , $\psi$ with IsFillingHyperbolicPlug $Y$ , IsStronglyTransverseGluing $Y\,\psi$ , StronglyIsotopic $X\,\varphi\,Y\,\psi$ , and for every type $N$ with a topology, charted-space structure over the half-space, $C^\infty$ manifold structure, Hausdorff, compact and boundaryless, every vector field $Z$ on $N$ (no regularity assumed) and every map $q:U\to N$ satisfying IsSelfGluing $Y\,\psi\,Z\,q$ (i.e. $q$ is a surjective $C^1$ map with injective derivative everywhere, $q(x)=q(y)$ iff $x=y$ or one of them lies in outBoundary $Y$ and $\psi$ sends it to the other, and $Dq_x(Y(x))=Z(q(x))$ for all $x$ ), both IsHyperbolicSet $Z$ (univ) and IsTransitiveFlow $Z$ hold.

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