onRatioOrbit_negativeOneRatio_toRat
plain-language theorem explainer
The rational display of the PRC J-cost on the ratio orbit of −1 equals −2. Anyone checking signed-unit calibration of native costs or characters cites this evaluation. The proof rewrites to the closed form of J at −1 and finishes by numeric simplification.
Claim. If $J$ is the ratio-orbit cost $J(q)=((q+q^{-1})/2)-1$ and $q$ is the ratio-orbit display of $-1$, then the verifier rational of $J(q)$ equals $-2$.
background
In the Primitive Recognition Calculus, costs are carried on ratio orbits rather than bare reals. The native J-cost on a ratio orbit is the orbit object $J(q)=((q+q^{-1})/2)-1$, matching the T5 uniqueness shape $\cosh(\log x)-1$ once transported to positives. The map toRat is only a verifier display: it sends a ratio orbit to $\mathbb{Q}$ by integer numerator over natural denominator (cross-multiplication is the internal equality).
The constant ratio orbit of $-1$ is the signed unit used to probe orientation. Its display is exactly $-1$. Applying $J$ at that point is the first place a purely absolute-value or prime-direction character can fail to match the native cost, because $J(-1)=-2$ is negative and forces a genuine sign choice.
Locally this sits in the native-cost uniqueness development: characters and absolute-value generators are compared to $J$ via cross-equality of ratio orbits, then read out in $\mathbb{Q}$.
proof idea
Term-mode, three lines. Rewrite the left-hand side by the general identity that the rational display of $J(q)$ is $(q^{\mathrm{rat}}+1/q^{\mathrm{rat}})/2-1$, then replace the display of the signed-unit orbit by $-1$. The resulting arithmetic expression simplifies by norm_num to $-2$.
why it matters
This pin is the numeric witness that $J(-1)=-2$. Downstream it feeds two uniqueness gates: that the absolute-value-generated native cost fails cross-equality with $J$ at the signed unit, and that any ratio character whose cost matches $J$ at $-1$ is forced to fix the signed unit. Those gates close the gap between prime-direction data and global orientation, which absolute values alone cannot supply.
In the broader RS chain this is a discrete calibration step under the T5 J-shape, not the analytic uniqueness theorem itself. It keeps the native cost on the RCL/J track when characters are assembled from local data, and it is the concrete place where missing sign calibration becomes a rational contradiction rather than a slogan.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.