Worked solution: Tucker's rigorous computer-assisted proof via interval arithmetic (1999)
Trapping trajectories inside a bounded region is not enough to prove chaos — a boring, perfectly repeating loop is trapped too. The extra ingredient needed is sensitive dependence on initial conditions: nearby points must reliably drift apart over time, not converge together. Tucker certifies this geometrically, by assigning to every point in the trapped region a narrow "cone" of allowed directions, and then verifying, again with guaranteed interval computation, that the flow's derivative always sends vectors pointing inside this cone to new vectors that are both still inside the (new) cone and measurably longer than before.
A cone that a map keeps sending to itself while stretching every vector inside it is a geometric certificate of instability: it means directions of expansion persist and compound step after step, rather than fading away — precisely the mechanism that amplifies tiny differences into the wildly divergent trajectories associated with chaos.
To certify chaos rather than merely boundedness, Tucker equips the trapping region from the previous step with a field of cones: at each point , a subset of the tangent space consisting of vectors within some angular threshold of a chosen expanding direction. Using rigorous interval bounds on the derivative of the return map (computed alongside the map itself, via the variational equation of the flow), Tucker verifies two properties throughout the trapped region: the cone field is invariant, , and expanding, for some fixed and every .
These two properties together are the geometric definition of the singular-hyperbolicity central to the Guckenheimer–Williams template: they guarantee that any two nearby points whose separation vector starts inside the cone field must separate at an exponential rate under repeated application of the return map, which is precisely the mathematical formalisation of sensitive dependence on initial conditions. Crucially, because the origin's saddle structure means the cone field cannot be uniformly hyperbolic in the classical (Anosov/Axiom A) sense across all of phase space, this weaker but sufficient singular-hyperbolic notion (due to Morales, Pacifico and Pujals) is exactly what the Guckenheimer–Williams template requires and what interval arithmetic is capable of certifying rigorously.
With both forward-invariance (previous step) and this expanding cone field established, the return map is verified to have exactly the combinatorial and geometric structure the Guckenheimer–Williams abstract model demands, setting up the final assembly step.
- Singular-hyperbolicity
- A weakening of classical (uniform) hyperbolicity designed to handle flows, like Lorenz's, whose attractor contains an equilibrium point; it requires expansion along a well-defined cone field rather than at every point of phase space in every direction uniformly.