wheel840_factorization
plain-language theorem explainer
The equality 840 = 2^3 * 3 * 5 * 7 is recorded as a stable arithmetic anchor in the RS constants module. Number theorists building modular lemmas around wheel840 cite this to restrict its prime factors. The proof reduces to a single native_decide call that confirms the factorization by direct computation.
Claim. $840 = 2^{3} 3 5 7$
background
The RSConstants module gathers small, decidable arithmetic facts about integers that recur in the Recognition Science development, including factorizations of 8, 45, 360, and 840. These serve as stable anchors that keep later bridge lemmas readable without repeated arithmetic proofs. The module doc states these are intentionally boring but stable anchors to avoid re-proving the same arithmetic in many places.
proof idea
The proof is a one-line wrapper that invokes the native_decide tactic to verify the equality by native computation.
why it matters
This factorization supports the theorem prime_dvd_wheel840, which concludes that any prime divisor of wheel840 must be 2, 3, 5, or 7. It fills a basic arithmetic slot in the NumberTheory.Primes section, enabling clean statements about divisors without re-deriving the product form each time. In the broader framework it anchors constants used in modular arithmetic steps that connect to the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.