axisTwistRat_inv
plain-language theorem explainer
The base-b axis twist on rationals intertwines with multiplicative inversion: twisting x inverse equals the inverse of the twist of x. Anyone assembling ratio characters from axis twists, or checking that those characters close under inversion, will cite this. The proof unfolds the definition, splits on zero, and finishes by the b-adic valuation rule v_b(x^{-1})=-v_b(x) plus elementary zpow algebra.
Claim. For every prime $b\in\mathbb{N}$ and every $x\in\mathbb{Q}$, writing $T_b(x):=x\cdot b^{-2\,v_b(x)}$ for the base-$b$ axis twist ($v_b$ the $b$-adic valuation on $\mathbb{Q}$), one has $T_b(x^{-1})=T_b(x)^{-1}$.
background
In Primitive Recognition Calculus, native-cost uniqueness is organized around ratio characters built from axis twists on rational displays. The base-$b$ axis twist multiplies a rational by a pure power of the prime $b$ that cancels twice the $b$-adic valuation:
$T_b(x)=x\cdot b^{-2 v_b(x)}$.
Along the prime axis $b$ the exponent is inverted; every other prime axis is left fixed. The cases $b=2$ and $b=3$ recover the two-adic and three-adic twists used elsewhere in the module.
The surrounding development matches doubled-trace D'Alembert structure to character-derived costs. Upstream, $T_b$ is defined via the rational $b$-adic valuation, and a short lemma records that a prime base remains nonzero when cast to $\mathbb{Q}$.
proof idea
Unfold $T_b$. On the zero case both sides simplify directly. For $x\neq 0$, rewrite with the valuation identity $v_b(x^{-1})=-v_b(x)$, rearrange the exponent identity $-2(-v_b(x))=-(-2 v_b(x))$, convert the negative integer power into a reciprocal via zpow_neg, and close by field simplification. Nonvanishing of the base and of the pure $b$-power comes from the prime-base lemma and zpow_ne_zero.
why it matters
Inverse-intertwining is a structural check that axis-twist maps behave like group characters under inversion. The immediate consumer is the theorem that the axis-twist character attached to a prime-orbit distinction satisfies the PRC ratio-character interface. That interface feeds the native-cost uniqueness argument: costs reconstructed from characters must agree with the doubled-trace native cost under the D'Alembert hypotheses. In the broader Recognition foundation, ratio characters and J-cost uniqueness sit upstream of the forcing-chain T5 step (uniqueness of $J$), so elementary multiplicative compatibilities keep the character side closed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.