结果族 179：The circulant Hadamard and Barker-sequence conjectures · 学科：Combinatorics · 验证状态：主结果已 Lean 形式化
一支仪仗队方阵，每人举 +1 或 −1 的牌子，要求任意两行牌子”对齐一半、错开一半”（数学上叫正交）。如果每一行都只是第一行整体向右挪一格（循环移位），这种方阵能有多大？答案悬置了六十多年，这篇论文给出终审：只有 1×1 和 4×4 两种，别无分店。此前最强的计算证据已把 4×10³⁰ 以内的候选阶排除到只剩 4489 个，但完整证明始终缺位，本文补上了最后一环。
关键词卡片
@@M@@HH^{\mathsf T}=nI@@。看个具体例子
唯一的非平凡例子是 4 阶：首行 @@M@@(1,1,1,-1)@@，其余各行依次右移一格。下图黑格记 +1、白格记 −1，白格恰好排成一条反对角线；可直接验证 @@M@@P_h(t)=0@@ 对一切 @@M@@1\le t<4@@ 成立：两行正交意味着同号位置恰好占一半，比如错位一格相乘得 @@M@@-1、+1、+1、-1@@，正负相抵总和为零。主定理断言 n=1、4 之外再无可能，并顺带证明 Barker 序列只在长度 2, 3, 4, 5, 7, 11, 13 存在。
为什么值得关心
一篇论文同时终结两个六十余年的名题（循环 Hadamard 猜想与 Barker 序列猜想），且证明经机器核验，含金量极高。
已 Lean 形式化
第一级台阶
导读的仪仗队方阵说：每人举 ±1 牌子，任意两行要对齐一半、错开一半；若每行都只是首行整体右挪一格，这种方阵最多多大？翻译成半数学语言：对象是由一串正负一号生成的移位方阵；操作是让行与行逐位相乘求和——正交即和为零；问题是对哪个阶数，一切非零移位处的乘积和能同时为零。
第二级台阶
用本科代数术语精确化。元素全为 ±1 的 n 阶方阵 H 是 Hadamard 矩阵，若 HH^T = nI；循环性指 H 的第 i 行是首行右移 i 格，由符号 h_0,…,h_{n−1} 决定。周期自相关 P_h(t) 是序列与自身错位 t 的逐位乘积之和；Hadamard 条件恰好等价于 P_h(t)=0 对一切 1 ≤ t < n。把首行看作循环群整数群环 Z[C_n] 中的元素 h，正交性浓缩为范数恒等式 hh* = n。
第三级台阶
定理陈述：实循环 Hadamard 矩阵的阶只能是 1 与 4，猜想归于 Ryser。证明先在素数 2 上下降，得 n = 4u² 且 u 为奇数（Turyn 下降的群环化简写）；再对 u 的素因子集合作交错积 Δ(x)，用 Kronecker 判据证明它是奇数阶单位根；最后在 2 上的极大理想处局部化，符号结构使交错积剩余 1，奇阶逼出恰为 1，一阶展开后公共项相消、只剩一个非零剩余项——矛盾推翻 u > 1。推论顺势完成 Barker 序列长度分类 {2,3,4,5,7,11,13}。
本文证明了循环 Hadamard 矩阵猜想：实循环 Hadamard 矩阵（circulant Hadamard matrix）的阶只能是 @@M@@1@@ 或 @@M@@4@@；并顺势证明 Barker 序列猜想——长度大于 @@M@@1@@ 的 Barker 序列恰在 @@M@@2,3,4,5,7,11,13@@ 七个长度存在，一举终结两个悬置六十余年的组合难题。
Hadamard 矩阵（Hadamard matrix）是元素全为 @@M@@\pm1@@ 且行两两正交的方阵，即满足 @@M@@HH^{\mathsf T}=nI_n@@；若每行都是首行的循环移位，则称为循环 Hadamard 矩阵。这一猜想传统上归于 Ryser（1963 年前后）：这种矩阵的阶只能是 @@M@@1@@ 和 @@M@@4@@。它之所以重要，是因为与循环差集（cyclic difference set）和 Barker 序列（Barker sequence）深刻等价——后者源自雷达与通信理论中理想脉冲压缩序列的设计，而长度大于 @@M@@2@@ 的偶长 Barker 序列经循环移位恰好构成循环 Hadamard 矩阵。此前最强进展包括 Turyn 1965 年的分圆特征和方法（证明大阶必为 @@M@@4u^2@@、@@M@@u@@ 为奇的非素数幂）、Schmidt 的域下降（field descent）与 Leung–Schmidt 的群环分解，以及 Logan–Mossinghoff 2017 年的大规模计算——把 @@M@@4\cdot 10^{30}@@ 以内的候选阶排除到只剩 @@M@@4489@@ 个。完整证明始终缺位，本文补上了最后一环。
主定理：@@M@@n@@ 阶实循环 Hadamard 矩阵存在当且仅当 @@M@@n\in\{1,4\}@@。四阶例子的首行是 @@M@@(1,1,1,-1)@@：记周期自相关（periodic autocorrelation）@@M@@P_h(t)=\sum_{j=0}^{n-1}h_jh_{j+t\bmod n}@@，Hadamard 条件恰等价于 @@M@@P_h(t)=0@@ 对一切 @@M@@1\le t<n@@ 成立，而该行满足此条件。
推论（Barker 序列长度分类）：对 @@M@@n>1@@，Barker 序列——即非平凡非周期自相关（aperiodic autocorrelation）@@M@@C_a(t)=\sum_{j=0}^{n-t-1}a_ja_{j+t}@@ 满足 @@M@@|C_a(t)|\le 1@@ 的 @@M@@\pm1@@ 序列——存在当且仅当 @@M@@n\in\{2,3,4,5,7,11,13\}@@。奇数长度部分是 Turyn–Storer（1961）与 Schmidt–Willms 的经典结论（论文直接引用后者得到精确列表）；偶数长度 @@M@@n>2@@ 时，Barker 不等式经奇偶性论证逼出所有非平凡周期自相关为零，循环移位便构成循环 Hadamard 矩阵，于是被主定理压到 @@M@@n=4@@。
全文按”先压阶数、再造交错积、最后模 @@M@@2@@ 出矛盾”三步推进。
先在素数 @@M@@2@@ 上下降。把首行写成群环（group ring）元素 @@M@@h=\sum_jh_jX^j\in\mathbb{Z}[C_n]@@，正交性等价于范数恒等式 @@M@@hh^*=n@@；增广逼出 @@M@@n=h(1)^2@@ 是平方数，行间内积为零又逼出 @@M@@n@@ 为偶数，故 @@M@@n=2^{2s}u^2@@。要证 @@M@@s=1@@，先把 @@M@@h@@ 投影到 2-准素分量，得到系数全为奇数的 @@M@@T@@，满足 @@M@@TT^*=2^{2s}u^2@@。核心工具是一条分圆可除性引理：在合适的局部化（localization）中，本原 @@M@@2^k@@ 次根处的特征值的赋值（valuation）等价于其分圆余式各系数的公共整除性。据此每做一次”群阶折半、范数除以 @@M@@4@@“的下降，新元素系数仍全为奇数；@@M@@s-1@@ 步后得到 @@M@@2^{s+1}@@ 个奇数系数，其平方和等于 @@M@@4u^2@@。但奇数平方模 @@M@@8@@ 余 @@M@@1@@，@@M@@s\ge2@@ 时个数 @@M@@2^{s+1}@@ 被 @@M@@8@@ 整除，平方和应模 @@M@@8@@ 余 @@M@@0@@，而 @@M@@4u^2@@ 模 @@M@@8@@ 余 @@M@@4@@——矛盾。故 @@M@@n=4u^2@@、@@M@@u@@ 奇，这正是 Turyn 下降的群环化简写。
再构造交错特征积。设 @@M@@u>1@@，@@M@@P=C_{u^2}@@，@@M@@I@@ 为 @@M@@u@@ 的素因子集。对每个 @@M@@p\in I@@ 固定本原 @@M@@p@@ 次单位根 @@M@@\rho_p@@，对子集 @@M@@S\subseteq I@@ 令 @@M@@x_S@@ 为相应特征下的取值，定义交错积 @@M@@\Delta(x)=\prod_Sx_S^{(-1)^{|S|}}@@。范数 @@M@@xx^*=u^2@@ 保证 @@M@@|x_S|=u@@。关键的比较引理（又一场”投影、除以 @@M@@p@@“的归纳下降）表明：因标量 @@M@@u^2@@ 中 @@M@@p@@ 的赋值恰与 @@M@@p@@-分量的阶指数吻合，相邻比值 @@M@@x_{S\cup\{p\}}/x_S@@ 在含 @@M@@p@@ 的每个极大理想（maximal ideal）处是剩余（residue）为 @@M@@1@@ 的单位；按 @@M@@p@@ 方向配对所有因子，便知 @@M@@\Delta(x)@@ 在这些素理想处剩余 @@M@@1@@，在其余素理想处范数保证整性。交错指数总和为零使它在每个复嵌入下绝对值为 @@M@@1@@，由 Kronecker 判据（Kronecker’s criterion）它是单位根（root of unity），而剩余 @@M@@1@@ 又把它的阶逼成 @@M@@p@@ 的幂——总之是奇数阶。
最后模 @@M@@2@@ 出矛盾。分解 @@M@@C_{4u^2}=C_4\times P@@，取三个归一化部分赋值 @@M@@c=\tfrac12h|_{Z=1}@@、@@M@@d=\tfrac12h|_{Z=-1}@@、@@M@@g=\tfrac12h|_{Z=i}@@；共同的符号系数保证 @@M@@c,d@@ 整属于 @@M@@\mathbb{Z}[P]@@、@@M@@g@@ 整属于 @@M@@\mathbb{Z}[i][P]@@，且范数均为 @@M@@u^2@@，故 @@M@@R=\Delta(d)/\Delta(c)@@、@@M@@W=\Delta(g)/\Delta(c)@@ 是奇数阶单位根。在含 @@M@@2@@ 的极大理想处局部化：奇范数使各 @@M@@c_S@@ 为单位，特征 @@M@@2@@ 下 @@M@@i\equiv1@@。符号结构给出差式 @@M@@d-c@@ 含因子 @@M@@2@@、@@M@@g-c@@ 含因子 @@M@@1+i@@（关键恒等式 @@M@@H_2+iH_3=(1+i)J+2U@@，其中 @@M@@J=\sum_{z\in P}z@@），故比值 @@M@@d_S/c_S\in1+2O@@、@@M@@g_S/c_S\in1+(1+i)O@@，剩余均为 @@M@@1@@；奇数阶在剩余特征 @@M@@2@@ 处逼出 @@M@@R=W=1@@。一阶项映射 @@M@@\lambda_t(1+tL)=L\bmod\mathfrak n@@ 把乘法群同态到加法群，对两个等于 @@M@@1@@ 的交错积展开并相加，公共的 @@M@@b_S@@ 项恰好相消，只剩 @@M@@\sum_S(-1)^{|S|}J_S/c_S\equiv0@@。但每个非平凡特征都消灭 @@M@@J_S@@，交错和里仅剩 @@M@@S=\varnothing@@ 一项 @@M@@u^2/c_\varnothing@@——它是个单位，剩余非零，矛盾。故 @@M@@u>1@@ 不可能，猜想得证。
本文主结果已完成 Lean 形式化证明，可信度属于最高档；按 OpenAI 官方声明，未经形式化的结果可能有问题，而主定理与 Barker 推论均在形式化覆盖之内。族内逻辑上，本篇与 Turyn–Storer、Schmidt–Willms 的经典奇长度分类互相拼合，才合成完整的 Barker 长度列表。值得留意的是，作者在引言中明确列出了多份此前声称完整证明该猜想的文献——这一领域的历史教训恰恰凸显了形式化验证的价值。
问 1：证明中最关键的一步是什么？
答：模 2 出矛盾的收官段（contradiction 一节）。把 C_{4u²} 拆成 C_4 × P，取三个归一化部分赋值 c、d、g，交错积之比 R = Δ(d)/Δ(c)、W = Δ(g)/Δ(c) 是奇数阶单位根；在含 2 的极大理想处，符号结构使 d_S/c_S ∈ 1+2O、g_S/c_S ∈ 1+(1+i)O，剩余均为 1，奇阶逼出 R = W = 1。对两者做一阶展开并相加，恒等式 L_{r,S} + L_{w,S} ≡ J_S/c_S 使公共项相消，交错和只剩 S = ∅ 一项 u²/c_∅——它是单位，剩余非零，矛盾。
问 2：为什么阶必须压成 n = 4u²、u 奇？
答：增广与行正交先逼出 n = 2^{2s}u²；2-准素分量的系数全为奇数，每次”群阶折半、范数除 4”的下降保持奇性，s−1 步后得 2^{s+1} 个奇数系数、平方和为 4u²。奇数平方模 8 余 1，s ≥ 2 时个数被 8 整除、平方和应模 8 余 0，而 4u² 模 8 余 4——矛盾。这是 Turyn 1965 分圆方法的群环化简写。
问 3：与 Turyn、Schmidt、Leung–Schmidt 相比真正的新意是什么？
| 答：前人给出越来越强的算术限制（u 非素数幂、域下降、群环分解）与大规模计算（Logan–Mossinghoff 把 4·10³⁰ 以内排除到剩 4489 个候选），但都未封顶。本文的完整证明核心是交错积 Δ(x) = Π x_S^{(−1)^{ | S | }} 机制：比较引理利用”标量 u² 中 p 的赋值恰与 p-分量阶指数吻合”做投影下降，证明 Δ(x) 是奇数阶单位根，再用 C_4 因子的符号结构在特征 2 处引爆矛盾。 |
问 4：这个领域有过多次”完整证明”的声称，本文凭什么可信？
答：引言明确列出多份此前声称证明该猜想的文献（Oh–Hashi、Orozco Lopez、Morris、Gallardo、Manjhi–Kumar 等）——这本身就是警示。本文主定理与 Barker 推论均已 Lean 形式化，属可信度最高档；剩余风险只在形式化陈述与论文定理的逐字对齐，机器已排除”隐蔽引理误用”这类历史失败模式。
问 5：为什么限定实（±1）矩阵？复值情形呢？
答：全部机制依赖符号系数（c、d 的整性、差式含 2 与 1+i 的因子都来自 ±1 结构）。复值循环 Hadamard（Butson 型）在别的阶有大量存在，是另一问题，论文未讨论。
问 6：Barker 推论是自包含的吗？
答：不是。奇数长度部分直接引用 Schmidt–Willms 的精确列表（其源头是 Turyn–Storer 1961），偶长 n > 2 经奇偶性论证化为循环 Hadamard 再由主定理压到 n = 4——推论是”本文主定理 + 经典外部结果”的拼合，论文对此交代得相当清楚。
问 7：谁会关心这个结果？
答：差集与设计理论社区（循环 Hadamard 等价于 (4u², 2u²−u, u²−u) 循环差集）得到不存在性终点；雷达与通信的序列设计拿到 Barker 长度的最终清单；对”猜想陵园”的编史者而言，这是六十余年名题被机器核验证明的标本。
总评
一篇论文终结两个六十余年悬题且经 Lean 形式化，是本批结果中可信度与含金量的双高点；其最大风险已被形式化化解，唯一遗留是形式化陈述与原文的对齐确认。