至多素数间隙 186

该存储库包含素数间隙界限的 Lean 4 形式化和 Python 数字证书。精益结果仍然以三个显式输入公理为条件；引用的数学估计和数值计算尚未转化为这些输入的精益证明。对于素数序列 $p_n$ ，目标界限是 $$\liminf_{n\to\infty}(p_{n+1}-p_n)\le 186.$$ 开发从以下输入导出 $\mathrm{DHL}[40,2]$：每个允许的四十个整数移位集合都有无限多个包含至少两个素数的平移。可接纳性意味着省略对每个素数取模的残数类。将其应用到所包含的直径为 186 的元组即可得出间隙界限。 PrimeGap186.lean 命名空间中的主要声明是： 声明结果 dhl_40_2 $\mathrm{DHL}[40,2]$ 对于每个允许的整数元组。 Infinity_two_prime_translates_admissibleTuple 显式元组的无限多个二素数转换。 primeGapLiminf_le_186 连续素数间隙界限。假设德利涅类型估计对于素数 $p$ ，写为 $e_p(x)=\exp(2\pi i\widetilde{x}/p)$ ，其中 $\widetilde{x}$ 是 $x\in\mathbb{F}_p$ 的任何整数表示。定义 $$\mathrm{Kl}_3(c;p) =\frac1p\sum_{\substack{x_1,x_2,x_3\in\mathbb{F}_p\\x_1x_2x_3=c}} e_p(x_1+x_2+x_3),$$ $$K_2(c;p)=\sum_{u\in\mathbb{F}_p^\times}e_p(u+c/u).$$ 公理 PrimeGap186.kloosterman3_bound 假设每个素数 $p$ 和所有 $c\in\mathbb{F}_p^\times$ 有以下界限： $$\left|\mathrm{Kl}_3(c;p)\right|\le 3.$$ 这是根据 Nicholas M. Katz、Gauss Sums、Kloosterman Sums 和 Monodromy Groups，Annals of Mathematics Studies 116，Princeton University Press (1988)，Theorem 4.1.1(1)–(2)，p. 中所述的 Deligne 定理得出的。 49.对于 $n=3$ ，简单的乘法字符和 $b_1=b_2=b_3=1$ ，排名第三和权重第二给出原始边界 $3p$ ；我们的标准化除以 $p$ 。公理 PrimeGap186.kloosterman2_correlation_bound 假设每个素数 $p$ 和所有 $A,B\in\mathbb{F}_p^\times$ 具有以下界限： $$\left|\sum_{t\in\mathbb{F}_p\setminus\{0,-1\}} K_2(A/t;p)\,K_2(B/(t+1);p)\right|\le 8p\sqrt p.$$ 这是 Étienne Fouvry、Emmanuel Kowalski 和 Philippe Michel，《Friedlander-Iwaniec 字符和》，2013 年 6 月 14 日，命题 2，第 14 页。 1.在反转求和变量后，它们的归一化 $\mathrm{Kl}_2(c)$ 等于 $K_2(c;p)/\sqrt p$，因此它们的 $8\sqrt p$ 界限在这里变为 $8p\sqrt p$。不施加任何条件 $A\ne B$；即使 $A=B$ ，两个极点也被排除。这些估计是在引用的文献中建立的，但在精益开发中仍然是未经证实的输入。数字输入和证书 PrimeGap186.physical_integral_bounds 假定 104 个外部物理积分上限和 45 个内部物理积分上限，以及三个上限。 Python证书从头开始重新计算试验。测试环境使用 Python 3.12.13、NumPy 2.2.6、python-flint 0.9.0 和带有修正符号多项式卷积（未捆绑）的自定义 FLINT 3.6.0 版本。 python3 -B prime_gap_186_certificate.py --workers 4 --output prime_gap_186_fresh.json 使用新的输出路径。保持 PYTHONOPTIMIZE 未设置并且不要使用 -O 或 -OO 。必须通过强制浮点和带符号卷积检查。成功运行会产生一个带有 passed: true 的收据；它不释放任何精益公理。构建和验证 该项目固定 Lean 4.34.0-rc2 及其 Mathlib 依赖项。安装 elan 后，运行： Lake exe cache get Lake build PrimeGaps186 注册的 Lean 构建已通过，没有错误或警告。 Comparator 将所有三个结果与 Challenge.lean 相匹配，并且 Nanoda 和 Lean 的内核在本地 Colima Linux VM 中接受了他们的证明。该配置允许三个记录的项目公理以及 propext 、 Quot.sound 和 Classical.choice （总共六个）；这验证了条件证明，而不是输入本身。数字证书与之前的合格证书相比没有变化。 Challenge.lean 指定陈述和输入假设，以及三个有意定理占位符。请参阅比较器说明和形式化元数据以了解检查设置和状态。项目贡献使用 Apache 2.0 ；现有的第三方通知仍然适用。