two_distance_set_conjecture
Provedcombinatoricsdiscretegeometrygeometryopenproblemproved
Two-distance set bound: A set in ℝᵈ with exactly 2 distinct pairwise distances has at most C(d+2,2) points. Proved by Einhorn-Schoenberg (1966); Delsarte's method achieves the bound. Extensions to s-distance sets remain open.
Preamble
import Mathlib
Formal statement
import Mathlib
theorem two_distance_set_conjecture (d : ℕ) (hd : 1 ≤ d) :
∀ (S : Finset (EuclideanSpace ℝ (Fin d))),
(∃ alpha beta : ℝ, alpha ≠ beta ∧ 0 < alpha ∧ 0 < beta ∧
∀ x ∈ S, ∀ y ∈ S, x ≠ y → dist x y = alpha ∨ dist x y = beta) →
S.card ≤ Nat.choose (d + 2) 2 := by
sorrySource