A region the orbit cannot leave

Every picture of a strange attractor in these essays has been drawn from a computed orbit — from the two lobes of the first picture to the distribution of time along them — and every conclusion about the attractor has been, strictly, a conclusion about what a computer produced when it followed the rule for a long time. The orbit a computer draws is not an orbit of the map; it is an orbit with a rounding error at every step, and in a chaotic system those errors grow as fast as any difference in the start. So a question has been waiting since the first picture: what, about these attractors, has actually been proved?

The answer divides cleanly. That there is an attractor — a bounded region every orbit eventually enters and never leaves, and something inside it that orbits accumulate on — is easy, and this essay proves it for both of the standard models with arithmetic that fits in a paragraph. That the attractor is strange — that orbits on it really do separate exponentially for ever, rather than settling after a long transient into a periodic cycle — is hard. For the Lorenz flow it was proved in 1999 by a computation of a very particular kind. For the Hénon map at the parameters drawn throughout, it has never been proved at all.

The figure below is the easy half for Hénon. A quadrilateral Michel Hénon drew in 1976, and its image under the map, lying strictly inside it.

A region carried inside itself #

Take any region of the plane and apply the map to every point of it. If the image lies inside the region, then applying the map again puts the second image inside the first, and so on: the images nest. Every orbit that starts in the region stays there. And the nested images shrink toward a set — the intersection of all of them — that the map carries onto itself and that every orbit from the region approaches. That set is the attractor, and a region with this property is called a trapping region.

Checking that a quadrilateral is a trapping region is a finite calculation, thanks to one topological fact. The Hénon map is one-to-one and continuous, so it carries the boundary of the quadrilateral to the boundary of the image, and the image is the region enclosed by that curve. If every point of the image of the boundary lies inside the quadrilateral, the enclosed image does too — the Jordan curve theorem doing its work. The hero checks two thousand points of the boundary’s image and finds every one inside. A proof would check the image of each side exactly — each side is a straight segment, its image a parabolic arc, and whether an arc crosses a line is a quadratic inequality, which settles the question with pencil and paper.

The images fold as they shrink. The first is a horseshoe-shaped band inside the quadrilateral; the second folds that band again; by the fourth there are several thin bands nested inside each other, which is the stretch-and-fold mechanism seen as a sequence of regions rather than a single orbit. The areas fall by exactly $0.3$ each time, measured here from the traced boundaries and matching the map’s constant Jacobian determinant. After $n$ steps the whole region holds $0.3^n$ of its starting area, so what the images shrink onto has area nought.

A quantity that falls, for the Lorenz flow #

A flow needs a different device, and Edward Lorenz supplied it in his 1963 paper. Take the function

$$V = x^2 + y^2 + (z - \sigma - \rho)^2,$$

which measures squared distance from a point on the $z$-axis. Along a trajectory of the Lorenz equations its rate of change works out, after a few lines of algebra in which the nonlinear terms cancel exactly, to

$$\dot V = -2\Big(\sigma x^2 + y^2 + \beta\big(z - \tfrac{\sigma+\rho}{2}\big)^2\Big) + \tfrac{\beta(\sigma + \rho)^2}{2}.$$

The bracket is positive except inside a fixed ellipsoid, and outside that ellipsoid $V$ must decrease.

So every trajectory eventually enters the set where $V$ is at most the largest value it takes on the ellipsoid, and stays: once below that level, $V$ can only rise where the trajectory is inside the ellipsoid, where $V$ is below the level anyway. That set is a ball, and it traps the flow. The trajectory in the figure starts at $V$ near ten thousand, falls below the level within a third of a unit of time, and oscillates below it for as long as it is followed. No computer is needed for the argument; the figure only shows it happening.

A function that decreases along trajectories outside some bounded set is called a Lyapunov function, after Aleksandr Lyapunov’s work on stability in the 1890s. Finding one is an art — there is no general recipe — but when it exists it proves boundedness for every trajectory at once, which no amount of simulation can.

Volume, gone at a known rate #

The Lorenz flow shrinks volume, and the rate is a constant anyone can compute: the divergence of the vector field, $-(\sigma + 1 + \beta)$, is the same at every point. The essay on dimension used this to show the attractor has no volume. The figure measures it directly.

