jcost_strictMono_on_one_le
plain-language theorem explainer
The cost function J is strictly increasing on the interval [1, ∞). Number theorists constructing the prime cost spectrum cite this result to guarantee that distinct primes receive distinct cost values. The algebraic proof rewrites J via its squared-ratio expression and verifies the rearranged inequality (y - x)(xy - 1) > 0 by case analysis on whether the lower argument equals 1.
Claim. The function $J(x) = (x-1)^2/(2x)$ is strictly increasing on the interval $[1, ∞)$.
background
The Prime Cost Spectrum module extends the real-valued cost function J to a completely additive arithmetic function on the naturals: for n ≥ 1, c(n) equals the sum over primes p of v_p(n) · J(p), where v_p is the p-adic valuation. This makes c(m n) = c(m) + c(n) for all positive m, n. The auxiliary definitions primeCost and costSpectrumValue simply restrict J to primes and assemble the total cost, respectively.
proof idea
The tactic proof introduces x and y satisfying 1 ≤ x < y, rewrites both J values with the squared-ratio lemma Jcost_eq_sq, clears the positive factor 2, and reduces the target inequality to (y-1)^2 x < (x-1)^2 y. It applies the ring identity (y-1)^2 x - (x-1)^2 y = (y-x)(xy-1), then splits on whether x = 1. When x > 1 both factors are positive; when x = 1 the left side vanishes while the right side remains positive.
why it matters
This lemma supplies the strict monotonicity needed by primeCost_strictMono (which lifts the result to primes) and by costSpectrumValue_le_omega_mul_jcost (which replaces each J(p) by the larger J(n)). It therefore ensures the cost spectrum separates distinct primes and supplies the analytic input for all subsequent bounds on c(n). In the Recognition framework it closes the step from the functional equation for J to the separation of irreducible cost quanta on the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.