Ryser's conjecture

Preamble. The file imports the definition of $\mathrm{statement}_{08}$ (item TenChallenges_Challenge_08, which in turn imports the hypergraph definitions of item TenChallenges_Hypergraph), fixes a universe variable $u$, and states one theorem, challenge_08, in the namespace TenChallenges. The theorem is stated with its proof left as a placeholder (no proof is given in this file).

The theorem challenge_08. It asserts: for every natural number $r$, $\mathrm{statement}_{08}(r)$ holds, instantiated at universe level $u$. Since $u$ is a universe variable of the theorem, the assertion is made for every universe. Fully unfolded, the theorem states:

For every $r \in \mathbb{N}$, every type $V$ (in universe $u$), every decidable-equality structure on $V$ (a typeclass assumption without mathematical content), and every finite hypergraph $H$ on $V$ — that is, every finite set $\mathrm{V}(H) \subseteq V$ together with a set $\mathrm{E}(H)$ of finite subsets of $V$ such that $e \subseteq \mathrm{V}(H)$ for all $e \in \mathrm{E}(H)$ — the following implication holds:

where:

• $H$ is $r$-partite means: there exist finite sets $P_0, \dots, P_{r-1} \subseteq V$ (indexed by $i \in \{0,\dots,r-1\}$, not required to be nonempty) such that (1) for every $v \in V$, $v \in \mathrm{V}(H)$ iff $v \in P_i$ for some $i$ (so $\bigcup_i P_i = \mathrm{V}(H)$); (2) $P_i \cap P_j = \varnothing$ whenever $i \ne j$; (3) $|P_i \cap e| = 1$ for every edge $e \in \mathrm{E}(H)$ and every index $i$;
• a vertex cover of $H$ is a finite set $C \subseteq \mathrm{V}(H)$ such that every edge $e \in \mathrm{E}(H)$ contains some $v \in C$;
• a matching of $H$ is a finite set $M$ of finite subsets of $V$ with $M \subseteq \mathrm{E}(H)$ and $e_1 \cap e_2 = \varnothing$ for all distinct $e_1, e_2 \in M$;
• $\tau(H)$ is the infimum in $\mathbb{N}$ of $\{\, n \mid \exists C,\ C \text{ is a vertex cover of } H,\ |C| = n \,\}$: the least element if the set is nonempty, $0$ if it is empty;
• $\nu(H)$ is the supremum in $\mathbb{N}$ of $\{\, n \mid \exists M,\ M \text{ is a matching of } H,\ |M| = n \,\}$: the least upper bound if the set is bounded above, $0$ if it is unbounded. This set always contains $0$ (the empty matching) and is always bounded above (a matching is a set of subsets of the finite set $\mathrm{V}(H)$), so $\nu(H)$ is the maximum number of pairwise disjoint edges;
• $r - 1$ is truncated natural-number subtraction, which under $2 \le r$ agrees with ordinary subtraction and is $\ge 1$; the product and the comparison are in $\mathbb{N}$, and the inequality is non-strict.

Edge cases included by the quantifiers. For $r \in \{0, 1\}$ the premise $2 \le r$ is false, so the claim for those $r$ is vacuously true. For $r \ge 2$, $r$-uniformity rules out the empty edge, so every edge is nonempty, $\mathrm{V}(H)$ is a vertex cover, the set defining $\tau(H)$ is nonempty, and $\tau(H)$ is the genuine minimum size of a vertex cover ($\tau(H) = 0$ exactly when $\mathrm{E}(H) = \varnothing$). The claim includes hypergraphs with $\mathrm{V}(H) = \varnothing$ or $\mathrm{E}(H) = \varnothing$, where $\tau(H) = \nu(H) = 0$ and the conclusion is $0 \le 0$; it includes partitions with an empty part $P_i$, which by condition (3) force $\mathrm{E}(H) = \varnothing$. The type $V$ may be empty or infinite; only $\mathrm{V}(H)$ is finite. Nothing in the statement requires the parts $P_i$ to be unique, the hypergraph to be nonempty, or $r$ to be bounded above.