[proofplan]
We prove that for fixed $n$, the set of irreducible uniform covers of $[n]$ is finite. The argument proceeds in two steps: first, we represent each cover by its multiplicity function $\psi: \mathcal{P}([n]) \to \mathbb{Z}_{\geq 0}$ and show that the irreducible covers form an antichain in $\mathbb{Z}_{\geq 0}^{2^n}$ under the componentwise partial order. Second, we invoke Dickson's lemma, which states that $\mathbb{Z}_{\geq 0}^m$ contains no infinite antichains, to conclude finiteness.
[/proofplan]
[step:Represent covers by multiplicity functions in $\mathbb{Z}_{\geq 0}^{2^n}$]
Fix $n$ and enumerate the subsets of $[n]$ as $S_1, S_2, \ldots, S_{2^n}$. A uniform cover $\mathcal{A}$ of $[n]$ is a multiset of subsets of $[n]$. We encode $\mathcal{A}$ by its multiplicity function
\begin{align*}
\psi_{\mathcal{A}}: \mathcal{P}([n]) &\to \mathbb{Z}_{\geq 0}, \\
S &\mapsto \text{the number of times } S \text{ appears in } \mathcal{A}.
\end{align*}
The uniformity condition (every $i \in [n]$ belongs to exactly $k$ members of $\mathcal{A}$) translates to: for each $i \in [n]$,
\begin{align*}
\sum_{\substack{S \subseteq [n] \\ i \in S}} \psi_{\mathcal{A}}(S) = k.
\end{align*}
We identify $\psi_{\mathcal{A}}$ with a vector in $\mathbb{Z}_{\geq 0}^{2^n}$ (via the enumeration of $\mathcal{P}([n])$) and define the componentwise partial order: $\psi_{\mathcal{A}} \leq \psi_{\mathcal{B}}$ if $\psi_{\mathcal{A}}(S) \leq \psi_{\mathcal{B}}(S)$ for all $S \subseteq [n]$. Write $\psi_{\mathcal{A}} < \psi_{\mathcal{B}}$ if $\psi_{\mathcal{A}} \leq \psi_{\mathcal{B}}$ with strict inequality for at least one $S$.
[/step]
[step:Show that the irreducible covers form an antichain]
[claim:Irreducible covers are incomparable under the componentwise order]
If $\mathcal{A}$ and $\mathcal{B}$ are both irreducible uniform covers of $[n]$ with $\psi_{\mathcal{A}} < \psi_{\mathcal{B}}$, then $\mathcal{B}$ is reducible, contradicting the hypothesis.
[/claim]
[proof]
Suppose $\psi_{\mathcal{A}} < \psi_{\mathcal{B}}$, so $\psi_{\mathcal{A}}(S) \leq \psi_{\mathcal{B}}(S)$ for all $S$ with strict inequality for some $S$. Define the difference multiset $\mathcal{C}$ by $\psi_{\mathcal{C}}(S) := \psi_{\mathcal{B}}(S) - \psi_{\mathcal{A}}(S) \geq 0$ for all $S$.
We verify that $\mathcal{C}$ is itself a uniform cover of $[n]$. Suppose $\mathcal{A}$ is a uniform $k_1$-cover and $\mathcal{B}$ is a uniform $k_2$-cover. For each $i \in [n]$:
\begin{align*}
\sum_{\substack{S \subseteq [n] \\ i \in S}} \psi_{\mathcal{C}}(S) = \sum_{\substack{S \subseteq [n] \\ i \in S}} \bigl(\psi_{\mathcal{B}}(S) - \psi_{\mathcal{A}}(S)\bigr) = k_2 - k_1.
\end{align*}
Since $\psi_{\mathcal{A}} < \psi_{\mathcal{B}}$ (so $\psi_{\mathcal{C}} \neq 0$), we have $k_2 > k_1$ (if $k_2 = k_1$, then $\sum \psi_{\mathcal{C}}(S) = 0$ for all $i$, forcing $\psi_{\mathcal{C}} = 0$, since every non-empty $S$ contains some $i$). Thus $\mathcal{C}$ is a uniform $(k_2 - k_1)$-cover of $[n]$, and $\mathcal{C}$ is non-empty.
Since $\mathcal{B} = \mathcal{A} \cup \mathcal{C}$ (as a multiset union, meaning $\psi_{\mathcal{B}} = \psi_{\mathcal{A}} + \psi_{\mathcal{C}}$), and both $\mathcal{A}$ and $\mathcal{C}$ are uniform covers, $\mathcal{B}$ is the disjoint union of two uniform covers. By definition, $\mathcal{B}$ is reducible.
[/proof]
Therefore no two distinct irreducible covers satisfy $\psi_{\mathcal{A}} < \psi_{\mathcal{B}}$, which means the set of multiplicity vectors $\{\psi_{\mathcal{A}} : \mathcal{A} \text{ is an irreducible uniform cover of } [n]\}$ is an antichain in the poset $(\mathbb{Z}_{\geq 0}^{2^n}, \leq)$.
[guided]
The key observation is that reducibility of a cover $\mathcal{B}$ corresponds to $\mathcal{B}$ being "decomposable" as a multiset sum of two non-trivial uniform covers. If $\mathcal{A}$ is a uniform cover with $\psi_{\mathcal{A}} \leq \psi_{\mathcal{B}}$ componentwise, then $\mathcal{A}$ can be "subtracted" from $\mathcal{B}$ to produce a remainder $\mathcal{C} = \mathcal{B} \setminus \mathcal{A}$, and the uniformity of $\mathcal{A}$ and $\mathcal{B}$ guarantees uniformity of $\mathcal{C}$.
This means: if an irreducible cover $\mathcal{B}$ sits above another irreducible cover $\mathcal{A}$ in the componentwise order, then $\mathcal{B}$ decomposes as $\mathcal{A} \cup \mathcal{C}$, contradicting irreducibility. So no irreducible cover can sit above another -- the irreducible covers form an antichain.
[/guided]
[/step]
[step:Apply Dickson's lemma to conclude finiteness]
Dickson's lemma states: in the poset $(\mathbb{Z}_{\geq 0}^m, \leq)$ under componentwise ordering, every antichain is finite. (Equivalently, every infinite sequence in $\mathbb{Z}_{\geq 0}^m$ contains an increasing pair.)
We apply Dickson's lemma with $m = 2^n$ (the number of subsets of $[n]$). Since the irreducible uniform covers of $[n]$ form an antichain in $\mathbb{Z}_{\geq 0}^{2^n}$, as shown in the previous step, Dickson's lemma guarantees that this antichain is finite.
[guided]
Dickson's lemma is the multidimensional generalisation of the fact that a non-negative integer sequence with no two comparable terms must be finite. In one dimension ($m = 1$), any antichain in $\mathbb{Z}_{\geq 0}$ has at most one element (the ordering is total). In higher dimensions, antichains can be larger but are always finite.
Why does Dickson's lemma apply here? The set $\mathbb{Z}_{\geq 0}^{2^n}$ is a well-quasi-order under $\leq$ (this is exactly the content of Dickson's lemma), meaning every infinite sequence contains an increasing pair $\psi_i \leq \psi_j$ with $i < j$. An antichain, by definition, contains no such pair, so it must be finite.
The finiteness result is not merely a structural curiosity. It is the essential ingredient in the proof of the [Box Theorem (Bollobas--Thomason)](/theorems/2611): the Box Theorem constructs a minimal array satisfying one constraint per irreducible cover. If there were infinitely many irreducible covers, the minimisation problem would involve infinitely many constraints and need not have a solution. Finiteness ensures the constraint system is finite-dimensional, making the minimisation well-posed.
[/guided]
[/step]
