Lemma 3.27 (Béguin–Bonatti–Yu), self-gluing case: the glued manifold U/φ exists

Open

AnosovPlugs.lemma_3_27_self_gluing_exists

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

3-manifoldsanosov-flowsdynamical-systemshyperbolic-dynamics

Let $(U,X)$ be a plug on a compact 3-manifold and $\varphi:\partial^{out}U\to\partial^{in}U$ a diffeomorphism. Then the quotient $U/\varphi$ carries a smooth structure making it a closed 3-manifold $N$ , such that the quotient map $q:U\to N$ is a C¹ immersion and $X$ induces a vector field $Z$ on $N$ :

Dq_x(X(x)) = Z(q(x))\quad\text{for all } x\in U.

This guarantees that the universally quantified conclusions about "the vector field induced on $U/\varphi$ " (Theorem 1.5, Proposition 1.6) are not vacuous.

Formalization Note Only the case used by Theorem 1.5 (gluing the whole exit boundary to the whole entrance boundary of one plug) is stated. The induced field $Z$ is not asserted to be C¹.

Preamble

import Mathlib
import Definitions.Def_AnosovPlugs_Gluing

open scoped Manifold ContDiff Topology
open Set

Formal statement

namespace AnosovPlugs

theorem lemma_3_27_self_gluing_exists {U : Type} [TopologicalSpace U] [ChartedSpace (EuclideanHalfSpace 3) U]
    [IsManifold I3 ∞ U] [T2Space U] [CompactSpace U]
    (X : (x : U) → TangentSpace I3 x) (φ : U → U) (hX : IsPlug X)
    (hφ : IsBoundaryDiffeo φ (outBoundary X) (inBoundary X)) :
    ∃ (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 X φ Z q := 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. 1862, Lemma 3.27 (special case

V_1=V_2=U

S_1=\partial^{out}U

S_2=\partial^{in}U

) and §1.3, p. 1841

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: $U$ Hausdorff compact $C^\infty$ manifold over the half-space in $\mathbb R^3$ ; $X$ a vector field on $U$ ; $\varphi:U\to U$ .

Hypotheses: IsPlug $X$ ( $C^1$ , nonsingular, $X(x)_0\neq0$ on $\partial U$ ); IsBoundaryDiffeo $\varphi$ (outBoundary $X$ ) (inBoundary $X$ ).

Conclusion: there exist a type $N$ with topology, charted-space structure over the half-space, $C^\infty$ manifold structure, Hausdorff, compact and boundaryless, a vector field $Z$ on $N$ and $q:U\to N$ with IsSelfGluing $X\,\varphi\,Z\,q$ ( $q$ $C^1$ , injective derivative at every point, surjective, $q(x)=q(y)$ iff $x=y$ or one is in outBoundary $X$ and $\varphi$ maps it to the other, $Dq_x(X x)=Z(q x)$ ). Connectedness of $N$ is not claimed; $Z$ need not be $C^1$ .

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