perfect_difference_set
Provedcombinatoricsnumber-theory
Perfect difference set / cyclic difference set: A (q²+q+1, q+1, 1)-difference set D in ℤ/(q²+q+1)ℤ exists for every prime power q. Equivalent to projective planes. Existence for non-prime-power q (if any projective planes of non-prime-power order exist) is open.
Preamble
import Mathlib
Formal statement
import Mathlib
theorem perfect_difference_set (q : ℕ) (hq : 2 ≤ q) (hpow : ∃ p k : ℕ, Nat.Prime p ∧ q = p ^ k) :
∃ (D : Finset (ZMod (q^2 + q + 1))),
D.card = q + 1 ∧
∀ d : ZMod (q^2 + q + 1), d ≠ 0 →
∃! p : D × D, p.1 ≠ p.2 ∧ p.1.val - p.2.val = d := by
sorrySource