A counterexample to a subadditivity conjecture of Cohen for Sophie Germain cyclic numbers

技术摘要：关于 Cohen 关于 Sophie Germain 循环数次加性猜想的反例

问题陈述
本文针对 J. E. Cohen 提出的关于“Sophie Germain 循环”整数分布的猜想进行了研究。一个整数 $n \ge 1$ 被定义为循环数（cyclic），如果 $\gcd(n, \phi(n)) = 1$（等价于阶数为 $n$ 的每个群都是循环群）。如果 $n$ 和 $2n+1$ 都是循环数，则称 $n$ 为 Sophie Germain 循环数。令 $C_\sigma(N)$ 表示区间 $[1, N]$ 内这些整数的计数函数。

Cohen 猜想 $C_\sigma$ 是次加的（subadditive），即对于所有整数 $1 \le m \le n$：
$$C_\sigma(m + n) \le C_\sigma(m) + C_\sigma(n)$$
这是循环数关于第二哈迪-李特尔沃思（Hardy–Littlewood）猜想（关于素数计数函数 $\pi$）的类似物。虽然 Cohen 通过验证了 $m, n \le 10^6$ 的情况未发现反例，但他并未对该不等式的普遍有效性做出定论。

方法论
作者采用直接的计算与逻辑方法来证伪该猜想：

1. 针对性搜索： 作者并非进行广泛搜索，而是确定了一个特定的窗口 $(m, m+n]$，其中 Sophie Germain 循环数的密度超过了初始段 $[1, m]$ 中的密度。
2. 显式枚举： 证明依赖于对特定范围内 Sophie Germain 循环数的有限枚举。作者计算了 $m=31$ 的精确值，并确定了一个长度为 31、起始于 $n=3928$ 的窗口（即区间 $(3928, 3959]$）。
3. 形式化验证： 结果通过 Lean 4 证明助手及其 mathlib 库进行了验证。该形式化通过 Nat.Coprime n (Nat.totient n) 定义了循环数，并验证了计数函数 $C_\sigma$。至关重要的是，该证明由 Lean 内核本身进行检查，仅依赖于标准公理（propext, Classical.choice, Quot.sound）并避免使用原生决策程序（native_decide），从而确保结果是一个定理而非计算产物。

关键结果
本文为 Cohen 猜想 66 提供了具体的反例：

• 参数： $m = 31$ 且 $n = 3928$。
• 计数：
  • $C_\sigma(31) = 10$（这些整数是 1, 2, 3, 5, 7, 11, 15, 17, 23, 29）。
  • 区间 $(3928, 3959]$ 包含 11 个 Sophie Germain 循环数：3929, 3931, 3935, 3941, 3943, 3945, 3947, 3949, 3953, 3957, 3959。
  • 因此，$C_\sigma(3959) = C_\sigma(3928) + 11$。
• 违反不等式：
  $$C_\sigma(3959) = C_\sigma(3928) + 11 > C_\sigma(3928) + 10 = C_\sigma(3928) + C_\sigma(31)$$
  因此，$C_\sigma(31 + 3928) > C_\sigma(31) + C_\sigma(3928)$，从而证伪了次加性主张。

作者指出，$C_\sigma(3928)$ 的具体数值对于证明并不重要；该证伪完全基于窗口 $(3928, 3959]$ 的密度高于 $[1, 31]$ 这一事实。

意义与主张
本文声称具有以下意义：

1. 解决开放问题： 它明确证明了 Cohen 猜想 66 是错误的，从而结束了在搜索至 $10^6$ 后仍悬而未决的问题。
2. 纠正前人工作： 作者指出，Cohen 在其原始搜索中未能发现反例是因为其计算机代码存在错误，这一点在本文发表后得到了 Cohen 本人的确认。
3. 理论一致性： Sophie Germain 循环数次加性猜想的失效，符合人们对素数类似猜想（哈迪-李特尔沃思猜想）同样是错误的，且与素数 $k$-元组猜想不相容的普遍看法。
4. 形式化严谨性： 该结果的特点在于其在 Lean 4 中的形式化验证，提供了一个经内核检查的证明，表明该反例确实位于此前搜索过的范围（$m, n \le 10^6$）之内。

文章总结道，此类性质的反例并不罕见，但本例之所以显著，是因为它恰好位于 Cohen 原本（错误的）搜索范围之内。