Develop CRT obstruction for Erdős Problem 7

[DomTheDeveloper]

Result

Formalizes a necessary structural condition for every finite congruence cover relevant to Erdős Problem 7.

For pairwise-coprime moduli m i > 1, the finite Chinese remainder theorem produces an integer satisfying

x ≡ a i + 1 [MOD m i]

for every index i. This integer avoids every original class a i (mod m i), so such classes cannot cover all natural numbers.

The file also proves the direct corollary that every finite congruence cover with nontrivial moduli contains two distinct non-coprime moduli.

Scope

This is a genuine search-pruning lemma, not a solution of Erdős Problem 7. A strict odd covering system, if one exists, must have overlapping prime factors among its moduli.

Verification

The source contains no placeholders or trust shortcuts and prints the axioms of both theorems. It must pass Lean before being marked verified.

[github-actions]

👋 This is an automated welcome message. 🤖
Thanks for the contributions!

A few friendly reminders while the review gets started:

• Please take a look at the style guidelines,
  especially the conventions for references, categories, AMS tags, and answer(sorry).
• You can manage some PR labels by leaving a comment with +label-name or -label-name; for example, +awaiting-author or -awaiting-author.
• This repository is mainly for formalised statements. Proofs longer than about 25-50 lines are usually out of scope; longer proofs are welcome to be included/linked via the formal_proof mechanism.

Thanks again for helping improve Formal Conjectures.