Coprimality proof for the general case

In the paper it is claimed in the proof of coprimality of a₃ and a₄ over there – isCoprime_natAdd_two_three here – that "as 101 is prime and 10y - 1 > 101, they have no common factor". This is not always true even with the paper's definition of y, but can be made so by adding 101 to the factors of y.

theorem GeneralCase.even_Y {F : Finset ℕ} : Even (Y F)

theorem GeneralCase.three_dvd_Y {F : Finset ℕ} : 3 ∣ Y F

theorem GeneralCase.ten_dvd_Y {F : Finset ℕ} : 10 ∣ Y F

theorem GeneralCase.eleven_dvd_Y {F : Finset ℕ} : 11 ∣ Y F

theorem GeneralCase.hundredone_dvd_Y {F : Finset ℕ} : 101 ∣ Y F

theorem GeneralCase.odd_X {F : Finset ℕ} {h : ℕ} : Odd (X F h)

theorem GeneralCase.X_coprime_Y {F : Finset ℕ} {h : ℕ} : (X F h).Coprime (Y F)

theorem GeneralCase.Yp1_coprime_10Yp1 {F : Finset ℕ} : (Y F + 1).Coprime (10 * Y F + 1)

theorem GeneralCase.Yp1_coprime_10Ym1 {F : Finset ℕ} : (Y F + 1).Coprime (10 * Y F - 1)

theorem GeneralCase.Ym1_coprime_10Yp1 {F : Finset ℕ} : (Y F - 1).Coprime (10 * Y F + 1)

theorem GeneralCase.Ym1_coprime_10Ym1 {F : Finset ℕ} : (Y F - 1).Coprime (10 * Y F - 1)

theorem GeneralCase.eventually_X_modEq_one_of_coprime {F : Finset ℕ} (Q : Finset ℕ → ℕ) (hQ : (Y F + 1).Coprime (Q F)) : ∀ᶠ (h : ℕ) in Filter.atTop, X F h ≡ 1 [MOD Q F]

Given Q independent of h with Y F + 1 coprime to Q F, X F h ≡ 1 mod Q F for sufficiently large h.

theorem GeneralCase.eventually_X_modEq_10Yp1 {F : Finset ℕ} : ∀ᶠ (h : ℕ) in Filter.atTop, X F h ≡ 1 [MOD 10 * Y F + 1]

theorem GeneralCase.eventually_X_modEq_10Ym1 {F : Finset ℕ} : ∀ᶠ (h : ℕ) in Filter.atTop, X F h ≡ 1 [MOD 10 * Y F - 1]

theorem GeneralCase.coprime_of_rough {F : Finset ℕ} (Q K L : Finset ℕ → ℕ) (hQ : ∀ {d : ℕ}, 3 ≤ d → d ∣ Q F → L F < d) (hK : Odd (K F)) (hL : K F ≤ L F) : (K F).Coprime (Q F)

In this file's context "rough" means "having only large ODD prime factors". All elements of tup n F h are odd by construction, except natAdd n 0 when n is odd, so the factor 2 is not an obstacle to pairwise coprimality.

theorem GeneralCase.isCoprime_natAdd_four_five {n : ℕ} {F : Finset ℕ} {h : ℕ} : IsCoprime (tup n F h (Fin.natAdd n 4)) (tup n F h (Fin.natAdd n 5))

theorem GeneralCase.isCoprime_natAdd_three_four {n : ℕ} {F : Finset ℕ} : ∀ᶠ (h : ℕ) in Filter.atTop, IsCoprime (tup n F h (Fin.natAdd n 3)) (tup n F h (Fin.natAdd n 4))

theorem GeneralCase.isCoprime_natAdd_three_five {n : ℕ} {F : Finset ℕ} : ∀ᶠ (h : ℕ) in Filter.atTop, IsCoprime (tup n F h (Fin.natAdd n 3)) (tup n F h (Fin.natAdd n 5))

theorem GeneralCase.isCoprime_natAdd_two_three {n : ℕ} {F : Finset ℕ} : ∀ᶠ (h : ℕ) in Filter.atTop, IsCoprime (tup n F h (Fin.natAdd n 2)) (tup n F h (Fin.natAdd n 3))

