primeDirection_isPosInt
plain-language theorem explainer
Any prime distinction natural, under the prime-orbit hypothesis, has prime direction whose rational display is a positive integer. Structural-ledger uniqueness cites this to place prime directions inside the positive-integer character lattice. The proof is a short existential: witness the underlying natural, discharge positivity from non-vanishing of the rational display, and match the display by rewriting.
Claim. Let $p$ be a distinction natural number whose orbit is prime. Then the prime direction of $p$ is a positive-integer orbit: there exists $n\in\mathbb{N}$ with $n\ge 1$ such that the rational display of that direction equals $n$.
background
This module builds the structural ledger for the primitive recognition calculus (PRC) native cost: axioms that never name the canonical cost, yet force it. Ratio orbits are the multiplicative displays on which cost characters act. A positive-integer orbit is one whose rational display equals some natural $n\ge 1$.
Distinction naturals are the arithmetic layer read off logic iteration counts (toNat). A prime orbit on such a $p$ singles out a preferred direction in ratio space, the prime direction. Upstream cost and character infrastructure (native cost packs, doubled-trace RCL identities, recognizer-induced costs) treats positive-integer orbits as the lattice on which factorization and calibration live.
Locally the declaration sits just before the two structural axioms (sign reversal of the doubled trace, and monotonicity in imbalance), which the ledger uses without mentioning the canonical $J$-cost.
proof idea
Term-mode existential introduction for IsPosIntOrbit. The witness is p.toNat. The display identity is primeDirection_toRat. Positivity $1\le n$ is obtained from primeDirection_toRat_ne_zero: rewrite the non-vanishing statement into the rational display, then cast and apply Nat.one_le_iff_ne_zero. No cost functional is invoked.
why it matters
Feeds the Round 5 terminal PRCStructuralNativeCostUniquenessTarget_proved: the structural ledger forces the canonical cost. That uniqueness path factorizes zero-calibrated native costs into characters; prime directions must sit on positive-integer orbits so the character lattice is discrete and the ledger can pin the cost without naming $J$ a priori.
In the broader forcing chain this is bookkeeping under T5 $J$-uniqueness and the Recognition Composition Law: once directions of primes are positive integers, the native cost on those orbits is forced by the structural axioms (antisymmetry and imbalance monotonicity) rather than by an external ansatz. It closes a small but necessary gap between arithmetic primes and the ratio-orbit displays used by the uniqueness target.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.