Transitive subtournaments

DefinitionTournaments#✓fully proved

Let \(n \in \mathbb{N}\). A relation \(T\) on \(\{0, \dots, n-1\}\) is a tournament when \(T(x, x)\) holds for no \(x\) and, for all distinct \(x\) and \(y\), exactly one of \(T(x, y)\) and \(T(y, x)\) holds.

def IsTournament {n : ℕ} (T : Fin n → Fin n → Prop) : Prop :=
  (∀ x, ¬ T x x) ∧ ∀ x y, x ≠ y → (T x y ↔ ¬ T y x)

Used by 2

Used byThe Erdős–Hajnal problem for the tournament \(T^*\) · Transitive subtournament number

DefinitionTransitivity on a vertex set#✓fully proved

Let \(n \in \mathbb{N}\), let \(T\) be a relation on \(\{0, \dots, n-1\}\) and let \(S\) be a set of its elements. Then \(T\) is transitive on \(S\) when, for all \(x, y, z \in S\), \(T(x, y)\) and \(T(y, z)\) imply \(T(x, z)\). For a tournament \(T\) this says that the subtournament of \(T\) on \(S\) is transitive.

def IsTransitiveOn {n : ℕ} (T : Fin n → Fin n → Prop) (S : Finset (Fin n)) : Prop :=
  ∀ x ∈ S, ∀ y ∈ S, ∀ z ∈ S, T x y → T y z → T x z

Used by 2

Used byThe Erdős–Hajnal problem for the tournament \(T^*\) · Transitive subtournament number

DefinitionTransitive subtournament number#✓fully proved

For \(n \in \mathbb{N}\), \(f(n)\) is the largest \(m\) such that every tournament \(T\) on \(\{0, \dots, n-1\}\) is transitive on some set of exactly \(m\) vertices, that is, contains a transitive subtournament on \(m\) vertices.

Such \(m\) exist (for instance \(m = 0\)) and are at most \(n\), so the largest one exists.

noncomputable def transitiveSubtournamentNumber (n : ℕ) : ℕ :=
  sSup {m : ℕ | ∀ T : Fin n → Fin n → Prop, IsTournament T →
    ∃ S : Finset (Fin n), S.card = m ∧ IsTransitiveOn T S}

Uses 2 · Used by 1

Statement usesTournaments · Transitivity on a vertex set

Used byErdős Problem 1216 (the Erdős–Moser formula)

DefinitionErdős Problem 1216 (the Erdős–Moser formula)#✓fully proved

For every \(n \ge 1\), \(f(n) = \lfloor \log_2 n \rfloor + 1\), where \(f(n)\) is the largest \(m\) such that every tournament on \(n\) vertices contains a transitive subtournament on \(m\) vertices.

def transitiveSubtournamentNumberEqLogTwo : Prop :=
  ∀ n : ℕ, 1 ≤ n → transitiveSubtournamentNumber n = Nat.log 2 n + 1

Uses 1 · Used by 1

Statement usesTransitive subtournament number

Used byErdős Problem 1216 is false

TheoremErdős Problem 1216 is false#●ready to prove

It is not the case that \(f(n) = \lfloor \log_2 n \rfloor + 1\) for every \(n \ge 1\), where \(f(n)\) is the largest \(m\) such that every tournament on \(n\) vertices contains a transitive subtournament on \(m\) vertices.

Reid and Parker proved \(f(n) \ge \lfloor \log_2 n + 4 - \log_2 7 \rfloor\) for all \(n \ge 14\); at \(n = 14\) this gives \(f(14) \ge 5 > 4 = \lfloor \log_2 14 \rfloor + 1\), while Stearns' bound \(f(n) \ge \lfloor \log_2 n \rfloor + 1\) holds for every \(n \ge 1\).

public theorem_wanted transitiveSubtournamentNumberEqLogTwo_refuted :
    ¬ transitiveSubtournamentNumberEqLogTwo

Sources

• T. F. Bloom, Erdős Problems, Problem #1216, https://www.erdosproblems.com/1216 (status DISPROVED); resolution: K. B. Reid and E. T. Parker, Disproof of a conjecture of Erdős and Moser on tournaments, J. Combinatorial Theory 9 (1970), 225-238, erdosproblems.com/1216: f(n) ≥ ⌊log₂ n + 4 - log₂ 7⌋ for all n ≥ 14, so f(14) ≥ 5 > ⌊log₂ 14⌋ + 1.

Uses 1

Statement usesErdős Problem 1216 (the Erdős–Moser formula)

DefinitionThe backward arcs of \(T^*\)#✓fully proved

