vp_840_two
plain-language theorem explainer
The exponent of the prime 2 in the factorization of 840 equals 3. Researchers anchoring the Recognition Science wheel modulus would cite this to fix the prime spectrum of 840 as {2,3,5,7}. The proof is a direct native computation of the factorization.
Claim. If $v_p(n)$ denotes the exponent of prime $p$ in the factorization of natural number $n$, then $v_2(840)=3$.
background
The RS constants module collects small decidable arithmetic facts about integers that recur in the reality repo, including 8, 45, 360, and 840 together with prime markers such as 11, 17, 37, 103, and 137. These facts serve as stable anchors that keep later bridge lemmas readable. The function vp p n returns the exponent of prime p in the factorization of n, implemented directly as n.factorization p.
proof idea
The proof is a one-line wrapper that applies native_decide to evaluate the factorization of 840 and extract the exponent of 2.
why it matters
This theorem supplies a base arithmetic anchor for the wheel modulus 840 inside the RS constants file. The module positions such facts as boring but stable anchors to avoid repeated arithmetic in downstream lemmas. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.