wheel840_rejects_of_gcd_ne_one
plain-language theorem explainer
wheel840_rejects_of_gcd_ne_one supplies the gcd-form of the wheel rejection property: when gcd(n,840) is not 1, n must be divisible by 2, 3, 5 or 7. Number theorists formalizing sieve filters or modular constraints on primes cite this variant when gcd hypotheses appear directly in proofs. The argument is a one-line wrapper that invokes wheel840_rejects after converting the gcd condition via the coprimality equivalence.
Claim. If $n$ is a natural number with $gcd(n,840)neq1$, then $2mid n$ or $3mid n$ or $5mid n$ or $7mid n$.
background
The module introduces modular tools for prime sieves, beginning with wheel filters. wheel840 is the modulus 840 = 2^3 * 3 * 5 * 7. The upstream theorem wheel840_rejects states that if n is not coprime to wheel840 then at least one of 2, 3, 5, 7 divides n. The module documentation frames this as the soundness property of the wheel: coprimality to 840 implies n avoids those small prime factors. The present declaration rewrites the same fact using the gcd predicate instead of the coprime predicate.
proof idea
The proof applies wheel840_rejects to n after an intro that assumes coprimality and derives a contradiction with the given gcd hypothesis. It invokes the equivalence Nat.coprime_iff_gcd_eq_one to convert gcd neq 1 into not coprime, then discharges the goal.
why it matters
The declaration supplies a convenient interface for the wheel-840 rejection property inside the modular primes tooling. It supports the soundness claim for wheel factorization that the module documentation positions as the starting point for mod-8 characters and prime sieves. No downstream uses are recorded, but the form aligns with Recognition Science use of wheel filters to isolate small prime factors before applying the phi-ladder mass formula or the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.