解法：梅纳德的多维筛法:素数之间的有界间隔(2013年)

梅纳德的命题4.3 陈述了两个显式的数值事实,是把多项式候选函数 $F$ 代入 $M_k$ 的定义中测试得到的:$M_5>2$,以及 $M_{105}>4$(梅纳德2013年,第4节,命题4.3,第1–2部分)。这两个数字都不被声称是真正的上确界——它们只是下界,通过对具体、明确写出的 $F$ 进行直接(尽管冗长)的计算得到,足以支撑接下来的论证。

梅纳德还证明了一个关于大 $k$ 的渐近陈述:当 $k$ 足够大时 $M_k > \log k - 2\log\log k - 2$(梅纳德2013年,第4节,命题4.3,第3部分),这是由一族更系统的测试函数而非临时选取得到的;正是这一点最终推出了定理1.1中关于有界窗口内出现任意多个素数的一般界。

这些数值事实是整个论证中唯一真正依靠显式计算——而非纯粹结构性推理——发挥作用的地方;证明的其余部分都是“只要 $M_k$ 至少这么大,那么……”。最后一步会把一切拼装起来。