wheel840
plain-language theorem explainer
The wheel modulus 840 is introduced as the product 2 cubed times 3 times 5 times 7 to serve as the base for wheel factorization filters in modular prime sieving. Researchers formalizing coprimality conditions and small-prime rejection in Recognition Science number theory would cite this constant when building soundness lemmas. The implementation is a direct constant assignment with no lemmas or computation steps required.
Claim. Let $w = 840 = 2^3 · 3 · 5 · 7$. This modulus ensures that any natural number coprime to $w$ is not divisible by 2, 3, 5 or 7.
background
The NumberTheory.Primes.Modular module supplies modular arithmetic and wheel filters motivated by theory documents on mod-8 gating and wheel factorization. The wheel modulus is the concrete product of the first four primes with the power on 2 chosen to match the eight-tick structure. The module states that this file formalizes only the soundness of the wheel: if a number is coprime to 840 then it is not divisible by the small primes 2, 3, 5, 7 that make up the wheel.
proof idea
The declaration is a direct definition that assigns the natural number 840. No upstream lemmas are invoked; the constant is simply named for reuse in the same module.
why it matters
This constant supplies the modulus required by the four downstream theorems that establish prime divisors of the wheel, acceptance under coprimality, and rejection under non-coprimality. It fills the initial concrete step in the modular tooling described in the module documentation. In the Recognition Science setting the wheel supports number-theoretic analysis needed for the phi-ladder and mass formulas, though it does not yet connect to the forcing chain or Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.