natOrbit_toRat
plain-language theorem explainer
For every natural number n, the ratio-orbit built from n displays back as the rational n. Anyone working with native-cost characters, monotone traces, or integer anchors on RatioOrbit cites this as the bridge between discrete naturals and verifier rationals. The proof is a one-line wrapper of the general recovery lemma for ratioOrbitOfRat.
Claim. For every natural number $n$, if $O_n$ is the ratio-orbit obtained by embedding $n$ as a rational, then the verifier display map sends $O_n$ back to $n$ as a rational: $\mathrm{toRat}(O_n) = n \in \mathbb{Q}$.
background
In the Recognition cost stack, ratio orbits are the native carriers of multiplicative data. The map ratioOrbitOfRat embeds an ordinary rational into that orbit type; the inverse display toRat recovers a rational by the signed-numerator over positive-denominator quotient (spec tag A5: a transport wrapper whose internal equality is cross-multiplication).
The local definition natOrbit n is exactly that embedding applied to the cast (n : ℚ). The same construction appears in the structural ledger as "the orbit whose display is the natural number n". The uniqueness layer already proves that embedding then displaying is the identity on all rationals: (ratioOrbitOfRat x).toRat = x.
This module sits in Cost.RealCharacterFactorization, where native costs are factored through real characters on ratio orbits, and positive integers serve as the discrete test lattice for monotonicity and small-trace rationality.
proof idea
One-line wrapper. Unfolding the definition of the natural-number orbit reduces the goal to the general recovery statement (ratioOrbitOfRat x).toRat = x at x = (n : ℚ), which is applied directly (placeholder argument filled by unification).
why it matters
Integer anchors are the discrete skeleton on which real-character candidates are evaluated. Downstream results use this identity to move freely between natOrbit n and the rational n: monotonicity of the rational trace along naturals, positivity of the real character candidate on positive integers, rationality of small traces at n = 2..5, and the arithmetic MonoMult package extracted from a monotone factorized cost.
In the gauge-orbit layer it underwrites the proofs that the sign-gauge native cost has character exponent zero and is not any positive odd power already at the anchor two. Without a clean display of natural orbits as rationals, the discrete half of the character-factorization program cannot talk to ordinary arithmetic. It is scaffolding glue rather than a forcing-chain landmark, but it is cited heavily wherever PRC native cost meets integer tests.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.