threeAdicTwistRat_mul
plain-language theorem explainer
The three-adic branch twist on rationals is completely multiplicative: T_3(xy)=T_3(x)T_3(y). Cost-uniqueness arguments that build ratio characters from prime-axis twists cite this identity. The proof is case analysis on vanishing factors, then padic-valuation additivity and integer-power multiplicativity.
Claim. For all rationals $x,y$, the three-adic twist $T_3(x):=x\cdot 3^{-2v_3(x)}$ (with $v_3$ the $3$-adic valuation on $\mathbb{Q}$) satisfies $T_3(xy)=T_3(x)\,T_3(y)$.
background
In the Primitive Recognition Calculus native-cost uniqueness development, one studies classical verifier twists that rescale a rational display along a single prime axis. The three-adic twist multiplies $x$ by $3$ raised to $-2$ times its $3$-adic valuation: it leaves every prime axis other than $3$ fixed and inverts the orbit-$3$ exponent. It is the base-$3$ analogue of the two-adic twist, introduced to test whether agreement of a native cost with the J-cost at one prime forces agreement on other primes.
The $3$-adic valuation $v_3$ on $\mathbb{Q}$ is additive on nonzero products, and the integer power map $a\mapsto 3^a$ is a group homomorphism from $(\mathbb{Z},+)$ into $(\mathbb{Q}^\times,\cdot)$. Those two algebraic facts are the only inputs needed for multiplicativity of the twist.
Local setting: the module builds ratio characters and doubled-trace cost functionals, then compares them to the unique J-cost forced by the Recognition Composition Law.
proof idea
Unfold the definition of the twist. Install the fact that $3$ is prime. Split on $x=0$ and $y=0$; both vanishing cases reduce by simp. On the nonzero branch, rewrite the product valuation via padicValRat.mul, distribute the factor $-2$ by ring, then apply zpow_add (base $3\neq 0$) and finish with ring.
why it matters
Downstream, the identity is the multiplicative step that installs the three-adic axis twist as a PRCRatioCharacter (via the ratio-character instance for that twist). That character is the counter-example witness that calibrating a native cost against J at the prime $2$ does not automatically force the same calibration on the prime-$3$ axis. In the broader Recognition Science forcing chain this protects the claim that J-uniqueness (T5) and the native-cost match are rigid: agreement must be checked, not inferred by prime-axis transport. Without multiplicativity the twist would not be a legitimate ratio character and the non-propagation argument would fail.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.