Challenge 8: Ryser's conjecture for $r$-partite $r$-uniform hypergraphs

Preamble. The file imports the hypergraph definitions (item TenChallenges_Hypergraph) and declares one definition, statement_08, in the namespace TenChallenges.

The definition statement_08. For a natural number $r$ (any $r \in \mathbb{N}$, including $0$ and $1$), $\mathrm{statement}_{08}(r)$ is the proposition: for every type $V$ (ranging over an arbitrary but fixed universe — the definition carries a universe parameter, so it is universe-polymorphic), for every decidable-equality structure on $V$ (a typeclass assumption with no mathematical content), and for every finite hypergraph $H$ on $V$,

Here all the notions are the ones from item TenChallenges_Hypergraph, unfolded as follows.

• A finite hypergraph $H$ on $V$ consists of a finite vertex set $\mathrm{V}(H) \subseteq V$ and a set $\mathrm{E}(H)$ of finite subsets of $V$ (the edges), together with the requirement $e \subseteq \mathrm{V}(H)$ for every $e \in \mathrm{E}(H)$. The vertex set and the edge set may be empty; nothing in the structure excludes the empty edge or edges of mixed sizes.
• $H$ is $r$-uniform iff $|e| = r$ for every $e \in \mathrm{E}(H)$.
• $H$ is $r$-partite iff there exist finite sets $P_0, \dots, P_{r-1} \subseteq V$ such that (1) $v \in \mathrm{V}(H) \iff \exists i,\ v \in P_i$ for every $v \in V$ (so $\bigcup_i P_i = \mathrm{V}(H)$); (2) $P_i \cap P_j = \varnothing$ for all $i \ne j$; (3) $|P_i \cap e| = 1$ for every $e \in \mathrm{E}(H)$ and every $i$. The parts are not required to be nonempty.
• A finite set $C \subseteq V$ is a vertex cover of $H$ iff $C \subseteq \mathrm{V}(H)$ and every edge $e \in \mathrm{E}(H)$ contains some $v \in C$.
• A finite set $M$ of finite subsets of $V$ is a matching of $H$ iff $M \subseteq \mathrm{E}(H)$ and any two distinct members of $M$ are disjoint.
• $\tau(H) = \inf\{\, n \mid \exists C,\ C \text{ is a vertex cover of } H,\ |C| = n \,\}$, with the convention that the infimum of the empty subset of $\mathbb{N}$ is $0$; otherwise it is the least element.
• $\nu(H) = \sup\{\, n \mid \exists M,\ M \text{ is a matching of } H,\ |M| = n \,\}$, with the convention that the supremum of an unbounded subset of $\mathbb{N}$ is $0$; otherwise it is the least upper bound. This set always contains $0$ and is always bounded (a matching is a set of subsets of the finite set $\mathrm{V}(H)$), so $\nu(H)$ is the maximum size of a matching.
• $r - 1$ is truncated natural-number subtraction, but under the hypothesis $2 \le r$ it coincides with ordinary subtraction and is at least $1$.

Edge cases made explicit by the quantifiers. For $r = 0$ and $r = 1$ the hypothesis $2 \le r$ fails, so $\mathrm{statement}_{08}(0)$ and $\mathrm{statement}_{08}(1)$ hold vacuously. For $r \ge 2$, the hypothesis of $r$-uniformity excludes the empty edge (its size is $0 \ne r$), so under the hypotheses every edge is nonempty, $\mathrm{V}(H)$ is a vertex cover, and $\tau(H)$ is the genuine minimum size of a vertex cover (it is $0$ iff $\mathrm{E}(H) = \varnothing$). The hypotheses do not exclude $\mathrm{V}(H) = \varnothing$ or $\mathrm{E}(H) = \varnothing$: in those cases $\tau(H) = \nu(H) = 0$ and the conclusion reads $0 \le 0$. The hypotheses do not exclude a part $P_i$ being empty, which forces $\mathrm{E}(H) = \varnothing$ and again gives $0 \le 0$. The universal quantification over $V$ includes empty and infinite types $V$; only the hypergraph's vertex set is required to be finite. The inequality is non-strict.