Erdős Problem 881

Reference: erdosproblems.com/881

def Erdos881.IsMinimalAsymptoticAddBasisOfOrder (k : ℕ) (A : Set ℕ) : Prop

We interpret "additive basis of order k" as an asymptotic additive basis of order k, using the predicate Set.IsAsymptoticAddBasisOfOrder from additive combinatorics.

A minimal additive basis of order k is a set A such that

• A is an asymptotic additive basis of order k, and
• for every infinite subset B ⊆ A, the complement A \ B is not an asymptotic additive basis of order k.

Equations

• Erdos881.IsMinimalAsymptoticAddBasisOfOrder k A = (A.IsAsymptoticAddBasisOfOrder k ∧ ∀ ⦃B : Set ℕ⦄, B ⊆ A → B.Infinite → ¬(A \ B).IsAsymptoticAddBasisOfOrder k)

theorem Erdos881.erdos_881 : sorry ↔ ∀ (k : ℕ) (A : Set ℕ), IsMinimalAsymptoticAddBasisOfOrder k A → ∃ B ⊆ A, B.Infinite ∧ (A \ B).IsAsymptoticAddBasisOfOrder (k + 1)

Let A ⊂ ℕ be an additive basis of order k which is minimal in the sense that if B ⊂ A is any infinite set, then A \ B is not a basis of order k.

Must there exist an infinite B ⊂ A such that A \ B is an additive basis of order k + 1?