primeDirection_toRat_ne_zero
plain-language theorem explainer
For every prime distinction-natural p, the rational display of its prime direction is nonzero. Cost-uniqueness and prime-axis calibration proofs cite this to keep denominators and orientations well-defined. The argument first rules out p mapping to zero from the prime-orbit hypothesis, then unfolds the direction construction and simplifies.
Claim. Let $p$ be a distinction-natural that is a prime orbit. Then the rational value of the prime direction of $p$ is nonzero: $\mathrm{toRat}(\mathrm{primeDirection}(p)) \neq 0$.
background
In the Primitive Recognition Calculus, distinction-naturals are the native counting type built from recognition steps; toNat reads off the iteration count, with zero mapping to $0$. A prime orbit is a distinction-natural whose orbit data satisfy the prime-orbit predicate (in particular, it is not the zero orbit).
Ratio orbits package a signed-orbit numerator over a nonzero distinction-natural denominator and display as rationals via toRat. The prime direction of a prime orbit $p$ is the ratio-orbit axis associated to that prime (constructed via orbitDirection); its integer numerator comes from ofOrbit, which satisfies (ofOrbit n).toInt = n.toNat.
This module develops uniqueness of the native cost on those axes. Non-vanishing of the prime-direction rational is the elementary positivity fact needed before calibration and orientation lemmas can run.
proof idea
First prove $p.\mathrm{toNat} \neq 0$: if it were zero, injectivity of toNat plus toNat_zero would force $p$ to be the zero distinction-natural, contradicting the first conjunct of the prime-orbit hypothesis.
Then unfold primeDirection, orbitDirection, and RatioOrbit.toRat. A single simp with SignedOrbit.ofOrbit_toInt, DistinctionNat.one_toNat, and the nonzero nat fact discharges the goal: the displayed rational is essentially $p.\mathrm{toNat}/1$, hence nonzero.
why it matters
Native cost uniqueness along prime axes needs the prime direction to be a genuine nonzero rational so calibration and orientation statements are well-posed. Downstream, primeDirection_isPosInt uses this non-vanishing (with the explicit toRat formula) to classify the prime direction as a positive integer orbit.
PRCPrimeCalibrationForcesLocalPrimeOrientationTarget_proved invokes it directly before transferring non-vanishing through the ratio character $\chi$. It also supports the transport theorem that prime-pair products plus two-point calibration force prime-direction cost calibration, and appears in the structural ledger path that forces the canonical cost (PRCStructuralNativeCostUniquenessTarget_proved). In the RS forcing picture this is bookkeeping under T5-style J-uniqueness: prime axes must stay off zero before the cost functional can be pinned down.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.