On factoring of unlimited integers

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 b : Fin ℓ → ℕ) (k : ℕ) : ℕ

Equations

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

theorem dickson_strong {ℓ : ℕ} (a 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 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 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 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 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)

Janitha Aswedige's part

theorem Div_by_3 (m : ℕ) : 3 ∣ 1 - (-2) ^ m

theorem help (m : ℕ) : 2 ^ m / (-2) ^ m = (-1) ^ m

def s : ℕ → ℕ → ℤ

Anchor function definition. For p > 2: s(p, n) = (p^n + 1)/2 For p = 2: s(p, n) = (1 - (-2)^n)/3

Equations

• s x✝¹ x✝ = if x✝¹ > 2 then (↑x✝¹ ^ x✝ + 1) / 2 else if x✝¹ = 2 then (1 - (-2) ^ x✝) / 3 else 0

theorem anchor (p m n : ℕ) (hp : Nat.Prime p) (hmn : m < n) : s p n ≡ s p m [ZMOD ↑p ^ m]

theorem anchor_trivial (p m n : ℕ) (hmn : m = n) : s p n ≡ s p m [ZMOD ↑p ^ m]

theorem anchor_leq (p m n : ℕ) (hp : Nat.Prime p) (hmn : m ≤ n) : s p n ≡ s p m [ZMOD ↑p ^ m]

noncomputable def n_p : ℕ → ℤ → ℕ

Equations

• n_p x✝¹ x✝ = sSup {n : ℕ | x✝ ≡ s x✝¹ n [ZMOD ↑x✝¹ ^ n]}

noncomputable def a : ℤ → ℕ

Equations

• a x✝ = ∏ p ∈ (2 * x✝.natAbs + 1).primesBelow, p ^ n_p p x✝

theorem CWeak (x y : ℤ) (p : ℕ) (hp : Nat.Prime p) (hpx : p ∣ a x) (hpy : p ∣ a y) (Hx : x ≡ s p (n_p p x) [ZMOD ↑p ^ n_p p x]) (Hy : y ≡ s p (n_p p y) [ZMOD ↑p ^ n_p p y]) : ↑p ∣ y - x