vp_prime_pow_ne
plain-language theorem explainer
For distinct primes p and q the exponent of p inside q raised to any natural power k equals zero. Number theorists maintaining the prime factorization interface inside Recognition Science cite the result when separating coprime factors in multiplicative identities. The argument converts the local Prime hypothesis to the standard Nat.Prime predicate, substitutes the single-term factorization of a prime power, and cancels the mismatched index under the distinctness assumption.
Claim. Let $p$ and $q$ be distinct primes and let $k$ be a nonnegative integer. Then the exponent of $p$ in the prime factorization of $q^k$ equals zero.
background
The module supplies a thin wrapper around Mathlib's factorization map that records the exponent of a chosen prime inside a natural number. This wrapper yields reusable algebraic rules for products and powers that later arguments on squarefree detection and Möbius functions can invoke directly. The local theoretical setting is a lightweight number-theoretic layer that embeds standard arithmetic facts into the Recognition Science development without introducing new constants or forcing axioms.
proof idea
Convert the hypothesis that q is Prime into the standard Nat.Prime predicate via the equivalence lemma. Unfold the definition of the exponent map together with the power rule for factorization to obtain a Finsupp whose only nonzero coefficient sits at q. The distinctness hypothesis then forces the coefficient at p to vanish by direct simplification.
why it matters
The result is invoked by the companion statement that sets the valuation to zero for any argument equal to a power of a different prime. It supplies a basic case inside the factorization toolkit required for later prime-based constructions such as those appearing in spectral emergence and complexity structure modules. The step aligns with the overall arithmetic interface that supports the forcing chain without touching J-cost minimization or the phi-ladder directly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.