Theorem conjecture_5_10_at_345 (k : nat) : (3 <= k <= 5)%N ->
  forall N : nat, exists T : tournament, kcritical k T /\ (N < #|T|)%N.

Source: theories/applications/unified.v:66

Decoded. For every \(k\) with \(3 \le k \le 5\) and every bound \(N\) there exists a \(k\)-\(\bar\omega \)-critical tournament on more than \(N\) vertices: the \(k\)-critical tournaments form an infinite family. (“\(T\) is \(k\)-critical” unfolds per 2.11: \(\bar\omega (T) = k\) and \(\bar\omega (T - v) = k - 1\) for every vertex \(v\).)