padicValRat_three_primeDirection_eq_zero_of_ne_three
plain-language theorem explainer
For any prime distinction-orbit other than the three-step orbit, the rational attached to its prime direction has 3-adic valuation zero: 3 does not divide that numerator. Cost-uniqueness and 3-adic twist arguments cite this to drop the twist on non-3 primes. The proof reduces to integer 3-adic valuation and uses native prime divisibility: a prime orbit divisible by three must be three itself.
Claim. Let $p$ be a prime finite distinction-orbit with $p \neq 3$ (the three-step orbit). Then the $3$-adic valuation of the rational display of the prime direction of $p$ vanishes: $v_3\bigl((\mathrm{primeDirection}\,p).\mathrm{toRat}\bigr) = 0$.
background
In Primitive Recognition Calculus, DistinctionNat is the base-neutral finite orbit of repeated distinction (zero and successor). Verifier toNat reads the orbit as an ordinary natural number. Native divisibility divides means there exists an orbit factor whose product recovers the target; it displays as ordinary Nat divisibility via divides_iff_toNat_dvd. A prime orbit is one whose only divisors are units or itself; the only multiplicative unit is the one-step orbit (unit_iff_toNat_eq_one).
threeOrbit is the three-step distinction orbit (display value 3). primeDirection p hp packages a ratio orbit associated to a prime $p$; toRat is the verifier display of a ratio orbit as a rational (num/den transport, Spec A5). The ambient module develops native-cost uniqueness via doubled-trace and d'Alembert structure, including 3-adic twist comparisons on those rationals.
Upstream arithmetic is purely orbit-native: divisibility and primality live on DistinctionNat, then transport to ℤ/ℚ only for Mathlib padicValInt / padicValRat.
proof idea
Rewrite the goal with primeDirection_toRat, cast the numerator to ℤ, and apply padicValRat.of_int, so it suffices that $v_3(p.\mathrm{toNat}:ℤ)=0$.
That integer valuation vanishes by padicValInt.eq_zero_of_not_dvd: if $3\mid p.\mathrm{toNat}$, cast to get threeOrbit.toNat ∣ p.toNat, hence native divides threeOrbit p via divides_iff_toNat_dvd. Prime-orbit dichotomy (unit_or_eq_of_divides_prime) yields either threeOrbit is a unit or $p=\mathrm{threeOrbit}$. The unit case forces threeOrbit.toNat=1, absurd by norm_num; the equality case contradicts p ≠ threeOrbit. Cast the integer vanishing back to rationals.
why it matters
Immediate parent is threeAdicTwistRat_primeDirection_of_ne_three: once $v_3=0$ on the prime-direction rational, the 3-adic twist acts as the identity on that display. That step sits in the native-cost uniqueness development (PRCNativeCostUniqueness), where cost functionals built from ratio characters and doubled traces must match uniquely under d'Alembert-type hypotheses.
In the broader Recognition stack this is bookkeeping on the arithmetic side of Primitive Recognition Calculus: primes other than 3 contribute no 3-power in the direction rational, so 3-adic corrections cannot move their cost data. It does not itself invoke T5–T8 or the RCL closed form of $J$, but it clears a divisibility obstruction inside the uniqueness pipeline that feeds those cost identities.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.