Anosov plugs I: C¹ vector fields, partial flows, orientability, topological equivalence

Definition

AnosovPlugs_Flows

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

3-manifoldsanosov-flowsdynamical-systemshyperbolic-dynamics

Basic vocabulary for flows of vector fields on smooth 3-manifolds, possibly with boundary.

Every 3-manifold $M$ is a smooth manifold modelled on the closed half-space $\mathbb H^3=\{x\in\mathbb R^3 : x_0\ge 0\}$ (model $I_3$ ); a closed 3-manifold is a compact one with empty boundary. Tangent vectors at $x$ are written in the chart at $x$ .

C¹ vector field. $X$ is C¹ if the section $x\mapsto (x,X(x))$ of $TM$ is C¹.
Partial flow. $\mathrm{FlowDefined}(X,x,t)$ holds when some integral curve $\gamma$ of $X$ with $\gamma(0)=x$ is defined (inside $M$ ) on the closed interval between $0$ and $t$ . The time- $t$ map $X^t(x)$ is $\gamma(t)$ for such a curve, and (by convention) $x$ when no such curve exists.
Transitivity. $X$ is transitive if some orbit $\{X^t(x):t\in\mathbb R\}$ is dense in $M$ .
Orientability. $M$ is orientable if it has an atlas of smooth charts covering $M$ whose transition maps all have positive Jacobian determinant.
Topological equivalence. A homeomorphism $h:M\to N$ is an orbit equivalence from $X$ to $Y$ if for every $x$ there is a continuous strictly increasing $\tau:\mathbb R\to\mathbb R$ with $\tau(0)=0$ , mapping the set of times at which the $X$ -orbit of $x$ is defined onto the corresponding set for the $Y$ -orbit of $h(x)$ , such that

h(X^t(x)) = Y^{\tau(t)}(h(x)).

$X$ and $Y$ are topologically equivalent if such an $h$ exists.

These notions are shared by every statement of the mission.

Formalization Note The flow is encoded through integral curves (IsMIntegralCurveOn), so that it also makes sense on manifolds with boundary, where orbits leave the manifold in finite time. Uniqueness of integral curves (C¹ fields) makes flowMap well defined.

Definition code

import Mathlib

/-!
Béguin–Bonatti–Yu, *Building Anosov flows on 3-manifolds*, Geom. Topol. 21 (2017) 1837–1930.
Basic layer: C¹ vector fields on smooth 3-manifolds (possibly with boundary), their (partial)
flows, orientability, transitivity, and topological (orbital) equivalence.

All 3-manifolds are modelled on the closed half-space `EuclideanHalfSpace 3`; a closed
3-manifold is a compact one with empty boundary (`BoundarylessManifold`).
-/

open scoped Manifold ContDiff Topology
open Set

namespace AnosovPlugs

/-- The model with corners of 3-manifolds with (possibly empty) boundary: the closed
half-space `{x ∈ ℝ³ | x₀ ≥ 0}`. -/
noncomputable abbrev I3 : ModelWithCorners ℝ (EuclideanSpace ℝ (Fin 3)) (EuclideanHalfSpace 3) :=
  𝓡∂ 3

variable {M : Type} [TopologicalSpace M] [ChartedSpace (EuclideanHalfSpace 3) M]
  [IsManifold I3 ∞ M]

/-- `X` is a C¹ vector field: the section `x ↦ (x, X x)` of the tangent bundle is C¹. -/
def IsC1VectorField (X : (x : M) → TangentSpace I3 x) : Prop :=
  ContMDiff I3 I3.tangent 1 (fun x => (⟨x, X x⟩ : TangentBundle I3 M))

/-- The orbit of `x` under `X` is defined on the whole closed time interval between `0` and `t`:
there is an integral curve `γ` of `X` with `γ 0 = x`, defined (inside `M`) on `[0, t]`
(or `[t, 0]` if `t < 0`). -/
def FlowDefined (X : (x : M) → TangentSpace I3 x) (x : M) (t : ℝ) : Prop :=
  ∃ γ : ℝ → M, γ 0 = x ∧ IsMIntegralCurveOn γ X (uIcc 0 t)

open Classical in
/-- The (partial) time-`t` map of the flow of `X`: the position at time `t` of the integral
curve of `X` through `x`, when this orbit is defined on the time interval between `0` and
`t`; by convention it is `x` otherwise. -/
noncomputable def flowMap (X : (x : M) → TangentSpace I3 x) (t : ℝ) (x : M) : M :=
  if h : FlowDefined X x t then h.choose t else x

/-- The flow of `X` is topologically transitive: some orbit is dense in `M`
(used for vector fields on closed manifolds, whose flows are complete). -/
def IsTransitiveFlow (X : (x : M) → TangentSpace I3 x) : Prop :=
  ∃ x : M, Dense (range fun t : ℝ => flowMap X t x)

