结果族 243：Separating choiceless counting from polynomial time and witnessed choice · 学科：Mathematical logic · 验证状态：暂无形式化证明，请以社区核验为准
还是那位公正裁判：他现在获准一项受严格约束的新权力——在真正别无差别时”整批挑一份代表”，但必须当场出示证明（一个保住全部历史记录的对称变换）表明这次挑选不破坏公正。这份新权力到底有没有实打实的用处？本文证明：有，而且严格有——他能断以前断不了的案子。
关键词卡片
看个具体例子
考题仍是姊妹篇那族”带电网格”上的模 3 方程组相容性查询。一个只出现一次 WSC 算子的固定句子，就能在每个有限输入上给出确定的”是/否”且从不中途失败；而任何 CPT 句子（哪怕允许计数与任意复杂的中间对象）都定义不出同样的查询——于是得到严格包含：
为什么值得关心
这肯定回答了 Lichter–Schweitzer 在 2023 年提出的问题，首次把两个系统严格分开；本篇最重的技术部件复用自已形式化的姊妹篇，但结论本身仍待核验。
暂无形式化证明（AI 结果待核验）
第一级台阶
导读里裁判新获的权力可以这样收紧表述：计算仍在对称对象的集合世界里进行，但允许一个特殊动作——从一批完全等价的候选中挑出一个代表，条件是必须当场构造出”搬运”证明：一个保持输入全部关系、又逐点固定此前所有中间记录的对称变换。挑得出证明，选择才算数；挑不出，计算只能失败。
第二级台阶
用本科术语精确化：基础系统 CPT 在以输入元素为原子的遗传有限集上做同构不变的多项式时间计算，允许计数；见证对称选择（WSC）算子则允许在一条轨道上选元素，同时给出稳定参数、保持词汇表并固定先前中间状态的自同构作为见证，失败时返回值 @@M@@\dagger@@。句子的真模型类指其取真的全体结构。
第三级台阶
定理 1.1 断言：存在八个二元关系的词汇表与固定多项式 @@M@@p@@，使一个只含一次 WSC 出现的句子 @@M@@(\Phi,p)@@ 在每个有限输入上都取布尔值（从不失败），且没有任何 CPT 句子——计数与任意有限秩都不受限——与它有相同的真模型类。于是定义能力严格包含。注意边界的诚实性：一次语法出现可在迭代中做多次相继选择；WSC 嵌套与是否捕获全部 P 是明确留开的独立问题。结论肯定回答 Lichter–Schweitzer 2023 年的表达能力问题。
本文证明：在带计数的无选择多项式时间（CPT）之上加入见证对称选择算子（witnessed symmetric choice, WSC）会严格增强表达能力——一个只含一次 WSC 出现的固定句子在所有有限输入上定义了一个布尔查询，却不能被任何 CPT 句子定义，肯定回答了 Lichter–Schweitzer 提出的表达能力问题。
许多多项式时间算法在中间步骤做任意选择而不影响最终答案，典型如高斯消元可以选不同的主元来判定同一个方程组的相容性。但在无序有限结构上，一个答案须同构不变的计算如何合法地做”中间选择”，是描述复杂性的老难题。Dawar–Richerby 曾为不动点逻辑发展对称选择；Lichter 与 Schweitzer 在 2023 年把见证对称 choice 引入遗传有限集模型：从轨道中选取元素时，必须同时构造保持整个输入词汇、稳定参数与全部先前中间状态的自同构来证明这次选择的合法性，否则计算失败（记为 @@M@@\dagger@@）。他们在该文第 7 节明确提出：WSC 扩展是否严格强于带计数的 CPT？此前只有条件性结果（其定理 1 把可定义的同构测试转化为规范化），严格分离一直悬而未决。
定理 1.1 断言：存在一个含八个二元关系的词汇表 @@M@@\tau@@、一个固定多项式 @@M@@p@@，以及一个只含一次 WSC 算子出现的 @@M@@\mathrm{CPT}+\mathrm{WSC}@@ 句子 @@M@@(\Phi,p)@@，使得 (i) 它在每个有限 @@M@@\tau@@-结构上都取布尔值，从不返回失败值 @@M@@\dagger@@；(ii) 没有任何 @@M@@\mathrm{CPT}@@ 句子——即使允许计数操作 @@M@@\Card@@ 与任意有限秩的遗传有限集（hereditarily finite sets）——与它有相同的真模型类。由于每个 CPT 句子本来就是 CPT+WSC 句子，这给出严格包含 @@M@@\operatorname{Def}_{\mathrm{CPT}}(\tau)\subsetneq\operatorname{Def}_{\mathrm{CPT}+\mathrm{WSC}}(\tau)@@。一次 WSC 的语法出现可在迭代与不同参数处做许多次相继选择，故结果对完整形式化的”真包含”成立；WSC 算子的嵌套与捕获全部多项式时间查询是另外的独立问题。
正方向在姊妹篇的带电三维盒网格结构 @@M@@A_{b^0},A_{b^1}@@ 上构造句子 @@M@@\Phi@@，分三段。先”定序取树”：用四个顶点块组成的可解元组（resolving tuple）@@M@@\alpha@@——其距离向量 @@M@@v\mapsto(d(a_1,v),\dots,d(a_4,v))@@ 在盒上单射——对块图给出字典序，并取定生成树 @@M@@T@@。再用 WSC 迭代选择：每次在 @@M@@T@@ 之外最小的未处理边上按字典序选一个边原子，要求与已选原子在共享面上匹配（论文证明该匹配恰检测面向量坐标相等）。合法性由传递性命题保证：把候选 @@M@@s@@ 送到 @@M@@s'@@ 的映射由两步复合而成——先作用在至多四个面上的平移对齐向量坐标（它只移动至多固定常数 @@M@@B@@ 个原子，且在已有选择的面上为零，故逐点固定全部历史选择），再沿新边与树返回路径构成的简单圈施加标量环流，修正残余的标量差；此圈不含任何已选非树边，故不扰动先前选择。两类映射都经过显式过滤器检查：是整个输入的自同构、固定所有块、逐个固定已选原子。守卫失败时句子退化为”纯哑选择”，从而在任意（非盒）输入上也是合法的 CPT+WSC 句子。最后用树上的单调删除迭代检验选定能否扩展为相容构形（configuration）：零电荷结构 @@M@@A_{b^0}@@ 总能通过（面向量逐面延拓，树上发散方程有唯一解），单位电荷结构 @@M@@A_{b^1}@@ 总失败（逐顶点求和迫使总电荷为零）。于是 @@M@@\Phi@@ 在两结构上答案相反。
反方向证明任何固定 CPT 句子 @@M@@\psi@@ 在充分大的结构对上答案相同。先证明 @@M@@\psi@@ 的完整实际求值轨迹——包括被资源界限拒绝的候选——构成大小至多 @@M@@N^q@@、自同构不变、成员传递的家族；由姊妹篇的秩无关支撑定理，它整体落入短支撑对象组成的域 @@M@@D_{L,i}^{(s)}@@，且不设秩上限。再对 @@M@@\psi@@ 的每个语法出现构造”图公式”@@M@@G_t@@，归纳证明：只要参数来自实际激活，@@M@@G_t@@ 不仅在真实值处为真，还在整个域上唯一确定输出——这一全域唯一性防止任意高秩对象伪造迭代不动点或篡改空集默认值，是直接比较 CPT 项（而非姊妹篇所用的解释程序刻画）的关键。公式长度可随输入增长，但变量名个数 @@M@@m@@ 只依赖 @@M@@\psi@@。最后，计数等价与转移定理（复用姊妹篇）给出两个支撑域在 @@M@@C^m@@ 上的等价，同一公式 @@M@@\widehat\psi_N@@ 刻画两侧求值，故真值必相等，与 @@M@@\Phi@@ 的相反答案矛盾。定理 1.1 的严格包含由此得证。
本篇暂无形式化证明，但最重的部件——秩无关支撑界、基计数等价与支撑域转移定理——直接复用姊妹篇《Choiceless polynomial time with counting does not capture polynomial time》，而姊妹篇主结果已 Lean 形式化。本篇的独立新贡献是合法的见证选择句子定义与任意 CPT 项的直接比较。按 OpenAI 官方声明，未经形式化的结果可能有问题，本篇结论宜以社区核验为准。
问 1：证明中最关键、最脆弱的一步是什么？
答：见证选择句子的合法性，即传递性命题：把候选 @@M@@s@@ 送到 @@M@@s'@@ 的映射须由”至多四个面上的平移对齐向量坐标”与”沿新边加树返回路径的标量环流”复合而成，且逐点固定全部已选原子与历史状态。若任何一个组合漏掉已选非树边上的扰动，合法性检查（显式过滤器）就会失败，句子的定义垮掉。
问 2：见证为什么必须固定”全部先前中间状态”，松一点行不行？
答：松了 WSC 就不再是受约束的选择。固定历史正是 Lichter–Schweitzer 形式化的核心约束：它保证选择虽逐次进行、整体仍对称。本文能分析该算子，恰恰因为见证的自同构被压到如此窄的通道里；放松约束会让表达能力失控，下界论证也无从下手。
问 3：与已有工作相比真正的新意是什么？
答：Lichter–Schweitzer 2023 年提出问题但只有条件性结果（其定理 1 把可定义同构测试转化为规范化）；本文给出首个严格分离。且反方向不走姊妹篇的解释程序刻画，而是对任意 CPT 项做直接比较——图公式在整个支撑域上唯一确定输出，防住高秩对象伪造不动点。
问 4：证明重度复用姊妹篇的部件，这是隐患吗？
答：是双刃剑。秩无关支撑估计、基计数等价与转移定理（姊妹篇命题 8、11、13 与定理 14）已在 Lean 形式化范围内，可靠性高；但本篇自身的图公式归纳与见证句子构造未形式化，一旦其中”全域唯一性”归纳有缺口，分离结论直接失效——这是本文最大的待验点。
问 5：定理只允许一次 WSC 出现，这算不算打了折扣？
答：不算实质折扣：一次语法出现可在迭代与不同参数处执行任意多次相继选择，故结果对完整形式化的真包含成立。真正的边界在别处——嵌套 WSC 算子的表达效应与 CPT+WSC 是否捕获全部多项式时间查询，论文明确声明是独立问题、本文未触及。
问 6：最可能出错的 AI 生成模式是什么？
答：这类证明的典型风险是”守卫退化”细节：论文声称守卫失败时句子退化为纯哑选择、从而在任意非盒输入上仍合法——覆盖所有病态输入的责任全在这类分情况记账上。此外宽度/资源界的多项式指数余量也靠手工核算，未形式化部分尤需社区复核。
问 7：谁会用这个结果？
答：描述复杂性社区直接受益：WSC 是”有序化中间选择能否对称化”这条路线的关键算子，严格分离确认它有真实代价与真实收益，为下一步研究嵌套 WSC、以及沿 Gurevich 猜想方向排除候选逻辑提供了校准点。
总评
这是 Lichter–Schweitzer 问题的首个无条件严格分离，借力已形式化的姊妹篇使重部件可信；最大风险在本文独有的见证句子合法性与图公式全域唯一性归纳——恰好是尚未形式化的部分。