natOrbit
plain-language theorem explainer
Embeds each natural number n as a ratio orbit whose classical display is the rational n. Cost and character lemmas cite it as the standard positive-integer test point (especially n = 2) when extracting real characters and exponents. The body is a one-line cast through the rational-to-orbit section.
Claim. For each natural number $n$, the associated ratio orbit is the orbit whose rational display equals $n$ (as $n/1$), obtained by the verifier-backed section from $\mathbb{Q}$ into ratio orbits.
background
In the primitive recognition calculus, a ratio orbit is an integer-numerator / nonzero-denominator display of a rational (K4.7): a signed orbit over a distinction-natural denominator. Costs and characters act on these orbits rather than bare reals, so integer bases must be reified as orbits before evaluation.
The map ratioOrbitOfRat is the verifier-backed section $\mathbb{Q}\to$ ratio orbits. It is not a new PRC primitive; it exists to test whether the character interface already admits classical rational countermodels. Casting $n:\mathbb{N}$ to $\mathbb{Q}$ and applying that section yields the orbit whose display is $n$.
This module sits in the native-cost structural ledger, which packages anchor-free cost hypotheses and feeds the real-character factorization pipeline.
proof idea
One-line definition: cast $n$ to a rational, then apply the existing section from rationals to ratio orbits. No proof obligations beyond those already discharged inside that section (nonzero denominator for the integer display).
why it matters
Integer base points are the probes that make the real-character factorization fire. Downstream, the exponent of a character is defined as $\log\chi(\mathrm{orbit\ of\ }2)/\log 2$, and many uniqueness and gauge lemmas evaluate candidates at the orbit of 2 (or other small naturals). The structural sans-anchor factorization theorem and the sign-gauge non-odd-power theorem both route through this embedding. In the broader RS chain it supplies the discrete bases against which multiplicative characters are read off, supporting the J-cost uniqueness and native-cost ledger story without introducing a separate integer primitive.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.