orbitDirection
plain-language theorem explainer
Embeds a nonzero finite distinction-orbit position as the rational display with that position in the numerator and unit denominator. Native-cost uniqueness and ratio-character arguments cite it as the canonical positive direction of a prime (or general) orbit. The body is a structure constructor: signed orbit from the position over one, with the unit-nonzero proof.
Claim. For a nonzero finite distinction-orbit position $p$, the associated ratio direction is the rational orbit display whose numerator is the nonnegative signed orbit built from $p$ and whose denominator is the unit orbit $1$.
background
In the Primitive Recognition Calculus, DistinctionNat is the base-neutral finite orbit of repeated distinction (zero and successor). A SignedOrbit is an integer-like difference of two such positions (intended meaning pos minus neg). ofOrbit builds the nonnegative signed orbit $\langle p, 0\rangle$ from a single position.
RatioOrbit (K4.7) is the rational display: a signed-orbit numerator over a nonzero distinction-orbit denominator. Cross-equality and the map to $\mathbb{Q}$ treat these as fractions in the orbit arithmetic used by native cost uniqueness.
This module develops uniqueness of the native cost via ratio characters and doubled-trace d'Alembert structure. The direction map supplies the standard positive generator $p/1$ against which products, successors, and reciprocals are compared.
proof idea
Definitional constructor, not a proof. Numerator is SignedOrbit.ofOrbit p (nonnegative signed orbit from $p$). Denominator is the unit distinction-orbit, with nonzeroness from DistinctionNat.one_ne_zero. The unused hypothesis $p \neq 0$ records that the direction is only formed for nonzero positions, matching downstream nonunit and prime-local lemmas.
why it matters
Feeds the native-cost uniqueness stack: orbitDirection_toRat identifies the display with $p$ as a rational; orbitDirection_succ_crossEq_add_one and orbitDirection_mul_crossEq transport successor and product into ratio arithmetic; orbitDirection_nonunit_not_crossEq_recip blocks orientation collapse under reciprocal for nonunits.
Character-level parents use it to force prime-local orientation and to show mixed nonunit identity/reciprocal witnesses reflect prime witnesses under a ratio character. That orientation control is part of pinning the unique native cost compatible with the Recognition Composition Law and the J-cost uniqueness step (T5) in the forcing chain, before phi and the eight-tick structure are forced downstream.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.