vp_prime_self
The result states that the exponent of a prime p in its own factorization equals one. Number theorists using the local valuation interface for prime factorization work would cite this identity as the base case. The proof converts the hypothesis via the prime equivalence and simplifies the definition against the self-factorization property.
claimLet $p$ be a prime natural number. Then the exponent of $p$ in the prime factorization of $p$ equals one.
background
The module supplies a thin wrapper around Mathlib's Nat.factorization. The function vp p n extracts the exponent of p in the factorization of n. The predicate Prime is the transparent alias for Nat.Prime, linked by the equivalence prime_iff that identifies the two notions directly.
proof idea
The proof applies prime_iff to obtain Nat.Prime p from the hypothesis. It then rewrites via simp on the definition of vp together with the Mathlib fact that a prime factors to itself with exponent one.
why it matters in Recognition Science
This identity supplies the self-case inside the factorization interface of the NumberTheory.Primes.Factorization module. It anchors the reusable laws vp_mul and vp_pow that later support squarefree detection and Möbius inversion steps in the Recognition pipeline. No open questions remain attached to this base fact.
scope and limits
- Does not address valuations when the base is composite.
- Does not compute exponents for arguments other than the prime itself.
- Does not connect to arithmetic functions beyond factorization.
formal statement (Lean)
58theorem vp_prime_self {p : ℕ} (hp : Prime p) : vp p p = 1 := by
proof body
Term-mode proof.
59 have hp' : Nat.Prime p := (prime_iff p).1 hp
60 simp [vp, hp'.factorization_self]
61
62/-- For distinct primes `p ≠ q`, `vp p q = 0`. -/