解法:塔克利用区间算术给出的严格计算机辅助证明(1999年)
通俗地说
洛伦兹系统在原点线性化后的特征值是三个具体的实数:一个为正(,一个向外的方向),两个为负(,向内的方向),满足 。由于这三个数不满足任何偶然的整数线性关系(「共振」),一个经典定理保证存在一个光滑坐标变换,使原点附近的非线性系统看起来恰好就是三个互不耦合、可平凡求解的方程 、、。
在这套新坐标下,一条轨道进入并离开小立方体 究竟需要多长时间,以及它究竟从哪里离开,都可以写出显式公式而无需近似——这把整个系统中最危险的那部分,变成了唯一一个用纸笔而非计算机就能解决的部分。
详细分析
在经典参数下,在原点线性化的洛伦兹向量场具有三个满足 的实特征值(具体为 、、),使原点成为一个具有二维稳定流形与一维不稳定流形的鞍点。由于这些特征值满足非共振条件(除平凡组合外,它们的任何小整数线性组合都不为零),Sternberg 线性化定理保证在原点的一个邻域内存在一个光滑(实际上是充分可微)的坐标变换,把非线性流共轭到其线性部分 。
塔克使这个经典的存在性定理变得可操作:在这套线性化坐标下,在原点周围一个小立方体 内工作,经过 各面的进入与离开时刻及位置,通过对线性系统的直接、闭式积分来计算,而所有近似误差(来自线性化所忽略的高阶项,以及坐标变换本身)都用区间算术对相关的泰勒展开进行严格界定。
这产生了显式的、经过严格验证的公式,精确描述了流是如何把靠近原点稳定流形附近进入的一小片初始条件,按不稳定流形的方向分裂成两部分,再重新注入并送回到下一步中由数值庞加莱映射接手的区域中的。
常见错误. 鞍点附近存在线性化坐标变换,这是一个经典的、纯粹定性的事实(可追溯到1950年代的 Sternberg);塔克在这一阶段的贡献并非这个存在性定理本身,而是把这些估计变成定量明确、且经过严格界定的形式,而这正是移交给证明中数值部分所真正需要的。