Doubly regular tournaments

A tournament on an index type ι is an orientation of the complete graph, encoded here as a function Arc : ι → ι → Bool. This file sets up the neighbourhood Finsets of such an Arc and the parametrised predicate saying that it is doubly regular.

Main definitions:

• IsTournament Arc — Arc has no loops and joins any two distinct vertices by exactly one arc;
• outNbrs Arc i / inNbrs Arc i — the out- and in-neighbours of i;
• commonOut Arc i j / commonIn Arc i j — their pairwise intersections;
• middles Arc u v — the vertices l with u → l → v;
• IsDRTournamentWith Arc d t — Arc is a doubly regular tournament with out-degree d and with t common out-neighbours and t common in-neighbours for every pair of distinct vertices.

IsDRTournamentWith follows the shape of Mathlib's SimpleGraph.IsSRGWith: the arc relation and the numeric parameters are arguments, not fields, so that lemmas stated about a bare Arc can consume it without being rephrased. The material is organised by hypothesis strength: first what needs no finiteness, then what needs Fintype ι, then what needs DecidableEq ι as well.

This file corresponds to Section 2 of bs_lambda.txt; the Paley tournament realising these axioms is built in BSLambda/Paley/Tournament.lean.

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

structure BSLambda.IsTournament {ι : Type u_1} (Arc : ι → ι → Bool) : Prop

IsTournament Arc: the relation Arc orients the complete graph on ι, i.e. there are no loops and any two distinct vertices are joined by exactly one arc.

• arc_self (i : ι) : Arc i i = false

  There is no arc from a vertex to itself.

• arc_eq_not_arc {i j : ι} : i ≠ j → Arc i j = !Arc j i

  Distinct vertices are joined by exactly one arc.

theorem BSLambda.IsTournament.ne_of_arc {ι : Type u_1} {Arc : ι → ι → Bool} (h : IsTournament Arc) {i j : ι} (hij : Arc i j = true) : i ≠ j

The endpoints of an arc are distinct.

theorem BSLambda.IsTournament.ne_of_arc' {ι : Type u_1} {Arc : ι → ι → Bool} (h : IsTournament Arc) {i j : ι} (hij : Arc i j = true) : j ≠ i

The endpoints of an arc are distinct. The primed name follows Mathlib's LT.lt.ne' convention: the conclusion is j ≠ i, the reverse of BSLambda.IsTournament.ne_of_arc.

theorem BSLambda.IsTournament.arc_eq_false_of_arc {ι : Type u_1} {Arc : ι → ι → Bool} (h : IsTournament Arc) {i j : ι} (hij : Arc i j = true) : Arc j i = false

Asymmetry in the Bool-equation form consumed by the certificate-conflict lemmas: an arc i → j forces Arc j i = false.

theorem BSLambda.IsTournament.arc_asymm {ι : Type u_1} {Arc : ι → ι → Bool} (h : IsTournament Arc) {i j : ι} (hij : Arc i j = true) : ¬Arc j i = true

The arc relation of a tournament is asymmetric.

theorem BSLambda.IsTournament.arc_or_arc {ι : Type u_1} {Arc : ι → ι → Bool} (h : IsTournament Arc) {i j : ι} (hij : i ≠ j) : Arc i j = true ∨ Arc j i = true

Any two distinct vertices of a tournament are joined by an arc.

theorem BSLambda.IsTournament.arc_of_not_arc {ι : Type u_1} {Arc : ι → ι → Bool} (h : IsTournament Arc) {i j : ι} (hij : i ≠ j) (hji : Arc j i = false) : Arc i j = true

The Bool-equation form of BSLambda.IsTournament.arc_or_arc: if j does not beat i then i beats j.

def BSLambda.outNbrs {ι : Type u_1} [Fintype ι] (Arc : ι → ι → Bool) (i : ι) : Finset ι

The out-neighbours of i: the vertices j with an arc i → j.

Equations

• BSLambda.outNbrs Arc i = {j : ι | Arc i j = true}

