A Lean-Certified Proof of $K_8(4, 2) = 23$

技术摘要：关于 $K_8(4,2) = 23$ 的 Lean 认证证明

问题陈述
本文旨在确定精确覆盖数 $K_q(n,r)$，即在 $q$ 进制汉明空间中长度为 $n$、半径为 $r$ 的最小覆盖码的大小。具体而言，本文解决了八进制情况下的长度 4、半径 2 的值：$K_8(4,2)$。在此项工作之前，现有的界限（特别是 Kéri 的表格）将该值置于 $[22, 23]$ 区间内。下界是由 Rodemich rook-domain 界限推导出的，而上界则由大字母表界限支持。本研究的目标是通过证明下界 $K_8(4,2) \ge 23$ 来封闭这一区间。

方法论
该证明在 Lean 4 定理证明器及其 mathlib 库中进行了形式化。它采用了一种“携带证明”（proof-carrying）的方法，通过两个独立的凭证来建立结果：一个显式的上界和一个结构性的下界。

1. 上界 ($K_8(4,2) \le 23$)：
   作者提供了一个由 23 个 $(\text{Fin } 8)^4$ 中码字组成的显式码。形式化证明验证了两个条件：集合的基数至多为 23，且环境空间（4096 个词）中的每个词与至少一个码字的汉明距离在 2 以内。这是一个穷举性的有限检查。

2. 下界 ($K_8(4,2) \ge 23$)：
   本文的核心是一个针对任何假设的覆盖集 $C^*$（若 $|C^*| \le 22$）的结构性非存在性论证。证明过程通过一系列归约进行：

   • 纤维计数 (Fiber Counting)： 对于一个假设的覆盖集，作者定义了“纤维” $C^*_{i,a}$（在坐标 $i$ 处符号为 $a$ 的码字）。他们证明每个纤维必须包含至少两个码字。这确立了每个坐标每种符号至少有 16 个码字（$8 \text{ 符号} \times 2$）的基准，从而为 $|C^*|=22$ 的情况留下了至多 6 个剩余码字的“预算”（对于 $|C^*| \le 21$ 则为 5 个）。
   • 缺失对图 (Missing-Pair Graphs)： 证明通过一种“逆向”视角进行，分析哪些符号对在码对坐标的投影中是“缺失”的。这些缺失对构成了图 $E_{ij}$。
   • 情形 $|C^*| \le 21$： 利用较小的剩余预算，作者通过组合计数证明，缺失对图必须包含一个“同时四部团”（即四个符号 $a,b,c,d$ 使得六个坐标对全部缺失）。引理 7 证明了这样的团在有效的半径-2 覆盖中不存在，从而排除了大小为 21 或更少的覆盖情况。
   • 情形 $|C^*| = 22$： 对于剩余的情况，证明将问题归约为缺失对图“轮廓”（profile）的有限分类。作者表明，任何有效的轮廓必须呈现特定的“共同 $3+3+2$ 块结构”。
   • SAT/LRAT 集成： 这些轮廓的分类规模过大，无法进行人工枚举。作者将约束条件（行/列度数界限和无团条件）编码为合取范式 (CNF) 实例。他们使用一个不可信的 SAT 求解器生成线性 RAT (LRAT) 反驳（即证明不满足性）。
   • 形式化验证： Lean 解析这些 LRAT 凭证，并机械地重放这些反驳过程，以证明不存在大小为 22 的有效覆盖。
   • 最终矛盾： 即使假设存在共同的块结构，作者也会在结构的“2-符号分量”中导出矛盾。该分量将要求一个长度为 4、最多只有 4 行的二进制强度-2 阵列，这在数学上是不可能的。

主要贡献

• 精确值： 本文确定了 $K_8(4,2) = 23$ 的精确值，封闭了此前已知的 $[22, 23]$ 区间。
• 形式化的下界： 提供了一个完整的 Lean 4 形式化证明，排除了所有 22 词覆盖的可能性。这并非通过体积论证，而是通过基于纤维计数和缺失对图的结构性障碍实现的。
• 证明携带人工制品： 结果被封装为一个 Lean 人工制品，其中包含了显式码、结构性引理、CNF 实例以及 LRAT 反驳。至关重要的是，SAT 求解器并不属于受信任的计算基座；Lean 会在内部验证 LRAT 凭证。
• 计算下界的模式： 本文引入了一种可重用的模式，用于将求解器生成的证据附加到覆盖码下界上。它将“发现”（不可信求解器）与“验证”（受信任的 Lean 内核）分离，使得大型有限分类问题可以在保持形式正确性的同时通过计算解决。

结果
主要结果是定理 $K_8(4,2) = 23$。

• 上界： 通过一个显式的 23 词码得到证明。
• 下界： 通过证明一个大小为 22 的覆盖会导致矛盾（即强制产生一个不可能的二进制阵列）而得到证明。
• 性能： 形式化验证涉及大量的计算资源。在内核模式下重放主证明文件大约需要 143 GiB 的 RAM，而在原生模式下该需求降至约 5.5 GiB。LRAT 检查阶段在内核模式下耗时约 17 分钟。

意义与声明
本文的意义主要在于形式化数学领域，以及将组合推理与计算凭证相结合的方法论。

• 方法论转变： 它展示了结构组合学如何与“携带证明”的计算证据相结合。SAT 求解器被用于发现有限障碍，但数学桥梁和对求解器输出的验证完全由定理证明器处理。
• 信任边界： 本文明确了涉及 SAT 求解器的形式化证明中的信任边界。求解器是不可信的；Lean 内核负责检查 LRAT 凭证以及将这些凭证连接到覆盖码陈述的逻辑演绎。
• 可扩展性： 该结果作为一个测试案例，展示了如何处理那些对于人工证明而言过于庞大、但对于 SAT 求解器而言足以通过有限分类问题解决的覆盖码问题。
• 无新应用： 本文并未声称对 $K_8(4,2)=23$ 这一数值本身有新的应用，也没有提出新的实验协议。其贡献严格在于解决编码理论表格中的一个特定开放问题，并演示了此类问题的形式化验证工作流。