costSpectrumValue_prime
plain-language theorem explainer
For any prime number p the cost spectrum value of p equals its prime cost J(p). Researchers building the Recognition cost function on integers cite this when reducing composite costs via unique factorization. The proof is a direct unfolding of the summation definition followed by the single-term factorization of a prime.
Claim. For every prime number $p$, the cost spectrum value $c(p)$ equals the prime cost $J(p)$, where $c(n)$ is the sum of $k·J(p)$ over the prime factorization of $n$.
background
The module extends the J-cost from positive reals to natural numbers by defining costSpectrumValue n as the sum over p^k || n of k·primeCost p, making c completely additive. primeCost p is Jcost applied to p, the irreducible cost quanta for the spectrum. costSpectrumValue is the total cost of an integer n defined via its prime factorization, with c(0) = 0 by convention.
proof idea
The proof unfolds the definition of costSpectrumValue, rewrites using the factorization of a prime (a single p^1 term), and simplifies the Finsupp sum to the single term primeCost p.
why it matters
This establishes the base case that primes carry cost exactly J(p), which feeds directly into the master certificate theorem cost_spectrum_certificate that collects all elementary spectrum properties. It completes the step in the NumberTheory module that permits reformulating classical prime-counting functions in terms of c, supporting the arithmetic extension of the J-cost within the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.