结果族 241：Rigidity of the Turing degrees · 学科：Mathematical logic · 验证状态：主结果已 Lean 形式化
把世上所有计算问题连成一张关系网：若”拿 B 当参考答案就能算出 A”，就在两者之间连一条线。现在把每个问题自己的名字全部涂掉，只留下这张纯粹的”谁难谁易”网。本文证明：光看网的结构就能认出每个难度是谁——任何保持上下级关系的”重新贴标签”，都只能是原样不动。
关键词卡片
@@M@@A\le_T B@@，即把 B 当”谕示”（随取随用的参考答案），图灵机就能算出 A。看个具体例子
难度网的最底层是 @@M@@\mathbf 0@@（可计算问题），往上是 @@M@@\mathbf 0'@@（停机问题的难度）、@@M@@\mathbf 0''@@……定理说：任何保序双射 @@M@@\pi@@ 都把每一个度送到它自己。下图虚线代表 @@M@@\pi@@ 想做的”搬运”，结果全部原地踏步。
为什么值得关心
这正面解决了 Slaman–Woodin 刚性猜想，并连带证实图灵度序与二阶算术可无参数互相解释——一张涂掉名字的抽象关系网，竟装得下整个二阶算术的信息。
已 Lean 形式化
第一级台阶
导读里那张”谁难谁易”的关系网，现在可以说得更严格：网上的点不是计算问题本身，而是按”互相可算”归并之后的难度档位；两点连线的规则是”把一个当随取随用的参考答案，就能机械地算出另一个”。涂掉名字后剩下的，就是这个”不难过”关系构成的纯序结构，而”重新贴标签”即保持这张网整体形状不动地置换节点。
第二级台阶
用本科术语精确化：图灵归约 @@M@@A\le_T B@@ 指以 @@M@@B@@ 为谕示的图灵机能算出 @@M@@A@@ 的特征函数；互相归约的集合归入同一个图灵度，全体度构成偏序 @@M@@(\mathcal D_T,\le_T)@@。序自同构 @@M@@\pi@@ 是满足 @@M@@\mathbf a\le_T\mathbf b\iff\pi(\mathbf a)\le_T\pi(\mathbf b)@@ 的双射；刚性问题问自同构群是否平凡。
第三级台阶
定理 1.1 断言：在 ZFC 中、不对 @@M@@\pi@@ 附加任何可定义性或正则性假设，每个序自同构都是恒等。此前经典结果（Jockusch–Solovay、Shore–Slaman、Slaman–Woodin）只能固定 @@M@@\mathbf 0''@@ 以上的公共锥，难点全在锥外。证明唯一的整体外部输入是 Slaman–Woodin 表示定理：任意自同构都由某个算术（从而 Borel）的函数诱导——正是这层正则性打开了 Baire 纲论证的入口。结论还顺带落下推论：度序与二阶算术无参数互相解释。
本文证明图灵度（Turing degrees）偏序 @@M@@(\mathcal{D}_T,\le_T)@@ 完全刚性：任何保序自同构必为恒等，正面解决刚性猜想，并连带证实 Slaman–Woodin 双解释猜想——”谁计算谁”的序关系足以唯一标记每个度。
图灵归约（Turing reducibility）@@M@@A\le_T B@@ 指以 @@M@@B@@ 为谕示（oracle）的图灵机能算出 @@M@@A@@ 的特征函数；互相归约的集合视为等同，其等价类即图灵度（Turing degree），全体度构成偏序 @@M@@(\mathcal{D}_T,\le_T)@@。这一相对可计算性概念源自 Turing 1939 年的谕示机。自同构问题（automorphism problem）问：丢掉集合的具体编码、只留下抽象的序，还保有多少信息？刚性猜想断言任何满足 @@M@@\mathbf a\le_T\mathbf b\iff\pi(\mathbf a)\le_T\pi(\mathbf b)@@ 的双射 @@M@@\pi@@ 都是恒等。此前进展：Jockusch–Solovay（1977）证明保跳算子（jump operator）的自同构固定 @@M@@\mathbf 0^{(4)}@@ 以上的度；Shore–Slaman（1999）证明跳算子可由序关系定义，因而被一切自同构保持；Slaman–Woodin（2005）进一步证明所有自同构共同固定 @@M@@\mathbf 0''@@ 以上的锥（cone），且自同构群可数、每个自同构有算术表示。悬而未决的正是锥外——@@M@@\mathbf 0''@@ 以下——的度。
刚性定理（定理 1.1） 在 ZFC 中，对任何序自同构 @@M@@\pi\in\mathrm{Aut}(\mathcal{D}_T,\le_T)@@ 与任何度 @@M@@\mathbf a@@ 均有 @@M@@\pi(\mathbf a)=\mathbf a@@；对 @@M@@\pi@@ 不附加任何可定义性或正则性假设。
推论 5.1（双解释） 图灵度序与二阶算术（full second-order arithmetic）无参数双解释（biinterpretable without parameters），这由 Slaman–Woodin 所证”刚性等价于双解释”直接得到。
支撑主定理的技术核心是恢复定理（recovery，命题 4.1）：设 Borel 函数 @@M@@F:\mathbb R\to 2^{\mathbb N}@@ 具可数纤维（countable fibers）且满足加法归约 @@M@@F(x+y)\le_T F(x)\oplus F(y)@@，则对每个无理数 @@M@@t\in(0,1)@@ 存在余贫集（comeager set）@@M@@G_t\subseteq\mathbb R^2@@，使对每对 @@M@@(u,v)\in G_t@@ 有有理数 @@M@@\delta\in(0,1)@@ 满足 @@M@@C(t)\le_T F(u)\oplus F(u-v)\oplus F(v-u+\delta t)\oplus F(v-u+\delta(t-1))@@，其中 @@M@@C(x)=\{i:q_i<x\}@@ 是有理切割（rational cut）编码。该命题与自同构无关，独立成立。
证明分三步：表示、恢复、消参。
先把自同构”落地”。本文唯一的外部输入是 Slaman–Woodin 表示定理（2005 年未刊手稿定理 6.3.1(2)）：任何自同构 @@M@@\pi@@ 都由某个算术的、因而 Borel 的函数 @@M@@\widehat F:2^{\mathbb N}\to 2^{\mathbb N}@@ 诱导，即 @@M@@\deg_T\widehat F(A)=\pi(\deg_T A)@@ 对每个集合成立。复合有理切割得 @@M@@F:\mathbb R\to2^{\mathbb N}@@：它 Borel、纤维可数（@@M@@\pi@@ 是单射而每个度只含可数多个集合），且由 @@M@@\pi@@ 保序又保上确界（join）推出加法归约。
再证四值恢复，机制是有界递推（bounded recurrence）加平均恒等式：状态 @@M@@s_0=0@@，每步读 @@M@@F(u+s_n)@@ 的一个固定比特位，据此选增量 @@M@@\delta t@@（向上）或 @@M@@\delta(t-1)@@（向下），记选择为 @@M@@r_n@@。求和得 @@M@@s_N=\delta(Nt-\sum_{n<N}r_n)@@；只要状态始终有界，频率 @@M@@A_N=\frac1N\sum_{n<N}r_n@@ 便以误差 @@M@@<1/(N\delta)@@ 逼近 @@M@@t@@，而 @@M@@t@@ 无理，故可由这些逼近算出 @@M@@C(t)@@。有界性如此保证：可数纤维使 @@M@@F@@ 在 @@M@@u@@ 两侧近处取到不同值，取差异比特 @@M@@j@@；Borel 函数在某个余贫集上连续，于是该比特在区间两端附近各取常值，等效于”端点附近永远指向内部”，中间行为任意也不越界。递推只需四个真实谕示：辅助对 @@M@@(u,v)@@ 把”从 @@M@@u+s@@ 前进 @@M@@a@@“拆成两次加法 @@M@@(u+s)+(v-u+a)=v+s+a@@、@@M@@(v+s+a)+(u-v)=u+s+a@@；最小归约指标 @@M@@e(x,y)@@ 是 Borel 的，在其连续点附近沿可数群 @@M@@H=\mathbb Q+\mathbb Qt@@ 平移时两个程序指标保持固定，于是初始值 @@M@@F(u)@@、返程值 @@M@@F(u-v)@@ 与两个增量处的值恰是全部谕示。
最后消参与收尾：四个自变量都是 @@M@@t,u,v@@ 的有理线性组合，度不超过 @@M@@\mathbf b=d(t)\vee d(u)\vee d(v)@@，故 @@M@@d(t)\le_T\pi(\mathbf b)@@；用 @@M@@\pi^{-1}@@ 作用得 @@M@@\pi^{-1}(d(t))\le_T d(t)\vee d(u)\vee d(v)@@ 在余贫集上成立。若 @@M@@\pi^{-1}(d(t))\not\le_T d(t)@@，范畴避锥引理（category avoidance，归功于 Sacks）断言满足该式的 @@M@@(u,v)@@ 只构成贫集，与 Baire 纲定理矛盾。于是 @@M@@\pi^{-1}(\mathbf a)\le_T\mathbf a@@ 对一切度成立（无理数的度穷尽非可计算度，最小度显然固定）；对 @@M@@\pi^{-1}@@ 再用一次并配合反对称性即得 @@M@@\pi(\mathbf a)=\mathbf a@@。
主结果已有 Lean 形式化证明（结果族 241 文档），这是目前最强的核验方式；切割编码、Borel 连续性、范畴避锥、四值恢复等关键引理在文中均有自足证明，唯一整体引用的外部输入是 Slaman–Woodin 未刊手稿中的表示定理。本结果族目前仅此一篇手稿，它直接建立在 Jockusch–Solovay、Shore–Slaman、Slaman–Woodin 的经典链条之上；与 Kjos–Hanssen 的置换自同构刚性、Lutz–Siskind 的完满集四元恢复属同族技术但假设各异。按 OpenAI 官方声明，未经形式化的结果可能有问题；本文主结果已形式化，可靠性相应较高。
问 1：证明里最关键、最脆弱的一步是哪一步？
答：命题 4.1 的四值恢复定理。其机制是有界递推加平均恒等式：状态 @@M@@s_N=\delta(Nt-\sum r_n)@@ 必须始终落在 @@M@@(-1,1)@@ 内，频率 @@M@@\frac1N\sum r_n@@ 才能以 @@M@@1/(N\delta)@@ 误差逼近 @@M@@t@@。有界性靠”可数纤维 + Borel 余贫集连续”保证端点附近各取常值，中间行为任意——这一步若失守，后面的消参无从谈起。
问 2：恢复定理里”可数纤维”和”Borel”这两个假设哪个能去掉？
答：都去不掉。可数纤维保证 @@M@@F@@ 在 @@M@@u@@ 两侧近处取不同值，从而能选出区分上下的比特；Borel 性则给出余贫集上的连续性，使该比特在端点邻域取常值。二者合起来正是自同构表示函数”算术诱导、单射”的产物——换成任意函数，恢复机制立即失效。
问 3：与 Groszek–Slaman、Lutz–Siskind、Kjos–Hanssen 的恢复技术相比，真正新意在哪？
答：恢复的来源不同。前两者从完满集的分支恢复实数、需额外谕示；Kjos–Hanssen 恢复 Bernoulli 参数、用测度锥定理且表示函数须来自置换。这里从单个 Borel 函数的加法归约关系出发、四个自变量全是有理仿射组合、无需额外实数谕示，消参用 Baire 纲而非测度。
问 4：整篇论文只外部引用了 Slaman–Woodin 未刊手稿的表示定理，这是风险吗？
答：是最大的结构性风险。定理 6.3.1(2) 出自 2005 年未发表手稿（亦见 Slaman 的综述），若其陈述或证明日后有修订，本文的”Borel 表示”入口就要重新校准。文章自身部分已 Lean 形式化，但表示定理作为外部输入不在形式化范围内。
问 5：恢复只在余贫集上成立，为什么这就够了？
答：因为消参用的是 Sacks 式范畴避锥引理：若 @@M@@\pi^{-1}(d(t))\not\le_T d(t)@@，则满足恢复不等式的辅助对 @@M@@(u,v)@@ 只构成贫集；而恢复又断言它们余贫——与 Baire 纲定理正面冲突。两个”贫/余贫”判断相撞，就把辅助度挤掉了。
问 6：这个结果谁会用、能推出什么？
答：推论 5.1 直接兑现 Slaman–Woodin 双解释猜想：度序与二阶算术无参数互相解释，意味着度序中每一步”可定义性”讨论都获得了完整的算术内容。对可计算性理论而言，这张涂掉名字的网被证明装着全部二阶算术信息。
总评
这是刚性猜想的完整正面解决，且主结果已有 Lean 形式化背书，分量十足；最大风险不在长技术链，而在其唯一外部支点——未刊的 Slaman–Woodin 表示定理——的可靠性与陈述精确性。