Counting Minimal Covering Systems: F(x) = exp(x^{1+o(1)})

The problem

A distinct covering system is a finite set of congruences $a_i\pmod{n_i}$ with pairwise distinct moduli $1<n_1<\cdots<n_k$ whose classes cover every integer; it is minimal if no proper subset covers. Let $F(x)$ count the minimal distinct covering systems with all moduli in $[1,x]$. Erdős asked to estimate $F(x)$ — he reportedly expected slow growth.

The answer is nearly doubly exponential:

theorem erdos1188_loglog_ratio_tendsto_one :
    Tendsto (fun x => Real.log (Real.log (coveringCount x)) / Real.log x)
      atTop (𝓝 1)

that is, $\log\log F(x)\sim\log x$, equivalently $F(x)=\exp\!\big(x^{1+o(1)}\big)$.

Why matching bounds are the whole game

The upper bound at this scale is straightforward — there are at most $\prod_{n\le x}(n+1)=\exp(O(x\log x))$ ways to pick at most one residue per modulus, and being a covering system only cuts this down. The problem lives entirely in the lower bound: one must construct enormously many genuinely distinct, minimal covering systems with bounded moduli. An earlier squarefree construction here produced a much weaker lower scale, and the first submission was rejected by the independent referee precisely because the lower and upper estimates did not meet. The accepted proof closes that gap with a sparser construction.

The sparse no-axis construction

Classical covering systems lean on a "primorial axis" — congruences whose moduli are products of all small primes — which is rigid and wastes modulus budget. The construction removes it entirely.

Fix base CRT prime coordinates $p_0,\dots,p_{m-1}$ and a closing prime $p_m$. For each late coordinate $i$, set $r_i=\lfloor\log_2(i+1)\rfloor+1$ and a window $h_i=2048\,r_i$, and assign every nonzero residue of $p_i$ injectively to a cross-pair support $\{u,v\}$ with $u<h_i\le v<i$; an explicit prime estimate guarantees enough pairs. Every residue of the closing coordinate receives its own support (empty, singletons, then cross-pairs), with reserved singletons keeping each base spike private — this yields coverage and a private witness for every congruence, which is exactly minimality. CRT transport converts the abstract frame into a minimal distinct integer covering system.

Counting. At every late coordinate the range of the residue-to-support injection is a free choice, and the finished system determines every choice (the family map is injective). This gives at least $2^{E_m}$ systems with $E_m\ge\binom{m-B}{2}$, while every support uses at most three primes of controlled size, so all moduli fit under an explicit cutoff polynomial in $m$ (up to log factors). Interpolating the parametric family at all cutoffs and comparing with the upper bound yields the limit statement.

Verification

The faithful counting object pins the exact convention: canonical residues, pairwise distinct moduli $>1$, coverage quantified over all integers, minimality as "no proper subfamily covers", systems counted as unordered sets. The final theorem builds sorry-free from a fresh directory with pinned toolchain and manifest, rejecting sorry/admit/native_decide (8,592 jobs; axioms [propext, Classical.choice, Quot.sound]). A concrete 70-class witness below modulus 1000 is verified by an independent exact Rust checker (with negative tests), tying the abstract construction to a concrete covering system anyone can inspect.

The download bundle contains the pinned definitions, the full proof chain, the witness and checker, and the one-command verifier.