natOrbit
plain-language theorem explainer
Embeds each natural number n as a ratio orbit by sending the rational n through the verifier-backed section from rationals. Cost and character-factorization arguments cite it whenever they need integer bases (especially 2) inside the RatioOrbit type. The body is a one-line abbreviation of that section.
Claim. For every natural number $n$, write $\mathrm{natOrbit}(n)$ for the ratio orbit obtained by viewing $n$ as a rational and applying the section from $\mathbb{Q}$ into ratio orbits (integer numerator over a nonzero orbit denominator).
background
In the Primitive Recognition Calculus, a ratio orbit is a display of a rational: a signed-orbit numerator over a nonzero distinction-nat denominator (K4.7). The map from classical rationals into this type is the verifier-backed section ratioOrbitOfRat, deliberately not a new PRC primitive; it exists to test whether the character interface already admits classical rational countermodels.
This module develops real-character factorization for anchor-free native costs on ratio orbits. Integer test points (bases 1, 2, and small naturals) must live in the same type as general orbits, so the natural-number embedding is the standard way to place those bases.
An identical one-line definition already appears in the structural ledger module; the present copy is the Cost-side re-export used by the factorization and gauge-orbit developments.
proof idea
Pure definition: cast $n$ to $\mathbb{Q}$ and apply the existing section from rationals to ratio orbits. No proof obligations beyond those already discharged inside that section (nonzero denominator for the image of a natural).
why it matters
Integer bases are the calibration points for real characters on ratio orbits. The exponent of a character is extracted as $\log\chi(\mathrm{natOrbit},2)/\log 2$; monotonicity of rational traces compares $\mathrm{natOrbit},m$ and $\mathrm{natOrbit},n$; principal-character and small-trace rationality lemmas evaluate on positive-integer orbits. Downstream, every structural anchor-free cost is shown to factor through a real ratio character, and the sign-gauge character is proved not to be any positive odd power already at the anchor, both of which evaluate the candidate at $\mathrm{natOrbit},2$. Without this embedding the factorization target and the d'Alembert/trace arguments cannot state their integer specializations inside the orbit type.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.