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

Step 3 of 8: Solving the hard part exactly: a normal form near the saddle

In plain words

The eigenvalues of the Lorenz system linearised at the origin are three specific real numbers: one positive ( $\lambda_1$ , an outward direction) and two negative ( $\lambda_2,\lambda_3$ , inward directions), with $\lambda_1 > 0 > \lambda_3 > \lambda_2$ . Because these three numbers do not satisfy any accidental integer-linear relationship (a "resonance"), a classical theorem guarantees a smooth change of coordinates that makes the nonlinear system near the origin look exactly like three uncoupled, trivially solvable equations $\dot x=\lambda_1 x$ , $\dot y=\lambda_2 y$ , $\dot z=\lambda_3 z$ .

In these new coordinates, exactly how long a trajectory takes to enter and leave the small cube $U_0$ , and exactly where it exits, can be written down with explicit formulas rather than approximated — turning the single most dangerous part of the whole system into the only part solved with pencil and paper instead of a computer.

\dot{x} = \lambda_1 x, \ \dot{y} = \lambda_2 y, \ \dot{z} = \lambda_3 z \ \ (\text{normal form near } 0), \quad \lambda_1 > 0 > \lambda_3 > \lambda_2

Detailed analysis

The Lorenz vector field linearised at the origin has three real eigenvalues satisfying $\lambda_1 > 0 > \lambda_3 > \lambda_2$ for the classical parameters (with $\lambda_1 \approx 11.83$ , $\lambda_2 \approx -22.83$ , $\lambda_3 = -\beta = -8/3$ ), making the origin a saddle with a two-dimensional stable manifold and a one-dimensional unstable manifold. Because these eigenvalues satisfy a non-resonance condition (no small-integer linear combination of them vanishes, other than the trivial one), the Sternberg linearisation theorem guarantees a smooth (in fact, sufficiently differentiable) change of coordinates in a neighbourhood of the origin conjugating the nonlinear flow to its linear part $\dot{x}=\lambda_1 x,\ \dot y=\lambda_2 y,\ \dot z=\lambda_3 z$ .

Tucker makes this classical existence theorem effective: working within a small cube $U_0$ around the origin in these linearising coordinates, entry and exit times and positions through the faces of $U_0$ are computed by direct, closed-form integration of the linear system, with all approximation errors (from the higher-order terms neglected by the linearisation, and from the coordinate change itself) rigorously bounded using interval arithmetic on the relevant Taylor expansions.

This produces explicit, rigorously verified formulas describing exactly how the flow carries a small patch of initial conditions entering near the stable manifold of the origin and re-injects it, split into two pieces by the direction of the unstable manifold, back out into the region where the numerical Poincaré map of the next steps takes over.

Knowledge used in this step

Chaos theory

Common mistake. The existence of a linearising change of coordinates near a saddle is a classical, purely qualitative fact (going back to Sternberg in the 1950s); Tucker's contribution at this stage is not this existence theorem itself but making the estimates quantitatively explicit and rigorously bounded, which is what is actually needed to hand off to the numerical part of the proof.