jq_lt_zero
plain-language theorem explainer
For every negative rational t, the rational J-display jq(t)=(t+t^{-1})/2-1 is strictly negative. Used when monotone multiplicative characters on N are forced positive above the unit. Proof rewrites to the closed form (t-1)^2/(2t) and reads off the sign of the fraction.
Claim. If $t\in\mathbb{Q}$ satisfies $t<0$, then $\displaystyle\frac{t+t^{-1}}{2}-1<0$. Equivalently, via the closed form valid for $t\neq 0$, $\displaystyle\frac{(t-1)^2}{2t}<0$.
background
In the Primitive Recognition Calculus native-cost ledger, the rational J-display is
$$jq(t):=\frac{t+t^{-1}}{2}-1$$
on $\mathbb{Q}\setminus{0}$. It is the exact rational specialization of the RS cost $J(x)=\cosh(\log x)-1$ forced at T5, and of the event cost used throughout ObserverForcing and the multiplicative-recognizer stack.
The sibling identity jq_closed rewrites it as
$$jq(t)=\frac{(t-1)^2}{2t}\qquad(t\neq 0).$$
That algebraic form makes sign analysis elementary: the numerator is a square, so the sign of $jq$ is controlled by the sign of $t$. The present lemma treats the negative case; the nonnegativity and zero-locus lemmas sit beside it in the same ledger.
proof idea
One short tactic proof. Rewrite with jq_closed (applicable because $t<0$ implies $t\neq 0$). The goal becomes
$$\frac{(t-1)^2}{2t}<0.$$
Apply div_neg_of_pos_of_neg: the numerator $(t-1)^2$ is positive by pow_two_pos_of_ne_zero (since $t<0$ forces $t\neq 1$), and the denominator $2t$ is negative by linarith. No further structure is used.
why it matters
This is a pure sign lemma for the rational J-display, but it is load-bearing for the monotone-character package in the same module. The structure MonoMult packages completely multiplicative maps $h:\mathbb{N}\to\mathbb{Q}$ whose cost $n\mapsto jq(h n)$ is nondecreasing. The theorem pos then uses jq_lt_zero to show that monotonicity alone rules out negative values of $h$ above the unit: if $h n<0$ for some $n\ge 2$, then $jq(h n)<0=jq(1)$, contradicting mono from $1$ (or from $2$ once $h2>0$ is fixed).
In RS terms this keeps native cost on the positive branch of the J-curve forced at T5, so the structural ledger stays compatible with the Recognition Composition Law and with the nonnegativity of event cost used upstream. It does not itself force uniqueness of characters; it only clears the negative orthant so later positivity and uniqueness arguments can run.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.