def IsPerfectDifferenceSet {N : ℕ} (B : Finset (ZMod N)) : Prop

A perfect difference set is a set where every nonzero element is uniquely representable as a difference of two elements of the set.

Equations

• IsPerfectDifferenceSet B = ∀ (d : ZMod N), d ≠ 0 → ∃! b : ↥B × ↥B, ↑b.1 - ↑b.2 = d

def IsPerfectDifferenceSet.map {N : ℕ} (B : Finset (ZMod N)) (p : ↥B × ↥B ⊕ Unit) : ZMod N ⊕ ↥B

Equations

• IsPerfectDifferenceSet.map B (Sum.inl p_2) = if p_2.1 = p_2.2 then Sum.inr p_2.1 else Sum.inl (↑p_2.1 - ↑p_2.2)
• IsPerfectDifferenceSet.map B (Sum.inr val) = Sum.inl 0

theorem IsPerfectDifferenceSet.card {N : ℕ} [NeZero N] {B : Finset (ZMod N)} (hdiff : IsPerfectDifferenceSet B) : B.card * B.card + 1 = N + B.card

class Mainstep.Hypotheses : Type

We will show that the following hypotheses are inconsistent; this is the bulk of the proof of Theorem 8.

• p : ℕ
• hp : Nat.Prime p
• N : ℕ
• hN : N = p ^ 2 + p + 1
• B : Finset (ZMod N)
• hdiff : IsPerfectDifferenceSet B
• embed : ↥{1, 2, 4, 8} → ↥B
• h_embed (n : ↥{1, 2, 4, 8}) : ↑(embed n) = ↑↑n
• h_inj : Function.Injective embed

theorem Mainstep.h1 [Hypotheses] : 1 ∈ B

theorem Mainstep.h2 [Hypotheses] : 2 ∈ B

theorem Mainstep.h4 [Hypotheses] : 4 ∈ B

theorem Mainstep.h8 [Hypotheses] : 8 ∈ B

theorem Mainstep.h2_ne_1 [Hypotheses] : 2 ≠ 1

theorem Mainstep.h4_ne_1 [Hypotheses] : 4 ≠ 1

theorem Mainstep.h4_ne_8 [Hypotheses] : 4 ≠ 8

theorem Mainstep.hodd [Hypotheses] : Odd N

theorem Mainstep.card_B [Hypotheses] : B.card = p + 1

theorem Mainstep.odd_P [Hypotheses] : Odd p

theorem Mainstep.heven [Hypotheses] : Even B.card

theorem Mainstep.mul_two_inj [Hypotheses] {x y : ZMod N} (h : 2 * x = 2 * y) : x = y

theorem Mainstep.diff_uniq [Hypotheses] {a b c d : ↥B} (ha : a ≠ b) (hsub : ↑a - ↑b = ↑c - ↑d) : a = c ∧ b = d

noncomputable def Mainstep.f [Hypotheses] {a : ZMod N} (ha : a ∉ B) (b : ↥B) : ↥B

Given a perfect difference set B and an element a not in B, the function f (a := a) maps each b ∈ B to the unique c ∈ B such that a - b = c - d for some d ∈ B.

Equations

• Mainstep.f ha b = (Exists.choose ⋯).1

noncomputable def Mainstep.g [Hypotheses] {a : ZMod N} (ha : a ∉ B) (b : ↥B) : ↥B

Though not defined in Theorem 8, it is convenient to also introduce the companion function g (a := a), defined to be the d element such that a - b = f (a := a) ha b - d.

Equations

• Mainstep.g ha b = (Exists.choose ⋯).2

theorem Mainstep.f_def [Hypotheses] {a : ZMod N} (ha : a ∉ B) (b : ↥B) : a - ↑b = ↑(f ha b) - ↑(g ha b)

theorem Mainstep.f_def' [Hypotheses] {a : ZMod N} (ha : a ∉ B) (b c d : ↥B) : a - ↑b = ↑c - ↑d ↔ c = f ha b ∧ d = g ha b

theorem Mainstep.f_inv [Hypotheses] {a : ZMod N} (ha : a ∉ B) : Function.Involutive (f ha)

f (a := a) is an involution.

theorem Mainstep.f_fixed [Hypotheses] {a : ZMod N} {ha : a ∉ B} {b : ↥B} (hb : f ha b = b) : 2 * ↑b = a + ↑(g ha b)

Fixed points of f (a := a) satisfy 2 * f ha b = a + g ha b.

@[implicit_reducible]

noncomputable def Mainstep.z2_vact [Hypotheses] {a : ZMod N} (ha : a ∉ B) : AddAction (ZMod 2) ↥B

Equations

• Mainstep.z2_vact ha = { vadd := fun (i : ZMod 2) (b : ↥Mainstep.B) => if i = 1 then Mainstep.f ha b else b, add_vadd := ⋯, zero_vadd := ⋯ }

theorem Mainstep.f_second_fixed [Hypotheses] {a : ZMod N} {ha : a ∉ B} {b : ↥B} (hb : f ha b = b) : ∃ (c : ↥B), c ≠ b ∧ f ha c = c

If there is one fixed point, there is another.

theorem Mainstep.two_mul_sub_one_notin [Hypotheses] {x : ↥B} (hx : ↑x ≠ 2) : 2 * (↑x - 1) ∉ B

theorem Mainstep.first_fixed [Hypotheses] {x : ↥B} (hx : ↑x ≠ 2) : f ⋯ x = x

theorem Mainstep.second_fixed [Hypotheses] {x : ↥B} (hx : ↑x ≠ 2) : ∃ (b : ↥B), b ≠ x ∧ f ⋯ b = b

noncomputable def Mainstep.b [Hypotheses] (x : ↥B) : ↥B

Equations

• Mainstep.b x = if hx : ↑x = 2 then ⟨2, ⋯⟩ else ⋯.choose

noncomputable def Mainstep.d [Hypotheses] (x : ↥B) : ↥B

Equations

• Mainstep.d x = if hx : ↑x = 2 then ⟨2, ⋯⟩ else Mainstep.g ⋯ ⋯.choose

theorem Mainstep.b_neq [Hypotheses] {x : ↥B} (hx : ↑x ≠ 2) : b x ≠ x

theorem Mainstep.bd_ident [Hypotheses] (x : ↥B) : 2 * ↑(b x) = 2 * (↑x - 1) + ↑(d x)

theorem Mainstep.d_injective [Hypotheses] : Function.Injective d

theorem Mainstep.d_surjective [Hypotheses] : Function.Surjective d

theorem Mainstep.d1_eq_4 [Hypotheses] : d ⟨1, ⋯⟩ = ⟨4, ⋯⟩

theorem Mainstep.d1_eq_8 [Hypotheses] : d ⟨1, ⋯⟩ = ⟨8, ⋯⟩

theorem Mainstep.contradiction [Hypotheses] : False