结果族 220：Directional zero–one laws beyond iid environments and iid ballisticity · 学科：Probability and statistical mechanics · 验证状态：主结果已 Lean 形式化
一只随机蚂蚁整体上朝东永不回头，它是匀速直线前进，还是可能像蜗牛越爬越慢、方向却不变？这篇论文给出裁决：在高维（@@M@@d\ge 2@@）独立且一致椭圆的环境里，只要几乎必然朝某方向逃逸，就必存在只依赖环境分布的确定极限速度 @@M@@v@@，且 @@M@@v@@ 在该方向上的投影为正——”永不回头”自动升级为”匀速前进”。
关键词卡片
@@M@@X_n/n\to v@@ 且 @@M@@v\cdot\ell>0@@。@@M@@\kappa@@。看个具体例子
数字版定理：@@M@@P_0(A_\ell)=1\ \Rightarrow\ P_0\big(\lim_n X_n/n=v\big)=1@@ 且 @@M@@v\cdot\ell>0@@；当 @@M@@d\ge 3@@ 时配合姊妹篇的 0-1 律，连”@@M@@P_0(A_\ell)>0@@“都自动升级为”@@M@@=1@@“。证明的关口在于：”再生时间几乎必然有限”推不出”平均值有限”，而算速度恰恰需要平均值；论文补上的决定性一步，是证明首达高层的概率衰减得足够快，恰好填上这个缺口。
为什么值得关心
它以”单方向瞬态”为唯一假设正面解决弹道性猜想，而此前的所有判据都需要额外的定量出口条件。它也是族内唯一通过 Lean 形式化检验的主结果，可信度目前在三篇姊妹作之中最高。
已 Lean 形式化
第一级台阶
入门导读问：整体向东、永不回头的随机蚂蚁，是匀速直线还是越爬越慢？换成半数学语言：对象是格点上的游走者与一套各点独立同分布的转移概率——每个方向的概率都有统一的正下界；操作是把长程行为分成两级来比较：只问”最终逃出每个后向半空间”，与要求”按线性速率前进”。要问的是：前者是否自动蕴含后者。
第二级台阶
用本科术语定义概念。方向瞬态指路径在固定方向上的投影趋于正无穷；弹道性指存在一个在该方向上投影为正的向量，使位置除以时间几乎必然收敛于它；再生结构指在路径创下新高、此后不再回落的时刻切割出的相互独立里程段；更新大数定律说，若里程段的平均时长有限，取平均即得速度。
第三级台阶
定理的语境：维度至少为二，环境行独立同分布且一致椭圆，游走在某固定方向几乎必然逃逸。维度假设挡住一维的反例——那里一致椭圆环境下确有零速度的瞬态游走；一致椭圆给每步一个统一的概率下界，挡住陷阱式退化。结论用这些话说：存在只依赖环境行分布的确定性速度向量，其在该方向投影为正，位置除以时间几乎必然收敛于它；不加漂移、可逆或任何矩假设。证明的关口在于：再生时长几乎必然有限推不出均值有限，而算速度恰恰需要均值——论文用首达高层概率的快速衰减估计补上这一缺口。
证明了 @@M@@\mathbb{Z}^d@@（@@M@@d\ge2@@）iid 一致椭圆环境中，沿固定方向几乎必然逃逸的游走必有确定性极限速度 @@M@@v@@ 且 @@M@@v\cdot\ell>0@@：方向瞬态与弹道性等价，正面解决了弹道性猜想（ballisticity conjecture）。
方向瞬态（directional transience）指游走最终离开每个后向半空间；弹道性（ballisticity）要求更强的线性进展 @@M@@X_n\cdot\ell/n@@ 有正下界。对随机环境中的随机游走（RWRE），反复陷入不利区域可能把两者分开：一维中 Solomon（1975）就构造出一致椭圆 iid 环境下零速度的瞬态游走。高维中额外空间路线是否杜绝这类减速，是长期未决的问题；Fribergh–Kious（2016）的猜想 1.1 正是以”单方向瞬态”为唯一假设来表述。技术核心在再生结构（regeneration，Sznitman–Zerner 1999）：在新高度记录处切割，再生段独立，若再生时间有有限均值，更新大数定律即给出速度；但几乎必然有限推不出均值有限。此前所有定量路线——Kalikow 条件、Sznitman 的 @@M@@(T)_\gamma@@/@@M@@(T')@@ 与有效判据、Berger–Drewitz–Ramírez 的多项式出口界、Guerra–Ramírez 与 Guerra 的后续判据——都从定量出口假设出发，没有人能从纯粹的几乎必然逃逸出发。
定理：设 @@M@@d\ge2@@，环境行为 iid（行内各项不必独立）且一致椭圆（存在 @@M@@\kappa>0@@ 使 @@M@@\min_e p(e)\ge\kappa@@ 几乎必然）。若 @@M@@P_0(A_\ell)=1@@，则存在只依环境行分布 @@M@@\nu@@ 的确定性向量 @@M@@v@@，使 @@M@@v\cdot\ell>0@@ 且 @@M@@P_0(\lim_n X_n/n=v)=1@@；特别地游走在同方向弹道。不加漂移、对称、可逆或再生时间矩假设。推论（@@M@@d\ge3@@）：借助姊妹篇严格椭圆方向 0-1 律，@@M@@P_0(A_\ell)>0@@ 即升级为 @@M@@=1@@ 并得同一结论；进而 @@M@@\{u:P_0(A_u)=1\}=\{u:P_0(A_u)>0\}=\{u:v\cdot u>0\}@@——逃逸方向集恰是一个开半球，赤道与反向概率全为 0。
证明把空间控制与时间控制分开。先做几何：在原始实方向上构造真实的”记录词”；对普通记录指标计数给出有限平均投影宽度——即使投影高度不离散；再在倾斜记录处放置前向模板（forward template）得到有限平均空间半径。于是在还没有任何时间矩时就得到确定性极限射线，并经带符号的坐标置换把高度设为 @@M@@x_1@@。对坐标高度，令 @@M@@a_N=P_{0,\omega}(T_N<T_{-1})@@ 为 quenched 首达 @@M@@N@@ 层先于 @@M@@-1@@ 层的概率。决定性估计是：固定 @@M@@0<\beta<1@@，事件 @@M@@\{a_N<N^{-\beta}\}@@ 的环境概率随 @@M@@N@@ 衰减快于任何幂次。论文证明这一估计恰好补上缺失的再生时间均值，从而由更新大数定律得到速度。该估计的证明是主体：先比较两条游走在整数层首击的位置。共享的独立公共再生词给出对称增量，尺度由其截断方差定义；在 Gauss 子序列上，共享环境的比较必须排除投影对角线上的正极限占据，其截断尺度论证同时覆盖未必 Gauss 的较小尺度；由此得到的两拷贝极限给出 quenched 逼近，全程不需要二阶矩或现成的 quenched 不变原理。再经裁剪（clipping）合并 Gauss 与非 Gauss 子尺度，在每个大尺度上保住首击位置落在窄管中的正 quenched 质量；核（kernel）一步把它转化为分离的端点种子、快速损失界与带指数可积局部余项的外向阶估计，所有自适应测试只使用被测顶层以下的出发行。最后反证：若关键估计失效，对坏环境条件化只花费对数级相对熵；多尺度阶段（stages）构造自适应选取的层段（episode），在有界阶段数上产生全局存活质量的正期望损失；对 episode 取平均得到局部端点轮廓（profile）及其上环境的平稳律；有限窗熵界排除质量的弥散与无穷多个分离类别；在存活的全支撑类中用尾部序统计量在两端远处检验，把局部环境偏置从外向阶余项中剥离，与持续的存活损失矛盾。
本文主结果已 Lean 形式化（家族说明链接 lean/docs/220.md），验证状态在族内最好。它以严格椭圆姊妹篇的方向 0-1 律为输入得到推论，而有限程依赖篇又与严格椭圆篇共用”半径—接触”架构，三篇互相咬合成完整图景。仍需说明：Lean 形式化针对本文主定理，两篇姊妹篇尚未形式化，且按 OpenAI 官方声明，未经形式化的结果可能有问题，引用族内结论时应分别区分验证状态。
问 1：证明的决定性一步是什么？
（答：对坐标高度的首达概率估计：固定零与一之间的指数，事件”游走在坏环境中先达 N 层先于负一层的机会小于 N 的负指数幂”的环境概率随 N 衰减快于任何幂次。正是它补上”再生时长几乎必然有限推不出均值有限”的缺口，使更新大数定律可以出手。论文其余全部篇幅都在证这条估计。）
问 2：这条估计的证明里最脆弱的环节在哪里？
（答：末段反证链条——条件化坏环境只花对数级相对熵，多尺度阶段构造自适应层段产生正期望存活质量损失，对层段平均得局部端点轮廓的平稳律，有限窗熵界排除质量弥散与无穷多分离类，最后用存活类两端的尾部序统计量把局部环境偏置从外向阶余项中剥出、与持续损失矛盾。任一环的熵界或平稳性失准，矛盾即失效。）
问 3：维度为何要求至少二？一致椭圆能否放宽？
（答：一维中 Solomon 早有反例——一致椭圆独立环境下瞬态却零速度，结论必假；高维的附加空间路线是定理成立的实质来源。一致椭圆是本文假设；姊妹篇的零一律只要求严格椭圆，一致蕴含严格，故推论可借用，但主定理本身未在严格椭圆下证明。）
问 4：与此前定量判据相比真正新意是什么？
（答：Kalikow 条件、Sznitman 的 (T)_γ/(T’) 与有效判据、Berger–Drewitz–Ramírez 的多项式出口界、Guerra 的弱判据，全部从定量出口假设出发；本文从纯粹的几乎必然逃逸出发，自行推导出所需的定量穿越估计，正面解决 Fribergh–Kious 猜想一点一。）
问 5：Lean 形式化覆盖到什么程度？
（答：主定理已形式化，是族内唯一；但高维推论依赖的姊妹篇方向零一律尚未形式化，推论的可信度仍系于那篇的核验。形式化也只覆盖主定理陈述的推理链，运行细节之外的解释性声明不在此列。）
问 6：方向半球推论该如何解读？
（答：推论断言三个方向集相等——概率一逃逸、正概率逃逸、与速度向量内积为正的开半球；赤道与反向方向概率为零。但这是对每个固定方向的退火概率断言，不是对所有方向同时成立的路径断言，文中特意区分。）
问 7：谁会用到它？
（答：RWRE 速度理论的后续问题——中心极限定理、大偏差、慢尾相变——现在可以在无矩条件下重新表述；逃逸方向集的完整半球刻画也为非平衡统计力学中的漂移模型提供参照。）
总评
正面解决弹道性猜想且主定理经 Lean 形式化，是族内可信度最高的结果；最大风险不在主定理而在推论链条上游那篇尚未形式化的零一律。