5.1 The \(\delta = 3\) path theorem

Theorem 5.1 ck_conj1_delta3

✓

Theorem ck_conj1_delta3 (D : orientedDigraph) :
  0 < #|D| -> (forall v : D, 3 <= outdeg v) -> 6 <= ell D.

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

Decoded. Let \(D\) be any nonempty finite oriented digraph in which every vertex has out-degree at least \(3\). Then \(\ell (D) \ge 6\) (2.22): \(D\) contains a directed simple path with \(6\) arcs (7 distinct vertices). The second form unfolds \(\ell \) into the explicit existence of such a path (2.21). This is the \(k = 3\) case of Cheng–Keevash Conjecture 1.

Theorem 5.2 ck_conj1_delta3_path

✓

Corollary ck_conj1_delta3_path (D : orientedDigraph) :
  0 < #|D| -> (forall v : D, 3 <= outdeg v) ->
  exists x : D, exists s : seq D, dipath x s /\ size s = 6.

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