vp_eq_zero_of_not_dvd
plain-language theorem explainer
When p does not divide n the exponent of p in the prime factorization of n is zero. Researchers building algebraic identities over the Recognition Science prime factorization interface cite this to drop vanishing terms. The proof is a one-line wrapper that unfolds the local exponent definition and invokes the matching Mathlib lemma.
Claim. If $p$ does not divide $n$, then the exponent of $p$ in the prime factorization of $n$ equals zero.
background
The NumberTheory.Primes.Factorization module supplies a thin stable wrapper over Mathlib's Nat.factorization. The exponent function is introduced by the definition vp p n := n.factorization p, which yields reusable algebraic laws for prime work, squarefree detection, and Möbius inversion inside the Recognition Science number theory layer. The upstream vp definition records exactly this implementation, while the imported for structure from UniversalForcingSelfReference supplies meta-realization context not invoked by the present statement.
proof idea
The proof is a one-line wrapper. It simplifies using the definition of the exponent function and then applies the Mathlib lemma Nat.factorization_eq_zero_of_not_dvd directly to the hypothesis that p does not divide n.
why it matters
This supplies a basic vanishing property for the exponent function inside the prime factorization interface. It supports the module goal of delivering reusable algebraic laws for downstream prime computations in the Recognition Science framework, aligning with the need for clean handling of absent primes in factorization identities. No downstream uses are recorded yet, but the fact closes a standard gap without new hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.