Out-degree, directed cycles and the Caccetta–Häggkvist statement at out-degree $r$

This file introduces three definitions. Throughout, a digraph $G$ on a vertex type $V$ is Mathlib's notion: nothing more than a binary relation $\mathrm{Adj}_G$ on $V$, where $\mathrm{Adj}_G(v,w)$ reads "there is an arc from $v$ to $w$". No axiom is imposed on this relation: loops $\mathrm{Adj}_G(v,v)$ are permitted, arcs in both directions between two vertices are permitted, and $V$ is not required to be finite.

Definition 1 (out-degree). For every type $V$ (in any universe), every digraph $G$ on $V$ and every vertex $v \in V$, the out-degree of $v$ is the natural number

where $\operatorname{ncard}$ is Mathlib's natural-number cardinality of a set: it is the number of elements when the set is finite, and it takes the junk value $0$ when the set is infinite. Hence a vertex with infinitely many out-neighbours has out-degree $0$. If $\mathrm{Adj}_G(v,v)$ holds, then $v$ is counted among its own out-neighbours. No hypothesis on $G$ or $V$ is needed for this definition.

Definition 2 (having a cycle of a given length). For every type $V$ (in any universe), every digraph $G$ on $V$ and every natural number $\ell$ (including $\ell = 0$), the proposition $\operatorname{HasCycle}_G(\ell)$ asserts:

there exists a function $f : \{0, 1, \dots, \ell-1\} \to V$ which is injective (the $\ell$ values $f_0, \dots, f_{\ell-1}$ are pairwise distinct) and such that for every index $i \in \{0, \dots, \ell-1\}$ the arc $\mathrm{Adj}_G\big(f_i,\, f_{\rho(i)}\big)$ is present, where $\rho$ is the cyclic shift of the index set: $\rho(i) = i+1$ for $i < \ell - 1$ and $\rho(\ell - 1) = 0$ (i.e. $\rho(i) = i + 1 \bmod \ell$; for $\ell \le 1$ the shift is the identity).

For $\ell \ge 2$ this says: $G$ contains $\ell$ pairwise distinct vertices $v_0, v_1, \dots, v_{\ell-1}$ with the arcs $v_0 \to v_1 \to \cdots \to v_{\ell-1} \to v_0$, each in the stated direction. Nothing is required about the absence of further arcs among these vertices (chords, reverse arcs); only the $\ell$ listed arcs must exist. Edge cases, exactly as the definition stands:

• $\ell = 0$: the index set is empty, the empty function is injective and the arc condition is vacuous, so $\operatorname{HasCycle}_G(0)$ is true for every digraph, even one with no vertices.
• $\ell = 1$: the shift is the identity, so the condition is "there is a vertex $v_0$ with a loop $\mathrm{Adj}_G(v_0, v_0)$".
• $\ell = 2$: two distinct vertices $v_0 \neq v_1$ with both $\mathrm{Adj}_G(v_0, v_1)$ and $\mathrm{Adj}_G(v_1, v_0)$.
• If $V$ has fewer than $\ell$ elements, no injective $f$ exists and the proposition is false.

Definition 3 (the conjecture at a given minimum out-degree). For every natural number $r$, $\operatorname{CH}(r)$ (the file's CaccettaHaggkvistFor r) is the following proposition:

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$, if

1. $G$ is loopless, i.e. for every vertex $v$, $\neg\, \mathrm{Adj}_G(v,v)$, and
2. for every vertex $v$, $\; r \le \operatorname{outDeg}_G(v)$ (out-degree as in Definition 1),

then there exists a natural number $\ell$ with

where $|V|$ is the number of elements of the finite type $V$, and the inequality is between natural numbers built only from multiplication and addition (no truncated subtraction or division occurs).

What the quantifiers silently include:

• For $r = 0$ the antecedent $0 < r$ is false, so $\operatorname{CH}(0)$ is true unconditionally.
• For $r \ge 1$ and natural $\ell$, the condition $\ell r < |V| + r$ is equivalent to $(\ell - 1)\, r < |V|$, i.e. to $\ell \le \lceil |V| / r \rceil$.
• Since $V$ is finite, every out-neighbourhood is finite, so in hypothesis 2 the out-degree is the honest count of out-neighbours and the junk value $0$ of $\operatorname{ncard}$ does not arise. Since $G$ is loopless, every out-degree is at most $|V| - 1$; thus if $r \ge |V|$ no digraph on $V$ satisfies hypothesis 2 and the implication holds vacuously for that $V$. (Correspondingly, $2 \le \ell$ together with $\ell r < |V| + r$ forces $r < |V|$.)
• The requirement $2 \le \ell$ excludes from the conclusion the always-true case $\ell = 0$ and the loop case $\ell = 1$ of Definition 2; the asserted cycle must consist of at least two distinct vertices. (Loops are in any case ruled out by hypothesis 1.)
• $V$ ranges only over types in the lowest universe, and $|V| \ge 1$ because of the nonemptiness assumption. The finiteness structure and the nonemptiness witness are universally quantified typeclass arguments.
• No hypothesis concerns in-degrees, and apart from looplessness nothing makes $G$ "simple": for distinct $u, w$ both arcs $u \to w$ and $w \to u$ may be present, and such a pair is by Definition 2 a cycle of length $2$.