primeDirection_toRat
plain-language theorem explainer
For each prime distinction orbit, the rational display of its prime direction equals that orbit's natural count as a rational. Native-cost uniqueness and minimality arguments cite this to pin prime axes to ordinary positive integers in the verifier rationals. The proof unfolds the direction construction and simplifies via the signed-orbit integer map and the unit orbit count.
Claim. Let $p$ be a finite distinction orbit that is prime. Then the rational display of the prime direction of $p$ equals the natural number read from $p$, viewed in $\mathbb{Q}$.
background
In the Primitive Recognition Calculus, DistinctionNat is the base-neutral finite orbit of repeated distinction (zero and successor). Its forward map toNat reads the iteration count into ordinary naturals. Integers appear as signed orbit differences (SignedOrbit: intended meaning pos minus neg); rationals appear as RatioOrbit, an integer numerator over a nonzero distinction-orbit denominator.
The verifier display toRat sends a ratio orbit to $\mathbb{Q}$ by $(q.\mathrm{num}.\mathrm{toInt}:\mathbb{Q})/(q.\mathrm{den}.\mathrm{toNat}:\mathbb{Q})$. Spec tag A5 treats this as a transport wrapper whose internal equality is cross-multiplication. Upstream, ofOrbit_toInt states that the signed orbit built from a distinction orbit $n$ has integer value $n.\mathrm{toNat}$, and the unit orbit has count one.
This module develops uniqueness of the native cost on ratio orbits. Prime directions are the axis generators used when calibrating characters and costs on prime axes; the present lemma identifies their rational display with the prime's ordinary natural number.
proof idea
Short tactic proof. Unfold the definitions of the prime direction, the underlying orbit direction, and the ratio-orbit rational display. The resulting fraction has numerator the signed orbit of $p$ and denominator the unit distinction orbit. Simplify with ofOrbit_toInt (numerator integer equals $p.\mathrm{toNat}$) and one_toNat (denominator count is $1$), yielding equality with $(p.\mathrm{toNat}:\mathbb{Q})$.
why it matters
Prime-axis calibration in the native-cost ledger needs the prime direction to sit at a concrete positive integer rational. Downstream, primeDirection_isPosInt rebuilds that positivity witness by rewriting with this identity. Absolute-value character identities (absValueCharacter_prime_identity, prime-pair product cost) reduce via crossEq_iff_toRat_eq to the same rational equality.
On the minimality side, character_pair_two_calibration_forces_prime_calibration transports two-point calibration plus prime-pair product consistency onto every native prime axis; the doc-comment calls this the missing round-1 transport. Certificate lemmas for Liouville-twist and RCL-spike slim fields, and the round-5 terminal PRCStructuralNativeCostUniquenessTarget_proved ("the structural ledger forces the canonical cost"), all sit on this identification.
In the broader Recognition chain this is foundation plumbing for native $J$-cost uniqueness (T5 landmark: $J(x)=(x+x^{-1})/2-1$), not a physical constant claim. It closes the prime-direction display so structural uniqueness can force the canonical cost without extra prime-axis data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.