twoAdicTwistRat_four
plain-language theorem explainer
The two-adic branch twist sends the rational 4 to 1/4. Anyone tracking the classical verifier twist on rational displays, or proving that the two-adic axis twist character is not orbit-direction identity, cites this evaluation. The proof multiplies the known value at 2 by itself via multiplicativity and simplifies.
Claim. The classical two-adic branch twist on rationals satisfies $\tau_2(4) = 1/4$, where $\tau_2(x) = x \cdot 2^{-2\,v_2(x)}$ and $v_2$ is the $2$-adic valuation on $\mathbb{Q}$.
background
In the primitive recognition calculus native-cost uniqueness development, the classical verifier two-adic branch twist on rational displays is the map $\tau_2(x) = x \cdot 2^{-2,v_2(x)}$. It fixes odd-prime axes and inverts the orbit-$2$ exponent, so powers of $2$ are sent to reciprocal powers of $2$.
Multiplicativity $\tau_2(xy)=\tau_2(x)\tau_2(y)$ is already proved, as is the base evaluation $\tau_2(2)=2^{-1}$. The present lemma is the next concrete power: $4=2\cdot 2$, so the twist value is forced by those two facts alone. The surrounding module builds character and doubled-trace cost data that must distinguish genuine native costs from twisted impostors.
proof idea
Apply multiplicativity at $x=y=2$ to get $\tau_2(4)=\tau_2(2)\tau_2(2)$. Rewrite the right-hand side with the known identity $\tau_2(2)=2^{-1}$, then finish by norm_num. Pure term-style chaining; no unfolding of the padic definition is needed at this step.
why it matters
Feeds directly into twoAdicAxisTwistCharacter_succ_three_not_identity, which shows the two-adic axis twist character fails PRC character orbit-direction identity on the successor of the three-orbit. That non-identity step is part of separating native recognition cost from two-adic twisted competitors in the PRC native-cost uniqueness argument.
Within Recognition Science foundation work, cost uniqueness under the Recognition Composition Law and the forcing chain (T5 J-uniqueness onward) requires that only the genuine cost character survive. Concrete rational evaluations of the two-adic twist supply the arithmetic witnesses that twisted characters break orbit-direction identity, so they cannot match the native cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.