Theorem 1.15 (Béguin–Bonatti–Yu): a transitive Anosov flow with infinitely many nonisotopic transverse tori

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 exist a type $M$ with a topology, a charted-space structure over the half-space $\{x_0\ge0\}\subset\mathbb R^3$, a $C^\infty$ manifold structure, Hausdorff, compact, connected, and boundaryless (every point is an interior point), which is orientable (IsOrientable), a vector field $Z$ on $M$ with IsAnosov $Z$ and IsTransitiveFlow $Z$, and a sequence $f_n:S^1\times S^1\to M$ ($n\in\mathbb N$) such that each $f_n$ is a $C^1$ injective immersion with $Z(f_n(p))\notin\operatorname{im}D(f_n)_p$ for all $p$, and for $m\neq n$ there is no $C^1$ map $F:\mathbb R\times(S^1\times S^1)\to M$ with each $F(t,\cdot)$ ($t\in[0,1]$) an embedded torus, $F(0,\cdot)=f_m$ and image of $F(1,\cdot)$ equal to the image of $f_n$.