IndisputableMonolith.NumberTheory.Primes.Factorization
The module defines vp p n as the exponent of prime p in the factorization of n and supplies elementary lemmas on its behavior under multiplication and powers. Number theorists in the Recognition Science setting cite it when extracting prime exponents for constants or squarefree predicates. It reuses Mathlib's Nat.factorization on top of the axiom-free Basic primes module.
claim$v_p(n)$ denotes the exponent of prime $p$ in the prime factorization of the natural number $n$.
background
The module lives in the NumberTheory.Primes namespace and imports Mathlib together with the Basic primes module. The upstream Basic module supplies axiom-free footholds that reuse Mathlib's Nat.Prime while keeping the layer sorry-free. Its central object is the valuation vp p n, implemented directly as n.factorization p, together with the listed sibling lemmas on products, powers, and boundary cases.
proof idea
This is a definition module, no proofs. It declares the valuation and records the standard algebraic identities for factorization that Mathlib already supplies.
why it matters in Recognition Science
The module is imported by the Primes aggregator, by RSConstants (which collects decidable facts about primes such as 137), and by Squarefree (which links the squarefree predicate to vp). It therefore supplies the stable algebraic layer required before any later analytic number theory in the Recognition framework.
scope and limits
- Does not introduce new axioms or sorries.
- Does not extend beyond basic multiplicative properties of the valuation.
- Does not contain analytic estimates or growth bounds.
used by (3)
depends on (1)
declarations in this module (19)
-
def
vp -
theorem
vp_def -
theorem
factorization_mul -
theorem
factorization_pow -
theorem
vp_mul -
theorem
vp_pow -
theorem
vp_zero -
theorem
vp_one -
theorem
vp_prime_self -
theorem
vp_prime_ne -
theorem
vp_prime_pow -
theorem
vp_prime_pow_ne -
theorem
vp_gcd -
theorem
vp_lcm -
theorem
vp_eq_of_eq_prime_pow -
theorem
vp_eq_zero_of_eq_prime_pow_ne -
theorem
pow_dvd_iff_le_vp -
theorem
vp_eq_zero_of_not_dvd -
theorem
prime_dvd_iff_vp_pos