Minimum modulus of covering systems

TheoremKrukenberg's conjecture for minimum modulus five#●ready to prove

Let \(C\) be a distinct covering system: a finite set of congruences \(x \equiv r \pmod m\) with \(r \in \mathbb{Z}\) and \(m \in \mathbb{N}\), no two with the same modulus, such that every integer satisfies at least one of them. If every modulus of \(C\) is at least \(5\) and some modulus equals \(5\), then some modulus of \(C\) is at least \(108\).

public theorem_wanted exists_modulus_ge_108_of_distinct_covering_min_five
    (classes : Finset (ℤ × ℕ)) (hcov : Int.IsCoveringSystem classes)
    (hdist : Set.InjOn Prod.snd (classes : Set (ℤ × ℕ))) (hmin : ∀ c ∈ classes, 5 ≤ c.2)
    (hfive : ∃ c ∈ classes, c.2 = 5) : ∃ c ∈ classes, 108 ≤ c.2

Sources

Jonah Klein, On a Conjecture of Krukenberg and a Problem of Dalton and Trifonov, INTEGERS 26 (2026), Article A38, Theorem 1.

TheoremA distinct covering system with moduli from 6 to 168#●ready to prove

There is a distinct covering system, that is, a finite set of congruences \(x \equiv r \pmod m\) with \(r \in \mathbb{Z}\), \(m \in \mathbb{N}\) and no two with the same modulus, such that every integer satisfies at least one of them, whose moduli all lie between \(6\) and \(168\) and include both \(6\) and \(168\).

public theorem_wanted exists_distinct_covering_min_six_max_168 :
    ∃ classes : Finset (ℤ × ℕ), Int.IsCoveringSystem classes ∧
      Set.InjOn Prod.snd (classes : Set (ℤ × ℕ)) ∧ (∀ c ∈ classes, 6 ≤ c.2 ∧ c.2 ≤ 168) ∧
      (∃ c ∈ classes, c.2 = 6) ∧ ∃ c ∈ classes, c.2 = 168

Sources

Jonah Klein, On a Conjecture of Krukenberg and a Problem of Dalton and Trifonov, INTEGERS 26 (2026), Article A38, Theorem 2; the paper's witness is due to Ognian Trifonov.

TheoremLeast common multiple of a covering system with minimum modulus five#●ready to prove

Let \(C\) be a distinct covering system: a finite set of congruences \(x \equiv r \pmod m\) with \(r \in \mathbb{Z}\) and \(m \in \mathbb{N}\), no two with the same modulus, such that every integer satisfies at least one of them. If every modulus of \(C\) is at least \(5\) and some modulus equals \(5\), then the least common multiple of the moduli of \(C\) is at least \(1440\).

public theorem_wanted lcm_moduli_ge_1440_of_distinct_covering_min_five
    (classes : Finset (ℤ × ℕ)) (hcov : Int.IsCoveringSystem classes)
    (hdist : Set.InjOn Prod.snd (classes : Set (ℤ × ℕ))) (hmin : ∀ c ∈ classes, 5 ≤ c.2)
    (hfive : ∃ c ∈ classes, c.2 = 5) : 1440 ≤ classes.lcm Prod.snd

Sources

Jonah Klein, On a Conjecture of Krukenberg and a Problem of Dalton and Trifonov, INTEGERS 26 (2026), Article A38, Theorem 3.

TheoremLeast common multiple of a covering system with minimum modulus six#●ready to prove

Let \(C\) be a distinct covering system: a finite set of congruences \(x \equiv r \pmod m\) with \(r \in \mathbb{Z}\) and \(m \in \mathbb{N}\), no two with the same modulus, such that every integer satisfies at least one of them. If every modulus of \(C\) is at least \(6\) and some modulus equals \(6\), then the least common multiple of the moduli of \(C\) is at least \(5040\).

public theorem_wanted lcm_moduli_ge_5040_of_distinct_covering_min_six
    (classes : Finset (ℤ × ℕ)) (hcov : Int.IsCoveringSystem classes)
    (hdist : Set.InjOn Prod.snd (classes : Set (ℤ × ℕ))) (hmin : ∀ c ∈ classes, 6 ≤ c.2)
    (hsix : ∃ c ∈ classes, c.2 = 6) : 5040 ≤ classes.lcm Prod.snd

Sources

