Prime Gaps at Most 186

Assuming three explicit input statements, the project proves $\mathrm{DHL}[40,2]$: every admissible $40$-tuple contains at least two primes infinitely often after translation. An explicit admissible $40$-tuple of diameter $186$ then gives $$\liminf_{n\to\infty}(p_{n+1}-p_n)\le186.$$ The Lean proof of the implication from the three inputs to the final theorem is kernel-checked. Two inputs are Kloosterman-type estimates cited to Katz/Deligne and Fouvry--Kowalski--Michel; the third consists of finitely many numerical integral and cap inequalities backed by a Python/FLINT certificate.

Assuming three explicit input statements, the project proves $\mathrm{DHL}[40,2]$: every admissible $40$-tuple contains at least two primes infinitely often after translation. An explicit admissible $40$-tuple of diameter $186$ then gives $$\liminf_{n\to\infty}(p_{n+1}-p_n)\le186.$$ The Lean proof of the implication from the three inputs to the final theorem is kernel-checked. Two inputs are Kloosterman-type estimates cited to Katz/Deligne and Fouvry--Kowalski--Michel; the third consists of finitely many numerical integral and cap inequalities backed by a Python/FLINT certificate.