Caccetta–Häggkvist conjecture

The theorem asserts: for every natural number $r$, the proposition $\operatorname{statement}_{03}(r)$ holds, where $\operatorname{statement}_{03}(r)$ is by definition exactly $\operatorname{CH}(r)$ (CaccettaHaggkvistFor r). The declaration carries a placeholder in place of a proof; it states the proposition without proving it. Unfolding everything, the theorem claims:

For every natural number $r$: 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$, read "there is an arc from $v$ to $w$", with no axioms -- 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 (its number of elements when finite, junk value $0$ when infinite -- which cannot occur here since $V$ is finite),

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

Here $|V|$ is the number of elements of $V$, the arithmetic is on natural numbers (multiplication and addition only, so no truncation), and $\operatorname{HasCycle}_G(\ell)$ means: there is an injective map $f : \{0, \dots, \ell-1\} \to V$ (the values $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 -- i.e. $\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 said about other arcs among them.

Since $r$ ranges over all natural numbers with no upper bound, this is a single statement covering every $r \ge 1$ simultaneously (the case $r = 0$ is included but holds trivially, as $0 < 0$ is false). 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$. For a given finite $V$ with $|V| \le r$, looplessness makes every out-degree at most $|V| - 1 < r$, so hypothesis 2 cannot hold and the claim for that $V$ is vacuous; the substantive content is for $1 \le r < |V|$. The clause $2 \le \ell$ excludes the length-$0$ cycle (which every digraph has vacuously) and the length-$1$ cycle (a loop, excluded anyway by hypothesis 1); a cycle of length $2$ is two distinct vertices with arcs in both directions, and such opposite arcs are not forbidden by any hypothesis. In-degrees are unconstrained, and $V$ ranges only over types in the lowest universe, with $|V| \ge 1$ guaranteed by the nonemptiness assumption.