The backward arcs of \(T^*\). The list of ordered pairs \((5, 0)\), \((5, 2)\), \((4, 1)\), \((3, 0)\) of vertices in \(\{0, \dots, 5\}\). These are the arcs of the six-vertex tournament \(T^*\) that go from a larger to a smaller vertex: \(6 \to 1\), \(6 \to 3\), \(5 \to 2\) and \(4 \to 1\) in the source's labelling \(1, \dots, 6\), with every vertex lowered by one.

def tStarBackArcs : List (Fin 6 × Fin 6) :=
  [(5, 0), (5, 2), (4, 1), (3, 0)]

Used by 1

Used byThe six-vertex tournament \(T^*\)

DefinitionThe six-vertex tournament \(T^*\)#✓fully proved

The six-vertex tournament \(T^*\). The tournament \(T^*\) is the relation on the vertex set \(\{0, \dots, 5\}\) with an arc \(i \to j\) if and only if either \((i, j)\) is one of the backward arcs \((5, 0)\), \((5, 2)\), \((4, 1)\), \((3, 0)\), or \(i < j\) and \((j, i)\) is not a backward arc.

def tStar (i j : Fin 6) : Prop :=
  (i, j) ∈ tStarBackArcs ∨ (i < j ∧ (j, i) ∉ tStarBackArcs)

Uses 1 · Used by 1

Statement usesThe backward arcs of \(T^*\)

Used byContaining \(T^*\) as a subtournament

DefinitionContaining \(T^*\) as a subtournament#✓fully proved

Containing \(T^*\) as a subtournament. A relation \(T\) on the vertex set \(\{0, \dots, n-1\}\) contains \(T^*\) when there is an injective map \(f\) from the vertex set \(\{0, \dots, 5\}\) of \(T^*\) to \(\{0, \dots, n-1\}\) such that for all vertices \(i, j\) of \(T^*\), \(i \to j\) in \(T^*\) if and only if \(T(f(i), f(j))\) holds.

def ContainsTStar {n : ℕ} (T : Fin n → Fin n → Prop) : Prop :=
  ∃ f : Fin 6 → Fin n, Function.Injective f ∧ ∀ i j, tStar i j ↔ T (f i) (f j)

Uses 1 · Used by 1

Statement usesThe six-vertex tournament \(T^*\)

Used byThe Erdős–Hajnal problem for the tournament \(T^*\)

DefinitionThe Erdős–Hajnal problem for the tournament \(T^*\)#✓fully proved

The Erdős–Hajnal problem for the tournament \(T^*\). There is a real number \(\varepsilon > 0\) such that for every natural number \(n\) and every tournament \(T\) on the vertex set \(\{0, \dots, n-1\}\) that does not contain \(T^*\) as a subtournament, there is a set \(S\) of vertices on which \(T\) is transitive with \(|S| \ge n^{\varepsilon}\).

This is Problem 1.12 of the AimPL problem list on graph Ramsey theory.

def tStarErdosHajnal : Prop :=
  ∃ ε : ℝ, 0 < ε ∧ ∀ (n : ℕ) (T : Fin n → Fin n → Prop), IsTournament T → ¬ ContainsTStar T →
    ∃ S : Finset (Fin n), IsTransitiveOn T S ∧ (n : ℝ) ^ ε ≤ S.card

Uses 3 · Used by 1

Statement usesContaining \(T^*\) as a subtournament · Tournaments · Transitivity on a vertex set

Used byNguyen–Scott–Seymour: \(T^*\) has the Erdős–Hajnal property

TheoremNguyen–Scott–Seymour: \(T^*\) has the Erdős–Hajnal property#●ready to prove

Nguyen–Scott–Seymour: \(T^*\) has the Erdős–Hajnal property. There is a real number \(\varepsilon > 0\) such that for every natural number \(n\) and every tournament \(T\) on the vertex set \(\{0, \dots, n-1\}\) that does not contain \(T^*\) as a subtournament, there is a set \(S\) of vertices on which \(T\) is transitive with \(|S| \ge n^{\varepsilon}\).

Resolved true: Nguyen, Scott and Seymour prove that every two-colourable tournament has the Erdős–Hajnal property, "which completes the verification of the conjecture for six-vertex tournaments"; Berger, Choromanski and Chudnovsky had proved it for every tournament on at most six vertices except T* (the remark recorded with the problem), and T* is two-colourable ({1, 2, 3} and {4, 5, 6} are transitive).

public theorem_wanted tStarErdosHajnal_holds : tStarErdosHajnal

Sources

• AimPL: Graph Ramsey Theory, Problem 1.12 [Maria Chudnovsky], http://aimpl.org/graphramsey/1/; resolution: T. Nguyen, A. Scott and P. Seymour, Induced subgraph density. VI. Bounded VC-dimension, Adv. Math. 482 (2025), 110601, arXiv:2312.15572, abstract and introduction, https://arxiv.org/abs/2312.15572.

Uses 1

Statement usesThe Erdős–Hajnal problem for the tournament \(T^*\)

8 fully proved2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.