wheel840_rejects
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not define wheel840 or prove its prime factorization.
- Does not treat coprimeness in the opposite direction.
- Does not extend the filter to primes larger than 7.
- Does not incorporate phi, J-cost or other Recognition Science constants.
Lean usage
apply wheel840_rejectsformal statement (Lean)
157theorem wheel840_rejects (n : ℕ) (h : ¬ Nat.Coprime n wheel840) :
158 2 ∣ n ∨ 3 ∣ n ∨ 5 ∣ n ∨ 7 ∣ n := by
proof body
Tactic-mode proof.
159 have hg_ne_one : Nat.gcd n wheel840 ≠ 1 := by
160 intro hg
161 apply h
162 exact (Nat.coprime_iff_gcd_eq_one).2 hg
163 obtain ⟨p, hpprime, hpdvg⟩ :=
164 (Nat.ne_one_iff_exists_prime_dvd (n := Nat.gcd n wheel840)).1 hg_ne_one
165 have hpdvn : p ∣ n := hpdvg.trans (Nat.gcd_dvd_left n wheel840)
166 have hpdv840 : p ∣ wheel840 := hpdvg.trans (Nat.gcd_dvd_right n wheel840)
167 have hp : Prime p := by
168 simpa [Prime] using hpprime
169 have hp_cases : p = 2 ∨ p = 3 ∨ p = 5 ∨ p = 7 :=
170 prime_dvd_wheel840 (p := p) hp hpdv840
171 rcases hp_cases with hp2 | hp_rest
172 · left
173 simpa [hp2] using hpdvn
174 · rcases hp_rest with hp3 | hp_rest2
175 · exact Or.inr (Or.inl (by simpa [hp3] using hpdvn))
176 · rcases hp_rest2 with hp5 | hp7
177 · exact Or.inr (Or.inr (Or.inl (by simpa [hp5] using hpdvn)))
178 · exact Or.inr (Or.inr (Or.inr (by simpa [hp7] using hpdvn)))
179
180/-- A gcd-form of `wheel840_rejects` (sometimes more convenient in proofs). -/