Worked solution: Tucker's rigorous computer-assisted proof via interval arithmetic (1999)
Tucker's proof divides the whole problem geographically. Inside a small cube around the troublesome saddle at the origin, he abandons numerical simulation entirely and instead uses exact, pen-and-paper-style estimates from the theory of normal forms — a region small enough, and simple enough, that calculus alone can fully describe what happens. Outside that cube, where the flow behaves nicely and return times are bounded, he lets a computer take over, tracking not individual points but entire small regions at once with mathematically guaranteed error bounds.
The target of the whole construction is to verify that the resulting return map matches a known blueprint — the "geometric Lorenz model" designed years earlier by John Guckenheimer and Robert Williams — whose properties were already known to guarantee a genuine, robust chaotic attractor, if only one could show the real equations actually satisfy that blueprint's requirements.
Tucker's strategy (as described in his 1999 announcement and the full 2002 paper) partitions a neighbourhood of the attractor into two regions with fundamentally different treatments. Around the origin, a small cube is chosen small enough that a change of coordinates (justified by classical normal form theory, since the eigenvalues of the linearisation at the origin satisfy a non-resonance condition) puts the flow into an explicit, exactly solvable form there; entry and exit behaviour through can then be bounded by direct calculation rather than simulation, sidestepping entirely the blow-up in return times near the saddle.
Outside , where trajectories move at a bounded rate and a genuine Poincaré return map to a cross-section can be defined with bounded return time, Tucker turns to rigorous computer-assisted estimates (detailed in the next steps). The two treatments are stitched together at the boundary , where the analytic estimates from inside hand off directly to the numerical estimates from outside.
The target of the whole construction, made precise here, is the geometric Lorenz model introduced by John Guckenheimer and Robert F. Williams (1979) and Robert Williams (1979): an abstract template of a flow with a singular-hyperbolic attractor, built from an expanding one-dimensional return map with a specific set of combinatorial and expansion properties. Guckenheimer and Williams had already proven that any flow satisfying this template has a robust, singular-hyperbolic strange attractor; what remained — and what had been open since 1979 — was showing the actual Lorenz equations at the classical parameters satisfy the template's hypotheses, which is precisely what the remaining steps verify.
- Normal form
- A simplified system of coordinates near an equilibrium point, obtained by a change of variables, in which the differential equation takes its simplest possible algebraic shape (often just the linear part), making its solutions explicit and easy to estimate.
- Poincaré return map
- Given a surface transverse to the flow of a differential equation, the map sending a point on the surface to the next point where its trajectory crosses the surface again; it turns a continuous-time flow into a discrete-time dynamical system that is often much easier to analyse.