长度为 9 时，10 · 2 · 846 就是尽头

在最小化什么

五条长度为 9、字母表为四个相位 1、i、−1、−i 的序列，按 210 个相关值计分：每一行的八个非零自相关错位，以及十个行对各自的十七个互相关。记 q 为一个相关值的模平方，依次最小化峰值 P = max q、达到峰值的个数 C、以及总和 T = Σq。

(P, C, T) = (10, 2, 846)

这是全局最优值，不是「目前找到的最好」。

达到它的构型

数字表示相位：p 代表 i 的 p 次幂。

000212332
020030132
022010310
002232110
010101210

它的 210 个相关值，按模平方分布：

数量之和为 210，能量之和为 846，只有两个相关值达到 10。本站的验证器用精确高斯整数把这些全部重算一遍——这也是上界可核对而非仅凭断言的原因。

为什么不存在更低的

把一行整体乘以一个单位相位，只会把涉及该行的相关值同步旋转，模不变，所以每行都可以取首符号为 0——候选行因此只有 4⁸ = 65,536 条。一个码本的全部计分相关值都不超过阈值 B，当且仅当五条候选行在「两行的十七个互相关都不超过 B」这张图里构成一个五顶点团。于是问题变成一次带权五团搜索，而这张图小到装得下。

接着由三次穷举搜索排除所有字典序更小的可能，三者合起来覆盖了全部情形：

• 不存在所有计分 q 都 ≤ 9 的码本；
• 峰值为 10 时，不存在只达到一次的码本；
• 峰值为 10 且恰好达到两次时，不存在总能量 ≤ 845 的码本。

四次搜索——第一项跑了两遍，其中一遍不使用最强的那条对称性约简——全部返回 INFEASIBLE，合计 58 亿次配对检查。它们用到的每条剪枝都是拿当前值加上「未选行还能贡献的下界」来比较，所以任何可能满足限制的码本都不会被丢掉。

这属于哪一类证明

一个可复现的计算机辅助证明，仅此而已。它不是 LRAT 或 VeriPB 证书，也没有进过证明助手；两段带权下界搜索共用同一份 JavaScript 核心，所以重跑它们检验的是确定性与完整性，而不是提供一份独立的第二实现。

独立的那一半是计分。证明包自带一份精确计分器，本站另有一份，两者都在上面这个构型上跑过：210 个相关值、同一张分布表、同样的 10 · 2 · 846。全部搜索都建立在这套算术之上，而它的两份互不相干的实现结论一致。