0. 摘要 ------------------------------------------------------------------------------------- (1) 九个实例共享四条结构律：完全交互图（无解耦）、正则设计（每格关联数恒为 5N-1）、 二平方可达格（z = a^2+b^2, |a|+|b| <= L, |a|+|b| = L mod 2）、尺度不变的纪录位置 (E/T ~ 0.84, M/N ~ 1.4, M/mean ~ 3.2)。 (2) 阻塞分两个层次： n = 13 : 联合定向约束系统【超定】(rho = 4.00, 连续下限 3.53 > 0) n >= 17: 【纯 90 度量化阻塞】(支撑集内连续解存在，联合下限 0.00) (3) n = 73 在四个可测维度上同时最优（自由度/约束 14.7、压线占比 2.4%、粒度 0.119、 前沿格相对间隙 0.069），且历史方法族（束/弹簧/软谱）恰好消耗"自由度 + 细粒度控制"。 (4) 另需诚实计入【预算错配】：n=73 每档耗时 4.5 天 / 15 小时 / 8.5 小时； 本轮小 n 每档仅 20-30 分钟（差 20-100 倍）。 (5) 三分量 (M,C,E) 在 k<=2 半径内【全部无下降方向】：停止在 C/E 上投入。 1. 问题与记号 ------------------------------------------------------------------------------------- 5 行 x N 列，相位取 Z_4（QPSK），规范固定（每行参考相位）。事件： 自相关 (a,a,k), k=1..N-1 共 5(N-1) 个 互相关 (a,b,k), a<b, k=-(N-1)..N-1 共 10(2N-1) 个 事件 e 的项数 L_e = N-|k|，事件值 R_e = sum_t x_a[t+k] * conj(x_b[t]), z_e = |R_e|^2 = a_e^2 + b_e^2 其中 a_e, b_e 为实/虚累积（见 L3）。总事件数 NEV = 25N-15，单元数 5N。 目标：字典序最小化 (M, C, E)，M = max_e z_e, C = #{e: z_e = M}, E = sum_e z_e。 2. 机器验证的结构律 ------------------------------------------------------------------------------------- L1 完全交互（无精确解耦） [LEAN] 项总数 T = 5*sum_{k=1}^{N-1}(N-k) + 10*N^2 = (25N^2-5N)/2 = C(5N,2)，对一切 N<=120 验证。 这是"项 <-> 不同单元无序对"双射的计数影子：任意两个不同单元恰好共现于一个项， 故交互图是 K_{5N} => 任何 N 都不存在精确分区解耦。 （N=73: T = 66430 = C(365,2)。） L2 正则设计 [EXACT] 精确枚举九档：每个单元的 (单元, 项) 关联数【恰为 5N-1】，无一例外； 扇出（单格翻转影响的事件数）区间 [(9N-1)/2, 5N-1]，中位 ~4.6N。 => 没有"边缘"单元；任何单格改动同时进入 Theta(N) 个事件。 L3 可达格（精确刻画，双向） [LEAN] 设事件有 L 项，n_0..n_3 为相位 0..3 的项数，a = n_0-n_2, b = n_1-n_3，则 z 可达 <=> exists a,b in Z: z = a^2+b^2, |a|+|b| <= L, |a|+|b| = L (mod 2) （验证：L <= 16 的全部 z <= L^2，逐一比对"相位计数枚举"与"配对规则"。） 推论（验证范围 |a|,|b| <= 60）： L 奇 => z = 1 (mod 4); L 偶 => z = 0 或 2 (mod 4); z 永不 = 3 (mod 4) 注：本轮之前所有搜索用的是【宽松版】|a|,|b| <= L，它在每档 25,50,75,75,125,100,125,150,200 个事件上高估了 cap（N=9..73）。 这不改变评分，但使梯子靶点系统性偏松。 L4 单格量子界 + 安全裕度剪枝 [LEAN] 单格翻转使 (a,b) -> (a+da, b+db)，|da|,|db| <= 2（一个单元在一个事件中至多出现于两个项），故 |dz| <= 4(|a|+|b|) + 8 <= 4L + 8 （验证：|a|,|b| <= 40 与全部 |d| <= 2。） 推论：余量 > 4L+8 的事件不可能被任何单格移动顶穿 => 只需精确复核余量 <= 4L+8 的事件。 L5 支撑引理 [EXACT/显然] 未触及事件 e 项集的改动不改变 z_e => 修好某违规事件的改动必然落在其支撑集内。 实测支撑集规模：13, 85, 64, 28, 145, 56, 66, 338（N=13..73。） L6 阶梯间隙证书 [LEAN] 九档的"下一可达值"(rung) 均由间隙证书确认：区间 (rung, M) 内任何事件类都不可实现， 而 rung 本身可实现。例：N=73 时 102,103 均非二平方和，故 rung = 101。 L7 前沿格粗糙度 [LEAN] 靶点处 cap 取值的去重个数 = [4,5,6,6,8,7,8,9,11]（N=9,13,17,21,25,29,33,37,73）； [0,rung] 内相邻可达值最大间隙 = [3,3,3,5,5,5,5,5,7]。 => 小 N 的 cap 格极粗（4-6 档），只有大 N 才有 11 档。 验证强度声明：八条定理的 #print axioms 审计显示各自仅依赖 1 条 native_decide 受信求值公理， 无 sorry、无附加假设。（native_decide 依赖 Lean 编译求值器的可信性；若要求纯内核归约， 可把 native_decide 换成 decide，代价是显著更长的编译时间。）
为什么当前搜索方法在任何 n 上都突不破，以及为什么 n=73 能从 113 推进到 104 全部 [LEAN] 结论由 Lean 4 + mathlib 机器验证
3. 纪录的尺度不变位置 [EXACT] ------------------------------------------------------------------------------------- N | NEV | 单元 | T | E | E/T | M | M/N | M/mean | rung | rung/M | q=2/sqrt(rung) 9 | 210 | 45 | 990 | 846 | 0.855 | 10 | 1.11 | 2.48 | 9 | 0.100 | 0.667 13 | 310 | 65 | 2080 | 1734 | 0.834 | 16 | 1.23 | 2.86 | 13 | 0.188 | 0.555 17 | 410 | 85 | 3570 | 3002 | 0.841 | 20 | 1.18 | 2.73 | 18 | 0.100 | 0.471 21 | 510 | 105 | 5460 | 4622 | 0.847 | 29 | 1.38 | 3.20 | 26 | 0.103 | 0.392 25 | 610 | 125 | 7750 | 6524 | 0.842 | 36 | 1.44 | 3.37 | 34 | 0.056 | 0.343 29 | 710 | 145 | 10440 | 8748 | 0.838 | 40 | 1.38 | 3.25 | 37 | 0.075 | 0.329 33 | 810 | 165 | 13530 | 11360 | 0.840 | 50 | 1.52 | 3.57 | 49 | 0.020 | 0.286 37 | 910 | 185 | 17020 | 14230 | 0.836 | 53 | 1.43 | 3.39 | 52 | 0.019 | 0.277 73 | 1810 | 365 | 66430 | 56006 | 0.843 | 104 | 1.42 | 3.36 | 101 | 0.029 | 0.199 三条尺度不变性：E/T in [0.834,0.855]（随机基线恰为 T => 所有纪录比随机能量低 ~16%）、 M/N in [1.11,1.52]、M/mean in [2.48,3.57]。 => 九个实例坐在同一条尺度不变曲线的同一点上：不是"不同难度的问题"，而是同一族的不同尺度。 4. 墙：为什么任何 n 现在都突不破 ------------------------------------------------------------------------------------- (a) 邻域内无解（精确闭合，覆盖 100%） N=13 k<=3 全局 1,179,360 候选 零改进 N=13 k<=4 全局 54,840,240 候选 零改进 N=13 k<=6 支撑集内 1,563,564 候选 零改进（其中 1,234,780 精确复核） N=17 k<=3 全局 2,666,790 候选 零改进 N=17 k<=4 全局（支撑=全盘）164,046,585 候选 零改进 N=21 k<=3 全局 5,061,420 候选 零改进 N=25 k<=3 全局 8,579,250 候选 零改进 N=29 k<=3 全局 13,166,145 候选 零改进 N=13..37 三分量 (M,C,E) k<=2 全局 全部 零改进 <= 连"廉价维度"都没有下降方向 （诚实标注：N=33 k<=3 因到时停在 71.03% 覆盖；N=37 k<=3 未跑完。） (b) 定向约束系统：靶点处"压线事件（不许升）+ 违规事件（必须降）"构成一组方向性约束。 压线占比随 N 单调下降： 33.9%(13) -> 16.1%(17) -> 15.3%(21) -> 10.0%(25) -> 8.3%(29) -> 6.4%(33) -> 5.6%(37) -> 2.4%(73) 在 N=9,13 上三分之一事件压线，任何改动都撞墙。 5. 两种阻塞机制的二分（决定性） [NUM] ------------------------------------------------------------------------------------- rho = (pinned + viol) / (2 * |support|)；支撑集内单元做连续松弛（其余冻结）： N | support | pinned+viol | rho | 联合连续下限(总超额) | 判定 13 | 13 | 104 | 4.000 | 3.53 (不可行) | 联合【超定】 17 | 85 | 83 | 0.488 | 0.00 | 纯量化阻塞 21 | 64 | 72 | 0.562 | 0.00 | 纯量化阻塞 25 | 28 | 54 | 0.964 | 0.00 | 纯量化阻塞 29 | 145 | 65 | 0.224 | 0.00 | 纯量化阻塞 33 | 56 | 46 | 0.411 | 0.00 | 纯量化阻塞 37 | 66 | 43 | 0.326 | 0.00 | 纯量化阻塞 73 | 338 | 46 | 0.068 | 0.00 | 纯量化阻塞 补充（同为 [NUM]）：【违规事件自身】在所有实例上都可被支撑集内连续移动修好（下限 0.000）。 => N=13 的困难在于【联合】系统：修好违规必然顶穿其它事件，且无法在支撑集内化解； 故 N=13 的下一档需要【换盆地】；N>=17 的下一档需要【量化感知的构造性移动】。 6. 为什么 n=73 能从 113 推进到 104 ------------------------------------------------------------------------------------- 四个可测维度上 n=73 同时最优，且全部随 N 单调改善： 量 13 17 21 25 29 33 37 73 自由度/约束 2|supp|/(pin+viol) 0.25 2.05 1.78 1.04 4.46 2.43 3.07 14.7 压线占比 33.9% 16.1% 15.3% 10.0% 8.3% 6.4% 5.6% 2.4% 实测单格相对冲击（中位） 0.400 0.333 0.231 0.235 0.216 0.163 0.163 0.119 前沿格相对间隙 0.231 0.167 0.192 0.147 0.135 0.102 0.096 0.069 历史上产生 113->104 的三类方法（行级束搜索、cap-ladder+弹簧网络、软谱 L11）恰好消耗 "自由度"与"细粒度控制"，而这正是小 N 最缺的两样。 同时必须计入预算错配：n=73 每档 4.5 天 / ~15 小时 / ~8.5 小时；小 n 每档 20-30 分钟。 结论：n=73 的推进 = 结构优势（四项指标）+ 方法族适配 + 足量预算； 其余不能 = 量化阻塞（n>=17）或联合超定（n=13）+ 预算与方法族双重缺位。
谢谢这么完整的分析。我把九档当前纪录重新送入本站验证器，均通过，文中列出的 (M,C,E) 也一致，包括 n=73 的 (104,7,56006)。事件计数和独立 QPSK 相位和的二平方可达格也能复核。但 L4 的单格变化界有一个需要先修正的问题。 自相关中，一个单元可能同时进入两个项；这并不能推出 |da|、|db|≤2，两项的变化可以叠加。具体反例：N=13，一行由 0111311222222 改成 0111111222222，只改第 5 个符号（0 基索引 4），首位规范不变。该行 k=1 自相关有 L=12 项，R 从 6+2i 变成 10+2i（采用相反共轭约定时虚部符号相反），z 从 40 变为 104，变化 64，大于 4L+8=56。取该长度可达的 cap=100，旧余量 60>56，但新值仍会越界。其余四行取全 0 即可组成本站接受的完整输入。这否定的是此通用变化界及其安全跳检推论，不是否定你已经提交并验证通过的 104 纪录。 另外，数值优化得到正残差 3.53，本身不是全局不可行性的下界证书；显示 0.00 也需要未舍入残差与可复核构型。小邻域穷举无改进只说明该起点、该邻域，不能推出所有 n 均不能突破。独立事件值可达，也不代表所有事件能在同一码本中同时满足。表中自由度/约束等指标并非全部随 N 单调改善，rung/M 那一栏实际填写的看起来是 (M−rung)/M。 方便的话请补上 Lean 源文件、lean-toolchain、依赖版本和各定理的 #print axioms，以及穷举程序、输入构型与覆盖日志。尤其需要核对 L4 的 Lean 定理是否只证明了假设 |da|、|db|≤2 后的代数结论，而没有证明真实单格改动满足这个假设。若搜索使用了上述跳检，应修正后重跑受影响部分；在补齐之前，我们将结构计数、实测结果与全局最优性结论分开看待。
找到一个有趣的值，标志着M不是必须N（ "n": 10, "M": 10,"C": 33,"E": 1065）： "sequences": [ "0032313221", "0001023030", "0130320100", "0200233011", "0031122113"]
M不是必须大于N
这组有价值，已经用本站的实际验证器独立复算：五条序列合法，结果确实是 n=10，(M,C,E)=(10,33,1065)。因此它是对“所有长度都必须 M>N”的有效反例。 结论的范围也一起说明：它给出 n=10 的一个可行上界 M≤10，但还没有证明 M=10 是全局最优，也不能直接推广到其他 n。n=10 目前不是开放子题，我们先把这个可复核构造作为研究线索保留下来；不会仅凭这一构造授予最优性证明分。谢谢补上完整序列，这让核验很直接。