The general case (Theorem 1.14)

theorem GeneralCase.tup_mem_factorFreeTuples {n : ℕ} {F : Finset ℕ} (hF : ∀ f ∈ F, 3 ≤ f) : ∀ᶠ (h : ℕ) in Filter.atTop, tup n F h ∈ factorFreeTuples F (n + 6)

theorem GeneralCase.radical_tup_dvd {n : ℕ} {F : Finset ℕ} : ∃ C > 0, ∀ (h : ℕ), UniqueFactorizationMonoid.radical (∏ i : Fin (n + 6), tup n F h i) ∣ C * (↑(X F h) ^ 2 + 10 * ↑(Y F) ^ 3) * (↑(X F h) ^ 2 - ↑(Y F) ^ 2)

theorem GeneralCase.radical_tup_le {n : ℕ} {F : Finset ℕ} : ∃ C > 0, ∀ (h : ℕ), UniqueFactorizationMonoid.radical (∏ i : Fin (n + 6), tup n F h i) ≤ C * ↑(X F h) ^ 4

theorem GeneralCase.le_tupleQuality {n : ℕ} {F : Finset ℕ} : ∃ (C : ℝ), ∀ᶠ (h : ℕ) in Filter.atTop, ENNReal.ofReal (5 * Real.log ↑(X F h) / (C + 4 * Real.log ↑(X F h))) ≤ tupleQuality (tup n F h)

theorem GeneralCase.liminf_tupleQuality_tup {n : ℕ} {F : Finset ℕ} : 5 / 4 ≤ Filter.liminf (tupleQuality ∘ tup n F) Filter.atTop

theorem quality_factorFreeTuples_ge {n : ℕ} {F : Finset ℕ} (hn : 6 ≤ n) (hF : ∀ f ∈ F, 3 ≤ f) : 5 / 4 ≤ quality (factorFreeTuples F n)

Theorem 1.14.

theorem not_ramaekersConjecture_ge_six {n : ℕ} (hn : 6 ≤ n) : ¬RamaekersConjecture n