costSpectrumValue_zero
plain-language theorem explainer
costSpectrumValue_zero establishes that the arithmetic cost function c vanishes at zero. Researchers extending the J-cost to integers via prime factorization cite this base case when verifying additivity and handling boundary cases over all natural numbers. The proof is a direct unfolding of the summation definition followed by simplification with the empty factorization of zero.
Claim. $c(0) = 0$, where $c(n)$ is the total cost of $n$ given by the sum over its prime factorization of $k · J(p)$ for each $p^k ‖ n$.
background
The Prime Cost Spectrum module extends the Recognition Science cost function J from positive reals to a completely additive arithmetic function c on natural numbers. For n ≥ 1, c(n) equals the sum over prime powers in the factorization of n of k · J(p), so that c(m · n) = c(m) + c(n). By explicit convention the definition sets c(0) = 0, making the function total on ℕ ∪ {0}.
proof idea
The proof unfolds the definition of costSpectrumValue and applies simp with Nat.factorization_zero, which reduces the empty sum over the factorization of zero to the value 0.
why it matters
This theorem supplies the zero base case for the cost spectrum, ensuring the convention in the definition of costSpectrumValue is realized as a theorem. It completes the initial segment of the module's main results (alongside costSpectrumValue_one) that allow reformulation of classical prime-counting functions in terms of c. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.