True ↔ ∃ B, ¬B.IsWeakAddBasis ∧ ∃ f, (∀ (α : ℝ), 0 < α → α < 1 → f α > 0) ∧ ∀ (A : Set ℕ) (N : ℕ), have α := schnirelmannDensity A; ∃ b ∈ B, ↑(Set.Ioc 0 N ∩ (A ∪ (A + {b}))).ncard ≥ (α + f α) * ↑N