结果族 243：Separating choiceless counting from polynomial time and witnessed choice · 学科：Mathematical logic · 验证状态：主结果已 Lean 形式化
想象一位极度公正的裁判，面前是一袋没有编号、完全对称的球。他拒绝”随手抓一颗”这类动作，只允许整批地、对称地处理。这种”不做任意选择”的计算模型（CPT，还配上数数功能）到底能不能断完所有多项式时间可断的案子？本文给出否定答案：确有一件 P 里的案子，他永远断不了。
关键词卡片
看个具体例子
具体输入是”带电的三维网格”：每个顶点带电荷，要判断对应的 @@M@@\mathbb F_3@@ 线性方程组是否相容。高斯消元多项式时间就能判（属于 P），但任何 CPT 程序都写不出这个判断——对两个总电荷不同的网格，正确答案一是一、一是零，而任何固定的对称程序在两者上被迫给出相同输出。
为什么值得关心
这确认了 Blass–Gurevich–Shelah 在 1999 年提出的非捕获猜想，朝着”无序结构上的 P 无法被任何逻辑捕获”这一著名猜想迈出实质一步。
已 Lean 形式化
第一级台阶
导读里那位拒绝”随手抓一颗球”的公正裁判，对应这样的计算观：输入是一堆没有编号、完全对称的对象，计算过程只能在由它们出发搭建的集合上整批进行，且一切操作都必须与输入的任意重排相容。要问的是：这种”不做任意选择”的多项式时间计算，配上数数能力，能否断完所有高效可断的性质？
第二级台阶
用本科术语精确化：无选择多项式时间（CPT）在以输入元素为原子的遗传有限集上运算，允许集合运算、概括与基数算子 @@M@@\mathsf{Card}@@，每个固定程序带多项式资源界；查询指同构不变的布尔性质。一个形式化”捕获 P”，指它能定义每个固定词汇表上全部多项式时间可判定的查询。
第三级台阶
定理 1 在含八个二元关系符号的固定词汇表上定义查询 @@M@@Q@@：由关联关系读出一个 @@M@@\mathbb F_3@@ 线性方程组，问其是否相容。同构不变性与多项式可判性（高斯消元）都直接；关键断言是 @@M@@Q@@ 不可被完整带计数的 CPT 定义——不设集合秩上限。证明靠一对大小相同、总电荷不同的网格结构：查询在两结构上答案相反，而任何固定 CPT 程序被迫在两结构上输出相同。这确认了 Blass–Gurevich–Shelah 1999 年的非捕获猜想。
本文证明了带计数的无选择多项式时间（choiceless polynomial time with counting, CPT）不能捕获无序有限结构上的多项式时间：在 @@M@@\mathbb F_3@@ 上的一个线性方程组相容性查询属于 P，却无法被 CPT 定义，从而确认了 Blass–Gurevich–Shelah 近三十年前提出的非捕获猜想。
描述复杂性（descriptive complexity）的核心问题之一是：哪种逻辑能表达全部多项式时间可判定的性质？Immerman–Vardi 定理（1982）给出有序情形的完满答案——最小不动点逻辑恰好捕获有序结构上的 P。但数据库等场景中的输入是无序结构（unordered structures），Gurevich 在 1988 年猜想不存在捕获无序 P 的逻辑。Blass、Gurevich、Shelah 于 1999 年提出 CPT：在由输入元素生成的遗传有限集（hereditarily finite sets）上对称地计算，所有运算与输入自同构交换，从而不做任意选择；他们猜想即使加上计数操作 @@M@@\mathsf{Card}@@，该形式化仍是 P 的真片段。此前所有下界都卡在限制条件上：Dawar–Richerby–Rossman 的著名结果表明集合秩限制在 @@M@@o(\log n/\log\log n)@@ 时计数也不够，但秩固定的下界无法直接推出对允许任意有限秩的完整形式化的分离；Rossman 与 Pago 的结果则是功能性障碍而非布尔查询的不可定义性。
论文固定一个含八个二元关系符号的词汇表 @@M@@\tau=\{\mathsf{Ed},\mathsf{Cf},\mathsf{EB},\mathsf{VB},\mathsf I,\mathsf Z_0,\mathsf Z_1,\mathsf Z_2\}@@，定义查询 @@M@@Q@@ 如下：由 @@M@@\mathsf{Ed},\mathsf{Cf}@@ 区分边原子集 @@M@@Y@@ 与构形原子集 @@M@@X@@，由 @@M@@\mathsf{VB}@@ 分块；对每块引入归一化方程 @@M@@\sum_{a\in X_t}\lambda_a=1@@，并通过关联测试对满足条件的对 @@M@@(t,y)@@ 引入相容方程 @@M@@\mu_y=\sum_{a\in X_t}\lambda_a C(y,a)@@，其中系数 @@M@@C(y,a)@@ 由关系 @@M@@\mathsf Z_\delta@@ 直接给出。@@M@@Q(A)@@ 定义为该线性方程组（linear system）在 @@M@@\mathbb F_3@@ 上是否相容。定理 1 断言：@@M@@Q@@ 是同构不变的、确定性多项式时间可判定的（高斯消元即可），但不可被完整带计数的 CPT 定义。推论还指出 @@M@@Q@@ 在线性代数逻辑 @@M@@\mathrm{FPS}_3@@ 与 @@M@@\mathrm{FPR}_3@@（FPC 加上 @@M@@\mathbb F_3@@ 上的可解性算子/秩算子）中可定义，因此这两个逻辑都不包含于 CPT。
先构造答案相反的结构对。以边长 @@M@@L@@ 的三维盒网格为基础，每条边挂一个 Heisenberg 型有限群（finite Heisenberg group），其元素成为边原子；每个顶点处满足共享面坐标条件与发散方程 @@M@@\sum_{e\ni v}\epsilon_{ve}z_e=b_v@@ 的相邻边状态组成为构形原子。取电荷向量 @@M@@b^0=0@@ 与 @@M@@b^1=\mathbf 1_{v_*}@@，得到大小同为 @@M@@N=\Theta(L^3)@@ 的结构 @@M@@A_{b^0},A_{b^1}@@。把查询方程逐顶点加权求和，每条有向边一进一出而相互抵消，于是相容性迫使总电荷 @@M@@\sum_v b_v=0@@；全零构形给出 @@M@@A_{b^0}@@ 的解，故 @@M@@Q@@ 在两结构上答案相反。关键在于该求和论证允许任意域值权重，不要求解”选出”每顶点唯一构形。
再证任何固定 CPT 程序在两结构上答案相同，分三步。第一步是秩无关的支撑定理（support theorem）：结构的自同构群 @@M@@H@@ 是面平移与其交换子生成的中心流的非交换中心扩张，含中心子群 @@M@@K=\ker\partial@@（无发散边流）。利用交错形式（alternating form）的秩论证与稀疏上链引理——减去显式构造的梯度，把检测稳定子的线性泛函集中到至多 @@M@@2Lt@@ 条边上——证明凡 @@M@@H@@-轨道大小至多 @@M@@N^q@@ 的遗传有限对象都有长度 @@M@@O_q(L(1+\log L)^2)@@ 的 @@M@@K@@-支撑，且界与对象的秩无关；这正是绕过以往秩限制下界的关键，非交换群的作用在此本质，仅有中心流不够。第二步是计数等价：仅作分析之用，给两结构附加区分原子类与比较标量差的扩张关系，证明两个扩张在至多 @@M@@M=\lfloor L^{7/4}\rfloor@@ 个变量名的一阶计数句子上不可区分；再对”自身及每个递归成员都有长度 @@M@@\le s@@ 支撑”的全体对象组成的域，沿用 BGS 的分子表示法（以在支撑元组处求值的有限形式表示对象）证明等式、隶属与精确计数均可转移，宽度代价 @@M@@O_{q,m}(L^{3/2}(1+\log L)^3)=o(M)@@。第三步把整个计算纳入比较：借助 Grohe–Schweitzer–Wiebking 的解释程序刻画（interpretation characterization），把程序完整运行轨迹用带序数标签的 Kuratowski 编码打包为 @@M@@H@@-不变、成员传递、大小至多 @@M@@9B^3\le N^q@@ 的族，从而整体落入被比较的支撑域，且不设秩上限；再由避免捕获的替换引理证明每个状态、停机测试与输出测试都有精确的计数公式定义，所需变量名个数 @@M@@m@@ 只依赖程序本身。先固定程序与 @@M@@q,m@@，再取 @@M@@L@@ 充分大：计数等价迫使两侧同阶段停机、输出相同，与查询答案相反矛盾。
本篇主结果已由 OpenAI 完成 Lean 形式化验证（族文档 lean/docs/243.md）。姊妹篇证明加入见证对称选择后表达能力严格增强，两文共享同一套网格构造与支撑—转移架构，互为印证。另需注意 OpenAI 官方声明：未经形式化的结果可能存在问题，故同族未形式化的姊妹篇宜以社区核验为准。
问 1：证明中最关键、最脆弱的一步是什么？
答：秩无关的支撑定理（第 3 节）。它断言凡 @@M@@H@@-轨道大小至多 @@M@@N^q@@ 的遗传有限对象都有长度 @@M@@O_q(L(1+\log L)^2)@@ 的 @@M@@K@@-支撑，界与对象秩无关——这正是绕开 Dawar–Richerby–Rossman 秩限制下界的关键。交错形式的秩论证与”减梯度集中泛函”若在任何一处失守，整个比较域就容纳不下高秩对象，分离失效。
问 2：为什么自同构群必须是非交换的，中心流不够吗？
答：不够。证明的杠杆是交换子：它迫使检测稳定子的线性泛函在少数面上有非零旋度，再减去显式构造的梯度把泛函集中到至多 @@M@@2Lt@@ 条边上。仅有中心流（无发散边流 @@M@@K=\ker\partial@@）提供不了这个论证——非交换性正是支撑界成立的引擎。
问 3：分离查询为什么选模 3 线性相容性，而不是别的 P 性质？
答：因为电荷机制干净：对查询方程逐顶点加权求和，每条有向边一进一出相互抵消，相容性迫使总电荷为零；该论证允许任意域值权重，不要求解”每顶点选出唯一构形”。于是总电荷 0 与 1 的两个同尺寸结构答案必然相反，而构造又能让两者各自可解/不可解。
问 4：与既有下界相比真正的新意是什么？
答：Dawar–Richerby–Rossman 只对秩 @@M@@o(\log n/\log\log n)@@ 的变体有效，Rossman–Pago 是功能性障碍；本文首次对不设秩上限的完整带计数形式化给出布尔查询的不可定义性，确认 BGS 非捕获猜想的原始形式。
问 5：这类组合论证最可能出错的模式是什么？
答：最危险的是宽度账本：一阶计数等价用 @@M@@M=\lfloor L^{7/4}\rfloor@@ 个变量名，转移论证的宽度代价 @@M@@O_{q,m}(L^{3/2}(1+\log L)^3)@@ 须为 @@M@@o(M)@@——指数余量紧（@@M@@7/4@@ 对 @@M@@3/2@@），任何一处多出一个 @@M@@L^{1/4}@@ 量级的因子就翻车。程序轨迹打包成大小 @@M@@\le 9B^3\le N^q@@ 的族的界同样紧。主结果已 Lean 形式化，是关键背书。
问 6：下游推论是什么、谁会用？
答：推论 3：@@M@@Q@@ 在线性代数逻辑 @@M@@\mathrm{FPS}_3@@ 与 @@M@@\mathrm{FPR}_3@@ 中可定义，故这两个逻辑都不包含于 CPT——FPC 谱系的包含关系图被改写。对描述复杂性社区，这是朝 Gurevich”无逻辑捕获无序 P”总猜想迈出的实质一步；姊妹篇再用同一构造分离见证对称选择。
总评
这是悬置近三十年的 BGS 非捕获猜想的完整确认，且有 Lean 形式化背书，分量很重；最大风险在支撑定理的非交换群论证与宽度指数余量的紧度，形式化覆盖与否值得核对。