Distinct covering systems with all moduli in an interval [n, kn] (Theorem 1.2 and the closing questions of arXiv:2506.11359)

Abstract

A covering system is distinct when its moduli are pairwise different. Dalton and Jones proved that for every integer m ≥ 3 no distinct covering system has all its moduli in the interval [m,10m], and asked the same question for [n,12n] with n ≥ 4 and for [n,15n] with n ≥ 5. Their proof filters the interval by Krukenberg's discard lemma and then applies the density condition; for twenty-three exceptional values of m it runs a bespoke argument, one ingredient of which is to recount the surviving moduli after a reduction and reduce again. We turn that recount into a uniform, machine-checkable certificate: a list of prime-power steps, each licensed by a count taken inside the set the earlier steps left, together with an integer test on the reciprocal sum of the survivors. A single step of the certificate closes twenty cells with k>10, namely [m,km] for k=11 and m ∈ {13,30,85}, for k=12 and m ∈ {12,28,78,79,127,128,129,154,155,156,169,170,171,173,174,175}, and for k=13 and m=145; no cell with k>10 appears to have been recorded before. We also compute the one-pass filter tables for 11 ≤ k ≤ 15, note five values of m that are missing from the exceptional list of Dalton and Jones, and prove a fixpoint theorem which shows that no certificate at all exists for four named cells, among them the interval [6,167] behind a conjecture of Klein. All statements are formally verified in Lean 4.

Open review

This founding-collection manuscript received AI review before publication. Independent human review is open. Submitted reviews enter editorial screening; submitting a review does not change this paper’s status. Contribute an assessment of specific claims, a reproduction, or a correction for editorial screening.

Archived files

1. Version 1 · current (opens in a new tab)

   Source snapshot 2026-08-30 15:34 UTC

   File fingerprint

   1c8c67943adb57f1adfb76503361bf763a2b41d6d2cf7cf61d9a439db707254c