Michael Schroeder · Preprint · Version 1.0 · 9 September 2026 · Revised 15 September 2026 · ORCID 0009-0004-3249-0195
Noncoverage for Distinct Odd Moduli with at Most Three Prime Divisors
Abstract
We prove that a finite family of congruence classes with pairwise distinct odd moduli greater than one cannot cover the integers if each modulus has at most three distinct prime divisors. The prime powers, residue classes, and total number of primes occurring across the family are unrestricted. A normalized distortion measure and a conditional convex comparison reduce the problem to a count of one-prime and two-prime cofactors. Twenty-eight factorial moments close under a positive recurrence; exact rational arithmetic through prime 997 and a bound for all larger primes give total charge less than 0.937076 < 15/16. We also prove that the three-divisor restriction is needed only for moduli whose largest prime divisor is at most 109. Thus every hypothetical odd distinct covering has a modulus with at least four distinct prime divisors, all at most 109. Two standalone exact-arithmetic implementations accompany the proof. A finite rational alternative to the integral tail bound underlies an end-to-end Lean 4 formalization of the first noncoverage theorem.
Read the Paper
Proof Package
The complete archive includes the PDF and LaTeX manuscript, Lean proof sources, two standalone exact-arithmetic checkers, the rational appendix checker, certificates, reproduction instructions and verification records.
The paper and ZIP are byte-identical to the Zenodo deposit. Start with README.md in the archive. The Lean sources are already unpacked in formal/; the toolchain and dependency versions are pinned. Third-party dependencies and compiled caches are not bundled.
Theorem 1.1 is formalized end to end in Lean 4. The separate largest-prime cutoff extension in Theorem 1.2 is proved in the paper and is outside the Lean formalization. Appendix B presents the finite rational tail argument developed during formalization. The release preserves the audited proof sources and distinguishes the earlier kernel checks from publication and packaging checks.
The paper and prose are licensed under CC BY 4.0; original verification code and exact inputs are licensed under MIT. These licenses apply to their respective components. See licensing and third-party notices.
Citation and verification
BibTeX · Website checksums · Release notes
Schroeder, Michael. Noncoverage for Distinct Odd Moduli with at Most Three Prime Divisors. Version 1.0, Zenodo, 2026. DOI: 10.5281/zenodo.22760638.
The archive contains a complete SHA-256 manifest and instructions for reconstructing the exact arithmetic and checking the Lean proof. The public Lean theorem is Erdos7.noncoverage_at_most_three_prime_factors. Its audited axioms are propext, Classical.choice and Quot.sound.
Explanation of the problem
A congruence class is a regularly spaced set of integers. For example, the class 1 modulo 3 is …, −5, −2, 1, 4, 7, …: all integers with remainder 1 on division by 3. A covering system is a finite collection of such classes whose union contains every integer.
The Erdős–Selfridge odd covering problem asks whether a covering is possible when every modulus is odd and greater than one, and no two classes have the same modulus. Classes may overlap; every integer must be covered at least once.
This paper counts distinct prime divisors within each individual modulus. For example, 675 = 33 × 52 uses two primes, and 1,155 = 3 × 5 × 7 × 11 uses four. Repeating a prime as a higher power does not increase this count.
The main theorem rules out a covering whenever every modulus uses at most three primes, even if many different primes occur across the whole family. The separate extension shows that any hypothetical odd distinct covering must contain a modulus with at least four distinct prime divisors, all at most 109. This bounds the prime divisors; the modulus itself may be much larger.
The rank-nine paper requires at least nine primes across the family. The present result gives a complementary condition on a single modulus. Neither result settles the unrestricted odd covering problem. The probability reserves in this paper refer to its constructed measure and do not give a uniform lower bound on ordinary uncovered density.
Explore a covering
Choose odd primes, then shift the classes to see covered integers, overlaps and gaps.
One to eight primes from 3 to 97. The illustration uses up to eight distinct moduli, each at most 100.
Click a class below to increase its remainder. For example, “1 mod 3” covers 1, 4, 7, …
Coverage is calculated exactly over a complete period; percentages are rounded. The starting remainders are a simple example, not an optimal arrangement. Exploring these choices illustrates the problem; the paper’s proof covers all admissible families.