one_toRat

In the Primitive Recognition Calculus integer-rational layer, a ratio orbit is an integer numerator (signed orbit) over a nonzero distinction-natural denominator. It is the internal display of a positive rational before transport to Mathlib $\mathbb{Q}$.

The map toRat is the A5 transport wrapper: it sends a ratio orbit $q$ to $(q.\mathrm{num}.\mathrm{toInt}:\mathbb{Q})/(q.\mathrm{den}.\mathrm{toNat}:\mathbb{Q})$. Internal equality of ratio orbits is characterized by cross-multiplication; the display is only a verifier face.

The unit ratio orbit is the multiplicative identity in this structure (numerator the unit signed orbit, denominator one). This lemma pins its display value so later arithmetic lemmas (add_toRat, mul_toRat, recip_toRat) can reduce cleanly at $1$.

One-line tactic proof: unfold the unit ratio-orbit constructor and the definition of the display map, then simp. After unfolding, both numerator and denominator are the unit constructions whose integer/natural coercions are $1$, so the quotient is definitionally $1$.

This is a base simp fact for the entire gauge-orbit cost stack. Downstream, cost_display rewrites the native cost of a ratio orbit as half the rational trace minus one, and the rewrite list explicitly includes this identity together with two_toRat, mul_toRat, and add_toRat. Zero-calibration theorems for signed-power and sign-gauge native costs likewise simp through the unit display when checking the doubled-trace value at the anchor.

In the Recognition framework the cost functional is forced (T5) to the unique $J$ satisfying the Recognition Composition Law; the ratio-orbit layer is the discrete ledger on which that $J$ is evaluated before real extension. Pinning $\mathrm{toRat}(\mathbf{1})=1$ keeps the discrete identity aligned with the real fixed point of $J$, so nondegeneracy statements (strict monotonicity iff the cost charges at orbit two) do not pick up spurious offsets at the unit.