ratioOrbitOfRat_toRat

In the primitive recognition calculus, rationals are not primitive. They are recovered from orbit displays. A signed orbit is a pair of distinction counts intended as $\mathrm{pos}-\mathrm{neg}$. A ratio orbit is a signed-orbit numerator over a nonzero distinction-count denominator (K4.6–K4.7). The recovery map on a ratio orbit reads those counts back to an ordinary rational via the integer and natural recovery maps from the logic-built arithmetic layer.

The companion constructor embeds an ordinary rational into that display language: numerator becomes a signed orbit built from positive and negative parts of the integer numerator, denominator becomes the distinction count of the natural denominator. This lemma is the left-inverse statement for that embedding: display then recover is the identity on $\mathbb{Q}$.

Locally the module develops native cost uniqueness for PRC characters on these displays, so free movement between $\mathbb{Q}$ and ratio orbits is infrastructure rather than a physics claim.

Tactic proof by unfolding the embedding and the two recovery maps (ratio-orbit to rational, signed orbit to integer). Three applications of the distinction-count round-trip on naturals clear the denominator and the absolute-value packaging of the numerator. A short omega lemma shows that casting $\mathrm{num}.\mathrm{toNat}$ and $(-\mathrm{num}).\mathrm{toNat}$ back to integers and subtracting recovers the original integer numerator for both signs. After rewriting with that identity, Rat.num_div_den finishes.

This is the bridge lemma that lets gauge-orbit cost classification work in RatioOrbit language while quoting ordinary rational arithmetic. Downstream, negative-display reduction rewrites with it to relate $F(q)$ to the display of $-q.\mathrm{toRat}$; the degenerate-branch identification with the sign gauge and the nondegenerate signed-power branch both thread through the same round-trip. Real-character factorizations (native signed-power and sign-gauge costs evaluated on rationals, rational-trace d'Alembert identities) likewise reduce display equalities to rational equalities only after this recovery.

In the Recognition stack it sits under native-cost uniqueness for PRC characters: once costs are classified on ratio orbits, this lemma exports the classification to $\mathbb{Q}$, which is where the J-cost and RCL comparisons are stated. It does not itself force $J$ or $\varphi$; it keeps the display layer faithful so those uniqueness theorems are not lost in encoding.