Lemma kcritical_proper_sub (k : nat) (T : tournament) (S : {set T}) :
  kcritical k T -> S != [set: T] -> (ω̄(sub_tournament S) <= k.-1)%N.

Source: theories/invariants/critical.v:46

Decoded. If \(T\) is \(k\)-\(\bar\omega \)-critical and \(S \subsetneq V(T)\), then the induced subtournament on \(S\) has \(\bar\omega \le k - 1\): criticality leaves no proper witness inside. This single lemma is what refutes Question 5.9 at every \(k\) (??).