onRatioOrbit_signed_unit_calibrated
plain-language theorem explainer
The rational J-cost on ratio orbits is calibrated at the signed unit −1: its value there is cross-equal to the reference J(−1). Anyone discharging the signed-unit repair for native PRC costs after the absolute-value no-go would cite this. The proof is a one-line reflexivity wrapper on cross-equality.
Claim. Let $J$ be the native rational cost on ratio orbits, $J(q)=((q+q^{-1})/2)-1$. Then $J$ is signed-unit calibrated: the ratio-orbit value $J(-1)$ is cross-equal to the reference $J(-1)$ (i.e., $J$ agrees with itself at the ratio-orbit display of $-1$).
background
In Primitive Recognition Calculus, costs act on ratio orbits: rational displays with a signed-orbit numerator and a nonzero distinction-nat denominator. The standard rational J-cost implements $J(q)=((q+q^{-1})/2)-1$ as a map on those orbits; the module notes this is a ratio-orbit object, not yet the real-analytic uniqueness theorem.
After an absolute-value no-go, native costs need a signed-unit repair: they must see $-1$, not only positive prime and prime-pair probes. The calibration predicate packages that as cross-equality between $F(-1)$ and the reference $J(-1)$. The ratio-orbit display of $-1$ is the probe used to expose missing signed-unit calibration in prime-to-global orientation propagation.
Cross-equality is the equality relation on ratio orbits from the integer-rational layer; its reflexivity is the upstream fact this proof uses.
proof idea
One-line wrapper. Instantiating the signed-unit calibration predicate at the rational J-cost demands cross-equality of $J(-1)$ with itself. Apply reflexivity of cross-equality to that common ratio-orbit value and stop.
why it matters
Discharges the signed-unit calibration conjunct for the canonical rational J-cost inside PRC native-cost uniqueness. It sits on the post absolute-value no-go repair path: the pass-274 strengthened hypotheses plus direct calibration at the signed unit. That repair is what lets native costs see orientation, not only absolute magnitude.
In the broader Recognition chain this is local bookkeeping for the same $J$ forced at T5, $J(x)=(x+x^{-1})/2-1$, and constrained by the Recognition Composition Law. No downstream edges are wired yet; the lemma is an interface discharge waiting on the assembled signed-repaired native-cost package.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.