wheel840_accepts
plain-language theorem explainer
Coprimality of a natural number n to 840 implies that none of the primes 2, 3, 5, or 7 divide n. Number theorists building wheel sieves or modular prime filters would cite this soundness result. The term proof derives pairwise coprimality via symmetry on the divisors of 840, then applies the prime-coprimality equivalence for each factor.
Claim. If $n$ is coprime to 840 then $2$ does not divide $n$, $3$ does not divide $n$, $5$ does not divide $n$, and $7$ does not divide $n$.
background
The result appears in the NumberTheory.Primes.Modular module, whose opening documentation describes it as the entry point for modular and wheel-filter tooling. The wheel840 is the integer whose prime factors are exactly 2, 3, 5, and 7 (with 2 raised to the third power). The module states that the theorem formalizes the soundness direction: coprimality to 840 guarantees that n avoids divisibility by those four small primes.
proof idea
The term proof first obtains Nat.Coprime n 2, n 3, n 5, and n 7 by applying coprime_dvd_right to the hypothesis together with native_decide facts that each prime divides wheel840, then taking symmetry. It finishes by refining the four coprimality statements into the required conjunction via Nat.Prime.coprime_iff_not_dvd applied to prime_two, prime_three, prime_five, and the decidable fact that 7 is prime.
why it matters
The declaration supplies the soundness half of the wheel840 filter inside the Recognition Science modular-arithmetic layer for primes. It directly supports the module's stated goal of preparing character and sieve tooling. With no downstream uses recorded, the lemma remains a foundational soundness claim rather than an active step in a larger chain; it aligns with the framework's emphasis on discrete, phi-derived structures but does not invoke J-cost or the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.