vp_fortyfive_three
plain-language theorem explainer
The declaration fixes the exponent of prime 3 in the integer 45 at exactly 2. Modelers working with Recognition Science constants cite it to lock the factorization of 45 when building expressions involving 360 or 840. The proof is a one-line wrapper that invokes native_decide on the decidable factorization computation.
Claim. $v_3(45)=2$, where $v_p(n)$ is the exponent of prime $p$ in the prime factorization of the natural number $n$.
background
The module collects small decidable arithmetic facts about integers that recur in the reality repo, including 8, 45, 360, 840 and the primes 11, 17, 37, 103, 137. These act as stable anchors that keep later bridge lemmas readable without repeated arithmetic derivations. The upstream definition states that vp p n is the exponent of p in the prime factorization of n, implemented as n.factorization p.
proof idea
The proof is a one-line wrapper that applies the native_decide tactic to evaluate the decidable expression obtained from the vp definition.
why it matters
The result supplies a fixed anchor for the factorization 45 = 3^2 * 5 inside the RSConstants module, supporting sibling facts on gcd, lcm and wheel840_factorization. It contributes to the stable arithmetic base required for later Recognition Science bridge lemmas that reference these constants, consistent with the module's role in avoiding re-derivation of small facts.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.