vp_fortyfive_two
plain-language theorem explainer
The 2-adic valuation of 45 is zero, confirming 45 is odd and free of the prime 2. Researchers maintaining the Recognition Science arithmetic anchors cite this to stabilize later bridge lemmas that reference 45 without repeated divisibility checks. The proof reduces to a single native_decide tactic that evaluates the factorization exponent by direct computation.
Claim. The 2-adic valuation satisfies $v_2(45) = 0$.
background
The module collects small decidable arithmetic facts about integers that recur in the reality repository, such as 8, 45, 360, 840, and prime markers including 11, 17, 37, 103, and 137. These act as stable anchors that keep later bridge lemmas readable by avoiding repeated elementary arithmetic proofs. The function vp p n returns the exponent of prime p in the factorization of n, implemented as n.factorization p.
proof idea
The proof is a one-line wrapper that invokes the native_decide tactic to evaluate the decidable equality vp 2 45 = 0 by direct computation of the factorization.
why it matters
This supplies one of the basic arithmetic facts in the RS constants module and contributes to the prime spectrum description of 45, which carries 3-content of exponent 2 and 5-content of exponent 1. It supports the surrounding collection of factorization lemmas such as fortyfive_eq_three_sq_mul_five and gcd_eight_fortyfive_eq_one, though no explicit downstream uses are recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.