Inadmissible tuples have a vanishing counting function
ProvedHardyLittlewood.inadmissible_tuple_count_zeroIf the doubled offsets of m cover all residue classes modulo some prime q — at every base point p, since coverage is translation-invariant — then no base point carries an admissible prime constellation, and the counting function π_P(n) is zero for every n. This is the degenerate half of the conjecture: an inadmissible tuple has a zero count against a vanishing singular series.
import Mathlib import Definitions.Def_HardyLittlewood_constellation import Definitions.Def_HardyLittlewood_counting import Definitions.Def_HardyLittlewood_series
namespace HardyLittlewood
/-- An inadmissible tuple contributes nothing to the count: if the residues of
the entries cover all of ZMod q for some prime q and every base point, then no
base point carries an admissible prime constellation, and the counting
function π_P(n) is identically zero. -/
theorem inadmissible_tuple_count_zero {k : ℕ} (m : Fin k.succ → ℕ)
(q : ℕ) (hq : q.Prime)
(h : ∀ p : ℕ, Function.Surjective (fun i : Fin k.succ => (p + 2 * m i : ZMod q)))
(n : ℕ) : primeTupleCounting m n = 0 := 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 q is prime and for every natural number p the map sending i to the residue of p + 2 · m i modulo q is surjective onto the residue classes modulo q, then for every natural number n the number "primeTupleCounting m n" — the cardinality of the set of base points p at most n satisfying "IsAdmissiblePrimeConstellation m p" — equals zero.
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.