theorem GeneralCase.isCoprime_natAdd_two_sq_sub_sq {n : ℕ} {F : Finset ℕ} : ∀ᶠ (h : ℕ) in Filter.atTop, IsCoprime (tup n F h (Fin.natAdd n 2)) (↑(X F h) ^ 2 - ↑(Y F) ^ 2)

theorem GeneralCase.isCoprime_natAdd_two_four {n : ℕ} {F : Finset ℕ} : ∀ᶠ (h : ℕ) in Filter.atTop, IsCoprime (tup n F h (Fin.natAdd n 2)) (tup n F h (Fin.natAdd n 4))

theorem GeneralCase.isCoprime_natAdd_two_five {n : ℕ} {F : Finset ℕ} : ∀ᶠ (h : ℕ) in Filter.atTop, IsCoprime (tup n F h (Fin.natAdd n 2)) (tup n F h (Fin.natAdd n 5))

theorem GeneralCase.isCoprime_natAdd_five_of_rough {n : ℕ} {F : Finset ℕ} {Q : Finset ℕ → ℕ} (hQ : ∀ {d : ℕ}, 3 ≤ d → d ∣ Q F → Y F + 1 < d) : ∀ᶠ (h : ℕ) in Filter.atTop, IsCoprime (↑(Q F)) (tup n F h (Fin.natAdd n 5))

theorem GeneralCase.isCoprime_natAdd_four_of_rough {n : ℕ} {F : Finset ℕ} {Q : Finset ℕ → ℕ} (hQ : ∀ {d : ℕ}, 3 ≤ d → d ∣ Q F → Y F + 1 < d) : ∀ᶠ (h : ℕ) in Filter.atTop, IsCoprime (↑(Q F)) (tup n F h (Fin.natAdd n 4))

theorem GeneralCase.isCoprime_natAdd_three_of_rough {n : ℕ} {F : Finset ℕ} {Q : Finset ℕ → ℕ} (hQ : ∀ {d : ℕ}, 3 ≤ d → d ∣ Q F → 10 * Y F - 1 < d) : ∀ᶠ (h : ℕ) in Filter.atTop, IsCoprime (↑(Q F)) (tup n F h (Fin.natAdd n 3))

theorem GeneralCase.isCoprime_natAdd_two_of_rough {n : ℕ} {F : Finset ℕ} {Q : Finset ℕ → ℕ} (hQ : ∀ {d : ℕ}, 3 ≤ d → d ∣ Q F → 10 * Y F ^ 3 + 1 < d) : ∀ᶠ (h : ℕ) in Filter.atTop, IsCoprime (↑(Q F)) (tup n F h (Fin.natAdd n 2))

theorem GeneralCase.tenY3p1_le_U {n : ℕ} {F : Finset ℕ} : 10 * Y F ^ 3 + 1 ≤ U n F

theorem GeneralCase.tenYm1_le_U {n : ℕ} {F : Finset ℕ} : 10 * Y F - 1 ≤ U n F

theorem GeneralCase.Yp1_le_U {n : ℕ} {F : Finset ℕ} : Y F + 1 ≤ U n F

theorem GeneralCase.isCoprime_natAdd_natAdd {n : ℕ} {F : Finset ℕ} {i j : Fin 6} (hij : i < j) : ∀ᶠ (h : ℕ) in Filter.atTop, IsCoprime (tup n F h (Fin.natAdd n i)) (tup n F h (Fin.natAdd n j))

theorem GeneralCase.primeChain_mem_Icc {n : ℕ} {F : Finset ℕ} {i : Fin n} : primeChain (100 * Y F ^ 6) ↑i ∈ Finset.Icc 3 (U n F)

theorem GeneralCase.isCoprime_castAdd_natAdd {n : ℕ} {F : Finset ℕ} {i : Fin n} {j : Fin 6} : ∀ᶠ (h : ℕ) in Filter.atTop, IsCoprime (tup n F h (Fin.castAdd 6 i)) (tup n F h (Fin.natAdd n j))

theorem GeneralCase.pairwiseCoprime_tup {n : ℕ} {F : Finset ℕ} : ∀ᶠ (h : ℕ) in Filter.atTop, PairwiseCoprime (tup n F h)