costSpectrumValue_pos
plain-language theorem explainer
The cost spectrum value c(n) is strictly positive for every integer n at least 2. Number theorists working within Recognition Science would cite this when establishing that the arithmetic cost function has no zeros for n greater than 1. The proof extracts a prime divisor p of n, shows the corresponding summand is positive via primeCost_pos, and splits the Finsupp sum to isolate that positive term from a nonnegative remainder.
Claim. For every natural number $n ≥ 2$, the cost $c(n) > 0$, where $c(n) := ∑_p v_p(n) · J(p)$ and $J(x) = (x + x^{-1})/2 - 1$.
background
The module extends the Recognition Science cost function J from positive reals to natural numbers via prime factorization. For n ≥ 1 the cost spectrum value is defined as c(n) = ∑_p v_p(n) · J(p), making c completely additive so that c(m n) = c(m) + c(n) for positive m, n. The set {J(p) : p prime} supplies the irreducible cost quanta out of which every integer cost is assembled.
proof idea
The tactic proof first obtains n ≠ 0 and n ≠ 1 by omega. It extracts a prime p dividing n via Nat.exists_prime_and_dvd, confirms p lies in the factorization support with positive exponent, and shows the p-summand is positive by primeCost_pos. The sum is rewritten with Finsupp.sum and Finset.sum_erase_add; add_pos_of_nonneg_of_pos then separates the positive p-term from the remaining sum, which is nonnegative by mul_nonneg applied to each other prime factor.
why it matters
This theorem is invoked by cost_spectrum_certificate, the master certificate that assembles positivity, monotonicity and additivity of the cost spectrum for the companion paper. It supplies the strict positivity needed for the spectrum to function as a basis of integer costs, consistent with convex J-cost minimization and the discrete phi-ladder structure. No open scaffolding questions are directly addressed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.