长度为 9 时的精确最优值 10 · 2 · 846

目标函数

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

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

这是所有五行 9 长码本的全局最小值。

达到最优值的构型

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

000212332
020030132
022010310
002232110
010101210

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

数量之和为 210，能量之和为 846，只有两个相关值达到 10。本站验证器用精确高斯整数独立重算了全部相关值，从而给出最优值的上界。

下界搜索

把某一行整体乘以一个单位相位，只会将该行参与的相关值同步旋转而不改变模长，因此不妨设每行首项相位均为 0，候选行共有 4⁸ = 65,536 条。一个码本的全部计分相关值都不超过阈值 B，当且仅当五条候选行在「两行的十七个互相关均不超过 B」所定义的图上构成五顶点团。这就把问题归结为 65,536 顶点图上的带权五团搜索。

三次穷举搜索排除了所有字典序更小的三元组：

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

四次搜索（第一项运行了两遍，其中一遍关闭了最强的对称性约简）在合计 58 亿次配对检查后全部返回 INFEASIBLE。每一步剪枝都用未选行仍需贡献的下界来比较，不会漏掉任何可行码本。

核验范围

这是一个可复现的计算机辅助证明，并非 LRAT 或 VeriPB 证书，也未经证明助手形式化。由于两段带权下界搜索共用同一份 JavaScript 核心，重跑主要检验确定性与完整性，而非提供第二套独立实现。

计分部分则经过独立核验：证明包自带的精确计分器与本站验证器分别计算了上述构型，得到的 210 个相关值、分布表及总分 10 · 2 · 846 完全一致。