padicValRat_two_primeDirection_eq_zero_of_ne_two
plain-language theorem explainer
For any prime distinction-orbit other than the two-orbit, the rational display of its prime direction has vanishing 2-adic valuation. Anyone proving that the two-adic twist fixes those directions cites this. The proof rewrites to an integer valuation and obtains a contradiction from native orbit divisibility: if 2 divided the orbit, the two-orbit would divide a prime orbit, forcing either a unit or equality with two.
Claim. Let $p$ be a prime finite orbit of repeated distinction, and assume $p$ is not the two-step orbit. Then the $2$-adic valuation of the rational associated to the prime direction of $p$ is zero: $v_2\bigl((\mathrm{prime\ direction\ of\ }p)^{\mathbb{Q}}\bigr)=0$.
background
In the Primitive Recognition Calculus, DistinctionNat is the base-neutral finite orbit of repeated distinction (K2.12): an inductive successor type whose verifier display is ordinary Nat via iteration count. Native divisibility on these orbits is existential multiplication (a divides b when some k satisfies a*k=b); it displays as ordinary Nat divisibility by the bridge divides_iff_toNat_dvd. A prime orbit is one whose only divisors are units and itself; the only multiplicative unit is the one-step orbit.
Prime directions package a prime orbit as a ratio orbit, then toRat is the verifier display of that ratio as a rational (spec tag A5: a transport wrapper whose internal law is cross-multiplication). The two-orbit is the distinction-orbit whose Nat display is 2. The claim sits in the native-cost uniqueness module, which studies how cost characters and doubled-trace d'Alembert data interact with 2-adic twisting of those rationals.
proof idea
Rewrite the prime-direction rational via primeDirection_toRat, cast the numerator to an integer, and apply padicValRat.of_int so the goal becomes padicValInt 2 (p.toNat)=0. That integer valuation vanishes by padicValInt.eq_zero_of_not_dvd: if 2 divided p.toNat, then (after twoOrbit_toNat) the two-orbit would divide p in the native sense. Because p is prime, unit_or_eq_of_divides_prime yields either that the two-orbit is a unit or that p equals the two-orbit. The unit case forces twoOrbit.toNat=1 (false by norm_num); the equality case contradicts p≠twoOrbit. Cast the integer conclusion back to rationals.
why it matters
Immediate parent is twoAdicTwistRat_primeDirection_of_ne_two, which unfolds the two-adic twist and needs vanishing 2-valuation so the twist acts as the identity on prime-direction rationals away from two. That identity is part of the native-cost uniqueness chain: cost characters built from prime directions must match doubled-trace d'Alembert data without spurious 2-power factors. In the broader Recognition forcing picture this keeps the arithmetic of distinction orbits aligned with the unique J-cost (T5) and the self-similar scale φ (T6), so that later mass-ladder and coupling extractions do not pick up an artificial 2-adic defect. The lemma is pure arithmetic scaffolding inside PRC; it does not itself force dimension or the eight-tick octave, but it closes a divisibility gap those later steps inherit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.