wheel840_rejects
plain-language theorem explainer
Any natural number sharing a factor with 840 must be divisible by 2, 3, 5 or 7. Number theorists building wheel sieves or modular prime filters cite this to certify the rejection property of the 840-wheel. The proof converts non-coprimeness to a gcd greater than 1, extracts a prime divisor of that gcd, classifies it among the four small primes via an auxiliary lemma, and dispatches the four cases by divisibility transfer.
Claim. Let $n$ be a natural number. If $n$ is not coprime to 840, then $2$ divides $n$ or $3$ divides $n$ or $5$ divides $n$ or $7$ divides $n$.
background
The module develops modular tools for wheel filters motivated by Recognition Science theory documents, beginning with the soundness claim that coprimeness to 840 implies no divisibility by the primes 2, 3, 5 or 7. Wheel840 is the integer 840 = 2^3 · 3 · 5 · 7 that serves as the modulus for this sieve. The present theorem is the contrapositive form of that soundness statement.
proof idea
The tactic proof first rewrites the negated coprimeness hypothesis into gcd(n, wheel840) ≠ 1. It invokes the existence of a prime divisor of this gcd to obtain p that divides both n and wheel840. The auxiliary lemma prime_dvd_wheel840 then forces p to be 2, 3, 5 or 7. Four nested rcases splits on this disjunction each apply the corresponding equality to transfer divisibility from p to n.
why it matters
The declaration supplies the core soundness lemma for the wheel-840 filter in the primes module and is applied directly by the downstream gcd-form variant wheel840_rejects_of_gcd_ne_one. It completes the modular arithmetic foundation described in the module documentation, enabling efficient rejection checks that align with the discrete phi-ladder and J-cost structures of the broader Recognition Science framework (T5–T8 forcing chain). No open scaffolding remains for this arithmetic claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.