twoAdicTwistRat
plain-language theorem explainer
Defines the classical two-adic branch twist on rational displays: multiply a rational by a power of 2 that cancels twice its 2-adic valuation. The map fixes odd-prime axes and signed units while inverting the orbit-2 exponent. Downstream uniqueness and minimality certificates for the native PRC cost cite it as the verifier's 2-axis correction on ratio orbits.
Claim. For any rational $x$, the two-adic twist is $x \cdot 2^{-2\,v_2(x)}$, where $v_2$ is the $2$-adic valuation on $\mathbb{Q}$. Equivalently, if $x = \pm 2^k \cdot m/n$ in lowest terms with $m,n$ odd, the twist returns $\pm 2^{-k} \cdot m/n$.
background
In the Primitive Recognition Calculus (PRC), ratio orbits are the native displays of multiplicative comparisons. Cost uniqueness arguments need a classical verifier map that corrects only the $2$-primary part of a rational while leaving odd-prime axes fixed.
The $2$-adic valuation $v_2(x)$ on $\mathbb{Q}$ records the net power of $2$ in the prime factorization of $x$ (with $v_2(0)$ handled so the product formula still yields $0$). Raising $2$ to $-2 v_2(x)$ exactly inverts that exponent twice, which is the branch twist required by the doubled-trace / d'Alembert side of the native cost.
This definition lives in the PRC native-cost uniqueness module, alongside ratio characters, doubled-trace values, and the bridge from $\delta$-native prime orbits to ordinary Nat.Prime. It is the rational-level kernel later lifted to ratio orbits.
proof idea
Pure definitional equation: the body is the single term $x \cdot 2^{-2,\mathrm{padicValRat},2,x}$. No lemmas are applied at the definition site; downstream simp and unfold lemmas discharge concrete cases (zero, $-1$, fourth powers, inverses) by evaluating the valuation.
why it matters
The twist is the classical verifier correction on the $2$-axis that the native cost uniqueness chain needs before characters and doubled traces can be compared. It is consumed by twoAdicAxisTwistCharacter (ratio-orbit realization of the same map) and by the minimality certificate lemmas that check fixed points at $0$ and $-1$. Further uses include prime-orbit bridges and the three-prime direction display. In the broader Recognition forcing picture this is local scaffolding for cost uniqueness on rational displays, not a T5–T8 landmark itself; it supplies the concrete $2$-primary normalization those uniqueness theorems quote.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.