4.1 \(\mathrm{AC}_n\) is 3-critical; its basic stats
Theorem AC_kcritical3 : (3 <= m)%N -> kcritical 3 (AC m' : tournament).
Source: theories/applications/k5/acn_base.v:431
Decoded. \(\mathrm{AC}_n\) is \(3\)-\(\bar\omega \)-critical (2.11), has exactly \(n\) vertices, and is vertex-transitive (2.15).