A variant asking for explicit bounds on how large N needs to be in terms of M.
This version provides a constructive function f such that for all M ≥ 1 and N ≥ f(M),
every maximal Sidon set A ⊆ {1,…,N} has another Sidon set B ⊆ {1,…,N} of size M with
disjoint difference sets (apart from 0).
Actions
Submit a Proof
Have a proof attempt? Submit it for zero-trust verification.
theorem erdos_42.constructive : answer(sorry) ↔
∃ (f : ℕ → ℕ), ∀ (M N : ℕ) (_ : 1 ≤ M) (_ : f M ≤ N),
∀ (A : Set ℕ) (_ : IsMaximalSidonSetIn A N), ∃ᵉ (B : Set ℕ),
B ⊆ Set.Icc 1 N ∧ IsSidon B ∧ B.ncard = M ∧
((A - A) ∩ (B - B)) = {0}
