Lean-verified lower bounds for the Shannon capacity of odd cycles

技术摘要：经 Lean 验证的奇数循环图香农容量下界

问题陈述
本文旨在解决确定 $n \geq 7$ 的奇数循环图 $C_n$ 的香农容量 $\Theta(G)$ 这一长期存在的开放问题。香农容量定义为 $\Theta(G) := \sup_{d \geq 1} \alpha(G^{\boxtimes d})^{1/d}$，其中 $\alpha$ 表示独立数，$\boxtimes$ 表示强图积。虽然 Lovász 利用 $\theta$ 函数 $\vartheta(G)$ 确定了 $\Theta(C_5) = \sqrt{5}$，但对于所有长度大于或等于 7 的奇数循环，其精确容量仍是未知的。主要的挑战在于如何在更高阶的强幂图中找到更大的独立集，以提高已知的下界。

方法论
作者采用了一种基于“小工具构造”（gadget construction）和最近由 Gao (2026) 提出的“乘积引理”（product lemma）的迭代程序，该引理本身建立在 Itty, Rosin, Carstensen 和 Reichman (2026) 的方法之上。核心方法论包括：

1. 有效元组（Valid Tuples）： 对于图 $G$，定义了一个有效元组 $\tau = (I, S, f_0, f_1, X)$，其中 $I$ 是一个独立集，$S \subseteq I$，且 $f_0, f_1$ 是满足严格邻域约束的特定映射。该元组生成一个“轮廓”（profile）$\Pi(\tau) = (|I|, |S|, |X|, |X \setminus (N_G[f_0(S)] \cup N_G[f_1(S)])|)$。
2. 乘积运算： 定义了轮廓的二元运算 $\star$。定理 1 确立了如果 $\tau$ 和 $\tau'$ 分别是图 $G$ 和 $H$ 的有效元组，则存在一个关于强积 $G \boxtimes H$ 的有效元组，其轮廓为各自轮廓的 $\star$-积。
3. 迭代构造： 从在特定幂次的奇数循环中通过计算发现的有效元组开始，作者迭代地应用 $\star$-积来生成更高幂次的轮廓。这一过程构造了强幂 $C_n^{\boxtimes d}$ 中的独立集，这些独立集比通过简单笛卡尔积基础独立集所能得到的独立集更大。
4. 形式化验证： 该方法论的一个关键组成部分是在 Lean 证明助手中对这些界限进行完整的形式化。基础元组（集合 $I, S, X$ 以及映射 $f_0, f_1$）被编码为显式的字面量，并在 Lean 环境内进行机械化验证。

主要贡献与结果
本文提出了七个小型奇数循环（$C_7, C_{11}, C_{13}, C_{15}, C_{19}, C_{21}, C_{23}$）的新型改进后的香农容量下界。这些界限是通过识别特定的基础有效元组并应用迭代乘积程序而得出的。结果如下：

• $\Theta(C_7)$： 提升至 $\geq 3.258805369885\dots$（此前为 Gao 2026 的 $3.2587891\dots$）。该构造利用了 $C_7^{\boxtimes 5}$ 中的一个基础元组，并迭代至 200 次幂。
• $\Theta(C_{11})$： 提升至 $\geq 5.294502522149\dots$（此前为 Itty 等人 2026 的 $5.2897736\dots$）。基础元组位于 $C_{11}^{\boxtimes 3}$ 中，迭代至 174 次幂。
• $\Theta(C_{13})$： 提升至 $\geq 6.302455083464\dots$（此前为 Itty 等人 2026 的 $6.3001091\dots$）。基础元组位于 $C_{13}^{\boxtimes 6}$ 中，迭代至 432 次幂。
• $\Theta(C_{15})$： 提升至 $\geq 7.301600534487\dots$（此前为 Itty 等人 2026 的 $7.3013990\dots$）。基础元组位于 $C_{15}^{\boxtimes 4}$ 中，迭代至 4096 次幂。
• $\Theta(C_{19})$： 提升至 $\geq 9.357192705918\dots$（此前为 Baumert 等人 1971 的 $9.3571200\dots$）。基础元组位于 $C_{19}^{\boxtimes 4}$ 中，迭代至 16384 次幂。
• $\Theta(C_{21})$： 提升至 $\geq 10.342455853338\dots$（此前为 Baumert 等人 1971 的 $10.3422729\dots$）。基础元组位于 $C_{21}^{\boxtimes 4}$ 中，迭代至 4096 次幂。
• $\Theta(C_{23})$： 提升至 $\geq 11.328224257774\dots$（此前为 Baumert 等人 1971 的 $11.3278379\dots$）。基础元组位于 $C_{23}^{\boxtimes 4}$ 中，迭代至 2048 次幂。

这些改进虽然在数值上很小（范围在 $10^{-5}$ 到 $10^{-3}$ 之间），但代表了这些特定循环目前的最高水平。

意义与主张
本文的主张主要通过对这些结果的严格验证体现。通过在 Lean 中将整个构造及所得界限形式化，作者确保了复杂的组合论证和特定的集合构造不存在人为错误。这项工作遵循了近期利用大语言模型（LLM）来发现初始构造的研究轨迹（如 [IRCR26] 和 [Gao26] 所见），但其区别在于提供了一个完全形式化的、经机器检查的关于基础元组有效性和迭代乘积定理应用正确性的证明。作者并不声称已经解决了奇数循环香农容量的一般问题，也不打算在应用 Gao 现有的乘积引理之外提出新的理论框架；相反，他们提供了这些特定实例目前已知的最佳数值下界，并以数学上的确定性进行了验证。