Lời giải: Chứng minh chặt chẽ có máy tính hỗ trợ của Tucker bằng số học khoảng (1999)

Bên ngoài khối lập phương nhỏ $U_0$, Tucker cố định một mặt cắt Poincaré hai chiều $\Sigma$ bên trong mặt phẳng $\{z=27\}$ (được chọn vì nó nằm trên điểm yên của gốc tọa độ và cắt hút tử theo cách ngang), rồi chia phần liên quan của $\Sigma$ thành một lưới mịn gồm hàng nghìn hình chữ nhật nhỏ $\{R_i\}$. Với mỗi hình chữ nhật $R_i$, một phép tích phân số học chặt chẽ dựa trên số học khoảng của dòng chảy Lorenz tính ra một hộp $\widehat{P}(R_i) \supset P(R_i)$ được đảm bảo chứa ảnh thực của $R_i$ dưới ánh xạ hồi quy đầu tiên $P$ về $\Sigma$ (nối vào các ước lượng giải tích từ các bước trước bất cứ khi nào một quỹ đạo tình cờ đi qua $U_0$).

Kiểm tra, từng hình chữ nhật một, rằng $\widehat{P}(R_i)$ nằm trong hợp $\bigcup_i R_i$ chứng thực rằng hợp này là bất biến tiến: không quỹ đạo nào bắt đầu trong đó có thể rời khỏi nó. Điều này loại trừ một trong hai kiểu thất bại logic khả dĩ cho hình ảnh của Lorenz — rằng hút tử biểu kiến thực ra không bị chặn, hay rò rỉ vào một hành vi dài hạn hoàn toàn khác một khi sai số dấu phẩy động được tính đến chặt chẽ.

Tự nó, tính bất biến tiến chỉ chỉ ra một tập bị chặn, phức tạp nào đó bẫy dòng chảy; nó chưa nói lên gì về việc chuyển động bên trong miền bị bẫy đó có hỗn loạn hay bí mật là một quỹ đạo ổn định chu kỳ dài. Sự phân biệt đó là chủ đề của bước tiếp theo.