negativeOneRatio_toRat
plain-language theorem explainer
The ratio-orbit encoding of −1 recovers the ordinary rational −1 under the verifier map toRat. Anyone checking signed-unit calibration or sign-reversal of a native cost cites this simp fact. The proof is a two-step rewrite: unfold the encoding, then apply the general ratioOrbitOfRat round-trip.
Claim. If $q_{-1}$ denotes the ratio-orbit display of the rational $-1$, then the verifier map sending a ratio orbit to $\mathbb{Q}$ satisfies $q_{-1}\mapsto -1$.
background
In the Primitive Recognition Calculus, ratio data live as ratio orbits (pairs of distinction naturals up to cross-multiplication), not as bare rationals. The map toRat is only a verifier display: it sends a ratio orbit to $(n:d)\in\mathbb{Q}$ by integer casts, with the internal equality criterion still cross-multiplication (spec tag A5).
The object negativeOneRatio is defined as the ratio-orbit image of the ordinary rational $-1$. It is the probe used throughout the native-cost uniqueness development to test whether a candidate cost is calibrated on the signed unit: a character (or cost) is signed-unit calibrated when it fixes this orbit in the expected way. Prime-direction data alone cannot force that calibration.
Upstream, the general round-trip ratioOrbitOfRat_toRat already states that embedding any $x\in\mathbb{Q}$ into a ratio orbit and reading it back with toRat returns $x$. The present lemma is the specialization at $x=-1$.
proof idea
One-line term-mode rewrite. Unfold negativeOneRatio (definitionally ratioOrbitOfRat (-1)), then apply the general round-trip theorem ratioOrbitOfRat_toRat at $-1$. No case splits or arithmetic beyond that identity.
why it matters
Signed-unit calibration is load-bearing in the native-cost uniqueness chain. Downstream, signReversing_forces_signed_unit derives the signed-unit field from ledger antisymmetry at the unit by rewriting negativeOneRatio.toRat = -(RatioOrbit.one.toRat) via this lemma; absValueGeneratedNativeCost_not_signReversing uses the same identity to exclude the absolute-value countermodel without referring to the canonical cost's values.
Minimality certificates also depend on it: twoAdicGeneratedNativeCost_signed_unit calibrates the two-adic axis-twist cost on the signed unit through this display; Liouville-twist and RCL-spike slim-field certificates, and the zero-flat prime-signed strengthened ledger, route through the same -1 probe. In framework terms this is bookkeeping for the signed orientation that separates genuine J-cost candidates (T5 uniqueness of $J(x)=(x+x^{-1})/2-1$) from absolute-value or prime-only twists that never propagate a global sign.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.