IndisputableMonolith.NumberTheory.Primes.Factorization
The Factorization module defines vp p n as the exponent of a prime p in the factorization of n, reusing Mathlib's Nat.factorization. Downstream modules such as RSConstants and Squarefree cite it to anchor arithmetic facts and connect to the squarefree predicate. The module supplies a core definition plus lemmas on multiplicativity and powers, all built axiom-free atop the Basic primes module.
claimLet $v_p(n)$ be the exponent of prime $p$ in the factorization of natural number $n$, given by $n.factorization p$.
background
This module extends IndisputableMonolith.NumberTheory.Primes.Basic, which reuses Mathlib's Nat.Prime to supply axiom-free prime footholds. It introduces the valuation vp together with supporting results on its action under multiplication and exponentiation. The local setting is algebraic number theory inside the Recognition monolith, with all material kept decidable and free of sorries.
proof idea
The module is a definition module. It opens with vp p n := n.factorization p, then adds lemmas such as factorization_mul and vp_mul that record the additive property of the valuation under products and powers.
why it matters in Recognition Science
The module supplies vp to the prime aggregator IndisputableMonolith.NumberTheory.Primes and to RSConstants for repeated arithmetic anchors such as 8, 45, and 137. It also feeds Squarefree by linking the standard squarefree predicate to the repo-local valuation. This completes the algebraic layer before any analytic number theory appears in the framework.
scope and limits
- Does not prove analytic estimates or results involving the zeta function.
- Does not depend on J-cost, phi-ladder, or other Recognition Science primitives.
- Does not introduce axioms, sorries, or hidden hypotheses.
- Does not claim uniqueness of factorization beyond what Mathlib already provides.
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