The conjecture yields infinitely many prime constellations
ProvedHardyLittlewood.first_implies_infinite_constellationsFor an admissible tuple of distinct offsets with m₀ = 0, the first Hardy–Littlewood conjecture implies that prime constellations with those offsets occur at arbitrarily large base points: for every N there is a base point p ≥ N whose constellation (p, p + 2m₁, ..., p + 2m_k) consists entirely of primes. The derivation runs through the positivity of the singular series and the divergence of the model integral.
import Mathlib import Definitions.Def_HardyLittlewood_constellation import Definitions.Def_HardyLittlewood_counting import Definitions.Def_HardyLittlewood_series
namespace HardyLittlewood
/-- The infinitude consequence: for an admissible tuple of distinct offsets
with m 0 = 0, the first Hardy–Littlewood conjecture implies that prime
constellations with those offsets occur at arbitrarily large base points. -/
theorem first_implies_infinite_constellations {k : ℕ} (m : Fin k.succ → ℕ)
(hm0 : m 0 = 0) (hinj : Function.Injective m) (hadm : IsAdmissibleTuple m)
(h : firstHardyLittlewoodFor m) (N : ℕ) :
∃ p : ℕ, N ≤ p ∧ IsPrimeConstellation m p := by
sorry
end HardyLittlewood
Read-back
What the Lean code literally says, in plain math · glm-5-latest-short
The statement says: for every natural number k and every function m from {0, 1, ..., k} to the natural numbers, if m evaluated at 0 is 0, m is injective, the doubled offsets are admissible, and the first Hardy–Littlewood conjecture holds for m — meaning the counting sequence of admissible constellations is asymptotic to the singular-series constant times the logarithmic integral — then for every natural number N there exists a natural number p at least N such that "IsPrimeConstellation m p" holds: m evaluated at 0 is 0, the other offsets are positive, and every number p + 2 · m i is prime.
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.