Jonah Klein, On a Conjecture of Krukenberg and a Problem of Dalton and Trifonov, INTEGERS 26 (2026), Article A38, Theorem 4.

TheoremA distinct covering system with minimum modulus 7 and moduli of lcm 15120#●ready to prove

There is a distinct covering system, that is, a finite set of congruences \(x \equiv r \pmod m\) with \(r \in \mathbb{Z}\), \(m \in \mathbb{N}\) and no two with the same modulus, such that every integer satisfies at least one of them, whose moduli are all at least \(7\), include \(7\), and have least common multiple \(15120\).

public theorem_wanted exists_distinct_covering_min_seven_lcm_15120 :
    ∃ classes : Finset (ℤ × ℕ), Int.IsCoveringSystem classes ∧
      Set.InjOn Prod.snd (classes : Set (ℤ × ℕ)) ∧ (∀ c ∈ classes, 7 ≤ c.2) ∧
      (∃ c ∈ classes, c.2 = 7) ∧ classes.lcm Prod.snd = 15120

Sources

Jonah Klein, On a Conjecture of Krukenberg and a Problem of Dalton and Trifonov, INTEGERS 26 (2026), Article A38, Theorem 5.

TheoremDiscarding the classes whose modulus is divisible by a large prime power#●ready to prove

Let \(C\) be a distinct covering system: a finite set of congruences \(x \equiv r \pmod m\) with \(r \in \mathbb{Z}\) and \(m \in \mathbb{N}\) (where \(x \equiv r \pmod 0\) means \(x = r\)), no two with the same modulus, such that every integer satisfies at least one of them. Let \(B \in \mathbb{N}\) be at least every modulus of \(C\), let \(p\) be a prime and \(a \ge 1\). If \(B < p^a (p + 1)\), then the congruences of \(C\) whose modulus is not divisible by \(p^a\) still cover every integer.

public theorem_wanted isCoveringSystem_filter_not_dvd_of_lt (classes : Finset (ℤ × ℕ))
    (hcov : Int.IsCoveringSystem classes) (hdist : Set.InjOn Prod.snd (classes : Set (ℤ × ℕ)))
    (B : ℕ) (hB : ∀ c ∈ classes, c.2 ≤ B) {p a : ℕ} (hp : p.Prime) (ha : 0 < a)
    (hpa : B < p ^ a * (p + 1)) :
    Int.IsCoveringSystem (classes.filter fun c => ¬ p ^ a ∣ c.2)

Sources

Jonah Klein, On a Conjecture of Krukenberg and a Problem of Dalton and Trifonov, INTEGERS 26 (2026), Article A38, Lemma 1, quoting Krukenberg, Corollary 2.3, and Dalton–Trifonov, Corollary 8.

TheoremMerging the p classes whose modulus is divisible by a prime power#●ready to prove

Let \(C\) be a covering system with positive moduli: a finite set of congruences \(x \equiv r \pmod m\) with \(r \in \mathbb{Z}\) and \(m \ge 1\) such that every integer satisfies at least one of them. Let \(p\) be a prime and \(a \ge 1\), and suppose exactly \(p\) congruences of \(C\) have modulus divisible by \(p^a\), with moduli \(p^a m_1, \dots, p^a m_p\). Then for some \(r \in \mathbb{Z}\), replacing these \(p\) congruences by the single congruence \(x \equiv r \pmod{p^{a-1} \operatorname{lcm}(m_1, \dots, m_p)}\) still gives a covering system.

public theorem_wanted exists_isCoveringSystem_merge_prime_power (classes : Finset (ℤ × ℕ))
    (hcov : Int.IsCoveringSystem classes) (hpos : ∀ c ∈ classes, 0 < c.2) {p a : ℕ}
    (hp : p.Prime) (ha : 0 < a) (hcard : (classes.filter fun c => p ^ a ∣ c.2).card = p) :
    ∃ r : ℤ, Int.IsCoveringSystem
      (insert (r, p ^ (a - 1) * (classes.filter fun c => p ^ a ∣ c.2).lcm fun c => c.2 / p ^ a)
        (classes.filter fun c => ¬ p ^ a ∣ c.2))

Sources

Jonah Klein, On a Conjecture of Krukenberg and a Problem of Dalton and Trifonov, INTEGERS 26 (2026), Article A38, Lemma 2, quoting Dalton–Trifonov, Corollary 9.

TheoremTranslating a covering system#●ready to prove

