Corollary 1.11 (Béguin–Bonatti–Yu): incoherent transitive hyperbolic attractors exist

Open

AnosovPlugs.cor_1_11_incoherent_attractors

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

3-manifoldsanosov-flowsdynamical-systemshyperbolic-dynamics

There exist incoherent transitive hyperbolic attractors on orientable manifolds: there is an orientable attracting hyperbolic plug $(U,X)$ whose maximal invariant set is transitive, and two compact leaves $\gamma_1,\gamma_2$ of $L^s(U,X)$ in the same connected component of $\partial^{in}U$ which, equipped with their contracting orientations, are not freely homotopic.

Formalization Note Contracting orientations are loop parametrisations along which the holonomy of the entrance foliation (on a C¹ transverse arc) is a contraction; free homotopy is taken in $\partial^{in}U$ .

Preamble

import Mathlib
import Definitions.Def_AnosovPlugs_Surfaces

open scoped Manifold ContDiff Topology
open Set

Formal statement

namespace AnosovPlugs

theorem cor_1_11_incoherent_attractors :
    ∃ (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)) ∧
        IsIncoherent X := 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, Corollary 1.11 and the definition of incoherence preceding it

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.

Conclusion only: there is a Hausdorff compact $C^\infty$ 3-manifold $U$ over the half-space model, with IsOrientable $U$ , and a vector field $X$ on $U$ with IsAttractingPlug $X$ , IsHyperbolicPlug $X$ , a point $x$ of the maximal invariant set $\Lambda$ with $\Lambda\subseteq\overline{\text{orbit of }x}$ , and IsIncoherent $X$ (two points $p_1,p_2$ of the entrance lamination with compact entrance leaves $K_1,K_2$ , $p_2$ in the component of $p_1$ in inBoundary $X$ , and $C^1$ loops $c_1,c_2$ parametrising $K_1,K_2$ , each with a $C^1$ transverse arc in inBoundary along which the holonomy of entrance leaves is contracting, such that $c_1,c_2$ are not freely homotopic in inBoundary $X$ ).

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