costSpectrumValue_le_mul
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not assert strict inequality when n > 1.
- Does not apply to m = 0 or n = 0.
- Does not supply explicit growth rates or bounds beyond the inequality.
- Does not connect c to the continuous J function outside the prime-factor definition.
formal statement (Lean)
189theorem costSpectrumValue_le_mul {m n : ℕ} (hm : m ≠ 0) (hn : n ≠ 0) :
190 costSpectrumValue m ≤ costSpectrumValue (m * n) := by
proof body
Term-mode proof.
191 rw [costSpectrumValue_mul hm hn]
192 have := costSpectrumValue_nonneg n
193 linarith
194
195/-- The cost is strictly positive for any integer `n ≥ 2`. -/