Let \(C\) be a covering system: a finite set of congruences \(x \equiv a_i \pmod{m_i}\) with \(a_i \in \mathbb{Z}\) and \(m_i \in \mathbb{N}\) (where \(x \equiv a_i \pmod 0\) means \(x = a_i\)) such that every integer satisfies at least one of them. Then for every \(t \in \mathbb{Z}\) the congruences \(x \equiv a_i + t \pmod{m_i}\) also form a covering system.

public theorem_wanted isCoveringSystem_translate (classes : Finset (ℤ × ℕ))
    (hcov : Int.IsCoveringSystem classes) (t : ℤ) :
    Int.IsCoveringSystem (classes.image fun c => (c.1 + t, c.2))

Sources

Jonah Klein, On a Conjecture of Krukenberg and a Problem of Dalton and Trifonov, INTEGERS 26 (2026), Article A38, Lemma 3.

TheoremSwapping two residues modulo a prime in a covering system#●ready to prove

Let \(C\) be a covering system with positive moduli: a finite set of congruences \(x \equiv a \pmod m\) with \(a \in \mathbb{Z}\) and \(m \ge 1\) such that every integer satisfies at least one of them. Let \(L\) be the least common multiple of its moduli, \(p\) a prime dividing \(L\), and \(a_1 < a_2 \le p - 1\) natural numbers. For a prime \(\ell\) write \(\nu_\ell(L)\) for the exponent of \(\ell\) in \(L\), and let \(C_p(\alpha)\) be the set of congruences \(x \equiv a \pmod m\) in \(C\) with \(p \mid m\) and \(a \equiv \alpha \pmod p\). Let \(t \in \mathbb{Z}\) satisfy \(t \equiv a_2 - a_1 \pmod{p^{\nu_p(L)}}\) and \(t \equiv 0 \pmod{q^{\nu_q(L)}}\) for every prime \(q \ne p\) dividing \(L\). Then the congruences of \(C\) outside \(C_p(a_1) \cup C_p(a_2)\), together with \(x \equiv a + t \pmod m\) for each \(x \equiv a \pmod m\) in \(C_p(a_1)\) and \(x \equiv a - t \pmod m\) for each \(x \equiv a \pmod m\) in \(C_p(a_2)\), form a covering system.

public theorem_wanted isCoveringSystem_swap_residues_mod_prime (classes : Finset (ℤ × ℕ))
    (hcov : Int.IsCoveringSystem classes) (hpos : ∀ c ∈ classes, 0 < c.2) {L p : ℕ}
    (hL : L = classes.lcm Prod.snd) (hp : p.Prime) (hpL : p ∣ L) {a₁ a₂ : ℕ} (h₁₂ : a₁ < a₂)
    (h₂ : a₂ ≤ p - 1) (t : ℤ)
    (htp : t ≡ (a₂ : ℤ) - a₁ [ZMOD ((p ^ L.factorization p : ℕ) : ℤ)])
    (htq : ∀ q : ℕ, q.Prime → q ∣ L → q ≠ p → t ≡ 0 [ZMOD ((q ^ L.factorization q : ℕ) : ℤ)]) :
    Int.IsCoveringSystem
      ((classes.filter fun c => ¬ (p ∣ c.2 ∧ (c.1 ≡ a₁ [ZMOD p] ∨ c.1 ≡ a₂ [ZMOD p]))) ∪
        (classes.filter fun c => p ∣ c.2 ∧ c.1 ≡ a₁ [ZMOD p]).image (fun c => (c.1 + t, c.2)) ∪
        (classes.filter fun c => p ∣ c.2 ∧ c.1 ≡ a₂ [ZMOD p]).image (fun c => (c.1 - t, c.2)))

Sources

Jonah Klein, On a Conjecture of Krukenberg and a Problem of Dalton and Trifonov, INTEGERS 26 (2026), Article A38, Lemma 4, from the author's thesis, Lemma 2.13.

TheoremMirsky–Newman bound for distinct covering systems#●ready to prove

Let \(a_1 \bmod m_1, \dots, a_k \bmod m_k\) be residue classes that cover \(\mathbb{Z}\), that is, every integer lies in at least one of them. If the moduli \(m_1, \dots, m_k\) are pairwise distinct and all at least \(2\), then \(\sum_{i=1}^{k} 1/m_i > 1\).

