jq_neg
plain-language theorem explainer
Sign reversal of a rational display argument negates the J-display and subtracts two. Anyone proving orientation-reversal for signed-power or odd-power native costs cites this identity. The proof unfolds the definition, applies inverse-of-negative, and closes by ring arithmetic on rationals.
Claim. For every rational $t$, writing $J(t)=\frac{t+t^{-1}}{2}-1$ for the J-display on rationals, one has $J(-t)=-J(t)-2$.
background
In the primitive recognition calculus structural ledger, the rational J-display is defined by $J(t)=(t+t^{-1})/2-1$. This is the same algebraic cost that the forcing chain isolates as unique (T5): the unique continuous solution of the Recognition Composition Law normalized at the identity. On positive reals it is $\cosh(\log t)-1$; here the same formula is kept on $\mathbb{Q}$, including negative arguments where the inverse is still defined for $t\neq 0$.
Sign reversal of a display is the algebraic counterpart of flipping the orientation of a distinction. Upstream, the ledger already treats the reciprocal event (swap source/target and invert the ratio) as an automorphism of recognition events. The present identity is the companion rule for pure sign flip of the rational argument, not ratio inversion.
Sibling facts already record nonnegativity, the zero locus, and the value at $1$. Sign reversal sits next to those structural lemmas so that later cost functors can track orientation.
proof idea
Term-mode, four lines. Unfold the definition of the rational J-display, rewrite the inverse of a negative rational via inv_neg (so $(-t)^{-1}=-t^{-1}$), and finish with ring on $\mathbb{Q}$. No external lemmas beyond the definition and field arithmetic are required.
why it matters
Native-cost functors that remember orientation must know how $J$ transforms under $t\mapsto -t$. Downstream, signedPowerNativeCost_signReversing rewrites through this identity after applying the signed-power negation rule, and powerGeneratedNativeCost_signReversing does the same for odd exponents ("odd exponents reverse orientation, because an odd power remembers the sign"). Both feed the gauge-orbit classification that the nondegenerate branch is a sign-extended power cost (nontrivial_is_signedPower).
In the broader RS picture this is bookkeeping for the unique J-cost (T5) once displays are allowed to carry a sign. It does not itself force $\phi$, the eight-tick period, or $D=3$; it keeps the cost ledger consistent when orientation is reversed inside those later constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.