vp_pow
The exponent of prime p in natural number n, written vp p n, scales linearly under powers. Thus the exponent of p in n^k equals k times the exponent of p in n. Number theorists constructing prime factorization interfaces or Möbius tools inside Recognition Science would cite this algebraic law. The proof is a one-line simplification that unfolds the local vp definition and invokes Mathlib's Nat.factorization_pow rule.
claimLet $v_p(m)$ denote the exponent of prime $p$ in the prime factorization of natural number $m$. Then for all natural numbers $p,n,k$, $v_p(n^k)=k·v_p(n)$.
background
The NumberTheory.Primes.Factorization module supplies a thin, stable wrapper around Mathlib's Nat.factorization. The function vp p n extracts the exponent of p inside n and is accompanied by a handful of algebraic identities (vp_mul, vp_pow) intended for reuse in squarefree and Möbius constructions. The module doc states the primary goal is to keep these laws unconditional and easy to apply downstream.
proof idea
One-line wrapper. The simp tactic is applied to the goals vp p (n^k) and k * vp p n, using the local definition of vp together with Nat.factorization_pow. The comment notes that factorization_pow already handles the n=0 case internally, so no separate boundary logic is required.
why it matters in Recognition Science
The result completes the basic multiplicative and power laws for the vp interface, directly supporting the module's stated purpose of supplying reusable algebraic laws for later prime-number work. It sits at the number-theoretic base layer that feeds squarefree and Möbius developments, consistent with the Recognition Science pattern of building discrete structures from forcing-derived constants without introducing new axioms.
scope and limits
- Does not treat real or fractional exponents.
- Does not define or use valuations on rings other than ℕ.
- Does not prove uniqueness of prime factorization.
- Does not link the exponent directly to phi-ladder or physical constants.
formal statement (Lean)
42theorem vp_pow (p n k : ℕ) : vp p (n ^ k) = k * vp p n := by
proof body
Term-mode proof.
43 -- `factorization_pow` is unconditional (it handles `n = 0` internally).
44 -- Evaluate at `p` and simplify `nsmul` on ℕ to multiplication.
45 simp [vp, Nat.factorization_pow]
46
47/-! ### Boundary cases for `vp` -/
48
49/-- The exponent of any prime in 0 is 0 (by convention). -/