vp
plain-language theorem explainer
vp p n extracts the exponent of prime p in the factorization of natural number n. Number theorists working on Möbius inversion or explicit prime counts cite it as the stable local alias to Mathlib factorization. It is implemented as a direct one-line abbreviation to n.factorization p.
Claim. Let $v_p(n)$ denote the exponent of prime $p$ in the prime factorization of the natural number $n$.
background
The module supplies a thin, stable wrapper around Mathlib's Nat.factorization to support prime-exponent calculations inside the Recognition Science codebase. vp is introduced precisely as the exponent of p in n, with sibling lemmas such as vp_mul and vp_pow supplying the algebraic rules needed for squarefree checks and arithmetic functions. The setting assumes only the standard Nat.factorization map from Mathlib, which returns the finite-support function sending each prime to its multiplicity.
proof idea
This is a definition implemented as a direct one-line alias to Nat.factorization p applied to n.
why it matters
The definition anchors the entire primes hierarchy: it is invoked in mobius_ne_zero_iff_vp_le_one to characterize squarefree numbers via the condition that vp p n ≤ 1 for all p, and it supplies the concrete values used in primeCounting_sevenhundredfifty and the factorial valuation theorems such as vp 2 (5!) = 3. It therefore supplies the valuation primitive required for downstream arithmetic-function work that feeds the Recognition Science number-theoretic layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.