jq_mono
plain-language theorem explainer
On rationals at least 1, the J-display J(x)=(x+x^{-1})/2-1 is nondecreasing. Anyone proving native-cost monotonicity along ratio orbits or power-generated costs cites this. The proof is a short algebraic identity: the difference of the two displays factors as a product of nonnegative terms over a positive denominator.
Claim. For rationals $s,t$ with $1\le s\le t$, one has $J_{\mathbb{Q}}(s)\le J_{\mathbb{Q}}(t)$, where $J_{\mathbb{Q}}(x)=\frac{x+x^{-1}}{2}-1$.
background
The module builds a structural ledger for native recognition costs on rationals. The central display is the rational J-cost
$$J_{\mathbb{Q}}(t)=\frac{t+t^{-1}}{2}-1,$$
the same functional form forced uniquely by the Recognition Composition Law (T5: $J(x)=\cosh(\log x)-1$). Sibling facts already record nonnegativity, the zero locus at $t=1$, and the closed-form identity on ratio orbits.
Monotonicity is the remaining elementary property needed before one can lift $J_{\mathbb{Q}}$ to a monotone native cost on positive rationals generated by integer powers or selected characters. The ambient setting is the Primitive Recognition Calculus: costs are read off rational characters, then certified monotone so that gauge-orbit comparisons are well-ordered.
proof idea
First obtain $s>0$ and $t>0$ from $1\le s\le t$. The key algebraic step rewrites
$$t+t^{-1}-(s+s^{-1})=\frac{(t-s)(st-1)}{st}$$
by field_simp and ring. The numerator is nonnegative: $t-s\ge 0$ by hypothesis and $st-1\ge 0$ because both factors are at least 1 (nlinarith). The denominator $st>0$, so the whole difference is nonnegative by div_nonneg. Unfolding $J_{\mathbb{Q}}$ and a final linarith yields $J_{\mathbb{Q}}(s)\le J_{\mathbb{Q}}(t)$.
why it matters
This is the monotone engine for every native-cost certificate in the structural ledger. Downstream it is applied directly by canonicalSelectedNativeCost_monotone and powerGeneratedNativeCost_monotone, and it feeds signedPowerNativeCost_monotone in the gauge-orbit layer and the MonoMult instance for natural embeddings.
In the forcing chain it is the rational shadow of T5 J-uniqueness: once $J$ is forced, its increase away from the fixed point $1$ is what makes larger ratio steps cost more. Without this inequality the ledger cannot certify that selected or power-generated native costs are PRC-monotone, blocking the passage from character data to ordered cost comparisons used later in mass and coupling extractions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.