cost_spectrum_certificate
plain-language theorem explainer
The cost_spectrum_certificate bundles eight elementary arithmetic properties of the cost spectrum c on positive integers, where c(n) sums J(p) over the prime-power factors of n with multiplicity. Number theorists in Recognition Science cite it when invoking positivity, strict monotonicity on primes, complete additivity, and the Omega bound for c. The proof is a one-line term wrapper that packages the eight component theorems already established in the module.
Claim. Let $c(n) = c(n)$ denote the cost spectrum value of a positive integer $n$, defined via its prime factorization as $c(n) = sum_p v_p(n) J(p)$ where $J$ is the Recognition cost function and $v_p(n)$ is the $p$-adic valuation. Let $Omega(n)$ be the total number of prime factors of $n$ counted with multiplicity. Then: (1) $0 < c(p)$ for every prime $p$; (2) $c(p) < c(q)$ for primes $p < q$; (3) $c(1) = 0$; (4) $0 < c(n)$ for all $n >= 2$; (5) $c(m n) = c(m) + c(n)$ for positive integers $m, n$; (6) $c(p) = J(p)$ for every prime $p$; (7) $c(n^k) = k c(n)$ for positive integers $n, k$; (8) $c(n) <= Omega(n) J(n)$ for all $n >= 2$.
background
The module extends the Recognition Science cost function J from positive reals to natural numbers by setting c(n) equal to the sum over primes p of v_p(n) times J(p). This construction makes c completely additive, so c(m n) = c(m) + c(n) for all positive m, n. Omega(n) is defined as the sum of the exponents in the prime factorization of n. The J-cost itself originates in the definitions of recognition-event cost and multiplicative-recognizer cost, both of which return the underlying J value of the state or comparator.
proof idea
The proof is a one-line term-mode wrapper that assembles a tuple from the eight component theorems: primeCost_pos, primeCost_strictMono, costSpectrumValue_one, costSpectrumValue_pos, costSpectrumValue_mul, costSpectrumValue_prime, costSpectrumValue_pow_general, and costSpectrumValue_le_omega_mul_jcost.
why it matters
This certificate supplies the basic arithmetic infrastructure for the cost spectrum inside Recognition Science number theory and is invoked directly by polyCost_pos to obtain positivity for nonzero non-unit polynomials. The complete additivity and prime decomposition align with the J-uniqueness property (T5) in the forcing chain, allowing classical prime-counting functions to be rewritten in terms of c. No open questions or scaffolding remain in this declaration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.