jq_nonneg
plain-language theorem explainer
On every positive rational the J-display is nonnegative. Cost-positivity arguments, monotone multiplicative characters, and the structural native-cost ledger all cite this bound. The proof rewrites J to its squared closed form and finishes by the positivity tactic.
Claim. For every rational $t>0$, the J-display $J(t)=\frac{t+t^{-1}}{2}-1$ satisfies $0\le J(t)$. Equivalently, after the algebraic identity $J(t)=\frac{(t-1)^2}{2t}$ (valid for $t\ne 0$), the right-hand side is nonnegative whenever $t>0$.
background
The module builds a structural ledger for native recognition costs on ratio orbits. The rational J-display is defined by $J_\mathbb{Q}(t)=(t+t^{-1})/2-1$, the same algebraic skeleton as the continuous cost forced at T5 of the unified forcing chain ($J(x)=\cosh(\log x)-1$).
An upstream closed-form identity rewrites the display, for any nonzero rational, as $J_\mathbb{Q}(t)=(t-1)^2/(2t)$. That squared numerator is the algebraic engine behind nonnegativity, zero-locus, and sign analysis of the ledger.
Locally the ledger treats $J_\mathbb{Q}$ as the cost read-out on positive rationals that later becomes the cost of a completely multiplicative character and of the canonical selected native cost.
proof idea
Term-mode, two steps. First rewrite the goal by the closed-form identity, using $t\ne 0$ from $t>0$. The goal becomes $0\le(t-1)^2/(2t)$. The positivity tactic then discharges the inequality from the squared numerator and the positive denominator.
why it matters
Nonnegativity is the first arithmetic fact the structural ledger needs before it can promote J from a display to a cost. Downstream, the canonical selected native cost is proved positive by reducing to this bound; the MonoMult structure packages nondecreasing $J_\mathbb{Q}\circ h$ as part of monotone completely multiplicative data; positivity of such characters above the unit uses the same inequality to rule out negative values; and the structural theorem that positivity is forced (not axiomatized) ultimately rests on cross-display comparisons that inherit this sign.
In the broader Recognition framework this is the rational shadow of T5 J-uniqueness: the cost that satisfies the Recognition Composition Law is nonnegative on the positive ray and vanishes only at balance. Without the bound, native-cost positivity and the no-pay-for-positive-imbalance slogan would remain hypotheses rather than theorems.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.