Definitions of the tuple sets and conjectures considered in the paper

def ABCConjecture : Prop

The abc conjecture itself, using quality.

Equations

• ABCConjecture = (quality {a : Fin 3 → ℤ | ∑ i : Fin 3, a i = 0 ∧ Finset.univ.gcd a = 1} = 1)

def nConjectureTuples (n : ℕ) : Set (Fin n → ℤ)

The tuples in Browkin and Brzeziński's n-conjecture. A(n) in the paper.

Equations

• nConjectureTuples n = {a : Fin n → ℤ | ∑ i : Fin n, a i = 0 ∧ SSC a ∧ Finset.univ.gcd a = 1}

def NConjecture (n : ℕ) : Prop

Browkin and Brzeziński's n-conjecture for a fixed n. The conjecture itself is ∀ n ≥ 3, NConjecture n.

Equations

• NConjecture n = (quality (nConjectureTuples n) = ↑(2 * n - 5))

def strongNConjectureTuples (n : ℕ) : Set (Fin n → ℤ)

The tuples in Browkin's strong n-conjecture. B(n) in the paper.

Equations

• strongNConjectureTuples n = {a : Fin n → ℤ | ∑ i : Fin n, a i = 0 ∧ PairwiseCoprime a}

def StrongNConjecture (n : ℕ) : Prop

Browkin's strong n-conjecture for a fixed n. The conjecture itself is ∀ n ≥ 3, StrongNConjecture n.

Equations

• StrongNConjecture n = (quality (strongNConjectureTuples n) < ⊤)

def ramaekersTuples (n : ℕ) : Set (Fin n → ℤ)

The tuples in Ramaekers's conjecture. R(n) in the paper.

Equations

• ramaekersTuples n = {a : Fin n → ℤ | ∑ i : Fin n, a i = 0 ∧ SSC a ∧ PairwiseCoprime a}

def RamaekersConjecture (n : ℕ) : Prop

Ramaekers's conjecture for a fixed n. The conjecture itself is ∀ n ≥ 3, RamaekersConjecture n.

Equations

• RamaekersConjecture n = (quality (ramaekersTuples n) = 1)

def factorFreeTuples (F : Finset ℕ) (n : ℕ) : Set (Fin n → ℤ)

U(F,n) in the paper.

Equations

• factorFreeTuples F n = {a : Fin n → ℤ | ∑ i : Fin n, a i = 0 ∧ StrongSSC a ∧ PairwiseCoprime a ∧ ∀ f ∈ F, ∀ (i : Fin n), ¬↑f ∣ a i}

theorem nConjecture_3_iff_ABC : NConjecture 3 ↔ ABCConjecture

theorem quality_factorFreeTuples_anti {n : ℕ} {F F' : Finset ℕ} (hF : F ⊆ F') : quality (factorFreeTuples F' n) ≤ quality (factorFreeTuples F n)

theorem quality_factorFreeTuples_le_nConjectureTuples {n : ℕ} {F : Finset ℕ} (hn : 2 ≤ n) : quality (factorFreeTuples F n) ≤ quality (nConjectureTuples n)

theorem quality_factorFreeTuples_le_ramaekersTuples {n : ℕ} {F : Finset ℕ} : quality (factorFreeTuples F n) ≤ quality (ramaekersTuples n)

theorem quality_ramaekersTuples_le_strongNConjectureTuples {n : ℕ} : quality (ramaekersTuples n) ≤ quality (strongNConjectureTuples n)