Erdős Problem 707: Embedding Sidon Sets in Perfect Difference Sets

Reference: erdosproblems.com/707

Let A ⊆ ℕ be a finite Sidon set. Is there some set B with A ⊆ B which is a perfect difference set modulo p^2 + p + 1 for some prime power p?

This problem is related to Erdős Problem 329 about the maximum density of Sidon sets. If this conjecture is true, it would imply that the maximum density of Sidon sets is 1.

def Erdos707.IsPerfectDifferenceSetModulo (B : Set ℕ) (n : ℕ) : Prop

B is a perfect difference set modulo n if every non-zero residue mod n can be uniquely expressed in the form a - b, where a, b ∈ B.

Equations

• Erdos707.IsPerfectDifferenceSetModulo B n = Set.BijOn (fun (x : ℕ × ℕ) => match x with | (a, b) => ↑a - ↑b) B.offDiag {x : ZMod n | x ≠ 0}

theorem Erdos707.erdos_707 : (∀ (A : Set ℕ), A.Finite → IsSidon A → ∃ (B : Set ℕ) (p : ℕ), IsPrimePow p ∧ A ⊆ B ∧ IsPerfectDifferenceSetModulo B (p ^ 2 + p + 1)) ↔ sorry

Erdős Problem 707: Any finite Sidon set can be embedded in a perfect difference set modulo p^2 + p + 1 for some prime power p.

theorem Erdos707.erdos_707.variants.smallest_prime : sInf {p : ℕ | IsPrimePow p ∧ ∃ (A : Set ℕ) (B : Set ℕ), A.Finite ∧ IsSidon A ∧ A ⊆ B ∧ IsPerfectDifferenceSetModulo B (p ^ 2 + p + 1)} = sorry

The smallest prime power p for which some finite Sidon set can be embedded in a perfect difference set modulo p^2 + p + 1.

theorem Erdos707.erdos_707.variants.constructive : (∃ (f : ℕ → ℕ), ∀ (A : Set ℕ), A.Finite → IsSidon A → ∃ (B : Set ℕ) (p : ℕ), IsPrimePow p ∧ p ≤ f A.ncard ∧ A ⊆ B ∧ IsPerfectDifferenceSetModulo B (p ^ 2 + p + 1)) ↔ sorry

A constructive version asking for explicit bounds on the size of p in terms of |A|.

theorem Erdos707.erdos_707.variants.weaker : (∀ (A : Set ℕ), A.Finite → IsSidon A → ∃ (B : Set ℕ) (n : ℕ), A ⊆ B ∧ IsPerfectDifferenceSetModulo B n) ↔ sorry

A weaker version asking for any modulus, not necessarily of the form p^2 + p + 1.

Perfect difference sets and their properties

theorem Erdos707.erdos_707.variants.perfect_difference_set_size_bound (B : Set ℕ) (n : ℕ) (hB : IsPerfectDifferenceSetModulo B n) : B.ncard ≤ n.sqrt + 1

A perfect difference set modulo n must have size ≤ √n + 1.

theorem Erdos707.erdos_707.variants.singer_construction (p : ℕ) (hp : IsPrimePow p) : ∃ (B : Set ℕ), IsPerfectDifferenceSetModulo B (p ^ 2 + p + 1) ∧ B.ncard = p + 1

The Singer construction gives perfect difference sets for n = p^2 + p + 1 where p is a prime power.

Examples and special cases

theorem Erdos707.erdos_707.variants.example_sidon_set : IsSidon {1, 2, 4}

The set {1, 2, 4} is a Sidon set.

theorem Erdos707.erdos_707.variants.example_embedding : ∃ (B : Set ℕ), {1, 2, 4} ⊆ B ∧ IsPerfectDifferenceSetModulo B 7

The set {1, 2, 4} can be embedded in a perfect difference set modulo 7.

theorem Erdos707.erdos_707.variants.small_sidon_sets (A : Set ℕ) (hA : A.Finite) (h : A.ncard ≤ 3) (hSidon : IsSidon A) : ∃ (B : Set ℕ) (p : ℕ), IsPrimePow p ∧ A ⊆ B ∧ IsPerfectDifferenceSetModulo B (p ^ 2 + p + 1)

For small Sidon sets, we can check the conjecture directly.