vp_840_three
plain-language theorem explainer
The theorem records that the exponent of prime 3 in the factorization of 840 is exactly one. Number theorists maintaining the Recognition Science constant tables would cite this fact to keep later bridge lemmas free of repeated arithmetic. The proof is a one-line native_decide computation that evaluates the factorization directly.
Claim. $v_3(840)=1$
background
The RSConstants module gathers small, decidable arithmetic facts about integers that recur in the reality repo, including 8, 45, 360, 840 and selected primes. These serve as stable anchors that keep downstream lemmas readable. The function vp p n is defined as the exponent of p in the prime factorization of n, implemented directly as n.factorization p.
proof idea
The proof is a one-line wrapper that applies native_decide to compute the factorization of 840 and read off the exponent of 3.
why it matters
This declaration supplies a pre-verified exponent that anchors arithmetic simplifications throughout the Recognition Science constants. It belongs to the collection of prime and factorization facts (alongside siblings such as prime_137 and wheel840_factorization) that prevent repeated recomputation in bridge lemmas. The module doc-comment describes these facts as boring but stable anchors for the framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.