costSpectrumValue_nonneg
The theorem establishes nonnegativity of the cost spectrum value c(n) for every natural number n, where c(n) is the sum of v_p(n) times J(p) over primes p dividing n. Number theorists extending the Recognition Science cost function to arithmetic settings would cite this when proving monotonicity or bounding integer costs. The proof unfolds the Finsupp sum definition and verifies each summand is nonnegative by combining primality extraction, valuation nonnegativity, and the strict positivity of prime costs.
claimFor every natural number $n$, $0 ≤ c(n)$ where $c(n) = ∑_p v_p(n) · J(p)$ and $J$ is the Recognition Science cost function on primes.
background
The Prime Cost Spectrum module extends the Recognition Science cost function J from positive reals to natural numbers by defining costSpectrumValue n via prime factorization: c(n) := Σ_p v_p(n) · J(p). This yields a completely additive arithmetic function satisfying c(m n) = c(m) + c(n) for m, n > 0, with the spectrum {J(p)} supplying the irreducible cost quanta. The module imports Cost and PrimeLedgerStructure to ground the extension in the ledger factorization of (ℝ₊, ×) and the phi-forcing calibration of J.
proof idea
The tactic proof unfolds costSpectrumValue to its Finsupp sum, applies Finsupp.sum_nonneg, then for each prime factor p extracts Nat.Prime p via Nat.prime_of_mem_primeFactors on the factorization support. It casts the valuation to a nonnegative real using Nat.zero_le, invokes primeCost_pos to obtain J(p) > 0, and closes with mul_nonneg on the product term.
why it matters in Recognition Science
This nonnegativity result is invoked directly by the downstream theorem costSpectrumValue_le_mul to prove monotonicity of c under multiplication by positive integers, via additivity plus the present nonnegativity. It completes one of the core listed properties in the module (c(n) ≥ 0) and supports the framework's treatment of c as a nonnegative completely additive function built from the J-cost spectrum. The result aligns with upstream J-cost structures from PhiForcingDerived and LedgerFactorization, ensuring nonnegativity propagates from the forcing chain to the integer arithmetic extension.
scope and limits
- Does not establish strict positivity for any n > 1.
- Does not apply to n = 0 or negative integers.
- Does not supply explicit positive lower bounds or growth estimates.
- Does not address asymptotic density or prime-counting reformulations.
Lean usage
rw [costSpectrumValue_mul hm hn]; have := costSpectrumValue_nonneg n; linarithformal statement (Lean)
175theorem costSpectrumValue_nonneg (n : ℕ) :
176 0 ≤ costSpectrumValue n := by
proof body
Tactic-mode proof.
177 unfold costSpectrumValue
178 apply Finsupp.sum_nonneg
179 intro p hp_mem
180 have hp_prime : Nat.Prime p := Nat.prime_of_mem_primeFactors
181 (Nat.support_factorization n ▸ hp_mem)
182 have hk_nonneg : (0 : ℝ) ≤ (n.factorization p : ℝ) := by
183 exact_mod_cast Nat.zero_le _
184 have hJ_nonneg : 0 ≤ primeCost p := le_of_lt (primeCost_pos hp_prime)
185 exact mul_nonneg hk_nonneg hJ_nonneg
186
187/-- Cost is monotonic under multiplication by positive integers
188 (a direct consequence of additivity and nonnegativity of prime costs). -/