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)

Chiến lược của Tucker (như mô tả trong thông báo năm 1999 và bài báo đầy đủ năm 2002) chia một lân cận của hút tử thành hai miền được xử lý về căn bản khác nhau. Quanh gốc tọa độ, một khối lập phương nhỏ $U_0$ được chọn đủ nhỏ để một phép đổi tọa độ (được biện minh bởi lý thuyết dạng chuẩn cổ điển, vì các giá trị riêng của phép tuyến tính hóa tại gốc thỏa một điều kiện phi cộng hưởng) đưa dòng chảy về dạng tường minh, giải được chính xác ở đó; hành vi vào và ra qua $\partial U_0$ khi đó có thể bị chặn bằng tính toán trực tiếp thay vì mô phỏng, né tránh hoàn toàn sự bùng nổ thời gian hồi quy gần điểm yên.

Bên ngoài $U_0$, nơi quỹ đạo chuyển động với tốc độ bị chặn và một ánh xạ hồi quy Poincaré thực sự tới một mặt cắt có thể được định nghĩa với thời gian hồi quy bị chặn, Tucker chuyển sang các ước lượng chặt chẽ có máy tính hỗ trợ (chi tiết ở các bước tiếp theo). Hai cách xử lý được khâu lại với nhau tại biên $\partial U_0$, nơi các ước lượng giải tích từ bên trong bàn giao trực tiếp cho các ước lượng số học từ bên ngoài.

Mục tiêu của toàn bộ phép xây dựng, được làm rõ ở đây, là mô hình Lorenz hình học do John Guckenheimer và Robert F. Williams (1979) cùng Robert Williams (1979) giới thiệu: một bản mẫu trừu tượng của một dòng chảy có hút tử kỳ dị-hyperbolic, xây từ một ánh xạ hồi quy một chiều giãn nở với một tập tính chất tổ hợp và giãn nở cụ thể. Guckenheimer và Williams đã chứng minh trước đó rằng bất kỳ dòng chảy nào thỏa mãn bản mẫu này đều có một hút tử lạ kỳ dị-hyperbolic bền vững; điều còn lại — và vẫn mở kể từ năm 1979 — là chỉ ra các phương trình Lorenz thực sự với tham số cổ điển thỏa mãn các giả thiết của bản mẫu, chính xác là điều các bước còn lại xác thực.