Tournaments, \(\bar\omega \)-criticality, and directed paths
The formal statements of the
digraph-theory
library, for mathematicians
1
How to use this site
2
The Dictionary: every definition you need
3
The unified theorem: Conjecture 5.10 at \(k = 3,4,5\)
▶
3.1
The headline: every \(k \in \{ 3,4,5\} \)
3.2
\(k = 3\): infinitely many, and Question 5.9 fails
3.3
\(k = 4\)
3.4
\(k = 5\)
4
The three critical families
▼
4.1
\(\mathrm{AC}_n\) is 3-critical; its basic stats
4.2
\(\bar\omega (\mathrm{AC}_n) = 3\)
4.3
\(\bar\omega (\mathrm{AC}_n - v) = 2\) for every \(v\)
4.4
\(\mathrm{AC}_n[C_3]\) is 4-critical, on \(3n\) vertices
4.5
\(\bar\omega (\mathrm{AC}_n[C_3]) = 4\)
4.6
\(\bar\omega (\mathrm{AC}_n[C_3] - v) = 3\) for every \(v\)
4.7
\(\bar\omega (\mathrm{AC}_n[\mathrm{AC}_n] - v) = 4\); 5-criticality; order \(n^2\)
4.8
\(\bar\omega (\mathrm{AC}_n[\mathrm{AC}_n]) = 5\)
5
Directed paths: the Cheng–Keevash results
▶
5.1
The \(\delta = 3\) path theorem
5.2
The \(\delta = 2\) case
5.3
Theorem 4, oriented version
5.4
Cheng–Keevash Lemma 7, uniform in \(\delta \)
5.5
No short-path strong counterexample at \(\delta = 3\)
6
General tournament theory
▶
6.1
The substitution lower bound
6.2
Vertex-transitive tournaments: one deletion decides criticality
6.3
Domination bounds the clique number
6.4
\(C_3\) is the unique 2-critical tournament
6.5
Proper subtournaments of critical tournaments
6.6
\(\bar\omega = 1\) exactly for transitive tournaments
Dependency graph
4.7 \(\bar\omega (\mathrm{AC}_n[\mathrm{AC}_n] - v) = 4\); 5-criticality; order \(n^2\)
Theorem
4.10
T5_kcritical5
✓
#
Uses
Definition 2.18
Definition 2.20
Definition 2.1
Definition 2.9
Definition 2.17
Definition 2.11
Definition 2.16
Definition 2.8
Definition 2.10
Definition 2.12
Definition 2.5
Rocq
Rocq declarations
Digraph.applications.k5.main.T5_kcritical5
Theorem T5_kcritical5 : kcritical 5 T5.
Source:
theories/applications/k5/main.v:71