在数论和动力系统领域，Collatz猜想长久以来吸引着数学家的关注。近日，研究者Lech Mazur在证明平台Lean上形式化了一个重要定理：自然密度几乎有界的Collatz轨道在对数时间内。该定理表明，对于几乎所有正整数，Collatz过程能在对数步骤内下降到任何给定的增长阈值以下。
具体而言，定理包含两个版本。第一个版本针对Syracuse步骤（仅考虑奇数到奇数的变换），对密度为1的奇数起始点，在最多145·log N步内达到阈值以下。第二个版本针对原始Collatz步骤（包括所有奇偶变换），对密度为1的正整数起始点，在最多436·log N步内达到阈值以下。这两个版本覆盖了不同的域，不可混淆。
此外，定理还得出一个推论：对于密度为1的起始点，存在一个指数m满足log N/(2 log 2) < m ≤ 436·log N，使得Collatz^m(N) < √N。即平方根目标在对数时间窗口内可达。
该证明的核心是利用Rhin相位间隙，通过定量速率引擎将固定目标控制转化为Syracuse结论，再利用2-adic提升得到原始Collatz结论。整个证明在Lean中完全形式化，包含599个Lean文件，超过18万行代码，所有证明步骤均通过检查。
值得注意的是，该定理并不证明Collatz猜想本身，也不保证所有起始点最终到达1。它允许一个密度为零的例外集存在。阈值必须趋向无穷，但不必单调。该结果与Terras的有限幂节省界是独立的，不可视为依赖关系。
这一形式化成果为Collatz问题提供了重要的密度视角，并为后续研究更强的时间常数、显式收敛速率以及类似动力系统提供了基础。