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.