jq_strictMono
plain-language theorem explainer
On rationals at or above the unit, the native J-display is strictly increasing: if 1 ≤ s < t then J(s) < J(t). Anyone proving order reflection for J, anchor injectivity of odd-power native costs, or that monotone characters stay above the unit cites this. The proof is a short field-identity plus positivity: the difference of the symmetric sums factors as (t−s)(st−1)/(st).
Claim. Let $s,t\in\mathbb{Q}$ with $1\le s<t$. Write $J(x)=(x+x^{-1})/2-1$. Then $J(s)<J(t)$.
background
In the primitive recognition calculus, the native cost on a positive rational is the J-display
$$J_q(t);:=;(t+t^{-1})/2-1,$$
the same functional form forced uniquely (up to scaling) by the Recognition Composition Law and the T5 uniqueness step of the forcing chain. The structural ledger develops elementary calculus of $J_q$ on $\mathbb{Q}$ before lifting to orbit characters and native-cost certificates.
The local setting is the region at or above the multiplicative unit: $s\ge 1$. There $J_q$ is nonnegative, vanishes only at $1$, and (by this lemma) is strictly monotone. Sibling facts already record $J_q(1)=0$, nonnegativity on $[1,\infty)$, and the closed-form identity used below. Downstream order-reflection and injectivity arguments need the strict direction, not merely weak monotonicity.
proof idea
From $1\le s<t$ one gets $s>0$ and $t>0$, hence $st>1$ by nlinarith. The algebraic key is the cleared identity
$$t+t^{-1}-(s+s^{-1})=(t-s)(st-1)/(st),$$
obtained by field_simp and ring. The numerator is a product of two positive terms (mul_pos/linarith), the denominator is positive, so the difference of symmetric sums is positive by div_pos. Unfolding $J_q$ and a final linarith yields $J_q(s)<J_q(t)$. No external analysis lemmas are required; everything is rational field arithmetic.
why it matters
Strict monotonicity of $J_q$ on $[1,\infty)$ is the order engine for the native-cost ledger. It feeds three immediate parents: jq_le_reflect (order reflection: $J_q(s)\le J_q(t)$ with both arguments $\ge 1$ forces $s\le t$), ge_one (a monotone multiplicative character with anchor $>1$ stays $\ge 1$ above the unit; dipping below would contradict cost comparison with the orbit $2$), and oddPowerGeneratedNativeCost_anchor_injective (distinct odd exponents give distinct costs at the orbit $2$ because $J_q(2^{2k+1})$ is strictly increasing in the exponent).
Framework-wise this is the elementary rational shadow of T5 J-uniqueness: the same $J(x)=(x+x^{-1})/2-1$ that the forcing chain isolates is here shown to be a strict order embedding on the half-line that the ledger uses for cost comparison. Without it, anchor separation and the "no dip below the unit" contradiction both fail.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.