jq_le_reflect
plain-language theorem explainer
On rationals at or above 1, the native J-display reflects order: J(s) ≤ J(t) forces s ≤ t. Anyone proving injectivity of J above the unit, or transferring inequalities through monotone multiplicative costs, cites this. The argument is a short contradiction that invokes strict monotonicity of J on [1, ∞).
Claim. Let $s,t\in\mathbb{Q}$ with $t\ge 1$, and write $J(x)=\frac{x+x^{-1}}{2}-1$. If $J(s)\le J(t)$, then $s\le t$. (The hypothesis $s\ge 1$ is present in the signature but unused once $t\ge 1$ and the order comparison are given.)
background
In the Primitive Recognition Calculus native-cost ledger, the rational display of the Recognition cost is
$$J_{\mathbb{Q}}(t)=\frac{t+t^{-1}}{2}-1,$$
the same algebraic shape as the unique J forced by the Recognition Composition Law (T5: $J(x)=\cosh(\log x)-1$). The ledger works over $\mathbb{Q}$ so that later gauge-orbit and character factorizations stay exact.
Upstream, jq_strictMono already shows that on the ray $[1,\infty)$ this display is strictly increasing: if $1\le s<t$ then $J(s)<J(t)$, via the identity
$$t+t^{-1}-(s+s^{-1})=(t-s)(st-1)/(st).$$
Order reflection is the converse inequality direction needed for antisymmetry and for inequality transfer along monotone multiplicative maps.
proof idea
Tactic proof by contradiction. Assume $\neg(s\le t)$, so $t<s$. Apply strict monotonicity of $J$ on $[1,\infty)$ at the pair $(t,s)$ (using $t\ge 1$ and $t<s$) to obtain $J(t)<J(s)$, i.e. $\neg(J(s)\le J(t))$. That contradicts the hypothesis $J(s)\le J(t)$. One by_contra / push_neg / absurd chain; no new algebra beyond the upstream strict-mono lemma.
why it matters
This is the order-reflection half of J-rigidity on the unit ray. Downstream, injectivity above 1 is immediate antisymmetry:
$$J(s)=J(t)\implies s=t$$
via two applications of reflection (jq_inj_ge_one). That injectivity is the first step toward gauge rigidity for monotone costs that factor through characters.
The same reflection feeds the ledger's transfer lemmas that push power inequalities between bases along monotone multiplicative $h:\mathbb{N}\to\mathbb{Q}$. In the broader RS chain this is local bookkeeping for T5 J-uniqueness: once J is known to be the unique cost shape, one still needs that its rational display sees order faithfully above the fixed point 1, so the phi-ladder and composition-law orbit cannot collapse distinct ratios.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.