threeAdicTwistRat_inv
plain-language theorem explainer
The three-adic branch twist on rationals is inversion-equivariant: twisting the reciprocal equals the reciprocal of the twist. Anyone assembling a ratio character from this twist cites the identity. The proof unfolds the definition, applies the p-adic valuation rule v_3(x^{-1})=-v_3(x), and cancels powers of 3.
Claim. For every rational $x$, the three-adic twist $\tau_3(x) := x \cdot 3^{-2 v_3(x)}$ satisfies $\tau_3(x^{-1}) = \tau_3(x)^{-1}$, where $v_3$ denotes the $3$-adic valuation on $\mathbb{Q}$ (with the usual convention at $0$).
background
In the primitive recognition calculus, native cost uniqueness is tested by twisting rational displays along a single prime axis while leaving the others fixed. The three-adic twist is the base-3 analogue of the two-adic twist: on $x\in\mathbb{Q}$ it multiplies by $3^{-2 v_3(x)}$, which inverts the orbit-3 exponent and leaves non-3 prime axes alone.
Its purpose is comparative. Calibrating the native cost so that it agrees with the J-cost on the prime-2 axis need not force the same agreement on other primes; the three-adic twist supplies an explicit counter-calibration on the 3-axis.
The present lemma records the elementary multiplicative property needed to promote the twist to a ratio character: it must send inverses to inverses.
proof idea
Unfold the definition $\tau_3(x)=x\cdot 3^{-2 v_3(x)}$. The zero case is immediate by simplification. For $x\neq 0$, rewrite via the valuation identity $v_3(x^{-1})=-v_3(x)$. The exponent identity $-2\cdot(-v_3(x))=-(-2 v_3(x))$ rearranges the power of 3 into a reciprocal; zpow_neg and field simplification then yield $\tau_3(x^{-1})=\tau_3(x)^{-1}$.
why it matters
Downstream, threeAdicAxisTwistCharacter_ratio_character packages the three-adic axis twist as a PRCRatioCharacter. The unit and inversion axioms of a ratio character need exactly this identity (together with the value at 1). Establishing the character structure lets the module exhibit a genuine alternative calibration on the 3-axis, showing that agreement of the native cost with J at the prime 2 does not propagate to other prime axes. That separation is the local content of native-cost uniqueness in the primitive recognition calculus, upstream of the forcing chain's J-uniqueness (T5) and the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.