3.2 \(k = 3\): infinitely many, and Question 5.9 fails
Theorem conjecture_5_10_at_k3 (N : nat) : exists T : tournament, kcritical 3 T /\ (N < #|T|)%N.
Source: theories/applications/unified.v:33
Decoded. First statement: for every \(N\) there is a 3-critical tournament on more than \(N\) vertices (the witness is \(\mathrm{AC}_n\) itself, \(n = 2\max (2,N){+}3\)). Second: moreover the witness can be chosen so that its only subtournament with \(\bar\omega \ge 3\) is the whole tournament — formally, any vertex subset \(S\) whose induced subtournament has \(\bar\omega \ge 3\) must be all of \(V\) ([set: T] is the full set). Hence no function \(\ell (3)\) as in Question 5.9 can exist: witnesses have unbounded size but no proper witnessing subtournament at all.
Theorem question_5_9_fails_at_k3 (L : nat) :
exists T : tournament,
[/\ kcritical 3 T, (L < #|T|)%N
& forall S : {set T}, (3 <= ω̄(sub_tournament S))%N -> S = [set: T]].