costSpectrumValue_one
plain-language theorem explainer
The cost of the unit integer under the prime factorization cost spectrum vanishes. Number theorists reformulating Chebyshev functions or Recognition Science practitioners building additive arithmetic functions cite this base case. The proof reduces directly to the empty sum in the definition of the cost via the factorization of 1.
Claim. Let $c : ℕ → ℝ$ be the completely additive function given by $c(n) = ∑_{p^k ‖ n} k · J(p)$, where $J$ is the Recognition Science cost function. Then $c(1) = 0$.
background
In this module the Recognition Science cost function $J$ on positive reals is extended to a completely additive arithmetic function $c$ on natural numbers. For each $n$ the value $c(n)$ is the sum over the prime factorization of $n$ of the term $k$ times $J(p)$ for each $p^k$ dividing $n$. By convention the cost of 1 is zero because its factorization is empty. The definition costSpectrumValue implements this sum using Nat.factorization. This base case supports the master certificate of elementary properties and the induction in the power rule for the cost function.
proof idea
The proof is a one-line wrapper that unfolds the definition of costSpectrumValue and simplifies using the empty factorization of 1.
why it matters
This result supplies the base case for the cost spectrum certificate, which collects the elementary properties of $c$ used in the companion paper. It also serves as the induction base for the general power rule costSpectrumValue_pow_general and appears in the recognition theta term at $n=1$. Within the framework it anchors the extension of $J$ to integers, consistent with the complete additivity required for reformulations of prime counting functions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.