The Paley tournament

This file formalizes Section 2 (THE PALEY TOURNAMENT) of bs_lambda.txt. The abstract interface BSLambda.IsDRTournamentWith lives in BSLambda/Defs/Tournament.lean; here we build the concrete example.

• BSLambda.paleyArc orients the pair {i, j} of elements of ZMod k by i → j iff j - i is a nonzero quadratic residue.
• BSLambda.paleyArc_isDRTournamentWith shows that for a prime k ≡ 3 mod 4 this is a doubly regular tournament with 2 * d + 1 = k and 4 * t + 3 = k; BSLambda.paley_isDR is the case k = 14011, d = 7005, t = 3502 used by the construction.

The mathematical content is the character-sum calculation at the end of Section 2: the Jacobsthal-type identity ∑ z, χ ((z - a) * (z - b)) = -1 for a ≠ b (sum_quadraticChar_mul_sub), together with the two counting corollaries two_mul_card_quadraticChar_eq_one and four_mul_card_quadraticChar_sub_eq_one. Those lemmas mention nothing from this development, so they live in the root namespace alongside Mathlib's quadraticChar API rather than in BSLambda.

Adapted for Lean Pool from Timeroot/BS_Lam at commit 7bd39a8d41ee7910d3296d0477ad18f8fff9d870; ported to Lean Pool with proof and dependency cleanup.

theorem sum_quadraticChar_sub {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (hF : ringChar F ≠ 2) (a : F) : ∑ z : F, (quadraticChar F) (z - a) = 0

The quadratic character sums to zero over any translate of F. (Section 2 of bs_lambda.txt.)

theorem sum_quadraticChar_mul_sub {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (hF : ringChar F ≠ 2) {a b : F} (hab : a ≠ b) : ∑ z : F, (quadraticChar F) ((z - a) * (z - b)) = -1

The Jacobsthal-type identity ∑ z, χ ((z - a) * (z - b)) = -1 for a ≠ b. This is the key identity of the character-sum calculation in Section 2 of bs_lambda.txt.

theorem two_mul_card_quadraticChar_eq_one {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (hF : ringChar F ≠ 2) : 2 * {a : F | (quadraticChar F) a = 1}.card + 1 = Fintype.card F

Exactly half of the nonzero elements of F are quadratic residues; this gives the out-degree (k - 1) / 2 of the Paley tournament. (Section 2 of bs_lambda.txt.)

theorem quadraticChar_sub_swap {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (hneg : (quadraticChar F) (-1) = -1) (a b : F) : (quadraticChar F) (a - b) = -(quadraticChar F) (b - a)

When -1 is a nonresidue, swapping the two arguments of a difference negates the quadratic character. (Section 2 of bs_lambda.txt.)

theorem four_mul_card_quadraticChar_sub_eq_one {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] (hF : ringChar F ≠ 2) (hneg : (quadraticChar F) (-1) = -1) {a b : F} (hab : a ≠ b) : 4 * {z : F | (quadraticChar F) (z - a) = 1 ∧ (quadraticChar F) (z - b) = 1}.card + 3 = Fintype.card F

For a ≠ b, exactly (#F - 3) / 4 elements z satisfy χ (z - a) = χ (z - b) = 1. This is the common-out-neighbour count of the Paley tournament. (Section 2 of bs_lambda.txt.)

def BSLambda.paleyArc (k : ℕ) [Fact (Nat.Prime k)] (i j : ZMod k) : Bool

The Paley tournament on F_k for a prime k ≡ 3 mod 4: i → j iff j - i is a nonzero quadratic residue. (Section 2 of bs_lambda.txt.)

Equations

• BSLambda.paleyArc k i j = decide ((quadraticChar (ZMod k)) (j - i) = 1)

theorem BSLambda.prime_14011 : Nat.Prime 14011

k = 14011 is prime. (Section 2 of bs_lambda.txt.)

instance BSLambda.factPrime14011 : Fact (Nat.Prime 14011)

theorem BSLambda.ringChar_zmod14011 : ringChar (ZMod 14011) ≠ 2

The characteristic of F_14011 is not 2. (Section 2 of bs_lambda.txt.)

theorem BSLambda.quadraticChar_neg_one_zmod14011 : (quadraticChar (ZMod 14011)) (-1) = -1

Since 14011 ≡ 3 mod 4, the element -1 is a nonresidue in F_14011; this is what makes the Paley orientation a tournament. (Section 2 of bs_lambda.txt.)

theorem BSLambda.paleyArc_isDRTournamentWith {k d t : ℕ} [Fact (Nat.Prime k)] (hchar : ringChar (ZMod k) ≠ 2) (hneg : (quadraticChar (ZMod k)) (-1) = -1) (hd : 2 * d + 1 = k) (ht : 4 * t + 3 = k) : IsDRTournamentWith (paleyArc k) d t

The Paley tournament is doubly regular. If F_k has odd characteristic and -1 is a nonresidue in it — equivalently, k ≡ 3 mod 4 — then the Paley orientation of F_k is a doubly regular tournament with out-degree d = (k - 1) / 2 and t = (k - 3) / 4 common neighbours. (Section 2 of bs_lambda.txt.)

theorem BSLambda.paley_isDR : IsDRTournamentWith (paleyArc 14011) 7005 3502

The Paley tournament on F_14011 is doubly regular with d = 7005 and t = 3502. (Section 2 of bs_lambda.txt.)