A question of Erdős and Graham on covering systems

TheoremNon-intersecting integers admit no covering system of divisor form#●ready to prove

Let \(n\) be a natural number and let \(D\) be the finite set of divisors of \(n\) greater than \(1\), taken empty when \(n = 0\). Call \(n\) non-intersecting if there are integers \(a_d\), one for each natural number \(d\), such that for all distinct natural numbers \(d, d' > 1\) dividing \(n\) (every \(d\) divides \(0\)), if the classes \(a_d \pmod d\) and \(a_{d'} \pmod{d'}\) have an integer in common, then \(d\) and \(d'\) are coprime. If \(n\) is non-intersecting, then there are no integers \(b_d\) for \(d \in D\) such that every integer lies in the class \(b_d \pmod d\) for some \(d \in D\).

The families \((a_d)\) and \((b_d)\) are independent; in particular, no family of classes \(a_d \pmod d\) for \(d \in D\) with the coprime-overlap property covers the integers.

theorem_wanted not_covering_of_nonintersecting (n : ℕ)
    (hnonint : ∃ a : ℕ → ℤ,
      ∀ d d' : ℕ, d ∣ n → d' ∣ n → 1 < d → 1 < d' →
        d ≠ d' →
          (∃ x : ℤ, x ≡ a d [ZMOD (d : ℤ)] ∧
            x ≡ a d' [ZMOD (d' : ℤ)]) →
          Nat.Coprime d d') :
    ¬ ∃ b : ℕ → ℤ, Int.IsCoveringSystem
        ((n.divisors.filter (fun d => 1 < d)).image
          (fun d => (b d, d)))

Sources

• Sarosh Adenwalla, "A Question of Erdős and Graham on Covering Systems", Theorem 3.2.

TheoremCovering systems have reciprocal-moduli sum at least one#●ready to prove

Let \(d_1, \dots, d_t\) be positive integers and \(a_1, \dots, a_t\) integers such that every integer \(z\) satisfies \(z \equiv a_i \pmod{d_i}\) for some \(i\). Then \(\sum_{i=1}^t 1/d_i \ge 1\).

theorem_wanted one_le_sum_inv_moduli {t : ℕ}
    (moduli : Fin t → ℕ) (residues : Fin t → ℤ)
    (hpos : ∀ i, 0 < moduli i)
    (hcov : Int.IsCoveringSystem
      (Int.indexedCoveringClasses moduli residues)) :
    (1 : ℚ) ≤ ∑ i, (1 : ℚ) / (moduli i : ℚ)

Sources

• Sarosh Adenwalla, "A Question of Erdős and Graham on Covering Systems", Lemma 2.2.

2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.