costSpectrumValue
The definition supplies the total cost c(n) of a natural number n as the sum of k times J(p) over each prime power p^k in the factorization of n, with c(0) set to zero by convention. Number theorists extending the Recognition Science cost function to integers cite it to obtain a completely additive arithmetic function on the naturals. It is realized as a direct sum over the factorization map that delegates each term to the primeCost helper.
claim$c(n) := 0$ if $n=0$, and $c(n) := ∑_{p^k ‖ n} k · J(p)$ otherwise, where the sum runs over the prime factorization of $n$ and $J$ denotes the Recognition cost function.
background
The Prime Cost Spectrum module extends the Recognition Science cost function J from positive reals to a completely additive arithmetic function on the naturals. For n ≥ 1 the cost is defined by c(n) := Σ v_p(n) · J(p), where v_p(n) is the p-adic valuation; this makes c(m·n) = c(m) + c(n) for positive m, n. The primeCost auxiliary isolates J(p) for each prime p, treating primes as the irreducible transactions whose costs form the spectrum basis.
proof idea
One-line definition that applies Nat.factorization.sum to the map sending each prime-exponent pair (p, k) to (k : ℝ) * primeCost p.
why it matters in Recognition Science
This definition is the central object of the PrimeCostSpectrum module and is invoked by the master certificate cost_spectrum_certificate, which packages positivity, strict monotonicity on primes, and complete additivity. It also feeds the twisted-cost constructions in CostTwistedLSeries and the monotonicity bounds costSpectrumValue_le_mul and costSpectrumValue_le_omega_mul_jcost. Within the Recognition framework it supplies the arithmetic extension of J required for reformulating prime-counting functions and for the cost spectrum that appears in the forcing chain.
scope and limits
- Does not prove that c is nonnegative or additive; those are separate theorems.
- Does not compute explicit numerical values for concrete n.
- Does not restrict the domain to primes or to square-free integers.
- Does not supply asymptotic growth estimates or prime-counting reformulations.
formal statement (Lean)
132def costSpectrumValue (n : ℕ) : ℝ :=
proof body
Definition body.
133 n.factorization.sum fun p k => (k : ℝ) * primeCost p
134
used by (15)
-
cost_twisted_certificate -
twistedCostSpectrumValue_one_char -
cost_spectrum_certificate -
costSpectrumValue_le_mul -
costSpectrumValue_le_omega_mul_jcost -
costSpectrumValue_mul -
costSpectrumValue_nonneg -
costSpectrumValue_one -
costSpectrumValue_pos -
costSpectrumValue_pow -
costSpectrumValue_pow_general -
costSpectrumValue_prime -
costSpectrumValue_zero -
chi8_periodic -
recognitionThetaTerm