Challenge 3: the Caccetta–Häggkvist conjecture at parameter $r$

For every natural number $r$, the proposition $\operatorname{statement}_{03}(r)$ is defined to be, with no change whatsoever, the proposition $\operatorname{CH}(r)$ (CaccettaHaggkvistFor r) from the imported file. Unfolded completely, $\operatorname{statement}_{03}(r)$ asserts:

If $0 < r$, then for every type $V$ in the lowest type universe, every finiteness structure on $V$ (so $V$ is a finite type), every witness that $V$ is nonempty, and every digraph $G$ on $V$ -- a digraph being merely a binary relation $\mathrm{Adj}_G$ on $V$ ("there is an arc from $v$ to $w$") with no axioms -- the following holds. If

1. for every vertex $v$, $\neg\, \mathrm{Adj}_G(v,v)$ (no loops), and
2. for every vertex $v$, $\; r \le \operatorname{ncard}\{\, w \in V \mid \mathrm{Adj}_G(v,w) \,\}$, where $\operatorname{ncard}$ is the natural-number cardinality of a set (the number of elements of a finite set; junk value $0$ for an infinite set, which cannot occur here because $V$ is finite),

then there exists a natural number $\ell$ such that

where $|V|$ is the number of elements of $V$, the arithmetic is on natural numbers (only multiplication and addition, no truncation), and $\operatorname{HasCycle}_G(\ell)$ means: there is an injective map $f : \{0, \dots, \ell - 1\} \to V$ (so $f_0, \dots, f_{\ell-1}$ are pairwise distinct) such that for every $i \in \{0, \dots, \ell-1\}$ the arc $\mathrm{Adj}_G(f_i, f_{i+1 \bmod \ell})$ is present; that is, $\ell$ distinct vertices $v_0 \to v_1 \to \cdots \to v_{\ell - 1} \to v_0$ joined by arcs in that direction, with nothing required about other arcs among them.

Edge cases carried over from the definition: $\operatorname{statement}_{03}(0)$ is true unconditionally because $0 < 0$ fails. For $r \ge 1$, the inequality $\ell r < |V| + r$ is equivalent to $(\ell - 1) r < |V|$, i.e. $\ell \le \lceil |V|/r \rceil$. Looplessness bounds every out-degree by $|V| - 1$, so when $r \ge |V|$ hypothesis 2 is unsatisfiable and the claim holds vacuously for that $V$. The clause $2 \le \ell$ excludes the length-$0$ "cycle" (which every digraph has vacuously) and the length-$1$ cycle (a loop); a length-$2$ cycle is a pair of distinct vertices with arcs in both directions. The digraph may contain, for distinct $u, w$, both arcs $u \to w$ and $w \to u$; in-degrees are unconstrained.