twoAdicTwistRat_one
plain-language theorem explainer
The classical two-adic branch twist on rational displays fixes the unit: it sends 1 to 1. Anyone assembling a PRC ratio character from the two-adic axis twist needs this unit check before the character axioms close. The proof unfolds the definition and uses that the 2-adic valuation of 1 vanishes.
Claim. Let $T_2:\mathbb{Q}\to\mathbb{Q}$ be the two-adic twist $T_2(x)=x\cdot 2^{-2\,v_2(x)}$, where $v_2$ is the $2$-adic valuation on rationals. Then $T_2(1)=1$.
background
In the primitive recognition calculus, native costs on ratio orbits are built from multiplicative characters on rational displays. The two-adic twist is the classical verifier map that leaves odd-prime axes fixed and inverts the orbit-$2$ exponent: on $x\in\mathbb{Q}$ it multiplies by $2^{-2 v_2(x)}$.
The $2$-adic valuation $v_2$ measures the power of $2$ in a reduced fraction (negative for denominators). For the unit rational $1$, that valuation is zero, so the twist factor is $2^0=1$.
This module develops uniqueness of native costs under d'Alembert-type hypotheses on doubled traces. The twist supplies the axis character whose cost must match the generated native cost on every ratio orbit.
proof idea
Unfold the definition of the twist. A short norm_num argument with the standard facts on padicValRat of integers shows $v_2(1)=0$ (since $2$ does not divide $1$). Rewrite the exponent to zero and simplify $1\cdot 2^{0}=1$.
why it matters
This is the unit clause for the two-adic axis twist as a PRC ratio character. Downstream, twoAdicAxisTwistCharacter_ratio_character invokes it after reducing the character unit to the rational display equality $T_2(1)=1$. The same fact seeds the base case of twoAdicGeneratedNativeCost_crossEq_generated, which equates the two-adic-generated native cost with the cost pulled back from that character on every ratio orbit (starting at the identity orbit).
In the Recognition foundation stack this sits inside native-cost uniqueness for the primitive calculus: characters must fix $1$ so that the cost functional is normalized before d'Alembert and cross-equation comparisons run. It is local arithmetic bookkeeping, not a forcing-chain step (T5–T8), but without it the two-adic branch of the uniqueness argument does not start.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.