Selberg Weights

This module defines the permitted residue classes $localInterval$ and the global surviving set $A$, as well as the indicator function $f(x)$ for survivors in the Krafft Sieve.

def KrafftSieve.localInterval (n : ℕ) (r : Fin (w n) → ℕ) (i : Fin (w n)) : Finset (ZMod (p n i))

Definition of the permitted residue classes localInterval. Define the set of permitted residue classes for each prime as $localInterval = (\mathbb{Z}/p_i\mathbb{Z}) \setminus \{\pm r_i \pmod{p_i}\}$.

Equations

• KrafftSieve.localInterval n r i = {x : ZMod (KrafftSieve.p n i) | x ≠ ↑(r i) ∧ x ≠ -↑(r i)}

def KrafftSieve.A (n : ℕ) (r : Fin (w n) → ℕ) : Finset (ZMod (q n))

Definition of the global set of surviving residues A. Define the global set of surviving residues $A \subseteq \mathbb{Z}/q\mathbb{Z}$ such that $x \in A$ if and only if $x \pmod{p_i} \in localInterval$ for all $1 \le i \le w$.

Equations

• KrafftSieve.A n r = {x : ZMod (KrafftSieve.q n) | ∀ (i : Fin (KrafftSieve.w n)), x.cast ∈ KrafftSieve.localInterval n r i}

noncomputable def KrafftSieve.f (n : ℕ) (r : Fin (w n) → ℕ) (x : ZMod (q n)) : ℝ

Definition of the indicator function f. Define the indicator function $f : \mathbb{Z}/q\mathbb{Z} \to \mathbb{R}$ such that $f(x) = 1$ if $x \in A$, and $f(x) = 0$ otherwise.

Equations

• KrafftSieve.f n r x = if x ∈ KrafftSieve.A n r then 1 else 0

theorem KrafftSieve.survives_iff (n : ℕ) (x : ZMod (q n)) : f n (krafftResidue n) x = 1 ↔ ∀ (i : Fin (w n)), x.cast ≠ ↑(krafftResidue n i) ∧ x.cast ≠ -↑(krafftResidue n i)

theorem KrafftSieve.krafft_algebraic_equivalence (p : ℕ) (hp : Nat.Prime p) (h_ge_5 : p ≥ 5) (x : ℤ) : have r := (p + 1) / 6; ↑x = ↑r ∨ ↑x = -↑r ↔ ↑p ∣ 6 * x - 1 ∨ ↑p ∣ 6 * x + 1

theorem KrafftSieve.interval_projection_bound (n x : ℕ) (hx : x ∈ evalInterval n) : 6 * x + 1 < (6 * n + 5) ^ 2

theorem KrafftSieve.primes_in_range_eq_P_n (n p : ℕ) (hp : Nat.Prime p) (h_ge_5 : 5 ≤ p) (h_lt : p < 6 * n + 5) : p ∈ primeWindow n

theorem KrafftSieve.prime_of_no_prime_factors_lt {k m : ℕ} (hk : 2 ≤ k) (h_sq : k < m ^ 2) (h_no_factors : ∀ (p : ℕ), Nat.Prime p → p < m → ¬p ∣ k) : Nat.Prime k

theorem KrafftSieve.not_dvd_of_survives (n x : ℕ) (h_survives : f n (krafftResidue n) ↑x = 1) (p_val : ℕ) (hp : p_val ∈ primeWindow n) : ¬↑p_val ∣ 6 * ↑x - 1 ∧ ¬↑p_val ∣ 6 * ↑x + 1

theorem KrafftSieve.sieve_equivalence (n : ℕ) (hn : n ≥ 1) (x : ℕ) (hx : x ∈ evalInterval n) : f n (krafftResidue n) ↑x = 1 ↔ Nat.Prime (6 * x - 1) ∧ Nat.Prime (6 * x + 1)

theorem KrafftSieve.additive_sieve_equivalence (n : ℕ) (hn : n ≥ 1) (x : ℕ) (hx : x ∈ evalInterval n) : c n ↑x = 0 ↔ Nat.Prime (6 * x - 1) ∧ Nat.Prime (6 * x + 1)

Additive Sieve Equivalence: Prove that an integer $x \in \mathcal{A}_n$ survives the Krafft sieve (meaning both $6x-1$ and $6x+1$ are prime) if and only if its global hit counter is exactly zero: $$ c(x) = 0 \iff x \text{ survives the Krafft sieve} $$

theorem KrafftSieve.non_negative_hits (n : ℕ) (x : ZMod (q n)) : c n x ≥ 0 ∧ (c n x < 1 → c n x = 0)

Non-negative Hits: Using the definition of $g_i(x)$ and $c(x)$, prove that for any $x$, the hit counter is non-negative: $c(x) \ge 0$. Furthermore, note that because $c(x)$ is a sum of indicator functions, if $c(x) < 1$, then $c(x) = 0$.

theorem KrafftSieve.weighted_existence_principle (n : ℕ) (W : ZMod (q n) → ℝ) (hW : ∀ (x : ZMod (q n)), W x ≥ 0) (h_ineq : sum2 n W < sum1 n W) : ∃ x ∈ evalInterval n, W ↑x > 0 ∧ c n ↑x = 0

The Weighted Existence Principle: Assume there exists a specific configuration such that $sum2(n, W) < sum1(n, W)$. Prove that there must exist at least one integer $x \in \mathcal{A}_n$ such that $W(x) > 0$ and $c(x) = 0$.

def KrafftSieve.KrafftSufficiency (n : ℕ) : Prop

Definition of the Krafft Sufficiency condition Existence of a weight function $W$ such that $sum2(n, W) < sum1(n, W)$.

Equations

• One or more equations did not get rendered due to their size.

theorem KrafftSieve.krafft_sieve_guarantee (n : ℕ) (hn : n ≥ 1) (h_admit : KrafftSufficiency n) : ∃ x ∈ evalInterval n, Nat.Prime (6 * x - 1) ∧ Nat.Prime (6 * x + 1)