Erdős Problem 741

References:

• erdosproblems.com/741
• [Er94b] Erdős, Paul, Some problems in number theory, combinatorics and combinatorial geometry. Math. Pannon. (1994), 261-269.

theorem Erdos741.erdos_741.density : sorry ↔ ∀ (A : Set ℕ), (A + A).HasPosDensity → ∃ (A₁ : Set ℕ) (A₂ : Set ℕ), A = A₁ ∪ A₂ ∧ Disjoint A₁ A₂ ∧ (A₁ + A₁).HasPosDensity ∧ (A₂ + A₂).HasPosDensity

Let $A\subseteq \mathbb{N}$ be such that $A+A$ has positive density. Can one always decompose $A=A_1\sqcup A_2$ such that $A_1+A_1$ and $A_2+A_2$ both have positive density?

theorem Erdos741.erdos_741.basis : sorry ↔ ∃ (A : Set ℕ), (A ∪ {0}).IsAddBasisOfOrder 2 ∧ ∀ (A₁ A₂ : Set ℕ), A = A₁ ∪ A₂ → Disjoint A₁ A₂ → ¬(IsSyndetic (A₁ + A₁) ∧ IsSyndetic (A₂ + A₂))

Is there a basis $A$ of order $2$ such that if $A=A_1\sqcup A_2$ then $A_1+A_1$ and $A_2+A_2$ cannot both have bounded gaps?