结果族 242：Single-fold Diophantine representations and undecidability under an at-most-one-solution promise · 学科：Mathematical logic · 验证状态：主结果已 Lean 形式化
有些判断问题可以写成一道多项式方程题：输入属于该问题，当且仅当方程有自然数解。经典 DPRM 定理早就保证这总能做到，但解可能有无穷多组——像一本字典里同一个词条散落在许多页。本文证明：字典总能重新排版，让每个词条恰好只出现在一页上。
关键词卡片
看个具体例子
先看玩具版：偶数集可写成 @@M@@a=2w@@——@@M@@a=6@@ 时恰有唯一见证 @@M@@w=3@@，@@M@@a=7@@ 时无解。主定理说这种”唯一编码”对每个递归可枚举集都能做到：存在多项式 @@M@@P@@ 使
@@M@@D\#\{w\in\mathbb{N}^m:\;P(a,w)=0\}=\begin{cases}1,&a\in S,\\0,&a\notin S.\end{cases}@@
即使复杂如停机问题的成员表也不例外。推论更出人意料：就算承诺输入多项式”至多一个解”，判定它有没有解仍然没有算法。
为什么值得关心
这解决了 Matiyasevich 1974 年提出的单重猜想，一个悬置半个世纪的问题；更弱的有限重猜想也随之成立。这也是希尔伯特第十问题自 DPRM 定理以来最引人注目的续章之一。
已 Lean 形式化
第一级台阶
导读把经典表示比作”同一词条散落在字典许多页”：一道多项式方程判 membership，但同一个成员可能被无穷多组解反复见证。主定理说这本字典总能重排——每个词条恰好落在一页上。翻译成半数学语言：对象是”能被机械过程逐步列举成员”的集合，刻画手段是一个整系数多项式方程；方程的每一组解就是成员资格的一个见证。
第二级台阶
用本科术语精确化：递归可枚举集 @@M@@S\subseteq\NN^n@@ 指某台确定型机器恰好接受其成员；@@M@@S@@ 有 Diophantine 表示，即存在整系数多项式 @@M@@P(A,W)@@ 使 @@M@@a\in S\iff P(a,w)=0@@ 有自然数解 @@M@@w@@（见证）。所谓单重（single-fold），是对每个 @@M@@a@@ 见证元组恰有一个（成员）或零个（非成员），且计数包含表达中间运算的全部辅助变量。
第三级台阶
定理 1.1 断言：每个递归可枚举集都有单重多项式表示，解决 Matiyasevich 1974 年的单重猜想。证明的关口在纯多项式截断：经典路线用 Pell 方程恢复幂，但”挑出目标解”的截断条件自身要用指数，循环依赖。本文以秩一椭圆曲线 @@M@@y^2=x^3-25x@@ 的 Néron–Tate 高度（误差一致有界的二次增长）造出介于幂函数与 @@M@@u^u@@ 之间的单重函数，解开死结。注意定理是纯存在性：常数被固定但未给数值；推论还给出”至多一解承诺”下可解性仍不可判定。
论文证明了悬置半个多世纪的单重猜想（single-fold conjecture）：每个递归可枚举集都有多项式 Diophantine 表示，其中每个成员恰对应一个辅助见证元组、非成员对应零个。由此有限重猜想（finite-fold conjecture）成立，且即使承诺”至多一个解”，多项式可解性依然不可判定。
称集合 @@M@@S\subseteq\NN^n@@ 有 Diophantine 表示（Diophantine representation），若存在整系数多项式 @@M@@P@@，使 @@M@@a\in S@@ 当且仅当 @@M@@P(a,w)=0@@ 有自然数解 @@M@@w@@（这样的 @@M@@w@@ 称为见证，witness）。DPRM 定理（Davis–Putnam–Robinson 1961；Matiyasevich 1970）断言每个递归可枚举集（recursively enumerable set）都有这种表示，从而给出希尔伯特第十问题（Hilbert’s tenth problem）的否定解答，但它完全不控制见证的个数：同一成员可能对应无穷多组解。Matiyasevich 在 1974 年证明允许指数运算的表示可以做到见证唯一，并据此提出多项式版的单重猜想，还把它归约到”二元指数函数本身有单重表示”这一步；允许有限多组见证的弱化版本是有限重猜想。此后的症结在于：经典路线靠 Pell 方程的解序列恢复指数，但需要一个纯多项式的”截断”机制来唯一挑出目标解，而截断条件通常又要用到指数函数，形成循环依赖。
主定理：对每个 @@M@@n\ge1@@ 与每个递归可枚举集 @@M@@S\subseteq\NN^n@@，存在 @@M@@m\ge1@@ 及多项式 @@M@@P\in\ZZ[A_1,\ldots,A_n,W_1,\ldots,W_m]@@，使得对一切输入 @@M@@a\in\NN^n@@，
@@M@@D\#\{w\in\NN^m:P(a,w)=0\}=\begin{cases}1,&a\in S,\\ 0,&a\notin S.\end{cases}@@
唯一性计入全部辅助变量，包括表达中间算术运算的变量。需注意这是纯存在性定理：证明固定了一批有理点等常数，但既不给出数值，也不提供数值选取它们的程序。推论（带至多一解承诺的不可判定性）：存在固定的变量个数 @@M@@m@@ 与总次数上界 @@M@@D@@，使得任何算法都无法在”输入多项式在 @@M@@\NN^m@@ 上至多一个零点”的承诺（promise）下判定可解性——证明取非递归 r.e. 集的单重表示多项式并按输入特化系数 @@M@@F_a=P(a,\cdot)@@，每个 @@M@@F_a@@ 都满足承诺，判定可解性即判定该集，矛盾。
全文策略是”先造唯一的算术见证，再给接受计算唯一的编码”，三大块接力完成。
第一块用秩一椭圆曲线（elliptic curve）@@M@@E:y^2=x^3-25x@@ 造一个增长速度适中的单重函数。其有理点群 @@M@@E(\QQ)\cong\ZZ P\oplus\mathcal T@@ 秩为一、挠群四元（附录用二同源下降证明）；有理数与点的加减都有唯一的多项式编码。核心工具是 Néron–Tate 典范高度（canonical height）：点列高度满足 @@M@@\log W_j=a_Ej^2+O(1)@@ 且误差一致有界，固定标量乘还能放大二次系数 @@M@@a_E@@ 而误差界不变。先按”陪集中 @@M@@x@@ 坐标最大且 @@M@@y\ge0@@“把每个正绝对指标 @@M@@j@@ 的点唯一选出，再施展关键一招——离散差分消去二次主项：乘积比 @@M@@\log\frac{W_{2k}W_rW_1}{W_k^2W_{r+1}}=2a_E(k^2-r)+O(1)@@，误差与两个指标无关。于是固定窗口 @@M@@\kappa@@ 后，比值落入窗口当且仅当 @@M@@r=k^2@@：整数分离把 @@M@@O(1)@@ 的误差变成精确的指标选择。对输入 @@M@@u@@，先用括号 @@M@@W_k\le u+W_1<W_{k+1}@@ 定出 @@M@@k@@，再以窗口选出指标 @@M@@k^2@@ 的点，令 @@M@@g(u)=W_{k^2}@@：它有单重图，且 @@M@@\delta(\log u)^2<\log g(u)<u\log u@@——比任何幂函数快、比 @@M@@u^u@@ 慢。
第二块从 @@M@@g@@ 提取幂运算，解开经典循环。两条 Pell 方程（Pell equation）@@M@@X^2-((bu)^2-1)F^2=1@@ 与 @@M@@Y^2-(u^2-1)H^2=1@@ 的正解各由一个指标唯一决定；上界 @@M@@g(u)<u^u<(2u-1)^{u-1}@@ 迫使两指标小于 @@M@@u@@，同余条件便在 @@M@@[1,u-1]@@ 内把它们钉死在 @@M@@n+1@@。Pell 序列的比率估计给出 @@M@@b^n\le F/H\le b^n(1+\frac1{2u-1})^n@@，取 @@M@@u=(c+1)^\ell(n+1)(b+1)+u_0@@ 使整数商的误差小于 1，商便恰为 @@M@@c=b^n@@；下界则保证预期的 Pell 坐标真能通过 @@M@@g(u)@@ 的截断。再用 @@M@@B=2^{y+1}@@、@@M@@N=(B+1)^y@@ 以大底数无进位地提出二项式系数 @@M@@\binom{y}{x}@@，由 Lucas 定理其二进制奇偶恰判定数字包含关系 @@M@@x\bits y@@，全程单重。
第三块编码计算。把确定型计数器机器（counter machine）的整条运行史压进几个整数的二进制位，每个时刻占一块，状态、分支与计数器更新全部写成移位递推方程（Jones–Matiyasevich 位掩码法）。唯一性靠两手：确定性钉死运行内容；时钟终值被压入 @@M@@[B/4,B/2)@@，而区间 @@M@@(2L,4L]@@ 恰含一个 2 的幂，故进制基 @@M@@B@@ 唯一——若块大小自由，同一条运行会有多种编码。解码方向用”绝对值小于 @@M@@B@@ 的系数和为零则逐项为零”排除进位与借位。最后按第 2 节的约定（选择子 @@M@@e_i(e_i-1)=0@@、非活跃分支的局部变量一律清零、不等式余量唯一）逐层展开所有调用，把方程组合并为单个多项式 @@M@@P=\sum F_i^2@@，完成主定理。
本篇任务元数据标记主结果已获 Lean 形式化证明；本批族 242 仅此一篇手稿，族描述（单重表示蕴含有限重猜想与承诺版不可判定性）与本文摘要一致，推论正是同一多项式的直接特化。论文自身声明多项式系数与算术常数只证存在、未给数值，附录含秩计算与完整见证清点。按 OpenAI 官方声明，未经形式化的结果可能有问题；本文主结果已形式化，其余技术细节建议以社区核验与论文原文为准。
问 1：证明中最关键、最脆弱的一步是什么？
答：椭圆曲线截断的离散差分恒等式 @@M@@\log\frac{W_{2k}W_rW_1}{W_k^2W_{r+1}}=2a_E(k^2-r)+O(1)@@。误差须与 @@M@@k,r@@ 双双无关，且 @@M@@a_E@@ 足够大以分离不同整数值，固定乘法窗口才能精确选出指标 @@M@@r=k^2@@。误差界来自 Néron–Tate 高度的性质，一旦失去一致性，整个指标选择机制崩塌。
问 2：为什么必须引入椭圆曲线，Pell 方程老路走不通吗？
答：走不通的症结是循环依赖：经典配对 Pell 表示需要指数式截断来唯一挑出目标解，而”截断”本身要用指数函数。曲线 @@M@@y^2=x^3-25x@@ 提供的增长带 @@M@@\delta(\log u)^2<\log g(u)<u\log u@@ 全程单重：上界把 Pell 指标压到模以下、由同余钉死，下界保证预期解真被 @@M@@g(u)@@ 放行。
问 3：单重性”计入全部辅助变量”这条约定能松掉吗？
答：不能。引理 2.2 的组合与分情况规则要求非活跃分支的局部变量一律清零（@@M@@(1-e_i)z=0@@）、不等式余量唯一。若允许未规定的 Bézout 系数或非活跃变量自由取值，”唯一见证”立即变成空话。这是全文最容易被读者低估的记账负担，附录专门列出见证清单。
问 4：与已有工作相比真正的新意是什么？
答：Matiyasevich 1974 年已得指数版单重并把多项式版归约到二元指数的单重表示，缺的正是纯多项式截断；本文用秩一曲线补上这块，五十年缺口闭合。与 Miller–Shlapentokh 的有理整数单重定义（见证域在多项式环）目标不同；Chaitin 的基选取思想被改造成时钟加二进区间来唯一确定编码基 @@M@@B@@。
问 5：这种证明最可能出错的模式是什么？
答：典型风险在”唯一性记账”的完备性：层层替换、嵌套调用中漏掉一个未清零的辅助变量或一个非唯一余量，主定理就会在审查细节时失效。其次，算术常数只证存在、未给数值（如曲线上的有理点选取），无法用机器直接抽查。主结果据称已 Lean 形式化，是重要背书。
问 6：下游能推出什么、谁会关心？
答：推论给出带承诺的不可判定性：存在固定的变量个数 @@M@@m@@ 与次数界 @@M@@D@@，即使承诺输入多项式至多一个零点，可解性仍不可判定——这对研究 H10 变体与承诺问题归约的人是直接素材。有限重猜想随之成立。
总评
单重猜想的解决是希尔伯特第十问题谱系里分量极重的续章，技术构思（高度差分做截断）堪称漂亮；最大风险集中在多层组合下唯一性记账的完备性与未数值化常数的存在性论证上。