vp_eight_three
plain-language theorem explainer
The theorem asserts that the exponent of prime 3 in the factorization of 8 is zero. Number theorists maintaining the Recognition Science constant tables cite it to lock in the prime factors of small powers of two without repeated computation. The proof reduces to a single native_decide tactic that evaluates the factorization directly.
Claim. $v_3(8) = 0$, where $v_p(n)$ denotes the exponent of prime $p$ in the prime factorization of $n$.
background
The RSConstants module collects small decidable arithmetic facts about integers such as 8, 45, 360, and 840. These facts serve as stable anchors that keep later bridge lemmas readable and avoid re-proving the same arithmetic repeatedly.
proof idea
The proof applies the native_decide tactic, which computes the prime factorization of 8 via the upstream vp definition and checks the equality directly.
why it matters
This supplies a leaf arithmetic fact for the prime factorization collection in the RSConstants module. It anchors the structure around 8 = 2^3, which supports the eight-tick octave in the forcing chain. No downstream uses appear, indicating it functions as a readability anchor rather than a bridge lemma.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.