The cube is stretched in one direction and crushed in another, and a direct computation of the volume of a squashed cube from its corners loses all precision long before a unit of time has passed — the volume becomes a tiny difference of large numbers. So the figure follows the cube’s three edge directions with the linearised flow, straightening them after every step and recording how much each was stretched, which keeps the calculation exact to many figures. The line it produces has slope $-13.667$ to six places.

Together the three facts — a trapping ball, constant volume contraction, and the continuity of the flow — prove that the Lorenz flow has an attracting set of zero volume. They say nothing about what that set looks like. A single stable periodic orbit is a set of zero volume. So is a stable fixed point. Everything that makes the Lorenz attractor strange is still unproved at this point.

A proof made of boxes #

What made the strangeness provable, for Lorenz, was a way of checking an infinite statement with a finite computation: interval arithmetic.

Ordinary arithmetic on a computer produces a number that is close to the right answer, with an error nobody tracks. Interval arithmetic, developed by Ramon Moore in the 1960s, computes instead with intervals guaranteed to contain the right answer: the sum of two intervals is an interval containing every possible sum, the square of an interval every possible square, and rounding is always directed outward. The output is a box that certainly contains the true value — too large, usually, but never wrong.

Apply that to a map, box by box. Cover the neighbourhood of the attractor with small boxes, compute the interval image of each, and note which boxes the images touch. If the set of boxes is closed — every box’s image lies within the set — then the union is a trapping region, proved by a finite number of interval calculations, each of which is exact about what it claims. The figure does this for the Hénon map on a grid six hundred boxes across: starting from the boxes a long orbit visits, it grows the set by adding every box touched by an image until nothing new appears, and after seven rounds it closes.

A coarser grid does not close. With a hundred boxes across, the overestimation of interval images near the tips of the attractor — where the map stretches most — is magnified at every step, and the set creeps outward until it leaves any finite window. That failure is the practical difficulty of every proof of this kind. The overestimation has to be kept smaller than the dynamics’ own contraction, which forces fine grids, many boxes, and in harder problems a great deal of cleverness about which coordinates to use.

What Tucker proved #

In 1998 Stephen Smale published a list of eighteen problems for the coming century, and the fourteenth asked whether the Lorenz equations at the classical parameters really have the strange attractor that everyone had seen for thirty-five years — specifically, whether the flow is equivalent to the “geometric Lorenz attractor”, a model built in the 1970s to have exactly the properties the pictures suggest and for which those properties had been proved.

Warwick Tucker answered it in 1999. His proof has two parts. Near the origin, where the flow slows to a stop and the numerical integration is least reliable, he used a normal form — an explicit approximation of the flow whose errors could be bounded by hand. Everywhere else he followed boxes of starting points through the flow with interval arithmetic, and proved two things: that a section across the attractor is carried into itself by the return map, the trapping half; and that the return map stretches a family of directions on that section uniformly, the strange half. The second is the part the Hénon calculation above does not attempt, and it is the part that took the new ideas.

The proof’s output is a certificate: a list of boxes and their interval images that anybody can check with another computer, faster than it was found. It is a proof of exactly the kind the earlier pictures are not, and it is what turned the Lorenz attractor from something seen into something known.

Why the Hénon attractor is still unproved #

For the Hénon map at $a = 1.4$, $b = 0.3$, the second half has never been done, and there is a specific reason to think it may be very hard.

As the parameter $a$ varies, the exponent is mostly positive — chaos — but it dips below zero again and again: periodic windows, parameter ranges in which the attractor is a stable cycle and every typical orbit eventually settles on it. Some windows are wide, like the one near $a = 1.23$; most are so narrow that a scan at this resolution sees them as single points, and there are narrower ones this scan cannot see at all. For one-dimensional maps like the logistic map it is a theorem that such windows are dense: arbitrarily close to every chaotic parameter there is a periodic one. For the Hénon family the corresponding statement is believed, and the Newhouse phenomenon shows that there are parameters with infinitely many coexisting stable cycles.

That is exactly the obstacle to a proof at $a = 1.4$. If a periodic window of width $10^{-20}$ contained $1.4$, the attractor there would be a stable cycle of enormous period, every orbit would eventually find it, and the chaotic picture every computer has drawn would be a transient lasting longer than any computation. A proof that the attractor is strange must rule that out, and no finite computation at finite precision can, unless it finds some robust property of the map that no periodic window could share.

