Prime constellation

Conjectura.Defs.Mathematics.NumberTheory.PrimeConstellation

/-
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 Conjectura.Defs.Mathematics.NumberTheory.AdmissibleTuple

/-! # Prime constellation -/

namespace Conjectura.NumberTheory

/-- A **prime constellation** at `n` for a set of shifts `H` is the assertion that `n + h` is
prime for every `h ∈ H`. Twin primes are the case `H = {0, 2}`; the conjecture that every
`IsAdmissible` tuple occurs infinitely often generalises all of them at once. -/
def IsPrimeConstellation (H : Finset ℕ) (n : ℕ) : Prop :=
  ∀ h ∈ H, Nat.Prime (n + h)

end Conjectura.NumberTheory