negativeOneRatio_self_recip
plain-language theorem explainer
The ratio-orbit display of −1 is cross-equivalent to its own reciprocal: (−1)⁻¹ = −1 holds inside the PRC rational layer. Anyone tracking signed-unit calibration or prime-to-global orientation propagation cites this. The proof reduces cross-equivalence to rational equality and finishes by norm_num on −1.
Claim. The ratio-orbit display of $-1$ is cross-equivalent (via balanced cross-multiplication of numerator and denominator orbits) to its reciprocal: $\mathrm{crossEq}(-1,\,(-1)^{-1})$ holds in the PRC rational orbit calculus.
background
In the Primitive Recognition Calculus, rationals are carried as RatioOrbit structures: a signed integer orbit numerator over a nonzero distinction-nat denominator. Equality of two such displays is not bare field equality; it is crossEq, the internal cross-multiplication relation that balances scaled signed orbits (K4.10). That relation is proved equivalent to equality of the verifier rationals toRat.
Reciprocals are total on ratio orbits (zero maps to zero, as in $\mathbb{Q}$), and recip_toRat says the display of the reciprocal is the field inverse of the display. The constant negativeOneRatio is the ratio-orbit packaging of $-1$, introduced specifically to expose signed-unit calibration when orientations propagate from primes to a global target.
This lemma sits in the native-cost uniqueness module, where character and doubled-trace data must respect the rational layer before uniqueness of the native cost can be forced.
proof idea
One short tactic proof. Rewrite crossEq via crossEq_iff_toRat_eq into equality of toRat values. Unfold both sides with negativeOneRatio_toRat and recip_toRat, so the goal becomes $(-1)^{-1} = -1$ in $\mathbb{Q}$. Close with norm_num.
why it matters
Signed coherence for prime-to-global orientation needs $-1$ to be a fixed point of inversion in the PRC rational layer; otherwise the missing signed-unit calibration cannot be stated cleanly. Downstream, PRCSignedCoherentPrimeOrientationPropagatesToGlobalTarget_proved consumes this fact while showing that a signed-coherent prime orientation extends to the global target.
In the broader Recognition stack this is bookkeeping on the rational substrate beneath native cost uniqueness, not a forcing-chain landmark (T5–T8). It keeps the signed character of the cost/trace side honest before J-cost uniqueness and the Recognition Composition Law are applied at higher layers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.