Worked solution: Tucker's rigorous computer-assisted proof via interval arithmetic (1999)
Three separate pieces of work now click together. The normal form estimates handle the one dangerous spot near the origin exactly. The forward-invariant trapping region, verified rectangle by rectangle, shows the attractor is a genuine bounded object, not a numerical mirage or an escape to infinity. The expanding cone field shows motion inside that region is truly unstable, not secretly a disguised periodic orbit.
Guckenheimer and Williams had already proven, back in 1979, that any system with exactly this combination of properties possesses a robust chaotic attractor. Tucker's achievement is showing, for the very first time and with full rigour, that the actual Lorenz equations at the actual parameters Lorenz used in 1963 really do have this combination — turning a twenty-year-old conditional theorem into an unconditional fact about the system everyone had been simulating all along.
The Guckenheimer–Williams geometric Lorenz model requires precisely three ingredients from a flow: (a) a saddle equilibrium with a linearising normal form satisfying certain eigenvalue inequalities (verified analytically in step 3); (b) a well-defined, forward-invariant Poincaré return map to a cross-section, whose domain is stratified appropriately by the stable manifold of the saddle (verified via the rigorous rectangle computation in step 5); and (c) an invariant, uniformly expanding cone field for the derivative of that return map, encoding singular-hyperbolicity (verified in step 6).
Each of these three ingredients was established rigorously and independently for the actual Lorenz equations at in Tucker's computation. Guckenheimer and Williams's 1979 theorem (and its refinements) states that any system meeting all three conditions possesses a robust singular-hyperbolic attractor: robust in the sense that the attractor persists under small perturbations of the vector field (in particular, small changes in near the classical values), and singular-hyperbolic in the precise technical sense of Morales, Pacifico and Pujals that generalises uniform hyperbolicity to flows with equilibria on the attractor.
Because Tucker verifies all three hypotheses hold, unconditionally, for the genuine Lorenz equations (not merely for an idealised nearby model), the Guckenheimer–Williams conclusion applies directly: the classical Lorenz system genuinely possesses a robust chaotic attractor with positive topological entropy.