Basic definitions and properties for the Krafft Sieve

This module provides basic bounds and properties for the primes and the primorial $q(n)$ used throughout the Krafft Sieve formalization.

instance KrafftSieve.q_ne_zero (n : ℕ) : NeZero (q n)

Instance proof that q is non-zero.

theorem KrafftSieve.mem_P_n_iff_exists_index (n p_val : ℕ) : p_val ∈ primeWindow n ↔ ∃ (i : Fin (w n)), p n i = p_val

A number p is in primeWindow if and only if it equals p_i for some index i.

theorem KrafftSieve.P_n_mono (n : ℕ) : primeWindow n ⊆ primeWindow (n + 1)

primeWindow is a subset of P_{n+1}.

theorem KrafftSieve.q_mono (n : ℕ) : q n ∣ q (n + 1)

q(n) divides q(n+1).

theorem KrafftSieve.p_mem_P_n (n : ℕ) (i : Fin (w n)) : p n i ∈ primeWindow n

Every p n i is in primeWindow n.

theorem KrafftSieve.p_prime (n : ℕ) (i : Fin (w n)) : Nat.Prime (p n i)

Every p n i is prime.

theorem KrafftSieve.p_ge_5 (n : ℕ) (i : Fin (w n)) : 5 ≤ p n i

Every p n i is at least 5.

theorem KrafftSieve.p_pos (n : ℕ) (i : Fin (w n)) : 0 < p n i

Every p n i is positive.

theorem KrafftSieve.p_ne_zero (n : ℕ) (i : Fin (w n)) : p n i ≠ 0

Every p n i is nonzero.

theorem KrafftSieve.p_lt_range (n : ℕ) (i : Fin (w n)) : p n i < 6 * n + 2

p n i is in the range [5, 6n+2).

theorem KrafftSieve.p_dvd_q (n : ℕ) (i : Fin (w n)) : p n i ∣ q n

p n i divides q n.

theorem KrafftSieve.q_ge_q10_very_large (n : ℕ) (hn : n ≥ 10) : q n ≥ 10 ^ 20

$q(n)$ is at least $10^{20}$ for $n \ge 10$.

theorem KrafftSieve.q_bound (n : ℕ) (hn : n ≥ 1) : 6 * n ^ 2 + 10 * n + 3 < q n

For $n \ge 1$, $6n^2 + 10n + 3 < q(n)$.