twoAdicTwistRat_inv
plain-language theorem explainer
The classical two-adic branch twist on rationals intertwines with inversion: twisting the reciprocal equals the reciprocal of the twist. Anyone building ratio characters or verifying that the two-adic axis twist is a PRC ratio character needs this identity. The proof unfolds the definition, splits on zero, and finishes by the valuation rule for inverses plus elementary zpow algebra.
Claim. For every rational $x$, if $\tau_2(x) := x \cdot 2^{-2\,v_2(x)}$ denotes the two-adic branch twist (with $v_2$ the $2$-adic valuation on $\mathbb{Q}$), then $\tau_2(x^{-1}) = \tau_2(x)^{-1}$.
background
In the Primitive Recognition Calculus native-cost uniqueness development, rational displays carry a classical two-adic branch twist
$$\tau_2(x) = x \cdot 2^{-2,v_2(x)}.$$
Its job is to fix odd-prime axes while inverting the orbit-$2$ exponent, so that two-adic data can be folded into a ratio character without spoiling the multiplicative skeleton used by cost reconstruction.
The ambient setting is uniqueness of native cost functionals built from ratio characters and doubled-trace d'Alembert data. Upstream, $\tau_2$ is defined pointwise via padicValRat; the present lemma records that $\tau_2$ is compatible with taking reciprocals on $\mathbb{Q}$. That compatibility is the algebraic step needed before one can promote the twist to a full PRC ratio character.
proof idea
Unfold $\tau_2$. Split on $x=0$: the zero case is immediate by simplification. For $x\neq 0$, rewrite $v_2(x^{-1})=-v_2(x)$ via the standard inverse rule for rational $2$-adic valuation. The remaining identity is pure exponent arithmetic: $-2\cdot(-v_2(x)) = -(-2,v_2(x))$, so the power of $2$ becomes a reciprocal by zpow_neg. A final field_simp (using that $2$ and the relevant power are nonzero) closes the equality.
why it matters
This is a small but mandatory homomorphism-style fact on the two-adic twist. Downstream it is cited inside the unit clause of twoAdicAxisTwistCharacter_ratio_character, which asserts that the two-adic axis twist character is a PRCRatioCharacter. Without inverse-compatibility, the character axioms (in particular the unit/cross-equation side) would not typecheck against the rational display model.
In the broader Recognition stack, ratio characters feed native-cost uniqueness and the doubled-trace d'Alembert route that pins the J-cost shape (the T5 uniqueness landmark $J(x)=(x+x^{-1})/2-1$). The lemma itself is pure arithmetic scaffolding: it does not force $\phi$ or the octave, but it keeps the two-adic branch of the verifier inside the multiplicative class required by that uniqueness program.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.