3.3 \(k = 4\)

Theorem 3.4 conjecture_5_10_at_k4

✓

Theorem conjecture_5_10_at_k4 (N : nat) :
  exists T : tournament, kcritical 4 T /\ (N < #|T|)%N.

Source: theories/applications/k4/k4_main.v:74

Decoded. As for \(k = 3\), with witness \(\mathrm{AC}_n[C_3]\) on \(3n\) vertices (2.19; the underlying values \(\bar\omega = 4\), \(\bar\omega (T - v) = 3\) are 4.7, 4.8).

Theorem 3.5 question_5_9_fails_at_k4

✓

Theorem question_5_9_fails_at_k4 (L : nat) :
  exists T : tournament,
    [/\ kcritical 4 T, (L < #|T|)%N
      & forall S : {set T}, (4 <= ω̄(sub_tournament S))%N -> S = [set: T]].

Source: theories/applications/k4/k4_main.v:89