Michael Schroeder · Preprint · Version 1.0.1 · 13 September 2026 · Revised 15 September 2026 · ORCID 0009-0004-3249-0195

Nine Prime Divisors in Odd Distinct Covering Systems

Abstract

We prove that every finite covering system with pairwise distinct odd moduli greater than one has at least nine distinct prime divisors in the least common multiple of its moduli. There is no restriction on the prime-power exponents. The proof combines completion of the congruence family with conditional reweighting that retains the joint geometry of the two smallest prime coordinates. Two deletion budgets reduce to a finite set of vertices by an explicit convex interpolation, and a prescribed mixed-modulus projection closes the remaining cases. Exact geometric sums and first moments control every omitted exponent range. A certificate of 28,001 integer inequalities completes the argument. We also prove that the least common multiple of an odd distinct cover is at least 9,704,539,845, and that every finite distinct odd family with moduli greater than one supported on at most eight primes leaves natural density at least 1/1,002,375 uncovered. A Lean formalization proves the rank theorem and both quantitative corollaries.

Read the Paper

Proof Package

The Zenodo edition includes the paper in PDF and LaTeX, the full Lean formalization, exact computational certificates, verification records and reproduction instructions.

This compact archive is byte-identical to the published Zenodo deposit. All 24,918 project Lean proof sources, including the generated proofs, are included in a compressed archive inside the ZIP. Start with README.md; the included unpack_lean.py extracts and verifies the sources. Compiled objects, dependency caches and bulky historical logs are omitted.

Version 1.0.1 adds the DOI, author ORCID, archived references and updated package instructions. The mathematical argument, Lean proof sources and exact certificate inputs are unchanged. This edition checks source identity and packaging; it does not claim a new full Lean kernel replay. The separate rank-ten method diagnostic remains outside the Lean formalization.

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.

Earlier 13 September release: paper and expanded companion

These preserved files belong to the original release before the DOI and ORCID were added. For the current edition, use the paper and compact companion above.

Original paper (PDF) · Original LaTeX source

Your download will be verified before it is saved.

The package also includes a separate study of the current method’s limitations at rank ten. This additional study is outside the Lean formalization.

Download details and verification

The ZIP is supplied in six parts to fit the website’s file-size limit. The download button joins them and checks that the result matches the final archive exactly.

For a command-line download, save download_companion.py and run python3 download_companion.py. It requires Python 3.9 or later, checks the downloaded files and will not overwrite an existing archive.

You can also download the parts individually:

  1. Part 1
  2. Part 2
  3. Part 3
  4. Part 4
  5. Part 5
  6. Part 6

On macOS or Linux, concatenate all six parts in order:

cat Rank9_Complete_Proof_Package.zip.part0[1-6] > Rank9_Complete_Proof_Package.zip
shasum -a 256 Rank9_Complete_Proof_Package.zip

The complete archive has 132,377,867 bytes and SHA-256:

c7aafd219c89979379ca4541e2c1f527ae90f70e68ed9eede8b133391c1e9af5

Download manifest · File checksums

Checksums identify the released files. The archive’s documentation describes the mathematical verification and how to reproduce it.

Citation and verification

BibTeX · Citation metadata · Website checksums · Release notes

Schroeder, Michael. Nine Prime Divisors in Odd Distinct Covering Systems. Version 1.0.1, Zenodo, 2026. DOI: 10.5281/zenodo.22759614.

The archive documentation distinguishes the accepted mathematical verification from this edition’s source-identity and packaging checks. Full reproduction requires the pinned Lean toolchain and dependencies; the extracted proof sources occupy approximately 500 MB before dependencies and build outputs.

This work follows the author’s rank-seven and rank-eight papers. The written reduction is self-contained; the Lean development reuses the proved rank-eight theorem for smaller prime supports.

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.

Each spacing is called a modulus. 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.

The rank is the number of different primes appearing across all moduli, equivalently the number of distinct prime divisors of their least common multiple. The set of these primes is called the prime support. For example, moduli 9 and 25 use only the primes 3 and 5; raising them to higher powers does not add new primes.

This paper proves that any odd distinct covering system must use at least nine distinct primes. Equivalently, every finite candidate supported on eight or fewer primes misses some integers, however large the prime powers are. This gives a necessary condition for a covering; the general existence question remains open.