4.8 \(\bar\omega (\mathrm{AC}_n[\mathrm{AC}_n]) = 5\)
Theorem omegabar_T5 : ω̄(T5) = 5.
Source: theories/applications/k5/main.v:54
Decoded. T5 abbreviates \(\mathrm{AC}_n[\mathrm{AC}_n]\) (2.20); its tournament clique number is exactly \(5\), for every odd \(n = 2m{+}1 \ge 7\).
Theorem omegabar_T5_del (v : T5) : ω̄(del_tournament v) = 4.
Source: theories/applications/k5/main.v:62
Decoded. Every single-vertex deletion has \(\bar\omega = 4\); hence \(\mathrm{AC}_n[\mathrm{AC}_n]\) is \(5\)-\(\bar\omega \)-critical, on \(n \cdot n\) vertices.
Lemma card_T5 : #|T5| = (n * n)%N.