twoAdicTwistRat_two
plain-language theorem explainer
The classical two-adic twist on rationals sends 2 to one half. Verifiers of the two-adic axis character and of two-adic generated native-cost hypotheses cite this base evaluation. The proof unfolds the twist, inserts the self-valuation identity v_2(2)=1, and finishes by arithmetic.
Claim. Let $\tau_2:\mathbb{Q}\to\mathbb{Q}$ be the two-adic branch twist $\tau_2(x)=x\cdot 2^{-2\,v_2(x)}$, where $v_2$ is the $2$-adic valuation on rationals. Then $\tau_2(2)=2^{-1}$.
background
Primitive Recognition Calculus builds native costs from ratio characters that must obey reciprocal symmetry and a doubled-trace d'Alembert law. On rational displays the classical verifier uses a two-adic branch twist: it fixes odd-prime axes and inverts the orbit-2 exponent.
Concretely the twist is $\tau_2(x)=x\cdot 2^{-2 v_2(x)}$. The only upstream ingredients needed here are that definition and the standard fact that the $2$-adic valuation of 2 itself equals 1. The local module assembles uniqueness of the native cost functional from such character and twist lemmas.
proof idea
Unfold $\tau_2$. Apply the library self-valuation lemma: since $1<2$, one has $v_2(2)=1$. Rewrite to obtain $2\cdot 2^{-2\cdot 1}$, then discharge the resulting rational arithmetic by norm_num.
why it matters
This base case is the arithmetic seed for three downstream results in the same uniqueness module. The two-adic axis twist character branch theorem rewrites its reciprocal cross-equation on the prime-2 direction exactly to this identity. The evaluation at 4 reduces, via the multiplicative law for the twist, to two copies of the value at 2. The generated native-cost hypotheses package sits on the same character infrastructure.
In the broader Recognition forcing chain these steps pin the two-adic branch of the classical verifier that supports uniqueness of the native cost (the J-cost lineage of T5 and the Recognition Composition Law).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.