padicValRat_axis_primeDirection_eq_zero_of_ne
plain-language theorem explainer
If two prime orbits p and r are distinct, the p-adic valuation of r's prime-direction rational display is zero. Cited when showing the b-axis twist fixes every off-axis prime. Proof: reduce to Nat non-divisibility via the native divides bridge, then unit-or-equal for primes.
Claim. Let $p$ and $r$ be prime orbits in the distinction naturals with $r \neq p$. Writing $v_{p(\mathbb{N})}$ for the $p$-adic valuation on $\mathbb{Q}$ and $\mathrm{dir}(r)$ for the prime-direction ratio orbit of $r$, one has $v_{p(\mathbb{N})}\bigl(\mathrm{dir}(r)\bigr) = 0$.
background
DistinctionNat is the base-neutral finite orbit of repeated distinction (K2.12): a Peano-style inductive type with verifier readout toNat. A prime orbit is the native predicate that the orbit has no nontrivial native factor; natPrime_toNat_of_primeOrbit bridges this to ordinary Nat.Prime on the display, so Mathlib factorization and p-adic tools apply.
Native divisibility divides a b means some orbit k satisfies a*k = b, and it is equivalent to ordinary divisibility of the Nat displays. Ratio orbits carry a verifier display toRat (num/den as rationals). The prime direction of a prime orbit r is the ratio-orbit realization used as the off-axis test point for the b-axis twist character (b = p.toNat).
Local setting is PRC native-cost uniqueness: characters built from axis twists must match the doubled-trace cost, which requires controlling p-adic valuations of those directions.
proof idea
Install Fact (Nat.Prime p.toNat) from natPrime_toNat_of_primeOrbit. Rewrite the goal through primeDirection_toRat and padicValRat.of_nat, then norm_cast to a Nat valuation claim. Apply padicValNat.eq_zero_of_not_dvd and assume for contradiction that p.toNat divides r.toNat. Transport via divides_iff_toNat_dvd to native divides p r. From unit_or_eq_of_divides_prime on the prime orbit r, either p is a native unit (so p.toNat = 1, contradicting primality) or r = p (contradicting hne).
why it matters
Sole downstream consumer is axisTwistCharacter_off_axis_identity: the b-axis twist character acts as the identity (cross-equality) on every prime direction other than the axis prime itself. That identity is the off-axis half of showing the twist character is a pure p-power scaling on the axis and trivial elsewhere, which feeds the PRC character/trace matching chain toward uniqueness of the native cost (siblings such as PRCCharacterTraceMatchesCost and the doubled-trace d'Alembert package).
In the broader Recognition stack this is arithmetic infrastructure under the Primitive Recognition Calculus, not a direct T5–T8 forcing step. It ensures the axis-twist realization of the cost character does not mix distinct prime directions, keeping the native cost factorization clean before J-uniqueness and the RCL are invoked higher up.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.