What is proved is weaker and still remarkable. Michael Benedicks and Lennart Carleson showed in 1991 that for small $b$ and a set of $a$ of positive measure — near $a = 2$, far from the classical value — the Hénon map does have a strange attractor. Chaos is not a thin set of parameters; it occupies a positive proportion of them, interleaved with the windows. Whether $1.4$ is among the chaotic ones is not known.

The one-dimensional precedent #

The windows are not special to Hénon’s map. They were understood first for the logistic map, $x \mapsto ax(1-x)$, which is the Hénon map with its second coordinate switched off, and what is known there shows both how deep the problem is and why it can be solved.

On the logistic family, the period-three window is the widest of infinitely many, and between any two chaotic parameters there are windows — the parameters at which the map has a stable cycle are dense. That was proved in 1997 by Jacek Graczyk and Grzegorz Świątek, and independently by Mikhail Lyubich, after decades of partial results. And yet the chaotic parameters are not a thin leftover: Michael Jakobson proved in 1981 that they have positive measure, so a parameter chosen at random has a positive chance of being chaotic even though every chaotic parameter is a limit of periodic ones. The two sets are interleaved like the rationals and the irrationals, with the difference that here both have positive measure in every interval where chaos occurs.

For a single parameter, deciding which set it lies in is a question about the whole future of one orbit — the orbit of the critical point, whose folds measure the chaos and whose landing place draws the dark lines of the bifurcation diagram. For the logistic map at $a = 4$ the answer is known exactly, because the map can be solved. For most parameters it cannot be decided by any finite computation, for the reason the window figure shows: a window of width $10^{-20}$ is invisible to every scan.

The Hénon map inherits all of this and adds a second dimension, in which the critical point becomes a whole curve of tangencies between stretched and squeezed directions. Benedicks and Carleson’s proof for Hénon was a two-dimensional version of Jakobson’s, and it is famous for its length and difficulty. The classical parameter sits in a region their method does not reach.

Machines that prove, and machines that show #

The distinction this essay turns on — between a computation that illustrates and a computation that proves — is one that has come up before. The universality of the Feigenbaum constant was first established by a computer-assisted proof of the same kind, bounding an infinite-dimensional calculation with intervals; the four-colour theorem was proved by checking a finite list of configurations by machine. In each case what makes the machine’s output a proof is that it certifies an inequality with rigorous error bounds, not that it produces a convincing picture.

Every figure of an attractor until now produced a convincing picture. The attractors were drawn, measured, counted into boxes and histograms, and every measurement agreed with every other. None of that is evidence against a periodic window of width $10^{-20}$, because no computation that follows orbits in floating point can see one. What Tucker’s method does differently is not to follow orbits at all: it follows boxes, and it proves about every point of each box something that no single orbit could establish.

What these pictures cannot establish #

Every figure here, including the ones that prove things, is drawn from computations in floating-point arithmetic, and only some of them are proofs. The box figure is a proof in the sense of interval arithmetic only if its rounding is directed outward, which ordinary floating point is not; the figure uses exact interval formulas and ordinary rounding, so it is a faithful illustration of the method rather than a certificate. The trapping-quadrilateral figure checks two thousand boundary points, where a proof checks the arcs exactly. The Lyapunov-function figure shows one trajectory obeying an inequality that the algebra proves for all of them.

The window scan is the least conclusive. A Lyapunov exponent estimated from twelve thousand steps can be positive at a parameter where the true attractor is a cycle of period a million, and negative dips can be artefacts of a transient that has not yet escaped. The figure shows the texture of the parameter space, which is real, and cannot certify any individual point of it.

Still open: the classical Hénon attractor #

Whether the Hénon map with $a = 1.4$ and $b = 0.3$ has a strange attractor — as opposed to a stable periodic orbit of very long period — is not known. Hénon chose those parameters in 1976 as a simple model of the Lorenz attractor’s structure, and his model has outlived its original: the Lorenz question was settled in 1999, and the Hénon question, about a map that fits on one line, is still open.

Partial results are rigorous. Computer-assisted proofs have shown that the map at these parameters has positive topological entropy — its orbits, counted appropriately, grow exponentially in number — and have located and certified many of its periodic orbits. What they have not shown is that the typical orbit, the one every picture draws, is chaotic. The distance between those two statements is the distance between a map with chaos somewhere in it and a map with chaos where it can be seen.