Worked solution: Tucker's rigorous computer-assisted proof via interval arithmetic (1999)

Step 5 of 8: Thousands of rectangles: certifying a region the flow can never escape

In plain words

Outside the small cube near the origin, Tucker picks a flat cross-section slicing through the attractor (the plane $z=27$ ) and chops it into many thousands of tiny rectangles. For each rectangle, he asks the computer to compute, using interval arithmetic, a guaranteed enclosure of exactly where every point in that rectangle ends up the next time its trajectory crosses the cross-section again.

By checking that the enclosure for every single rectangle lands back inside the union of all the rectangles, Tucker certifies that a specific, precisely delimited region is a trap: once a trajectory enters it, it can never escape, no matter how long you follow it. This single fact rules out the attractor secretly leaking away to infinity or to some entirely different part of space.

\Sigma \subset \{z = 27\} = \bigsqcup_i R_i, \qquad P(R_i) \subset \text{rigorously-verified image} \subset \Sigma

Detailed analysis

Away from the small cube $U_0$ , Tucker fixes a two-dimensional Poincaré cross-section $\Sigma$ inside the plane $\{z=27\}$ (chosen because it lies above the origin's saddle and intersects the attractor transversally), and partitions the relevant portion of $\Sigma$ into a fine mesh of many thousand small rectangles $\{R_i\}$ . For each rectangle $R_i$ , a rigorous, interval-arithmetic-based numerical integration of the Lorenz flow computes a box $\widehat{P}(R_i) \supset P(R_i)$ guaranteed to contain the true image of $R_i$ under the first-return map $P$ to $\Sigma$ (splicing in the analytic estimates from the previous steps whenever a trajectory happens to pass through $U_0$ ).

Checking, rectangle by rectangle, that $\widehat{P}(R_i)$ is contained in the union $\bigcup_i R_i$ certifies that this union is forward-invariant: no trajectory starting in it can ever leave. This rules out one of the two logically possible failure modes for Lorenz's picture — that the apparent attractor is not actually bounded, or leaks into some entirely different long-term behaviour once floating-point error is accounted for rigorously.

On its own, forward-invariance only shows some bounded, complicated set traps the flow; it says nothing yet about whether motion inside that trapped region is chaotic or is secretly a long stable periodic orbit. That distinction is the subject of the next step.

Knowledge used in this step

Chaos theory