costSpectrumValue_le_mul
plain-language theorem explainer
The cost spectrum value c(m) satisfies c(m) ≤ c(m n) for all positive integers m and n. Number theorists extending the Recognition Science cost function to arithmetic would cite this monotonicity when bounding costs of composites from prime factors. The proof is a one-line algebraic reduction that invokes additivity of c and non-negativity of the extra factor.
Claim. For positive integers $m, n$, the cost $c(m) ≤ c(m n)$, where $c(k) = ∑_p v_p(k) J(p)$ is the completely additive function built from the prime cost spectrum.
background
The module defines the prime cost spectrum by extending the Recognition Science cost J from positive reals to natural numbers via prime factorization. For each n ≥ 1 the cost is c(n) := ∑_{p^k || n} k · J(p) = ∑_p v_p(n) · J(p), making c completely additive: c(m n) = c(m) + c(n) for m, n > 0. The spectrum {J(p) : p prime} supplies the irreducible quanta from which every integer cost is assembled. This theorem relies on the sibling results costSpectrumValue_mul (additivity) and costSpectrumValue_nonneg (c(n) ≥ 0 for all n).
proof idea
One-line wrapper that applies the additivity theorem costSpectrumValue_mul to rewrite costSpectrumValue (m * n) as costSpectrumValue m + costSpectrumValue n, then invokes costSpectrumValue_nonneg on the second summand and closes with linarith.
why it matters
The result supplies the monotonicity property required for the prime cost spectrum, completing the list of basic theorems in the module (additivity, non-negativity, values on primes and powers). It supports reformulations of classical prime-counting functions in terms of c and follows directly from the completely additive structure induced by J. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.