natOrbit_toRat
plain-language theorem explainer
The rational display of the ratio orbit built from a natural number n recovers n itself as a rational. Cost and character-factorization proofs that evaluate native cost or traces on integer anchors cite this as a simp fact. The proof is a one-line application of the general display identity for orbits constructed from rationals.
Claim. For every natural number $n$, if $O_n$ is the ratio orbit constructed from the rational $n$, then the verifier rational display of $O_n$ equals $n$ as an element of $\mathbb{Q}$.
background
In the primitive recognition calculus, ratio orbits are the native carriers of positive rational data. The map that builds an orbit from a rational, and the display map that reads an orbit back as a rational (numerator integer over denominator natural, via cross-multiplication), are inverse on the nose for ordinary rationals.
The local definition natOrbit n is the orbit obtained by feeding the cast of $n$ into that construction: it is "the orbit whose display is the natural number $n$". The display itself is tagged as a transport wrapper (spec A5): internal equality is cross-multiplication, not a new arithmetic.
Upstream, the uniqueness layer already proves that displaying the orbit of any rational $x$ recovers $x$. The present statement is the specialization of that identity to natural numbers, which are the integer anchors used throughout native-cost and real-character arguments.
proof idea
One-line term wrapper. Unfold the definition of the natural orbit (orbit of the rational cast of $n$) and apply the general lemma that the rational display of the orbit of any rational $x$ equals $x$. No extra arithmetic or positivity side conditions are needed.
why it matters
Integer anchors are the standard test points for native-cost characters and gauge-orbit extractions. Downstream, this identity feeds monotonicity of the rational trace on naturals, the claim that the real-character candidate is at least one on positive integers, rationality of small-trace values at $n=2..5$, and the structural ledger facts that the natural orbit is a positive integer orbit and that multiplicative characters act monotonically on it.
In the cost layer it is re-exported and used to show that the sign-gauge native cost has character exponent zero and is not an odd positive power already at the anchor two. Within Recognition Science this is bookkeeping on the rational skeleton that later supports J-cost uniqueness (T5) and character factorization of native cost, not a new physical law by itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.