costSpectrumValue_pow
plain-language theorem explainer
For a prime p and natural number k the cost spectrum value of p^k equals k times the prime cost of p. Number theorists in Recognition Science cite this when decomposing costs of prime powers into irreducible quanta. The proof reduces directly by unfolding the spectrum definition, invoking the prime-power factorization identity, and simplifying the resulting sum.
Claim. If $p$ is prime and $k$ a natural number, then the cost spectrum value of $p^k$ equals $k$ times the prime cost of $p$, that is $c(p^k) = k · J(p)$.
background
The module defines the cost spectrum value $c(n)$ for each natural number $n$ as the sum over primes $p$ of the p-adic valuation $v_p(n)$ times $J(p)$. This construction makes $c$ completely additive, satisfying $c(m n) = c(m) + c(n)$ for positive integers $m$ and $n$, as described in the module documentation. Prime cost of a prime $p$ is defined to be $J(p)$. The upstream cost definitions from MultiplicativeRecognizerL4 and ObserverForcing supply the J-cost as the derived cost of recognition comparators and events, grounding the arithmetic extension.
proof idea
The proof unfolds costSpectrumValue to expose the factorization sum, rewrites using the lemma that the factorization of a prime power $p^k$ is a single term $k$ at $p$, and applies simplification to the Finsupp sum over a singleton support.
why it matters
This result fills one of the core theorems in the Prime Cost Spectrum module, confirming linear scaling of cost with exponent for prime powers. It reinforces the interpretation of the cost spectrum as the irreducible quanta from which all natural-number costs are assembled, consistent with the Recognition Science derivation of arithmetic functions from the J-equation. The module lists it among the zero-sorry results that enable clean reformulations of classical prime-counting functions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.