解法: 区間演算による厳密な計算機支援証明、Tucker(1999年)
Tuckerの証明は問題全体を地理的に分割する。原点にある厄介な鞍点周りの小さな立方体の内部では、数値シミュレーションを完全に放棄し、代わりに標準形理論からの厳密な、紙とペンによる評価を用いる—微積分だけで何が起こるかを完全に記述できるほど小さく単純な領域である。その立方体の外側、流れがよく振る舞い帰還時間が有界であるところでは、コンピュータに引き継がせ、個々の点ではなく小さな領域全体を一度に、数学的に保証された誤差評価とともに追跡する。
構成全体の目標は、得られた帰還写像が既知の設計図—数年前にJohn GuckenheimerとRobert Williamsによって設計された「幾何学的Lorenzモデル」—と一致することを確認することである。その性質は、実際の方程式がその設計図の要件を本当に満たすことさえ示せれば、真に頑健なカオス的アトラクタを保証することが既に知られていた。
Tuckerの戦略(1999年の発表と2002年の完全な論文で説明される)は、アトラクタの近傍を根本的に異なる扱いを受ける二つの領域に分割する。原点周りでは、(原点での線形化の固有値が非共鳴条件を満たすことから正当化される古典的標準形理論による)座標変換によって、そこでの流れを明示的で厳密に解ける形にできるほど小さな立方体 が選ばれる。 を通る流入・流出の挙動は、シミュレーションではなく直接計算によって評価でき、鞍点近くでの帰還時間の発散を完全に回避する。
の外側、軌道が有界な速度で動き、有界な帰還時間を持つ断面への真のPoincaré帰還写像が定義できるところでは、Tuckerは厳密な計算機支援評価(次の段階で詳述される)に転じる。二つの扱いは境界 でつなぎ合わされ、内側からの解析的評価が外側からの数値的評価へと直接引き継がれる。
ここで明確にされる構成全体の目標は、John GuckenheimerとRobert F. Williams(1979年)、およびRobert Williams(1979年)によって導入された幾何学的Lorenzモデルである:特異双曲的アトラクタを持つ流れの抽象的テンプレートであり、特定の組合せ論的・拡大的性質の集合を持つ拡大的な一次元帰還写像から構築される。GuckenheimerとWilliamsは、このテンプレートを満たすあらゆる流れが頑健な特異双曲的ストレンジアトラクタを持つことをすでに証明していた;残っていたこと—そして1979年以来未解決であったこと—は、古典的パラメータにおける実際のLorenz方程式がそのテンプレートの仮定を満たすことを示すことであり、まさにそれを残りの段階が検証する。
- 標準形
- 平衡点付近の座標を変数変換によって単純化したもので、微分方程式が可能な限り単純な代数的形(多くの場合は線形部分のみ)をとり、その解が明示的で評価しやすくなる。
- Poincaré帰還写像
- 微分方程式の流れに横断的な曲面が与えられたとき、その曲面上の点を、軌道が再びその曲面を横切る次の点へ送る写像。これは連続時間の流れを、しばしば解析がはるかに容易な離散時間力学系へと変える。