orbitDirection_toRat
plain-language theorem explainer
The rational display of the orbit direction of a nonzero distinction orbit equals that orbit's iteration count, cast to rationals. Anyone transporting direction identities through the verifier embedding cites this. The proof unfolds the direction construction and simplifies via the signed-orbit integer map and the unit-orbit count.
Claim. For every nonzero distinction orbit $p$, writing $\mathrm{dir}(p)$ for its orbit direction (a ratio orbit), one has $\mathrm{dir}(p)^{\sim}=\overline{n(p)}$ in $\mathbb{Q}$, where $n(p)$ is the iteration count of $p$ and $(\cdot)^{\sim}$ is the rational display of a ratio orbit.
background
In the Primitive Recognition Calculus, DistinctionNat is the base-neutral finite orbit of repeated distinction (zero and successor). Its forward map toNat reads off the iteration count as an ordinary natural number.
Integers and rationals are rebuilt from orbits before any classical arithmetic is assumed. A signed orbit is a difference of two distinction orbits (intended meaning pos minus neg). A ratio orbit is an integer numerator over a nonzero distinction-orbit denominator. The verifier display toRat sends a ratio orbit $q$ to $(\mathrm{num}(q):\mathbb{Q})/(\mathrm{den}(q):\mathbb{Q})$; the internal equality notion is cross-multiplication, and toRat is only a transport wrapper (spec tag A5).
Orbit direction packages a nonzero distinction orbit $p$ as the ratio orbit with numerator the signed orbit of $p$ and denominator the unit orbit. The companion lemma ofOrbit_toInt states that the integer display of that signed orbit is exactly $n(p)$. The unit orbit has count one (one_toNat).
proof idea
Term-mode, three lines. Unfold the definitions of orbit direction and of the rational display of a ratio orbit. The goal becomes a quotient of integer and natural displays. Simplify with ofOrbit_toInt (numerator integer equals $n(p)$) and one_toNat (denominator count is $1$). The resulting identity $n(p)/1=n(p)$ in $\mathbb{Q}$ is immediate.
why it matters
Native cost uniqueness in PRC needs a faithful rational readout of orbit directions so that character and cross-equality statements can be checked in $\mathbb{Q}$ and pulled back. This lemma is the basic transport step: direction of $p$ displays as the count of $p$.
Downstream it is applied in orbitDirection_mul_crossEq, orbitDirection_succ_crossEq_add_one, and orbitDirection_nonunit_not_crossEq_recip, which establish multiplicative, successor, and non-reciprocal cross-equalities for directions. Those feed the character-orbit identity extension and contraction lemmas under additive compatibility, the positive-orbit identity and reciprocal theorems from prime data, and ultimately the native-cost-uniqueness blocker certificate in the same module.
In the broader forcing picture this sits under the arithmetic-from-logic layer that precedes J-cost uniqueness (T5) and the Recognition Composition Law; it does not itself force $\phi$ or the eight-tick structure, but keeps the rational skeleton of orbit calculus aligned with classical $\mathbb{Q}$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.