Definitions for the odd case

The lower bound s for primeChain in U was originally max 16 (F.sup id). This could be lowered because strongSSC_vwTup only requires m ≤ s, not 2m ≤ s.

def OddCase.U (n : ℕ) (F : Finset ℕ) : ℕ

The sum of tup over all indices save n and n + 1, i.e. the input u to VWPair.

Equations

• OddCase.U n F = 8 + ∑ i ∈ Finset.range n, primeChain (max 8 (F.sup id)) i

def OddCase.VW (n : ℕ) (F : Finset ℕ) : VWPair (U n F) (max (U n F) (F.sup id))

The VWPair generated from the inputs u = U n F, m = max (U n F) (F.sup id).

Equations

• OddCase.VW n F = VWPair.of (OddCase.U n F) (max (OddCase.U n F) (F.sup id))

def OddCase.Y (n : ℕ) (F : Finset ℕ) : ℕ

We require x in tup to be a multiple of this number, an optimised version of the paper's y.

Equations

• OddCase.Y n F = (10 * (F.erase 0).prod id * ∏ i ∈ Finset.range n, primeChain (max 8 (F.sup id)) i) * (OddCase.VW n F).v * (OddCase.VW n F).w

def OddCase.tup (n : ℕ) (F : Finset ℕ) (x : ℤ) (i : Fin (n + 5)) : ℤ

The sequence of (n + 5)-tuples containing an infinite subsequence in factorFreeTuples whose qualities tend to 5 / 3, assuming n is even and 0, 1, 2, 5, 10 ∉ F.

Equations

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

theorem OddCase.tup_castAdd {n : ℕ} {F : Finset ℕ} {x : ℤ} {i : Fin n} : tup n F x (Fin.castAdd 5 i) = ↑(primeChain (max 8 (F.sup id)) ↑i)

@[simp]

theorem OddCase.tup_natAdd_zero {n : ℕ} {F : Finset ℕ} {x : ℤ} : tup n F x (Fin.natAdd n 0) = ↑(VW n F).v

@[simp]

theorem OddCase.tup_natAdd_one {n : ℕ} {F : Finset ℕ} {x : ℤ} : tup n F x (Fin.natAdd n 1) = -↑(VW n F).w

@[simp]

theorem OddCase.tup_natAdd_two {n : ℕ} {F : Finset ℕ} {x : ℤ} : tup n F x (Fin.natAdd n 2) = (x - 1) ^ 5

@[simp]

theorem OddCase.tup_natAdd_three {n : ℕ} {F : Finset ℕ} {x : ℤ} : tup n F x (Fin.natAdd n 3) = 10 * (x ^ 2 + 1) ^ 2

@[simp]

theorem OddCase.tup_natAdd_four {n : ℕ} {F : Finset ℕ} {x : ℤ} : tup n F x (Fin.natAdd n 4) = -(x + 1) ^ 5

theorem OddCase.sum_tup {n : ℕ} {F : Finset ℕ} {x : ℤ} : ∑ i : Fin (n + 5), tup n F x i = 0

theorem OddCase.primeChain_lt_U {n : ℕ} {F : Finset ℕ} {i : Fin n} : primeChain (max 8 (F.sup id)) ↑i < U n F

theorem OddCase.ten_lt_primeChain {n : ℕ} {F : Finset ℕ} : 10 < primeChain (max 8 (F.sup id)) n

theorem OddCase.primeChain_mem_Icc {n : ℕ} {F : Finset ℕ} {i : Fin n} : primeChain (max 8 (F.sup id)) ↑i ∈ Finset.Icc 3 (max (U n F) (F.sup id))

theorem OddCase.U_lt_V {n : ℕ} {F : Finset ℕ} : U n F < (VW n F).v

theorem OddCase.U_lt_W {n : ℕ} {F : Finset ℕ} : U n F < (VW n F).w

theorem OddCase.V_lower_bound {n : ℕ} {F : Finset ℕ} : 9 ≤ (VW n F).v

theorem OddCase.W_lower_bound {n : ℕ} {F : Finset ℕ} : 17 ≤ (VW n F).w

theorem OddCase.Y_lower_bound {n : ℕ} {F : Finset ℕ} : 1530 ≤ Y n F

theorem OddCase.Y_pos {n : ℕ} {F : Finset ℕ} : 0 < Y n F

theorem OddCase.dvd_of_Y_dvd {n : ℕ} {F : Finset ℕ} {x : ℤ} (dx : ↑(Y n F) ∣ x) : 10 ∣ x ∧ (∀ f ∈ F.erase 0, ↑f ∣ x) ∧ (∀ (i : Fin n), ↑(primeChain (max 8 (F.sup id)) ↑i) ∣ x) ∧ ↑(VW n F).v ∣ x ∧ ↑(VW n F).w ∣ x

theorem OddCase.isCoprime_tup_castAdd_natAdd {n : ℕ} {F : Finset ℕ} {x : ℤ} {i : Fin n} {j : Fin 5} (dx : ↑(Y n F) ∣ x) : IsCoprime (tup n F x (Fin.castAdd 5 i)) (tup n F x (Fin.natAdd n j))

theorem OddCase.V_coprime_ten {n : ℕ} {F : Finset ℕ} (hn : Even n) : (VW n F).v.Coprime 10

This lemma is where we need evenness of n, i.e. oddness of the whole tuple's length.

theorem OddCase.W_coprime_ten {n : ℕ} {F : Finset ℕ} : (VW n F).w.Coprime 10

theorem OddCase.pairwiseCoprime_tup {n : ℕ} {F : Finset ℕ} {x : ℤ} (hn : Even n) (dx : ↑(Y n F) ∣ x) : PairwiseCoprime (tup n F x)

theorem OddCase.lt_primeChain_of_mem_F {n : ℕ} {F : Finset ℕ} {f : ℕ} (hf : f ∈ F) : f < primeChain (max 8 (F.sup id)) n

theorem OddCase.not_dvd_tup {n : ℕ} {F : Finset ℕ} {x : ℤ} (dx : ↑(Y n F) ∣ x) (dF : Disjoint {0, 1, 2, 5, 10} F) (f : ℕ) : f ∈ F → ∀ (i : Fin (n + 5)), ¬↑f ∣ tup n F x i