costSpectrumValue_pow
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.
claimIf $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 in Recognition Science
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.
scope and limits
- Does not hold if the base fails to be prime.
- Does not cover real or negative exponents.
- Does not include bounds or inequalities on the cost value.
- Does not address composite numbers directly, though additivity covers them separately.
formal statement (Lean)
153theorem costSpectrumValue_pow {p k : ℕ} (hp : Nat.Prime p) :
154 costSpectrumValue (p ^ k) = (k : ℝ) * primeCost p := by
proof body
Term-mode proof.
155 unfold costSpectrumValue
156 rw [Nat.Prime.factorization_pow hp]
157 simp [Finsupp.sum_single_index]
158
159/-- The cost is completely additive over coprime products.
160 For arbitrary products with positive factors, the same identity holds
161 because `Nat.factorization` is additive on positive multiplications. -/