def BSLambda.inNbrs {ι : Type u_1} [Fintype ι] (Arc : ι → ι → Bool) (i : ι) : Finset ι

The in-neighbours of i: the vertices j with an arc j → i.

Equations

• BSLambda.inNbrs Arc i = {j : ι | Arc j i = true}

@[simp]

theorem BSLambda.mem_outNbrs {ι : Type u_1} [Fintype ι] {Arc : ι → ι → Bool} {i j : ι} : j ∈ outNbrs Arc i ↔ Arc i j = true

@[simp]

theorem BSLambda.mem_inNbrs {ι : Type u_1} [Fintype ι] {Arc : ι → ι → Bool} {i j : ι} : j ∈ inNbrs Arc i ↔ Arc j i = true

theorem BSLambda.sum_card_outNbrs_eq_sum_card_inNbrs {ι : Type u_1} [Fintype ι] (Arc : ι → ι → Bool) : ∑ x : ι, (outNbrs Arc x).card = ∑ x : ι, (inNbrs Arc x).card

Counting the arcs of Arc by tail and by head.

theorem BSLambda.IsTournament.disjoint_outNbrs_inNbrs {ι : Type u_1} [Fintype ι] {Arc : ι → ι → Bool} (h : IsTournament Arc) (v : ι) : Disjoint (outNbrs Arc v) (inNbrs Arc v)

The out-neighbourhood and the in-neighbourhood of a vertex are disjoint.

def BSLambda.commonOut {ι : Type u_1} [Fintype ι] [DecidableEq ι] (Arc : ι → ι → Bool) (i j : ι) : Finset ι

The common out-neighbours of i and j.

Equations

• BSLambda.commonOut Arc i j = BSLambda.outNbrs Arc i ∩ BSLambda.outNbrs Arc j

def BSLambda.commonIn {ι : Type u_1} [Fintype ι] [DecidableEq ι] (Arc : ι → ι → Bool) (i j : ι) : Finset ι

The common in-neighbours of i and j.

Equations

• BSLambda.commonIn Arc i j = BSLambda.inNbrs Arc i ∩ BSLambda.inNbrs Arc j

def BSLambda.middles {ι : Type u_1} [Fintype ι] [DecidableEq ι] (Arc : ι → ι → Bool) (u v : ι) : Finset ι

The middle vertices of the arc u → v: those l with u → l → v.

Equations

• BSLambda.middles Arc u v = BSLambda.outNbrs Arc u ∩ BSLambda.inNbrs Arc v

@[simp]

theorem BSLambda.mem_commonOut {ι : Type u_1} [Fintype ι] [DecidableEq ι] {Arc : ι → ι → Bool} {i j l : ι} : l ∈ commonOut Arc i j ↔ Arc i l = true ∧ Arc j l = true

@[simp]

theorem BSLambda.mem_commonIn {ι : Type u_1} [Fintype ι] [DecidableEq ι] {Arc : ι → ι → Bool} {i j l : ι} : l ∈ commonIn Arc i j ↔ Arc l i = true ∧ Arc l j = true

@[simp]

theorem BSLambda.mem_middles {ι : Type u_1} [Fintype ι] [DecidableEq ι] {Arc : ι → ι → Bool} {l u v : ι} : l ∈ middles Arc u v ↔ Arc u l = true ∧ Arc l v = true

theorem BSLambda.sum_card_commonOut_eq_sum_card_middles {ι : Type u_1} [Fintype ι] [DecidableEq ι] (Arc : ι → ι → Bool) (u : ι) : ∑ y ∈ outNbrs Arc u, (commonOut Arc u y).card = ∑ y ∈ outNbrs Arc u, (middles Arc u y).card

Counting the arcs inside the out-neighbourhood of u by tail and by head: a pure double-counting identity, with no regularity assumption on Arc.

theorem BSLambda.IsTournament.outNbrs_union_inNbrs {ι : Type u_1} [Fintype ι] [DecidableEq ι] {Arc : ι → ι → Bool} (h : IsTournament Arc) (v : ι) : outNbrs Arc v ∪ inNbrs Arc v = Finset.univ.erase v