/-- `M` is orientable: it admits an atlas of charts from its (smooth) maximal atlas, covering
`M`, all of whose transition maps have positive Jacobian determinant. -/
def IsOrientable (M : Type) [TopologicalSpace M] [ChartedSpace (EuclideanHalfSpace 3) M] : Prop :=
  ∃ A : Set (OpenPartialHomeomorph M (EuclideanHalfSpace 3)),
    A ⊆ IsManifold.maximalAtlas I3 ∞ M ∧ (∀ x : M, ∃ e ∈ A, x ∈ e.source) ∧
    ∀ e ∈ A, ∀ e' ∈ A, ∀ x ∈ e.source ∩ e'.source,
      0 < LinearMap.det
        (fderivWithin ℝ (e'.extend I3 ∘ (e.extend I3).symm) (range I3) (e.extend I3 x) :
          EuclideanSpace ℝ (Fin 3) →ₗ[ℝ] EuclideanSpace ℝ (Fin 3))

variable {N : Type} [TopologicalSpace N] [ChartedSpace (EuclideanHalfSpace 3) N]
  [IsManifold I3 ∞ N]

/-- `h : M ≃ₜ N` is a topological (orbital) equivalence from `X` to `Y`: it maps every oriented
orbit (segment) of `X` onto an oriented orbit (segment) of `Y`. Precisely, for every `x` there
is a continuous increasing reparametrisation `τ` with `τ 0 = 0`, mapping the set of times for
which the `X`-orbit of `x` is defined onto the set of times for which the `Y`-orbit of `h x`
is defined, with `h (X^t x) = Y^{τ t} (h x)`. -/
def IsOrbitEquivalence (X : (x : M) → TangentSpace I3 x) (Y : (y : N) → TangentSpace I3 y)
    (h : M ≃ₜ N) : Prop :=
  ∀ x : M, ∃ τ : ℝ → ℝ, Continuous τ ∧ StrictMono τ ∧ τ 0 = 0 ∧
    τ '' {t | FlowDefined X x t} = {s | FlowDefined Y (h x) s} ∧
    ∀ t, FlowDefined X x t → h (flowMap X t x) = flowMap Y (τ t) (h x)

/-- `X` (on `M`) and `Y` (on `N`) are topologically equivalent. -/
def TopologicallyEquivalent (X : (x : M) → TangentSpace I3 x)
    (Y : (y : N) → TangentSpace I3 y) : Prop :=
  ∃ h : M ≃ₜ N, IsOrbitEquivalence X Y h

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, §1.1–1.3 and §3.1 (Definitions 3.1; conventions for flows and topological equivalence)

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.

This file fixes the model $I_3$ : the closed half-space $\{x\in\mathbb R^3 : x_0\ge0\}$ with its standard model-with-corners structure. Throughout, $M$ (and $N$ ) are topological spaces with a charted-space structure modelled on this half-space and a $C^\infty$ manifold structure; no compactness, Hausdorffness or boundary condition is imposed in this file. A vector field is an arbitrary (not necessarily continuous) choice $X(x)\in T_xM$ , where $T_xM$ is identified with $\mathbb R^3$ via the chart at $x$ .

IsC1VectorField $X$ : the map $x\mapsto (x,X(x))$ from $M$ to the tangent bundle is $C^1$ .
FlowDefined $X\,x\,t$ : there exists a map $\gamma:\mathbb R\to M$ with $\gamma(0)=x$ which is an integral curve of $X$ on the closed interval $[\min(0,t),\max(0,t)]$ (one-sided derivatives at endpoints, computed within that interval). For $t=0$ this is automatically true (the interval is $\{0\}$ ).
flowMap $X\,t\,x$ $=\gamma(t)$ for some (arbitrarily chosen) such $\gamma$ if one exists, and $=x$ otherwise. The code does not itself prove that the choice is independent of $\gamma$ .
IsTransitiveFlow $X$ : there is $x$ with $\{\mathrm{flowMap}\,X\,t\,x : t\in\mathbb R\}$ dense in $M$ . (If $M$ has boundary, flowMap returns the junk value $x$ at times where the orbit is undefined.)
IsOrientable $M$ : there is a family $A$ of charts belonging to the $C^\infty$ maximal atlas, covering $M$ , such that for all $e,e'\in A$ and all $x$ in both domains, the derivative (within the half-space) at $e(x)$ of the transition map $e'\circ e^{-1}$ (in extended-chart coordinates) has determinant $>0$ .
IsOrbitEquivalence $X\,Y\,h$ for a homeomorphism $h:M\to N$ : for every $x\in M$ there is $\tau:\mathbb R\to\mathbb R$ , continuous, strictly increasing, $\tau(0)=0$ , such that $\tau$ maps $\{t : \mathrm{FlowDefined}\,X\,x\,t\}$ onto $\{s : \mathrm{FlowDefined}\,Y\,(h x)\,s\}$ and $h(\mathrm{flowMap}\,X\,t\,x)=\mathrm{flowMap}\,Y\,(\tau t)\,(h x)$ whenever $\mathrm{FlowDefined}\,X\,x\,t$ .
TopologicallyEquivalent $X\,Y$ : some homeomorphism $h:M\to N$ satisfies item 6. Note that the definition is stated in one direction only ( $X$ to $Y$ ).

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