twoAdicTwistRat_mul
plain-language theorem explainer
The classical two-adic branch twist on rational displays is a group homomorphism under multiplication: twisting a product equals the product of the twists. Anyone building ratio characters or verifying the orbit-2 inversion step cites this. The proof unfolds the definition, splits on zero factors, then uses additivity of the 2-adic valuation and the exponential law for integer powers of 2.
Claim. For all rationals $x,y\in\mathbb{Q}$, the two-adic branch twist satisfies $\tau_2(xy)=\tau_2(x)\,\tau_2(y)$, where $\tau_2(x)=x\cdot 2^{-2\,v_2(x)}$ and $v_2$ is the $2$-adic valuation on $\mathbb{Q}$ (with the usual convention that the zero case is handled separately so both sides vanish).
background
In the Primitive Recognition Calculus native-cost uniqueness development, rational displays carry a classical verifier twist on the two-adic place. The map $\tau_2$ multiplies a rational by a pure power of $2$ that exactly cancels twice the $2$-adic valuation: $\tau_2(x)=x\cdot 2^{-2 v_2(x)}$. Odd-prime axes are left fixed; only the orbit-$2$ exponent is inverted.
The $2$-adic valuation $v_2:\mathbb{Q}^\times\to\mathbb{Z}$ is additive on products, $v_2(xy)=v_2(x)+v_2(y)$ whenever $x,y\neq 0$. Integer powers of the base $2$ therefore convert that additivity into a multiplicative law for $\tau_2$. Zero is treated as a separate case so that both sides of the claimed identity remain well-defined and equal.
This lemma sits inside the module that constructs native cost uniqueness from character and doubled-trace data, feeding the ratio-character interface used later in the same file.
proof idea
Unfold $\tau_2$. Case-split on $x=0$; if so both sides are zero by simplification. Otherwise case-split on $y=0$ and simplify likewise. In the nonzero regime apply additivity of the $2$-adic valuation on products, rewrite the combined exponent $-2(v_2(x)+v_2(y))$ as a sum of exponents by a ring identity, invoke the exponential law $2^{a+b}=2^a 2^b$ (valid since the base $2\neq 0$), and finish by ring simplification.
why it matters
Multiplicativity is the algebraic backbone that lets the two-adic axis twist become a genuine ratio character. Downstream, twoAdicAxisTwistCharacter_ratio_character installs the PRC ratio-character structure on the twisted map, using the unit case of this law; twoAdicTwistRat_four evaluates the twist at $4$ by applying the same identity to $2\cdot 2$.
Inside Recognition Science this is local foundation work for native-cost uniqueness: the two-adic branch must invert the orbit-$2$ exponent while remaining a homomorphism, so that cost-from-character constructions stay compatible with the Recognition Composition Law and the doubled-trace d'Alembert identities developed in the same module. It does not itself touch the forcing chain T5–T8, but it keeps the rational display layer coherent for those later uniqueness arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.