解法: 区間演算による厳密な計算機支援証明、Tucker(1999年)
三つの独立した作業が今かみ合う。標準形の評価は、原点付近の唯一の危険な場所を厳密に処理する。長方形ごとに検証された前方不変なトラップ領域は、アトラクタが数値的な幻影でも無限遠への脱出でもない、真に有界な対象であることを示す。拡大する錐場は、その領域内の運動が本当に不安定であり、ひそかに偽装された周期軌道ではないことを示す。
GuckenheimerとWilliamsは、1979年にすでに、まさにこの性質の組み合わせを持つあらゆる系が頑健なカオス的アトラクタを持つことを証明していた。Tuckerの成果は、1963年にローレンツが実際に用いたパラメータにおける実際のローレンツ方程式が、本当にこの組み合わせを持つことを、初めて完全な厳密さで示したことにある—これにより、二十年来の条件付き定理が、誰もがずっとシミュレートしてきたその系についての無条件の事実へと変わったのである。
Guckenheimer–Williamsの幾何学的Lorenzモデルは、流れに対してまさに三つの要素を要求する:(a)一定の固有値不等式を満たす線形化標準形を持つ鞍点型平衡点(ステップ3で解析的に検証)、(b)断面への明確に定義された前方不変なPoincaré帰還写像であり、その定義域が鞍点の安定多様体によって適切に階層化されているもの(ステップ5の厳密な長方形計算で検証)、そして(c)その帰還写像の導関数に対する不変で一様に拡大する錐場であり、特異双曲性を符号化するもの(ステップ6で検証)。
これら三つの要素はそれぞれ、Tuckerの計算において における実際のLorenz方程式に対して厳密かつ独立に確立された。GuckenheimerとWilliamsの1979年の定理(およびその洗練版)は、これら三条件をすべて満たすあらゆる系が頑健な特異双曲的アトラクタを持つと述べる:頑健とは、ベクトル場の小さな摂動(特に、古典的な値付近での の小さな変化)のもとでアトラクタが存続することを意味し、特異双曲的とは、アトラクタ上に平衡点を持つ流れへ一様双曲性を一般化する、Morales、Pacifico、Pujalsの正確な技術的意味においてである。
Tuckerがこれら三つの仮定すべてを、(理想化された近似モデルに対してではなく)真のLorenz方程式に対して無条件に成り立つことを検証したため、Guckenheimer–Williamsの結論が直接適用される:古典的Lorenz系は、正の位相的エントロピーを持つ頑健なカオス的アトラクタを真に持つのである。