Jcost_strict_mono_on_one_infty
plain-language theorem explainer
The J-cost function J(x) = (x + 1/x)/2 - 1 is strictly increasing for x > 1. Researchers modeling defect costs or strain ordering in the Recognition Science framework would cite this result when comparing positive arguments on the phi-ladder. The proof rewrites both sides via the squared identity J(x) = (x-1)^2/(2x), then shows the auxiliary map f(t) = (t-1)^2/t is strictly increasing on [1, ∞) by factoring the difference (a-1)^2 b - (b-1)^2 a = (a-b)(ab-1) and applying sign analysis.
Claim. Let $J(x) = (x + x^{-1})/2 - 1$. For real numbers $x, y > 0$ satisfying $1 ≤ x < y$, one has $J(x) < J(y)$.
background
J-cost is the central cost function of the Recognition Science framework, defined by J(x) = (x + x^{-1})/2 - 1 (equivalently cosh(log x) - 1). The JcostCore module develops its algebraic and ordering properties to support cost comparisons along the forcing chain. The upstream lemma Jcost_eq_sq supplies the equivalent squared form J(x) = (x-1)^2/(2x) for x ≠ 0, which converts monotonicity statements into rational inequalities.
proof idea
The tactic proof applies Jcost_eq_sq to both sides, reduces the target inequality to (x-1)^2 y < (y-1)^2 x after clearing positive denominators, and introduces the auxiliary f(t) = (t-1)^2/t. It proves f strictly increasing on [1, ∞) by direct expansion: (a-1)^2 b - (b-1)^2 a = (a-b)(ab-1), whose sign is negative when 1 ≤ a < b. Scaling by the positive constant 2 recovers the original comparison.
why it matters
This lemma supplies the basic ordering property of J-cost on (1, ∞) required for consistent defect ranking in the Recognition framework. It aligns with T5 J-uniqueness and the positive-strain regime above the Berry threshold phi^{-1}. Although no immediate downstream uses are recorded, the result closes a prerequisite for cost-based arguments in the eight-tick octave and D = 3 derivations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.