costSpectrumValue_nonneg
plain-language theorem explainer
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.
Claim. For 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.