Admissible tuple

Conjectura.Defs.Mathematics.NumberTheory.AdmissibleTuple

/-
Copyright (c) 2026 The Conjectura Authors. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: The Conjectura Authors
-/
import Mathlib.Data.ZMod.Basic
import Mathlib.Data.Nat.Prime.Basic

/-! # Admissible tuple -/

namespace Conjectura.NumberTheory

/-- A finite set of shifts is **admissible** when, for every prime `p`, the shifts miss at least
one residue class mod `p`. Inadmissible tuples are blocked from being prime infinitely often for
a trivial congruence reason, so admissibility is exactly the hypothesis under which the
Hardy–Littlewood conjectures are stated. -/
def IsAdmissible (H : Finset ℕ) : Prop :=
  ∀ p : ℕ, p.Prime → ∃ r : ZMod p, ∀ h ∈ H, (h : ZMod p) ≠ r

end Conjectura.NumberTheory