toRat
plain-language theorem explainer
Maps a ratio orbit (signed numerator over a nonzero orbit denominator) to an ordinary rational by converting the numerator to an integer, the denominator to a natural, and dividing. Spec tag A5: a pure transport wrapper; the internal equality of orbits is cross-multiplication, not this display. Cited throughout gauge-orbit cost classification whenever a cost or character value must be read as a rational.
Claim. Given a ratio orbit $q$ with signed-orbit numerator $n$ and nonzero distinction-natural denominator $d$, the verifier display is the ordinary rational $\frac{\iota(n)}{\nu(d)}\in\mathbb{Q}$, where $\iota$ recovers an integer from the signed orbit and $\nu$ recovers a natural from the distinction count.
background
In the Primitive Recognition Calculus, rationals are not taken as primitive. A RatioOrbit (K4.7) is a display pair: a signed orbit numerator together with a distinction-natural denominator forced nonzero by a structure field. Signed orbits recover ordinary integers via the Integers-from-Logic map; distinction naturals recover ordinary naturals via the Arithmetic-from-Logic iteration count.
The module builds verifier arithmetic on these orbit displays before quotienting. The true PRC rationals (K4.8) are the quotient of ratio orbits by the cross-multiplication setoid; equality of classes is internal and does not mention $\mathbb{Q}$. The present map is only a bridge out to Mathlib rationals for statements that need ordinary field arithmetic or real embeddings.
Upstream recovery maps are definitional: toInt lifts the core integer recovery through the logic-integer quotient, and toNat reads off the successor iteration count from a logic natural.
proof idea
Definitional, three-token body: cast the numerator through the signed-orbit integer recovery to $\mathbb{Q}$, cast the denominator through the distinction-natural recovery to $\mathbb{Q}$, and divide. Nonzeroness of the denominator is already a structure field on the ratio orbit, so the division is well-typed with no extra proof obligation at this site.
why it matters
This display is the standard exit ramp from orbit-level cost data into ordinary rationals. Downstream, GaugeOrbitClassification uses it everywhere a cost or character must be compared with $0$, read as positive, or identified with a $J$-value: cost at zero and negative displays, the halved-and-shifted cost display identity, positive-branch power laws, nondegeneracy as exclusion of the sign gauge, and existence of natural exponents. Without the transport, those theorems could only speak in cross-multiplication language.
In the broader Recognition chain the map is scaffolding for reading the unique $J$-cost (T5) and its gauge-orbit classification on concrete rational arguments; it does not itself force $J$, $\varphi$, or the eight-tick structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.