Complete residue coverage kills prime constellations
ProvedHardyLittlewood.no_constellation_of_complete_residuesNecessity of admissibility: if the residues of the constellation entries p + 2m_i cover all classes modulo a prime q with q < p, then the entries cannot all be prime — one of them is a positive multiple of q strictly larger than q. A prime constellation at p therefore forces its residue coverage to miss a class modulo every prime smaller than p.
import Mathlib import Definitions.Def_HardyLittlewood_constellation import Definitions.Def_HardyLittlewood_counting import Definitions.Def_HardyLittlewood_series
namespace HardyLittlewood
/-- Necessity of admissibility, locally: if the residues of the constellation
entries p + 2·m i cover all of ZMod q for a prime q smaller than p, then the
entries cannot all be prime — one of them is a positive multiple of q
strictly larger than q. -/
theorem no_constellation_of_complete_residues {k : ℕ} (m : Fin k.succ → ℕ)
(q p : ℕ) (hq : q.Prime) (hqp : q < p)
(h : Function.Surjective (fun i : Fin k.succ => (p + 2 * m i : ZMod q))) :
¬ 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, every function m from {0, 1, ..., k} to the natural numbers, and all natural numbers q and p, if q is prime, q is less than p, and the map sending i to the residue of p + 2 · m i modulo q is surjective onto the residue classes modulo q, then "IsPrimeConstellation m p" is false — that is, it is not the case that m evaluated at 0 is 0, all other offsets are positive, and all entries p + 2 · m i are prime.
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.