public theorem_wanted one_lt_sum_inv_moduli_of_distinct_covering (classes : Finset (ℤ × ℕ))
    (hcov : Int.IsCoveringSystem classes) (hdist : Set.InjOn Prod.snd (classes : Set (ℤ × ℕ)))
    (htwo : ∀ c ∈ classes, 2 ≤ c.2) : (1 : ℚ) < ∑ c ∈ classes, (1 : ℚ) / c.2

Sources

Jonah Klein, On a Conjecture of Krukenberg and a Problem of Dalton and Trifonov, INTEGERS 26 (2026), Article A38, Lemma 5, quoting Mirsky and Newman.

TheoremReplacing the largest prime factor of the modulus set#●ready to prove

Let \(m, L \in \mathbb{N}\), let \(p \ge m\) be a prime with \(p \nmid L\), let \(q > p\) be the largest prime dividing \(L\), and write \(\nu_q(L)\) for the exponent of \(q\) in \(L\). Suppose there are residues \(r_d \in \mathbb{Z}\), one for each divisor \(d \ge m\) of \(L\), such that every integer \(x\) satisfies \(x \equiv r_d \pmod d\) for some such \(d\). Then the same holds with \(L\) replaced by \(p^{\nu_q(L)} L / q^{\nu_q(L)}\): there are residues \(s_d \in \mathbb{Z}\), one for each divisor \(d \ge m\) of \(p^{\nu_q(L)} L / q^{\nu_q(L)}\), such that every integer \(x\) satisfies \(x \equiv s_d \pmod d\) for some such \(d\).

public theorem_wanted exists_covering_divisors_replace_largest_prime {m p q L : ℕ} (hp : p.Prime) (hmp : m ≤ p)
    (hpL : ¬ p ∣ L) (hq : q.Prime) (hqL : q ∣ L)
    (hpq : p < q) (hqmax : ∀ r : ℕ, r.Prime → r ∣ L → r ≤ q)
    (h : ∃ res : ℕ → ℤ, Int.IsCoveringSystem
      ((L.divisors.filter fun d => m ≤ d).image fun d => (res d, d))) :
    ∃ res : ℕ → ℤ, Int.IsCoveringSystem
      (((p ^ L.factorization q * (L / q ^ L.factorization q)).divisors.filter
        fun d => m ≤ d).image fun d => (res d, d))

Sources

Jonah Klein, On a Conjecture of Krukenberg and a Problem of Dalton and Trifonov, INTEGERS 26 (2026), Article A38, Lemma 6.

DefinitionCovering systems with arbitrarily large distinct moduli (OPG-493)#✓fully proved

The statement that for every natural number \(N\) there are finitely many residue classes \(a_1 \bmod m_1, \dots, a_k \bmod m_k\) that cover \(\mathbb{Z}\) (every integer lies in at least one of them) whose moduli are pairwise distinct and all at least \(N\).

def conjecture : Prop :=
  ∀ N : ℕ, ∃ classes : Finset (ℤ × ℕ),
    Int.IsCoveringSystem classes ∧
      (∀ c ∈ classes, N ≤ c.2) ∧
      ∀ c₁ ∈ classes, ∀ c₂ ∈ classes, c₁.2 = c₂.2 → c₁ = c₂

Used by 1

Used byHough's minimum modulus theorem

TheoremHough's minimum modulus theorem#●ready to prove

There is a natural number \(N\) such that no finite set of residue classes covering \(\mathbb{Z}\) has pairwise distinct moduli that are all at least \(N\). Hence the conjecture of Open Garden problem OPG-493 is false.

theorem_wanted conjecture_refuted : ¬ conjecture

def conjecture : Prop :=
  ∀ N : ℕ, ∃ classes : Finset (ℤ × ℕ),
    Int.IsCoveringSystem classes ∧
      (∀ c ∈ classes, N ≤ c.2) ∧
      ∀ c₁ ∈ classes, ∀ c₂ ∈ classes, c₁.2 = c₂.2 → c₁ = c₂

WantedExt/NumberTheory/LargeModulusCoveringSystemsWanted.lean:24

Sources

Bob Hough, Solution of the minimum modulus problem for covering systems, Annals of Mathematics 181 (2015), 361-382; arXiv:1307.0874, https://arxiv.org/abs/1307.0874.

Uses 1

Statement usesCovering systems with arbitrarily large distinct moduli (OPG-493)

1 fully proved12 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.