threeAdicTwistRat_three
plain-language theorem explainer
The three-adic branch twist on rationals sends 3 to its reciprocal 1/3. Anyone checking that a native-cost character twisted along the 3-adic axis agrees with the reciprocal orbit character on the prime-3 direction will cite this evaluation. The proof unfolds the twist definition, inserts the p-adic valuation identity v_3(3)=1, and finishes by arithmetic.
Claim. Let $T_3:\mathbb{Q}\to\mathbb{Q}$ be the three-adic branch twist $T_3(x)=x\cdot 3^{-2v_3(x)}$, where $v_3$ is the $3$-adic valuation on rationals. Then $T_3(3)=3^{-1}$.
background
In the Primitive Recognition Calculus, native cost uniqueness is probed by twisting ratio characters along prime axes. The three-adic twist on rational displays multiplies by a pure power of 3 that inverts the orbit-3 exponent while fixing all other prime axes: $T_3(x)=x\cdot 3^{-2v_3(x)}$. Per its doc-comment, it is the base-3 analogue of the two-adic twist and exists to show that calibrating the native cost at one prime (agreement with J at 2) does not propagate to the other prime axes (here, 3).
The local module develops uniqueness and non-propagation statements for PRC native costs via doubled-trace and d'Alembert-type identities on ratio orbits. The elementary fact $v_3(3)=1$ (the 3-adic valuation of the integer 3) is the only arithmetic input needed to evaluate the twist at the generator 3.
proof idea
Unfold the definition $T_3(x)=x\cdot 3^{-2v_3(x)}$. Invoke the Mathlib identity that the 3-adic valuation of 3 itself equals 1 (valid since $1<3$). Rewrite to obtain $3\cdot 3^{-2\cdot 1}=3\cdot 3^{-2}$, then close by numeric normalization to $3^{-1}$.
why it matters
This evaluation is the arithmetic kernel of the parent theorem that the three-adic axis twist character is cross-equal to the reciprocal of the prime-3 direction: that proof rewrites cross-equality to rational equality and applies this fact exactly. In the PRC native-cost uniqueness program, the point is negative and structural: agreement of a native cost with the J-cost along the 2-axis need not force the same calibration on the 3-axis, because a pure 3-adic twist still matches the reciprocal orbit character there. Within the Recognition Science foundation layer this sits beneath T5 J-uniqueness (the cost $J(x)=(x+x^{-1})/2-1$ forced by the Recognition Composition Law); the twist family isolates which prime axes remain free once one prime is fixed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.