threeAdicTwistRat_primeDirection_of_ne_three
plain-language theorem explainer
For any native prime orbit other than the orbit of 3, the classical three-adic branch twist acts as the identity on that prime's rational direction. Cost-uniqueness and character-calibration arguments cite this to separate the 3-axis from other primes. The proof unfolds the twist, inserts vanishing 3-adic valuation, and reduces by arithmetic.
Claim. Let $p$ be a native prime orbit distinct from the orbit of $3$. Write $r$ for the rational display of the ratio direction of $p$. Then the three-adic branch twist fixes $r$: $r \cdot 3^{-2\,v_3(r)} = r$.
background
In the Primitive Recognition Calculus, finite distinction orbits (DistinctionNat) carry a native notion of primality: nonzero, non-unit, and free of nontrivial factorization. Each such prime orbit has an associated ratio direction, displayed as a rational via the transport wrapper toRat (spec tag A5: internal equality is cross-multiplication).
The three-adic twist on rational displays is $x \mapsto x \cdot 3^{-2 v_3(x)}$. By design it fixes every non-$3$ prime axis and inverts the exponent along the orbit-$3$ axis. It is the base-$3$ analogue of the two-adic twist, introduced to show that calibrating native cost at one prime (agreement with $J$ at $2$) does not force the same calibration on other prime axes.
The immediate upstream fact is that $v_3$ of any non-$3$ prime direction vanishes, so the twist power is $3^0$.
proof idea
Term-mode, three steps. Unfold the definition of the three-adic twist to $x \cdot 3^{-2 v_3(x)}$. Rewrite with the lemma that $v_3$ of (primeDirection p hp).toRat is $0$ whenever $p$ is prime and $p \neq$ the orbit of $3$. The remaining identity $x \cdot 3^{0} = x$ is discharged by norm_num.
why it matters
This lemma is the prime-axis fixed-point step for the three-adic twist character. Downstream, threeAdicAxisTwistCharacter_two_identity applies it at the prime orbit of $2$ to obtain cross-equality of the twisted character with the two-prime direction: calibrating at $2$ is compatible with a nontrivial twist on the $3$-axis.
In the PRC native-cost uniqueness program, that separation is the point. Agreement of a ratio character's generated cost with canonical $J$-cost on one prime orbit does not propagate automatically to every other prime. The three-adic twist is the explicit counter-model on the remaining axes, and this identity shows the twist is invisible exactly where it should be (all primes other than $3$).
Relative to the forcing chain, the result sits in the foundation layer that isolates $J$-uniqueness (T5) from accidental base-dependent identifications among prime directions; it does not itself force $\varphi$ or the eight-tick structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.