Tournaments, \(\bar\omega \)-criticality, and directed paths
The formal statements of the digraph-theory library, for mathematicians

5.5 No short-path strong counterexample at \(\delta = 3\)

Theorem 5.6 no_short_strong3
✓
#

Uses

Rocq declarations

Lemma no_short_strong3 (H : orientedDigraph) :
  (forall v : H, outdeg v = 3) -> 0 < #|H| -> strongb H ->
  ell H <= 5 -> False.

Source: theories/applications/ck3/ck3_main.v:28

Decoded. There is no strong oriented digraph with \(\delta ^+ \ge 3\) and \(\ell \le 5\): the reduction target of the main theorem, stated separately.