On factoring of unlimited integers

by KAREL HRBACEK

We prove a special case of Dickson's Conjecture as stated in the paper: the case where

• gcd(a,b)>1 or b=1

n = gcd(a,b) > 1 implies n | f(k) = a+bk for all k, violating the main hypothesis of Dickson's conjecture.

See dickson_strong.

Dickson's Conjecture is trivial for ℓ = 0 and we do not need Hrbacek's assumption that ℓ ≥ 1.

def prod_f {ℓ : ℕ} (a : Fin ℓ → ℕ) (b : Fin ℓ → ℕ) : ℕ → ℕ

Equations

• prod_f a b k = ∏ i : Fin ℓ, (a i + b i * k)

theorem dickson_strong {ℓ : ℕ} (a : Fin ℓ → ℕ) (b : Fin ℓ → ℕ) (ha : ∀ (i : Fin ℓ), (a i).gcd (b i) > 1 ∨ b i = 1) (hc : ¬∃ n > 1, ∀ (k : ℕ), n ∣ prod_f a b k) (i : Fin ℓ) (n₀ : ℕ) : ∃ n ≥ n₀, Nat.Prime (a i + b i * n)

theorem dickson_gcd {ℓ : ℕ} (a : Fin ℓ → ℕ) (b : Fin ℓ → ℕ) (ha : ∀ (i : Fin ℓ), (a i).gcd (b i) > 1) (hc : ¬∃ n > 1, ∀ (k : ℕ), n ∣ prod_f a b k) (i : Fin ℓ) (n₀ : ℕ) : ∃ n ≥ n₀, Nat.Prime (a i + b i * n)

theorem gt_one (k : ℕ) (hk₀ : k ≠ 0) (hk₁ : k ≠ 1) : k > 1

theorem dvd_helper' {a : ℕ} {b : ℕ} (ha : b ∣ a) (h_b : b > 1) : a.gcd b > 1

theorem dvd_helper {a : ℕ} {b : ℕ} (ha : b ∣ a) (hb : b ≥ 1) : a.gcd b > 1 ∨ b = 1

theorem dickson_dvd {ℓ : ℕ} (a : Fin ℓ → ℕ) (b : Fin ℓ → ℕ) (hb : ∀ (i : Fin ℓ), b i ≥ 1) (ha : ∀ (i : Fin ℓ), b i ∣ a i) (hc : ¬∃ n > 1, ∀ (k : ℕ), n ∣ prod_f a b k) (i : Fin ℓ) (n₀ : ℕ) : ∃ n ≥ n₀, Nat.Prime (a i + b i * n)

theorem dickson_linear {ℓ : ℕ} {a : Fin ℓ → ℕ} {b : Fin ℓ → ℕ} {hb : ∀ (i : Fin ℓ), b i ≥ 1} (ha : ∀ (i : Fin ℓ), a i = 0) (hc : ¬∃ n > 1, ∀ (k : ℕ), n ∣ prod_f a b k) (i : Fin ℓ) (n₀ : ℕ) : ∃ n ≥ n₀, Nat.Prime (a i + b i * n)