Proposition 1.3 (Béguin–Bonatti–Yu): strongly transverse gluing preserves filling MS laminations

Open

AnosovPlugs.prop_1_3_gluing_filling_plugs

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

3-manifoldsanosov-flowsdynamical-systemshyperbolic-dynamics

In the setting of Proposition 1.1, assume furthermore that the plugs $(U,X)$ and $(V,Y)$ have filling MS laminations and that $\varphi_*(L^u_X)$ is strongly transverse to $L^s_Y$ . Then

(W,Z) \text{ has filling MS laminations.}

Formalization Note As in Proposition 1.1, $W$ is any compact smooth manifold realising the gluing. The conclusion states that $Z$ is nonsingular and transverse to $\partial W$ , that its maximal invariant set is hyperbolic, and that every complementary component of its entrance and exit laminations is a strip.

Preamble

import Mathlib
import Definitions.Def_AnosovPlugs_Gluing

open scoped Manifold ContDiff Topology
open Set

Formal statement

namespace AnosovPlugs

theorem prop_1_3_gluing_filling_plugs
    {U : Type} [TopologicalSpace U] [ChartedSpace (EuclideanHalfSpace 3) U]
    [IsManifold I3 ∞ U] [T2Space U] [CompactSpace U]
    {V : Type} [TopologicalSpace V] [ChartedSpace (EuclideanHalfSpace 3) V]
    [IsManifold I3 ∞ V] [T2Space V] [CompactSpace V]
    {W : Type} [TopologicalSpace W] [ChartedSpace (EuclideanHalfSpace 3) W]
    [IsManifold I3 ∞ W] [T2Space W] [CompactSpace W]
    (X : (x : U) → TangentSpace I3 x) (Y : (y : V) → TangentSpace I3 y)
    (hX : IsFillingHyperbolicPlug X) (hY : IsFillingHyperbolicPlug Y)
    (Tout : Set U) (Tin : Set V) (hTout : IsUnionOfComponents Tout (outBoundary X))
    (hTin : IsUnionOfComponents Tin (inBoundary Y)) (φ : U → V)
    (hφ : IsBoundaryDiffeo φ Tout Tin)
    (hstrong : StronglyTransverse Tin (φ '' (exitLamination X ∩ Tout))
      (entranceLamination Y ∩ Tin) (pushLeaf φ Tout (exitLeaf X)) (entranceLeaf Y))
    (Z : (w : W) → TangentSpace I3 w) (iU : U → W) (iV : V → W)
    (hglue : IsPlugGluing X Y Tout φ Z iU iV) :
    IsNonsingularTransverse Z ∧ IsHyperbolicSet Z (maxInvSet Z) ∧
      HasFillingLaminations 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. 1841, Proposition 1.3 (proof in §4.2)

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 as Proposition 1.1. Hypotheses: IsFillingHyperbolicPlug $X$ , IsFillingHyperbolicPlug $Y$ ; $T^{out}$ , $T^{in}$ unions of components of outBoundary $X$ , inBoundary $Y$ ; $\varphi$ a $C^1$ boundary diffeomorphism $T^{out}\to T^{in}$ ; StronglyTransverse on the surface $T^{in}$ of $L_1=\varphi(\text{exitLamination }X\cap T^{out})$ (leaves: $\varphi$ -images of exit leaves of $X$ ) and $L_2=\text{entranceLamination }Y\cap T^{in}$ (leaves: entrance leaves of $Y$ ) — leaves transverse at every common point, and every component of $T^{in}\setminus(L_1\cup L_2)$ a $C^1$ immersed square with sides in leaves; IsPlugGluing $X\,Y\,T^{out}\,\varphi\,Z\,i_U\,i_V$ .

Conclusion: IsNonsingularTransverse $Z$ , the maximal invariant set of $Z$ is a hyperbolic set, and HasFillingLaminations $Z$ (every component of inBoundary $Z\setminus$ entranceLamination $Z$ and of outBoundary $Z\setminus$ exitLamination $Z$ is a strip). No $C^1$ claim about $Z$ .

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