结果族 028：Uniformly bounded components of Gaussian-prime graphs · 学科：Number theory · 验证状态：主结果已 Lean 形式化
把复数 a+bi 看成平面上的格子点，其中”素数格子”是可以落脚的石头，其余全是护城河。1962 年有人提问：能不能踩着石头、每步跨度不超过固定长度 D，永远跳下去而不落水？这篇论文证明：不能——而且不论从哪块石头出发，你能踏遍的石头总数有一个统一上限 B_D。
关键词卡片
看个具体例子
此前的计算表明：从原点出发、步长不超过 6 时能走到的范围有限——但那只是一个起点的经验。新定理覆盖一切有限步长 D：每个连通分量至多含 B_D 个素数，起点任选（界存在但未给出具体数值）。数轴上 4k+3 型素数（3、7、11、19…）也是石头，同样被管住。
为什么值得关心
六十年老问题一步关闭，而且”分量一致有界”远强于”没有无穷路径”；周期筛法加信息论计数的组合拳本身就是新方法。
已 Lean 形式化
第一级台阶
导读的图景是护城河里的踏脚石：对象是平面上无穷铺开的格子点，其中少数是能踩的”石头”，其余是水；操作是石头之间一步跨度不超过给定长度的跳跃。要问的是：石头永远跳不完吗？还是说，无论从哪块石头出发，能踏遍的石头总数都有一个统一上限？
第二级台阶
换成标准语言：格子点是形如 a+bi 的高斯整数，其中不可再分解的叫高斯素数，就是那些石头。给定步长上界 D，把所有高斯素数作为顶点、距离不超过 D 的两点连一条边，得到一张无穷图；互相连通的点组成一个连通分支，”永远跳下去”即图中一条不自交的无穷路径。
第三级台阶
定理的语境是：对每个固定的有限步长 D，存在有限数 B_D，使这张图的每个连通分支至多含 B_D 个顶点——界与出发点无关，连坐标轴上的素数也算在内。证明分两级：先挑出一组有限的小素数，证明”避开这些素数所选零类”的点集里根本没有步长受控的无穷自交回避路径；再利用该点集在格点平移下的周期性，把每个分支单射进一个有限环面，从而有界。”D 固定”挡住的是证明里尺度选择对 D 的依赖，因此 B_D 只保证存在而非显式。结论即导读的谜底：护城河不可跨越，六十年悬案关闭。
证明了高斯护城河猜想（Gaussian moat conjecture）：不存在步长一致有界、经过两两不同高斯素数的无穷游走；更强的是，对每个步长上界 @@M@@D@@，高斯素数图的连通分支（connected component）大小有一致上界 @@M@@B_D@@，与起点无关——悬置六十余年的问题得到完整解决。
高斯整数环 @@M@@\mathbb{Z}[i]@@（Gaussian integers）中的不可约元称为高斯素数（Gaussian prime），把 @@M@@a+bi@@ 等同于格点 @@M@@(a,b)@@，范数 @@M@@N(a+bi)=a^2+b^2@@。对给定 @@M@@D@@，以全部高斯素数为顶点、距离 @@M@@\le D@@ 的两点连边，得到图 @@M@@G_D@@；高斯护城河问题问：是否某个 @@M@@G_D@@ 含无重复顶点的无穷路径，即能否用有界步长在素数”岛屿”间永远跳跃而不落入合数”护城河”。问题可追溯至 Basil Gordon 在 1962 年斯德哥尔摩国际数学家大会上的提问，Erdős 后来又归于 Gordon 与 Motzkin（1963 年 Pasadena 数论会议）。此前进展分两路：Gethner–Wagon–Wick 构造了任意大的无素数圆盘与任意孤立的实高斯素数（Vardi 独立证明后者），但平面上的游走可以绕开局部障碍；Tsuchimura 的计算表明步长 @@M@@\le 6@@ 时从原点出发可达距离有限，却只针对特定起点。最接近的前身是 Gethner–Stark 的有限周期筛法（finite periodic sieving）：他们对步长 @@M@@\sqrt2@@ 与 @@M@@2@@ 建立了周期障碍，并提议用小高斯素数筛法处理更大步长。真正的卡点在”一致性”：一般局部有限图中”没有无穷路径”推不出”分支大小有界”，必须依靠周期结构。
主定理（一致分支界，uniform component bound）：对每个有限实数 @@M@@D@@ 存在有限数 @@M@@B_D@@，使 @@M@@G_D@@ 的每个连通分支至多含 @@M@@B_D@@ 个顶点；界与起始素数无关，坐标轴上的素数也包括在内。因此任何由不同高斯素数组成、相邻距离 @@M@@\le D@@ 的序列至多 @@M@@B_D@@ 项，无穷有界步长游走不存在。界是非显式的（nonexplicit）：固定 @@M@@D@@ 后证明只保证尺度足够大；@@M@@D<1@@ 时不同格点不能相邻，@@M@@B_D=1@@ 即可。
核心中间结果是有限筛障碍定理（finite sieve obstruction）：对每个 @@M@@D\ge1@@，存在有限的有理素数集 @@M@@\mathcal{P}_D@@（全为 @@M@@p\equiv1\pmod 4@@），使得避让集 @@M@@\mathcal{A}(\mathcal{P}_D)@@——即模每个选定素数的两个共轭高斯因子 @@M@@\pi_p,\overline{\pi_p}@@ 都不为零的格点——中不存在步长 @@M@@\le D@@ 的无穷自回避（self-avoiding）序列。
整体分两级：先证有限筛障碍，再用周期性归约升级为一致分支界。周期归约较短：@@M@@\mathcal{A}(\mathcal{P})@@ 在 @@M@@Q\mathbb{Z}^2@@（@@M@@Q=\prod p@@）平移下不变；若某有限分支含相差 @@M@@Q\mathbb{Z}^2@@ 中向量的两点，该平移把分支映到自身，与有限性矛盾，故每个分支单射入 @@M@@(\mathbb{Z}/Q\mathbb{Z})^2@@，至多 @@M@@Q^2@@ 个点；被筛除的高斯素数只是所选因子的相伴元（associates），共有限多个，补一个显式修正项即可。
筛法定理是重头戏。反设存在避开全部选定零类的无穷自回避 @@M@@D@@ 步游走——游走本身是确定的，随机性只来自采样时刻与对每个分裂素数（split prime）选取哪个共轭因子的”符号”。先做几何采样制造熵：一段 @@M@@n@@ 步线段含很多不同差值，证明用环面度数论证（torus degree argument）——由直径端点与离直径最远点构造的连续映射在平坦环面上度为 @@M@@-1@@ 因而满射，差值集的 @@M@@2D@@ 圆盘覆盖面积为 @@M@@A=RW@@ 的环面，得 @@M@@|E-E|\ge c_DA@@；再证随机符号乘积以高概率避开细矩形（用行列式被范数整除排除非零倍数、Hoeffding 集中控制单条直线、布尔立方体的等周不等式避免枚举直线），于是模约化在差值集上单射。从差值中均匀采样并随机取一个端点，得到熵增补（entropy enrichment）不等式：端点的剩余熵分数至少是起点熵分数与最大值的一半之和再减 @@M@@O_D(g)@@，迭代后熵亏指数式衰减。接着做覆盖传递（coverage transfer）：联合熵只给出平均意义下的接近均匀，需升级为”除 @@M@@p^{1-\beta}@@ 个例外剩余外，几乎每个坐标的边缘分布质量 @@M@@\ge\tau/p@@“；诀窍是让 @@M@@n@@ 次重复位移构成一个共享数据向量，其熵只在联合熵中支付一次，若覆盖失败，Fano 不等式的短列表版本会强制过大的条件信息，与联合熵预算矛盾。然后排公共调度（schedule）：把几何操作按递减尺度排成三个带（参数 @@M@@g_0@@、@@M@@e^{-M^3}@@、@@M@@e^{-100M^{20}}@@），并以公共终态时间律 @@M@@t_*@@（加均匀偏移使其在小平移下几乎不变）统一测量；从最底带极精确的单坐标熵基例出发反向归纳，得到在每个检查点、每个精确起点下的终态剩余覆盖。最后收网于信息论矛盾：既然游走避开零类，长度 @@M@@L_T\approx T^{2/5}@@ 的短增量词就能测试候选起始剩余——词内各偏移的命中事件互不相交（两次命中意味着差被 @@M@@\pi@@ 整除，而 @@M@@\pi@@ 的非零倍数长度 @@M@@\ge\sqrt p@@，该差又 @@M@@\le DL<\sqrt p@@，矛盾），故每个批次每步增量至少付出 @@M@@c_1/\log T@@ 的信息。再用嵌套剩余向量与二进分块，把各批次代价在公共时间律下望远镜求和，上界为单个有界增量的熵 @@M@@\log K_D@@；但批次横跨约 @@M@@M@@ 个几何窗口，下界随 @@M@@M@@ 发散，矛盾。此收尾与 Tao 的熵递减（entropy-decrement）论证方法相通。
本文主结果已由作者完成 Lean 形式化证明（结果族文档附 Lean 链接），验证等级最高。本族仅此一篇手稿，内部呈”有限筛障碍 + 周期归约”两级结构，两条定理分别独立陈述、后者由前者推出，逻辑自洽。界 @@M@@B_D@@ 非显式，具体数值不在定理范围。按 OpenAI 官方声明，未经形式化的结果可能有问题；本文主结果已形式化，读者可对照 Lean 证明核查。
问 1：证明里最脆弱的一环在哪里？
（答：信息论收尾（information/budget 两节）。反设游走避开全部选定零类后，须证长度约 T^{2/5} 的短增量词能测试候选起始剩余、每批次每步至少付出 c/log T 的条件信息，再用嵌套剩余向量与二进分块在公共时间律 t* 下把各批代价望远镜求和，上界是单个有界增量的熵。这一多尺度记账中三带尺度（g_0、e^{−M³}、e^{−100M^{20}}）与”近似平移不变的时间律”稍有错位，上下界就不再矛盾。）
问 2：为什么必须做周期归约，而不能只证”无无穷路径”？
（答：一般局部有限图中”没有无穷路径”推不出”分支大小一致有界”——分量可以越来越大却每个都有限。周期性是补齐这一步的关键：避让集在 Q·Z² 平移下不变，若某有限分支含相差 Q·Z² 向量的两点，该平移把分支映回自身，与有限性矛盾，于是每分支单射入 (Z/QZ)²，至多 Q² 点。这是 Vardi 已指出的路线，本文首次把它接上了对一切 D 的筛法障碍。）
问 3：与 Gethner–Stark 的有限周期筛法相比，真正的新意是什么？
（答：Gethner–Stark 只对步长 √2 与 2 建立周期障碍，并提议用小高斯素数筛更大步长。本文对任意固定 D 构造出有限素数集 P_D：靠环面度数论证制造差值熵、随机符号乘积分离差值、Fano 短列表版的覆盖传递，最后以 Tao 熵递减式论证收网——把筛法障碍变成了信息论定理，这是方法层面的换代。）
问 4：B_D 为什么是非显式的，这算不算缺陷？
（答：证明在固定 D 后才选择足够大的尺度与素数集，全过程无显式常数追踪，故定理只保证存在性。对猜想的定性解决而言这已足够；显式化需要重做参数管理，论文未尝试，也不影响已被形式化验证的逻辑链条。）
问 5：AI 生成证明最可能的出错模式？这里为何风险较低？
（答：此类证明的典型风险是多尺度熵记账的自洽性——熵增补不等式里 O_D(g) 余项的迭代衰减、覆盖传递中”联合熵只付一次”的技巧，都是符号演算易 silently 出错处。但本文主结果已由作者完成 Lean 形式化（结果族 028 附 Lean 链接），验证等级最高，机器已核对逻辑闭环，风险集中于形式化范围之外的辅助性陈述。）
问 6：谁会用到这个结果？
（答：直接关闭 1962 年 Gordon 提出、Erdős 归于 Gordon–Motzkin 的高斯护城河问题，计算数论界（Gethner–Wagon–Wick、Tsuchimura 一线）长期关注的经验现象就此定案。方法论的下游更广：周期筛法加熵论证的组合对”其他格点素数集上的有界步长游走”、以及任何需要从局部同余障碍推出全局一致界的组合数论问题都有借鉴意义。）
总评
一项以全新信息论机制关闭六十年老问题的工作，且主结果已 Lean 形式化、可信度在本批中最高；其代价是证明高度技术化、界非显式，方法能否移植到其他游走问题仍有待检验。