costSpectrumValue_pow_general
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not apply when n = 0.
- Does not address non-integer exponents.
- Does not supply bounds or asymptotic estimates.
- Does not connect to the phi-ladder or physical constants.
Lean usage
theorem example_use (n : ℕ) (hn : n ≠ 0) : costSpectrumValue (n ^ 2) = 2 * costSpectrumValue n := by exact costSpectrumValue_pow_general hn 2formal statement (Lean)
259theorem costSpectrumValue_pow_general {n : ℕ} (hn : n ≠ 0) (k : ℕ) :
260 costSpectrumValue (n ^ k) = (k : ℝ) * costSpectrumValue n := by
proof body
Term-mode proof.
261 induction k with
262 | zero => simp [costSpectrumValue_one]
263 | succ k ih =>
264 have hnk : n ^ k ≠ 0 := pow_ne_zero k hn
265 rw [pow_succ, costSpectrumValue_mul hnk hn, ih]
266 push_cast
267 ring
268
269/-- The cost spectrum value is bounded by `Ω(n) · J(p_max)` where
270 `p_max` is the largest prime factor of `n`. Specialized to the
271 weaker bound `c(n) ≤ Ω(n) · J(n)` using monotonicity of `J` on
272 `[1, ∞)`. Useful for asymptotic upper bounds. -/