Prime chains

These are sequences of primes where the next prime is at least twice the last.

def primeChain (s : ℕ) : ℕ → ℕ

primeChain s is the lexicographically earliest sequence of primes with primeChain s 0 > s and each succeeding element more than twice the last.

Equations

• primeChain s 0 = Nat.find ⋯
• primeChain s n.succ = Nat.find ⋯

theorem prime_primeChain {s n : ℕ} : Nat.Prime (primeChain s n)

theorem primeChain_zero_gt {s : ℕ} : s < primeChain s 0

theorem primeChain_succ_gt {s n : ℕ} : 2 * primeChain s n < primeChain s (n + 1)

theorem strictMono_primeChain {s : ℕ} : StrictMono (primeChain s)

theorem primeChain_gt {s n : ℕ} : s < primeChain s n

def chainTup (n m s : ℕ) (i : Fin (n + 2)) : ℤ

An (n + 2)-tuple that satisfies the strong subsum condition if 0 < m ≤ s.

Equations

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

theorem chainTup_zero {m s : ℕ} : chainTup 0 m s = fun (x : Fin (0 + 2)) => match x with | 0 => ↑m | 1 => -↑m

theorem chainTup_induction_compl {n : ℕ} : {Fin.natAdd n 0, Fin.natAdd n 2}ᶜ = insert (Fin.natAdd n 1) (Finset.map (Fin.castAddEmb 3) Finset.univ)

theorem add_sum_lt_primeChain {n m s : ℕ} (h : m ≤ s) : m + ∑ i ∈ Finset.range n, primeChain s i < primeChain s n

theorem isSubsumBlock_chainTup {n m s : ℕ} (h : m ≤ s) : IsSubsumBlock (chainTup (n + 1) m s) {Fin.natAdd n 0, Fin.natAdd n 2}

theorem tupReduce_chainTup {n m s : ℕ} {c : n + 1 = n + 1 + 2 - {Fin.natAdd n 0, Fin.natAdd n 2}.card} : tupReduce (chainTup (n + 1) m s) {Fin.natAdd n 0, Fin.natAdd n 2} c = chainTup n m s

theorem strongSSC_chainTup {n m s : ℕ} (hm : 0 < m) (hs : m ≤ s) : StrongSSC (chainTup n m s)