primeCost_strictMono
plain-language theorem explainer
The result shows that the prime cost function is strictly monotonic on the primes. If p and q are primes satisfying p less than q, then the cost of p is less than the cost of q. Workers on the cost spectrum in Recognition Science cite this when assembling the master certificate of spectrum properties. The short tactic proof unfolds the definition and reduces the claim to the strict monotonicity of the underlying J function on the reals from 1 onward.
Claim. For primes $p, q$ in the natural numbers with $p < q$, the prime cost satisfies $J(p) < J(q)$, where $J$ is the recognition cost function and primeCost denotes its restriction to primes.
background
The Prime Cost Spectrum module extends the J-cost function from the Cost module to an arithmetic function on the naturals by prime factorization. primeCost p is defined as J(p) cast to the reals for a prime p. The full costSpectrumValue n sums the terms k · J(p) over the prime-power factors of n, yielding a completely additive function c(m · n) = c(m) + c(n) for positive m, n.
proof idea
The tactic proof unfolds primeCost, then builds real inequalities showing both p and q are at least 1 (via the fact that primes exceed 1) and that p is strictly less than q. It finishes by applying the sibling lemma jcost_strictMono_on_one_le, which encodes the strict increase of J on the reals from 1 onward.
why it matters
This theorem supplies the strict-monotonicity clause inside the master certificate cost_spectrum_certificate, which collects the elementary spectrum properties for the companion paper. It guarantees that the irreducible cost quanta J(p) increase with the prime index, supporting the extension of J to number theory while preserving the ordering from J-uniqueness in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.