costSpectrumValue_pow_general
plain-language theorem explainer
The theorem states that the cost spectrum function c satisfies c(n^k) = k · c(n) for every positive integer n and natural number k. Number theorists extending the Recognition Science cost function to arithmetic would cite this when scaling costs under repeated multiplication. The proof is a direct induction on k that applies the multiplicative property of c at the successor step together with the base case c(1) = 0.
Claim. For every positive integer $n$ and every natural number $k$, $c(n^k) = k · c(n)$, where $c(m)$ denotes the cost spectrum value of $m$ given by the sum of $v_p(m) · J(p)$ over the prime factorization of $m$.
background
The module extends the Recognition Science cost function J from positive reals to a completely additive arithmetic function c on the positive integers. For each n ≥ 1 one defines c(n) := Σ_p v_p(n) · J(p), where v_p(n) is the p-adic valuation; this yields c(m n) = c(m) + c(n) for all m, n > 0. The present result lifts the multiplicative property to arbitrary powers.
proof idea
The proof is by induction on k. The zero case reduces directly to costSpectrumValue_one. In the successor step one rewrites n^{k+1} via pow_succ, applies costSpectrumValue_mul to the product n^k · n, substitutes the inductive hypothesis, casts the coefficient, and closes with ring arithmetic.
why it matters
The result is invoked by the master certificate cost_spectrum_certificate that assembles the elementary properties of the cost spectrum for the companion paper. It completes the demonstration that c is completely additive on the positive integers, consistent with the Recognition Composition Law. No open questions are addressed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.