Admissibility does not depend on the base point
ProvedHardyLittlewood.admissible_constellation_iffA prime constellation at the base point p is admissible if and only if it is a prime constellation and the tuple of doubled offsets is admissible: residue coverage modulo a prime is invariant under translation by p, so admissibility is a property of the offsets alone. This is the translation-invariance lemma that lets the conjecture's admissibility condition be read off the tuple itself, and it is the gateway to the tuple-based singular series.
import Mathlib import Definitions.Def_HardyLittlewood_constellation import Definitions.Def_HardyLittlewood_counting import Definitions.Def_HardyLittlewood_series
namespace HardyLittlewood
/-- Admissibility does not depend on the base point: a prime constellation at
p is admissible exactly when it is a prime constellation and the tuple of
doubled offsets is admissible — residue coverage modulo a prime is invariant
under translation by p. -/
theorem admissible_constellation_iff {k : ℕ} (m : Fin k.succ → ℕ) (p : ℕ) :
IsAdmissiblePrimeConstellation m p ↔
IsPrimeConstellation m p ∧ IsAdmissibleTuple m := 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 the finite set {0, 1, ..., k} to the natural numbers, and every natural number p, the proposition "IsAdmissiblePrimeConstellation m p" holds exactly when both "IsPrimeConstellation m p" holds and "IsAdmissibleTuple m" holds. Here the first proposition means: m evaluated at 0 is 0, every offset m i with i ≠ 0 is positive, every number p + 2 · m i is prime, and for every prime q the map sending i to the residue of p + 2 · m i modulo q is not surjective onto the residue classes modulo q; the third proposition means: for every prime q the map sending i to the residue of 2 · m i modulo q is not surjective onto the residue classes modulo q.
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.