Seven Prime Divisors in Odd Distinct Covering Systems

Abstract

More than seventy-five years after Erdős introduced distinct covering systems in 1950, the Erdős–Selfridge odd covering problem (Erdős Problem 7) remains open: does there exist a finite covering system with pairwise distinct odd moduli greater than one? We prove that the least common multiple N of the moduli in any such system has at least seven distinct prime divisors, without any squarefreeness or prime-power-height hypothesis. The proof passes to a residual product of prime trees on which all prime-power classes are absent, then charges every remaining cylinder at the last digit that it fixes. A normalized fibre distortion and a reverse causal comparison for increasing supermodular functionals reduce the estimate to five exact rational charges. Their sum is 0.914634…<1, giving the contradiction uniformly in all prime-power heights. A complete Lean 4 formalization and an independent exact rational checker accompany the argument.