axisTwistRat_mul
plain-language theorem explainer
The base-$b$ axis twist on rationals is completely multiplicative: $T_b(xy)=T_b(x)T_b(y)$ for every prime $b$. Anyone assembling a ratio character from a $p$-adic axis twist cites this identity. The proof is zero-case analysis plus additivity of the $b$-adic valuation and the usual power law $r^{m+n}=r^m r^n$.
Claim. Let $b$ be a prime natural number and let $x,y\in\mathbb{Q}$. Define the axis twist $T_b(x):=x\cdot b^{-2\,v_b(x)}$, where $v_b$ is the $b$-adic valuation on rationals (with the usual convention at $0$). Then $T_b(xy)=T_b(x)\,T_b(y)$.
background
In the Primitive Recognition Calculus native-cost uniqueness development, an axis twist on rational displays inverts the exponent along one prime axis $b$ and leaves every other prime axis fixed. Concretely, $T_b(x)=x\cdot b^{-2,v_b(x)}$. Special cases recover the two-adic and three-adic twists used elsewhere in the module.
The $b$-adic valuation $v_b:\mathbb{Q}\to\mathbb{Z}\cup{\infty}$ is additive on products of nonzero rationals: $v_b(xy)=v_b(x)+v_b(y)$. The base $b$, being prime, is nonzero as a rational; that fact is recorded as a small lemma used whenever integer powers of $b$ are rewritten.
The ambient goal is to promote such twists to ratio characters (multiplicative maps on $\mathbb{Q}^\times$ compatible with the PRC cost axioms), so multiplicativity of $T_b$ is the first algebraic checkpoint.
proof idea
Unfold the definition of the axis twist. Split on whether $x=0$; if so both sides vanish by simplification. Otherwise split on $y=0$ and again both sides vanish. In the nonzero case apply additivity of the $b$-adic valuation on products, rewrite the combined exponent $-2(v_b(x)+v_b(y))$ as a sum of exponents by a one-line ring identity, then invoke $r^{m+n}=r^m r^n$ for nonzero base $r=b$, and finish by ring.
why it matters
This identity is the algebraic engine behind axisTwistCharacter_ratio_character, which packages the axis twist into a full PRC ratio character on a prime orbit. Ratio characters are the bridge from discrete display data to the native cost functional whose uniqueness the module targets.
In the broader Recognition Science forcing picture, native-cost uniqueness sits under the J-cost / RCL layer (T5 and the Recognition Composition Law): once the cost is forced to be the unique J-shaped functional on positive displays, axis twists supply the residual discrete symmetries that must still act as characters. Without multiplicativity, those symmetries would not preserve the ratio structure required by the doubled-trace and d'Alembert hypotheses developed in the same file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.