The out- and in-neighbours of v are exactly the vertices other than v.

theorem BSLambda.IsTournament.card_outNbrs_add_card_inNbrs {ι : Type u_1} [Fintype ι] {Arc : ι → ι → Bool} (h : IsTournament Arc) (v : ι) : (outNbrs Arc v).card + (inNbrs Arc v).card + 1 = Fintype.card ι

Out-neighbours and in-neighbours of a vertex partition the remaining vertices.

structure BSLambda.IsDRTournamentWith {ι : Type u_1} [Fintype ι] [DecidableEq ι] (Arc : ι → ι → Bool) (d t : ℕ) extends BSLambda.IsTournament Arc : Prop

IsDRTournamentWith Arc d t: Arc is a doubly regular tournament — a tournament in which every vertex has out-degree d, and every two distinct vertices have t common out-neighbours and t common in-neighbours. (Section 2 of bs_lambda.txt.)

• arc_self (i : ι) : Arc i i = false
• arc_eq_not_arc {i j : ι} : i ≠ j → Arc i j = !Arc j i
• card_outNbrs (i : ι) : (outNbrs Arc i).card = d

  Every vertex has out-degree d.

• card_commonOut {i j : ι} : i ≠ j → (commonOut Arc i j).card = t

  Distinct vertices have t common out-neighbours.

• card_commonIn {i j : ι} : i ≠ j → (commonIn Arc i j).card = t

  Distinct vertices have t common in-neighbours.

theorem BSLambda.IsDRTournamentWith.card_inNbrs {ι : Type u_1} [Fintype ι] [DecidableEq ι] {Arc : ι → ι → Bool} {d t : ℕ} (h : IsDRTournamentWith Arc d t) (i : ι) : (inNbrs Arc i).card = d

Every vertex of a doubly regular tournament has in-degree d as well.

theorem BSLambda.IsDRTournamentWith.card_eq_two_mul_add_one {ι : Type u_1} [Fintype ι] [DecidableEq ι] {Arc : ι → ι → Bool} {d t : ℕ} (h : IsDRTournamentWith Arc d t) [Nonempty ι] : Fintype.card ι = 2 * d + 1

A doubly regular tournament on a nonempty ι has 2 * d + 1 vertices.

theorem BSLambda.IsDRTournamentWith.card_middles_add_add_one {ι : Type u_1} [Fintype ι] [DecidableEq ι] {Arc : ι → ι → Bool} {d t : ℕ} (h : IsDRTournamentWith Arc d t) {u v : ι} (huv : Arc u v = true) : (middles Arc u v).card + t + 1 = d

Along an arc u → v the out-neighbours of u split into v itself, the middles of the arc, and the t common out-neighbours of u and v.

theorem BSLambda.IsDRTournamentWith.d_pos {ι : Type u_1} [Fintype ι] [DecidableEq ι] {Arc : ι → ι → Bool} {d t : ℕ} (h : IsDRTournamentWith Arc d t) [Nontrivial ι] : 0 < d

A doubly regular tournament with at least two vertices has positive out-degree.

theorem BSLambda.IsDRTournamentWith.d_eq_two_mul_t_add_one {ι : Type u_1} [Fintype ι] [DecidableEq ι] {Arc : ι → ι → Bool} {d t : ℕ} (h : IsDRTournamentWith Arc d t) [Nontrivial ι] : d = 2 * t + 1

A doubly regular tournament with at least two vertices satisfies d = 2 * t + 1; in particular d - 1 - t = t.

theorem BSLambda.IsDRTournamentWith.card_middles {ι : Type u_1} [Fintype ι] [DecidableEq ι] {Arc : ι → ι → Bool} {d t : ℕ} (h : IsDRTournamentWith Arc d t) {u v : ι} [Nontrivial ι] (huv : Arc u v = true) : (middles Arc u v).card = t

In a doubly regular tournament with at least two vertices, every arc u → v has exactly t middle vertices.