vp_eight_two
plain-language theorem explainer
The declaration establishes that the exponent of prime 2 in the factorization of 8 equals 3. Researchers anchoring arithmetic facts in the Recognition Science constants module cite this to fix the 2-power content of 8 without recomputing factorizations each time. The proof applies a native decision tactic directly to the valuation definition.
Claim. $v_2(8) = 3$, where $v_p(n)$ denotes the exponent of prime $p$ in the prime factorization of $n$.
background
The module collects small decidable arithmetic facts about integers such as 8, 45, 360, and 840 that appear repeatedly in the reality repo. These serve as stable anchors to keep later bridge lemmas readable and avoid re-proving the same arithmetic in many places. The function vp p n extracts 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 invokes native_decide on the equality vp 2 8 = 3.
why it matters
This fact anchors calculations involving the prime spectrum of 8 in the RS constants file. It supports downstream uses of prime factorizations without repeated arithmetic. No open questions are touched here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.