The odd case (Theorem 1.13)

def OddCase.tupPell (n : ℕ) (F : Finset ℕ) (k : ℕ) : Fin (n + 5) → ℤ

The sequence of (n + 5)-tuples completely contained in factorFreeTuples F n (for n even and 0, 1, 2, 5, 10 ∉ F) and having qualities tending to 5 / 3.

Equations

• OddCase.tupPell n F k = OddCase.tup n F (↑(OddCase.pell (OddCase.Y n F ^ 2) k).1 * ↑(OddCase.Y n F))

theorem OddCase.injective_tupPell {n : ℕ} {F : Finset ℕ} : Function.Injective (tupPell n F)

theorem OddCase.strongSSC_tupPell {n : ℕ} {F : Finset ℕ} {k : ℕ} : StrongSSC (tupPell n F k)

theorem OddCase.tupPell_mem_factorFreeTuples {n : ℕ} {F : Finset ℕ} {k : ℕ} (hn : Even n) (dF : Disjoint {0, 1, 2, 5, 10} F) : tupPell n F k ∈ factorFreeTuples F (n + 5)

theorem OddCase.maxAbs_tupPell {n : ℕ} {F : Finset ℕ} {k : ℕ} : maxAbs (tupPell n F k) = ((pell (Y n F ^ 2) k).1 * Y n F + 1) ^ 5

theorem OddCase.radical_tupPell_dvd {n : ℕ} {F : Finset ℕ} : ∃ C > 0, ∀ (k : ℕ), UniqueFactorizationMonoid.radical (∏ i : Fin (n + 5), tupPell n F k i) ∣ C * ((↑(pell (Y n F ^ 2) k).1 * ↑(Y n F)) ^ 2 - 1) * ↑(pell (Y n F ^ 2) k).2

theorem Nat.one_lt_mul_iff' {m n : ℕ} : 1 < m * n ↔ 0 < m ∧ 1 < n ∨ 0 < n ∧ 1 < m

Upstreamable to core!

theorem OddCase.radical_tupPell_le {n : ℕ} {F : Finset ℕ} : ∃ C > 0, ∀ (k : ℕ), UniqueFactorizationMonoid.radical (∏ i : Fin (n + 5), tupPell n F k i) ≤ C * (↑(pell (Y n F ^ 2) k).1 * ↑(Y n F)) ^ 3

theorem OddCase.le_tupleQuality {n : ℕ} {F : Finset ℕ} : ∃ (C : ℝ), ∀ (k : ℕ), ENNReal.ofReal (5 * Real.log ↑((pell (Y n F ^ 2) k).1 * Y n F) / (C + 3 * Real.log ↑((pell (Y n F ^ 2) k).1 * Y n F))) ≤ tupleQuality (tupPell n F k)

theorem OddCase.liminf_tupleQuality_tupPell {n : ℕ} {F : Finset ℕ} : 5 / 3 ≤ Filter.liminf (tupleQuality ∘ tupPell n F) Filter.atTop

theorem quality_factorFreeTuples_ge_of_odd_of_disjoint {n : ℕ} {F : Finset ℕ} (hn : 5 ≤ n ∧ Odd n) (dF : Disjoint {0, 1, 2, 5, 10} F) : 5 / 3 ≤ quality (factorFreeTuples F n)

Theorem 1.13.

theorem not_ramaekersConjecture_odd_ge_five {n : ℕ} (hn : 5 ≤ n ∧ Odd n) : ¬RamaekersConjecture n