Theorem 1.9 (Béguin–Bonatti–Yu): a 3-manifold with both transitive and nontransitive Anosov flows
OpenAnosovPlugs.thm_1_9_transitive_and_nontransitiveThere exists a closed orientable three-manifold supporting both a transitive Anosov vector field and a nontransitive Anosov vector field :
This answers a question of A. Katok.
Formalization Note Closed means compact, Hausdorff, boundaryless and (by the standing convention of the field) connected; vector fields are C¹.
import Mathlib import Definitions.Def_AnosovPlugs_Hyperbolic open scoped Manifold ContDiff Topology open Set
namespace AnosovPlugs
theorem thm_1_9_transitive_and_nontransitive :
∃ (M : Type) (_ : TopologicalSpace M) (_ : ChartedSpace (EuclideanHalfSpace 3) M)
(_ : IsManifold I3 ∞ M) (_ : T2Space M) (_ : CompactSpace M) (_ : ConnectedSpace M)
(_ : BoundarylessManifold I3 M), IsOrientable M ∧
∃ X Y : (x : M) → TangentSpace I3 x,
IsAnosov X ∧ IsTransitiveFlow X ∧ IsAnosov Y ∧ ¬ IsTransitiveFlow Y := by sorry
end AnosovPlugsRead-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 (no hypotheses): there exist a type with a topology, a charted-space structure over the half-space , a manifold structure, Hausdorff, compact, connected, and boundaryless (every point is an interior point), which is orientable (IsOrientable), and two vector fields on with IsAnosov , IsTransitiveFlow , IsAnosov and not IsTransitiveFlow (no orbit of is dense).
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.