twoAdicTwistRat_ne_zero
plain-language theorem explainer
Any nonzero rational remains nonzero after the classical two-adic branch twist that multiplies by a power of two inverting the 2-adic valuation. Cost-uniqueness and ratio-character arguments cite this to keep twisted displays inside the multiplicative group of rationals. The proof unfolds the twist and applies the product-of-nonzeros rule with a nonzero power of two.
Claim. For every rational $x \neq 0$, the two-adic twist $x \cdot 2^{-2\,v_2(x)}$ is nonzero, where $v_2$ is the $2$-adic valuation on $\mathbb{Q}$.
background
In the Primitive Recognition Calculus native-cost uniqueness development, displays are rational orbit positions and characters act by multiplicative twists that must preserve nonzeroness so ratio-orbit identities stay well-defined.
The classical verifier two-adic branch twist on rational displays is defined by $x \mapsto x \cdot 2^{-2,v_2(x)}$. It fixes the odd-prime axes and inverts the orbit-$2$ exponent, so the $2$-primary part of the display is normalized while the odd part is left alone.
Upstream, the orbit-arithmetic product rule records that a product of nonzero positions is nonzero. Here the same multiplicative idea is used on $\mathbb{Q}$: nonzero $x$ times a nonzero power of two cannot vanish.
proof idea
Unfold the definition of the two-adic twist to $x \cdot 2^{-2,v_2(x)}$. Record that $2 \neq 0$ in $\mathbb{Q}$ by a numeric check. Conclude with the standard product rule: the product of two nonzero rationals is nonzero, using that every integer power of a nonzero base is nonzero. The argument is a four-line tactic proof with no case split on the valuation.
why it matters
Native-cost uniqueness needs ratio characters that stay nonzero on nonzero displays so cross-equation and doubled-trace comparisons remain inside the multiplicative monoid. This lemma feeds the theorem that the two-adic axis twist character is a PRC ratio character, which rewrites the unit axiom via the rational display of the twist and the fact that the twist sends $1$ to $1$.
In the broader Recognition forcing picture this is bookkeeping on the classical verifier side of cost uniqueness, not a T5–T8 landmark. It closes a small nonzero-preservation gap so character-to-cost matching can proceed without ad-hoc side conditions on the $2$-primary axis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.