4.2 \(\bar\omega (\mathrm{AC}_n) = 3\)
Theorem omegabar_AC : (3 <= m)%N -> ω̄((AC m' : tournament)) = 3.
Source: theories/applications/k5/acn_base.v:374
Decoded. For every odd \(n = 2m+1\) with \(m \ge 3\), the tournament clique number of \(\mathrm{AC}_n\) is exactly \(3\). ((AC m’ : tournament) is \(\mathrm{AC}_n\) viewed as a tournament; the hypothesis 3 <= m is \(m \ge 3\).)