解法: 区間演算による厳密な計算機支援証明、Tucker(1999年)
原点で線形化されたLorenz系の固有値は、三つの具体的な実数である:一つは正(、外向きの方向)、二つは負(、内向きの方向)であり、 を満たす。これら三つの数は偶然の整数線形関係(「共鳴」)を満たさないため、古典的な定理は、原点付近の非線形系を、自明に解ける三つの独立した方程式 、、 に正確に見えるようにする滑らかな座標変換を保証する。
この新しい座標において、軌道が小さな立方体 に出入りするのにかかる正確な時間、そして正確にどこから出るかは、近似ではなく明示的な公式で書き下すことができる—系全体の中で最も危険な部分を、コンピュータではなく紙とペンだけで解ける唯一の部分に変えるのである。
古典的パラメータにおいて、原点で線形化されたLorenzベクトル場は (具体的には 、、)を満たす三つの実固有値を持ち、原点を二次元の安定多様体と一次元の不安定多様体を持つ鞍点にしている。これらの固有値が非共鳴条件(自明なもの以外、それらの小さな整数線形結合が零にならない)を満たすため、Sternbergの線形化定理は、原点の近傍における滑らかな(実際には十分に微分可能な)座標変換の存在を保証し、非線形の流れをその線形部分 に共役させる。
Tuckerはこの古典的な存在定理を実効的なものにする:この線形化座標において原点周りの小さな立方体 の内部で作業し、 の面を通る流入・流出の時刻と位置を、線形系の直接的で閉じた形の積分によって計算し、すべての近似誤差(線形化によって無視された高次項、および座標変換自体によるもの)を、関連するTaylor展開に区間演算を用いて厳密に評価する。
これにより、原点の安定多様体近くに入る初期条件の小さなパッチを流れがどのように運び、不安定多様体の方向によって二つに分割して再注入し、次の段階の数値的Poincaré写像が引き継ぐ領域へと戻すかを正確に記述する、明示的で厳密に検証された公式が生み出される。