The "warm-up" result (Theorem 2.1)

def KonyaginPrelude.tup (k : ℕ) : Fin 5 → ℤ

The quintuple defined in Section 2.1.

Equations

• KonyaginPrelude.tup k 0 = (6 ^ 2 ^ k + 1) ^ 3
• KonyaginPrelude.tup k 1 = -(6 ^ 2 ^ k - 1) ^ 3
• KonyaginPrelude.tup k 2 = -6 * (6 ^ 2 ^ k) ^ 2
• KonyaginPrelude.tup k 3 = -31
• KonyaginPrelude.tup k 4 = 29

theorem KonyaginPrelude.sum_tup (k : ℕ) : ∑ i : Fin 5, tup k i = 0

theorem KonyaginPrelude.injective_tup : Function.Injective tup

theorem KonyaginPrelude.six_pow_two_pow_mod_29_mem (k : ℕ) : 6 ^ 2 ^ k % 29 ∈ [6, 7, 20, 23]

theorem KonyaginPrelude.six_pow_two_pow_mod_31_mem (k : ℕ) : 6 ^ 2 ^ k % 31 ∈ [5, 6, 25]

theorem KonyaginPrelude.isCoprime_29 (k : ℕ) : IsCoprime 29 ((6 ^ 2 ^ k + 1) ^ 3) ∧ IsCoprime 29 (-(6 ^ 2 ^ k - 1) ^ 3) ∧ IsCoprime 29 (-6 * (6 ^ 2 ^ k) ^ 2)

theorem KonyaginPrelude.isCoprime_31 (k : ℕ) : IsCoprime 31 ((6 ^ 2 ^ k + 1) ^ 3) ∧ IsCoprime 31 (-(6 ^ 2 ^ k - 1) ^ 3) ∧ IsCoprime 31 (-6 * (6 ^ 2 ^ k) ^ 2)

theorem KonyaginPrelude.pairwiseCoprime_tup (k : ℕ) : PairwiseCoprime (tup k)

def KonyaginPrelude.tupReduced (k : ℕ) : Fin 5 → ℤ

The quintuple defined in Section 2.1 with k in place of 6 ^ 2 ^ k for easier term manipulation.

Equations

• KonyaginPrelude.tupReduced k 0 = (↑k + 1) ^ 3
• KonyaginPrelude.tupReduced k 1 = -(↑k - 1) ^ 3
• KonyaginPrelude.tupReduced k 2 = -6 * ↑k ^ 2
• KonyaginPrelude.tupReduced k 3 = -31
• KonyaginPrelude.tupReduced k 4 = 29

theorem KonyaginPrelude.sum_tupReduced_lt_tupReduced_one (k : ℕ) (hk : 10 ≤ k) : ∑ i ∈ {0, 1}ᶜ, (tupReduced k i).natAbs < (tupReduced k 1).natAbs

theorem KonyaginPrelude.sum_tupReduced_lt_tupReduced_zero (k : ℕ) (hk : 10 ≤ k) : ∑ i ∈ {0, 1}ᶜ, (tupReduced k i).natAbs < (tupReduced k 0).natAbs

def KonyaginPrelude.tupReduced2 (k : ℕ) : Fin 4 → ℤ

tupReduced with the first two terms added together.

Equations

• KonyaginPrelude.tupReduced2 k 0 = -6 * ↑k ^ 2
• KonyaginPrelude.tupReduced2 k 1 = -31
• KonyaginPrelude.tupReduced2 k 2 = 29
• KonyaginPrelude.tupReduced2 k 3 = 6 * ↑k ^ 2 + 2

theorem KonyaginPrelude.tupReduce_tupReduced (k : ℕ) {c₁ : 3 = 5 - {0, 1}.card} : tupReduce (tupReduced k) {0, 1} c₁ = tupReduced2 k

theorem KonyaginPrelude.sum_tupReduced2_lt_tupReduced2_zero (k : ℕ) (hk : 10 ≤ k) : ∑ i ∈ {0, 3}ᶜ, (tupReduced2 k i).natAbs < (tupReduced2 k 0).natAbs

theorem KonyaginPrelude.sum_tupReduced2_lt_tupReduced2_three (k : ℕ) (hk : 10 ≤ k) : ∑ i ∈ {0, 3}ᶜ, (tupReduced2 k i).natAbs < (tupReduced2 k 3).natAbs

theorem KonyaginPrelude.tupReduce_tupReduced2 (k : ℕ) {c₂ : 2 = 4 - {0, 3}.card} : tupReduce (tupReduced2 k) {0, 3} c₂ = ![-31, 29, 2]

theorem KonyaginPrelude.strongSSC_tupReduced (k : ℕ) (hk : 10 ≤ k) : StrongSSC (tupReduced k)

theorem KonyaginPrelude.strongSSC_tup (k : ℕ) : StrongSSC (tup k)

theorem KonyaginPrelude.six_pow_pos {n : ℕ} (hn : n ≠ 0) : 0 < 6 ^ n - 1

theorem KonyaginPrelude.radical_tup_dvd (k : ℕ) : UniqueFactorizationMonoid.radical (∏ i : Fin 5, tup k i) ∣ (6 ^ (2 * 2 ^ k) - 1) * 5394

theorem KonyaginPrelude.log_radical_tup_le (k : ℕ) : Real.log ↑(UniqueFactorizationMonoid.radical (∏ i : Fin 5, tup k i)) ≤ 2 * 2 ^ k * Real.log 6 + Real.log 5394

theorem KonyaginPrelude.maxAbs_tup (k : ℕ) : maxAbs (tup k) = (6 ^ 2 ^ k + 1) ^ 3

theorem KonyaginPrelude.le_tupleQuality (k : ℕ) : ENNReal.ofReal (3 * 2 ^ k * Real.log 6 / (2 * 2 ^ k * Real.log 6 + Real.log 5394)) ≤ tupleQuality (tup k)

theorem KonyaginPrelude.liminf_tupleQuality_tup : 3 / 2 ≤ Filter.liminf (tupleQuality ∘ tup) Filter.atTop

theorem KonyaginPrelude.tup_mem_factorFreeTuples (k : ℕ) : tup k ∈ factorFreeTuples ∅ 5

theorem konyagin_prelude : 3 / 2 ≤ quality (factorFreeTuples ∅ 5)

Theorem 2.1.

theorem not_ramaekersConjecture_five : ¬RamaekersConjecture 5