costSpectrumValue_mul
plain-language theorem explainer
The cost spectrum value on positive integers is completely additive: c(m n) equals c(m) plus c(n) for m, n positive. Number theorists building arithmetic extensions of the J-cost for prime spectra, twisted L-series, and certificates would cite this. The proof unfolds the definition to the Finsupp sum, rewrites the factorization of the product, and applies sum_add_index' with simp and ring to verify additivity of the indices.
Claim. Let $c(k) = ∑_p v_p(k) · J(p)$ be the cost spectrum value of a positive integer $k$. Then for positive integers $m, n$, $c(m · n) = c(m) + c(n)$.
background
The Prime Cost Spectrum module extends the Recognition Science cost function J to natural numbers by defining costSpectrumValue n as the sum over primes p of the p-adic valuation v_p(n) times J(p). This construction yields a completely additive arithmetic function on positive integers. The module draws on cost definitions from MultiplicativeRecognizerL4 (derived cost of a comparator on positive ratios) and ObserverForcing (J-cost of a recognition event), together with the ledger factorization structure that calibrates J on the positive reals.
proof idea
Unfold costSpectrumValue to expose the Finsupp sum over the prime factorization. Rewrite the factorization of the product via Nat.factorization_mul. Apply Finsupp.sum_add_index' and discharge the two side conditions: simp handles the zero-index case while push_cast followed by ring verifies the additive case for the indices.
why it matters
This result supplies the complete additivity of the cost spectrum that feeds directly into the master certificate cost_spectrum_certificate, the twisted power rule in CostTwistedLSeries, the monotonicity lemma costSpectrumValue_le_mul, and the general power rule costSpectrumValue_pow_general. It completes the arithmetic extension step required for reformulating prime-counting functions in terms of c and aligns with the Recognition Composition Law by making the integer cost additive under multiplication.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.