jq_inv
plain-language theorem explainer
The rational J-display is invariant under reciprocals: J(t^{-1})=J(t) for every t in Q. Workers on native cost, ratio-orbit characters, and monotone multiplicative data cite it whenever cost must ignore reciprocal orientation. The proof is a two-branch algebraic identity: the zero case is immediate, and the nonzero case unfolds the definition and closes by ring.
Claim. For every rational $t$, $J_{\mathbb{Q}}(t^{-1})=J_{\mathbb{Q}}(t)$, where the rational J-display is $J_{\mathbb{Q}}(t)=\frac{t+t^{-1}}{2}-1$.
background
In the primitive recognition calculus, the native cost on ratio data is read through the rational J-display $J_{\mathbb{Q}}(t)=\frac{t+t^{-1}}{2}-1$. This is the same functional form forced at T5 in the unified forcing chain (equivalently $\cosh(\log t)-1$ on positives), specialized here to $\mathbb{Q}$ so that ledger arithmetic stays exact.
The surrounding module builds the structural ledger for PRC native cost: characters on ratio orbits, completely multiplicative maps on positive integers, and the cost they induce. Reciprocal symmetry of the display is the elementary algebraic fact that lets cost treat an orbit and its reciprocal as the same observable.
Upstream, the definition of the display is purely algebraic; no analytic continuation or positivity hypothesis is required for the identity itself.
proof idea
Term-mode proof by cases on whether $t=0$.
If $t=0$, both sides simplify directly (the inverse of zero is handled by the rational field conventions already in scope).
If $t\neq 0$, unfold the definition of the display, rewrite with $\mathrm{inv_inv}$ so both sides become $\frac{t+t^{-1}}{2}-1$ in matching order, and finish with ring.
why it matters
Reciprocal symmetry is the reason native cost cannot see orientation on ratio orbits. Downstream it discharges the reciprocal field of the native-cost hypothesis packages for power-generated and signed-power costs, and it is the rewrite that proves native cost is unchanged under orbit reciprocal.
It also underwrites the monotone-multiplicative structure on positive integers: cost comparisons are stated in terms of the display, so invariance under $h\mapsto h^{-1}$ keeps the mono axiom well-defined when characters flip sign or orientation. The structural-character calibration theorem (round-5 engine) likewise rewrites through this identity when matching display values on integer orbits.
Framework landmark: this is the rational shadow of T5 J-uniqueness and of the Recognition Composition Law's evenness in the second argument; without it the ledger cannot identify cost with a gauge-invariant observable.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.