threeAdicTwistRat_one
plain-language theorem explainer
The three-adic branch twist on rationals fixes the multiplicative unit: it sends 1 to 1. Ratio-character constructions that use this twist cite the fact for the unit axiom of a PRC ratio character. The proof is a short 3-adic valuation computation: v_3(1)=0, so the twist multiplies by 3^0=1.
Claim. Let $T_3:\mathbb{Q}\to\mathbb{Q}$ be the three-adic branch twist $T_3(x)=x\cdot 3^{-2\,v_3(x)}$, where $v_3$ is the $3$-adic valuation on rationals. Then $T_3(1)=1$.
background
In the Primitive Recognition Calculus native-cost uniqueness development, one studies classical verifier twists on rational displays that reweight a single prime axis. The three-adic twist $T_3(x)=x\cdot 3^{-2 v_3(x)}$ fixes every prime axis other than 3 and inverts the orbit-3 exponent. It is the base-3 analogue of the two-adic twist, introduced to show that calibrating the native cost at one prime (agreement with the J-cost at 2) does not force the same calibration on other prime axes (here 3).
A PRC ratio character is a multiplicative map on ratio orbits satisfying a unit axiom and a cross-equation. The three-adic axis twist character is built by applying $T_3$ on rational displays; establishing $T_3(1)=1$ is the elementary unit check for that construction.
proof idea
Unfold the definition $T_3(x)=x\cdot 3^{-2 v_3(x)}$. It remains to show $v_3(1)=0$. That valuation identity is obtained by reducing to the integer case via padicValRat.of_int and applying padicValInt.eq_zero_of_not_dvd (3 does not divide 1), discharged by norm_num. Rewrite the exponent to zero and finish with norm_num to get $1\cdot 3^0=1$.
why it matters
This unit identity is the first obligation in proving that the three-adic axis twist character is a PRC ratio character (threeAdicAxisTwistCharacter_ratio_character). That parent theorem rewrites the unit goal through the cross-equation/toRat bridge and applies this lemma directly against RatioOrbit.one_toRat.
In the broader uniqueness story, the three-adic twist is a counter-calibration: agreement of the native cost with J along the 2-axis need not propagate to the 3-axis. Securing the unit axiom keeps the twisted character inside the ratio-character interface used to compare native costs against the forced J-cost (T5 in the forcing chain, $J(x)=(x+x^{-1})/2-1$). Without $T_3(1)=1$, the twisted map would fall outside the character class and could not serve as a clean separator between prime axes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.